:: Subalgebras of a Order Sorted Algebra. {L}attice of Subalgebras
::  by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, ORDERS_2, OSALG_1, PBOOLE, SUBSET_1, XXREAL_0, FUNCT_1,
      TARSKI, RELAT_1, MSUALG_1, MSUALG_2, SEQM_3, STRUCT_0, UNIALG_2, CARD_3,
      ZFMISC_1, QC_LANG1, SETFAM_1, BINOP_1, LATTICES, EQREL_1, XXREAL_2,
      OSALG_2, SETLIM_2;
 notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, SETFAM_1, BINOP_1,
      CARD_3, MBOOLEAN, PBOOLE, FINSEQ_2, STRUCT_0, LATTICES, MSUALG_1,
      ORDERS_2, MSUALG_2, OSALG_1;
 constructors SETFAM_1, MBOOLEAN, MSUALG_2, ORDERS_3, OSALG_1, RELSET_1,
      CARD_3;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, LATTICES, MSUALG_1,
      MSUALG_2, ORDERS_3, OSALG_1, FUNCT_1, RELAT_1, PBOOLE, FINSEQ_1;
 requirements BOOLE, SUBSET;


begin :: Auxiliary facts about Order Sorted Sets.

reserve x for set,
  R for non empty Poset;

:: should be clusters, but that requires redef of the operation

theorem :: OSALG_2:1
  for X,Y being OrderSortedSet of R holds X (/\) Y is OrderSortedSet of R;

theorem :: OSALG_2:2
  for X,Y being OrderSortedSet of R holds X (\/) Y is OrderSortedSet of R;

:: new and bad

definition
  let R be non empty Poset, M be OrderSortedSet of R;
  :: can be for ManySortedSet
  mode OrderSortedSubset of M -> ManySortedSubset of M means
:: OSALG_2:def 1

    it is OrderSortedSet of R;
end;

registration
  let R be non empty Poset, M be non-empty OrderSortedSet of R;
  cluster non-empty for OrderSortedSubset of M;
end;

begin

::
::  Constants of an Order Sorted Algebra.
::

definition
  let S be OrderSortedSign, U0 be OSAlgebra of S;
  mode OSSubset of U0 -> ManySortedSubset of the Sorts of U0 means
:: OSALG_2:def 2

    it is OrderSortedSet of S;
end;

:: very strange, the cluster in OSALG_1 should take care of this one

registration
  let S be OrderSortedSign;
  cluster monotone strict non-empty for OSAlgebra of S;
end;

registration
  let S be OrderSortedSign, U0 be non-empty OSAlgebra of S;
  cluster non-empty for OSSubset of U0;
end;

theorem :: OSALG_2:3
  for S0 being non void all-with_const_op strict non empty
  ManySortedSign holds OSSign S0 is all-with_const_op;

registration
  cluster all-with_const_op strict for OrderSortedSign;
end;

begin

::
::   Subalgebras of a Order Sorted Algebra.
::

theorem :: OSALG_2:4
  for S being OrderSortedSign, U0 being OSAlgebra of S holds
  MSAlgebra (#the Sorts of U0,the Charact of U0#) is order-sorted;

registration
  let S be OrderSortedSign, U0 be OSAlgebra of S;
  cluster order-sorted for MSSubAlgebra of U0;
end;

definition
  let S be OrderSortedSign, U0 be OSAlgebra of S;
  mode OSSubAlgebra of U0 is order-sorted MSSubAlgebra of U0;
end;

registration
  let S be OrderSortedSign, U0 be OSAlgebra of S;
  cluster strict for OSSubAlgebra of U0;
end;

registration
  let S be OrderSortedSign, U0 be non-empty OSAlgebra of S;
  cluster non-empty strict for OSSubAlgebra of U0;
end;

:: the equivalent def, maybe not needed

theorem :: OSALG_2:5
  for S being OrderSortedSign for U0 being OSAlgebra of S for U1
  being MSAlgebra over S holds U1 is OSSubAlgebra of U0 iff the Sorts of U1 is
  OSSubset of U0 & for B be OSSubset of U0 st B = the Sorts of U1 holds B is
  opers_closed & the Charact of U1 = Opers(U0,B);

reserve S1 for OrderSortedSign,
  OU0 for OSAlgebra of S1;
reserve s,s1,s2,s3,s4 for SortSymbol of S1;

definition
  let S1,OU0,s;
  func OSConstants(OU0,s) -> Subset of (the Sorts of OU0).s equals
:: OSALG_2:def 3
  union {
  Constants(OU0,s2) : s2 <= s};
end;

:: maybe
:: theorem S1 is discrete implies OSConstants(OU0,s) = Constants(OU0,s);

theorem :: OSALG_2:6
  Constants(OU0,s) c= OSConstants(OU0,s);

definition
  let S1;
  let M be ManySortedSet of the carrier of S1;
  func OSCl M -> OrderSortedSet of S1 means
:: OSALG_2:def 4

  for s be SortSymbol of S1 holds it.s = union { M.s1: s1 <= s};
end;

theorem :: OSALG_2:7
  for M being ManySortedSet of the carrier of S1 holds M c= OSCl M;

theorem :: OSALG_2:8
  for M being ManySortedSet of the carrier of S1, A being
  OrderSortedSet of S1 holds M c= A implies OSCl M c= A;

theorem :: OSALG_2:9
  for S being OrderSortedSign, X being OrderSortedSet of S holds OSCl X = X;

:: following should be rewritten to use OSCl Constants(OU0) instead;
:: maybe later

definition
  let S1,OU0;
  func OSConstants (OU0) -> OSSubset of OU0 means
:: OSALG_2:def 5

  for s be SortSymbol of S1 holds it.s = OSConstants(OU0,s);
end;

theorem :: OSALG_2:10
  Constants(OU0) c= OSConstants(OU0);

theorem :: OSALG_2:11
  for A being OSSubset of OU0 holds Constants(OU0) c= A implies
  OSConstants(OU0) c= A;

theorem :: OSALG_2:12
  for A being OSSubset of OU0 holds OSConstants(OU0) = OSCl Constants( OU0);

theorem :: OSALG_2:13
  for OU1 being OSSubAlgebra of OU0 holds OSConstants(OU0) is OSSubset of OU1;

theorem :: OSALG_2:14
  for S being all-with_const_op OrderSortedSign, OU0 being non-empty
OSAlgebra of S, OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants(OU0)
  is non-empty OSSubset of OU1;

begin

::
::  Order Sorted Subsets of an Order Sorted Algebra.
::
:: this should be in MSUALG_2

theorem :: OSALG_2:15
  for I being set for M being ManySortedSet of I for x being set
  holds x is ManySortedSubset of M iff x in product bool M;

:: Fraenkel should be improved, to allow more than just Element type

definition
  let R be non empty Poset, M be OrderSortedSet of R;
  func OSbool(M) -> set means
:: OSALG_2:def 6
  for x being set holds x in it iff x is OrderSortedSubset of M;
end;

definition
  let S be OrderSortedSign, U0 be OSAlgebra of S, A be OSSubset of U0;
  func OSSubSort(A) -> set equals
:: OSALG_2:def 7
  { x where x is Element of SubSort(A): x is
  OrderSortedSet of S};
end;

theorem :: OSALG_2:16
  for A being OSSubset of OU0 holds OSSubSort(A) c= SubSort(A);

theorem :: OSALG_2:17
  for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort( A);

registration
  let S1,OU0;
  let A be OSSubset of OU0;
  cluster OSSubSort(A) -> non empty;
end;

definition
  let S1,OU0;
  func OSSubSort(OU0) -> set equals
:: OSALG_2:def 8
  { x where x is Element of SubSort(OU0): x
  is OrderSortedSet of S1};
end;

theorem :: OSALG_2:18
  for A being OSSubset of OU0 holds OSSubSort(A) c= OSSubSort(OU0);

registration
  let S1,OU0;
  cluster OSSubSort(OU0) -> non empty;
end;

:: new-def for order-sorted

definition
  let S1,OU0;
  let e be Element of OSSubSort(OU0);
  func @e -> OSSubset of OU0 equals
:: OSALG_2:def 9
  e;
end;

:: maybe do another definition of ossort, saying that it contains
:: Elements of subsort which are order-sorted (or ossubsets)

theorem :: OSALG_2:19
  for A,B be OSSubset of OU0 holds B in OSSubSort(A) iff B is
  opers_closed & OSConstants(OU0) c= B & A c= B;

theorem :: OSALG_2:20
  for B be OSSubset of OU0 holds B in OSSubSort(OU0) iff B is opers_closed;

:: slices of members of OSsubsort

definition
  let S1,OU0;
  let A be OSSubset of OU0, s be Element of S1;
  func OSSubSort(A,s) -> set means
:: OSALG_2:def 10

  for x be object holds x in it iff ex B
  be OSSubset of OU0 st B in OSSubSort(A) & x = B.s;
end;

theorem :: OSALG_2:21
  for A being OSSubset of OU0, s1,s2 being SortSymbol of S1 holds
  s1 <= s2 implies OSSubSort(A,s2) is_coarser_than OSSubSort(A,s1);

theorem :: OSALG_2:22
  for A being OSSubset of OU0, s being SortSymbol of S1 holds
  OSSubSort(A,s) c= SubSort(A,s);

theorem :: OSALG_2:23
  for A being OSSubset of OU0, s being SortSymbol of S1 holds (the
  Sorts of OU0).s in OSSubSort(A,s);

registration
  let S1,OU0;
  let A be OSSubset of OU0, s be SortSymbol of S1;
  cluster OSSubSort(A,s) -> non empty;
end;

definition
  let S1,OU0;
  let A be OSSubset of OU0;
  func OSMSubSort(A) -> OSSubset of OU0 means
:: OSALG_2:def 11

  for s be SortSymbol of S1 holds it.s = meet (OSSubSort(A,s));
end;

registration
  let S1,OU0;
  cluster opers_closed for OSSubset of OU0;
end;

theorem :: OSALG_2:24
  for A be OSSubset of OU0 holds OSConstants(OU0) (\/) A c= OSMSubSort(A);

theorem :: OSALG_2:25
  for A be OSSubset of OU0 st OSConstants(OU0) (\/) A is non-empty holds
  OSMSubSort(A) is non-empty;

theorem :: OSALG_2:26
  for o be OperSymbol of S1 for A be OSSubset of OU0 for B be
OSSubset of OU0 st B in OSSubSort(A) holds ((OSMSubSort A)# * (the Arity of S1)
  ).o c= (B# * (the Arity of S1)).o;

theorem :: OSALG_2:27
  for o be OperSymbol of S1 for A be OSSubset of OU0 for B be
OSSubset of OU0 st B in OSSubSort(A) holds rng (Den(o,OU0)|(((OSMSubSort A)# *
  (the Arity of S1)).o)) c= (B * (the ResultSort of S1)).o;

theorem :: OSALG_2:28
  for o be OperSymbol of S1 for A be OSSubset of OU0 holds rng ((
  Den(o,OU0))|(((OSMSubSort A)# * (the Arity of S1)).o)) c= ((OSMSubSort A) * (
  the ResultSort of S1)).o;

theorem :: OSALG_2:29
  for A be OSSubset of OU0 holds OSMSubSort(A) is opers_closed & A
  c= OSMSubSort(A);

registration
  let S1,OU0;
  let A be OSSubset of OU0;
  cluster OSMSubSort(A) -> opers_closed;
end;

begin :: Operations on Subalgebras of an Order Sorted Algebra.

registration
  let S1,OU0;
  let A be opers_closed OSSubset of OU0;
  cluster OU0|A -> order-sorted;
end;

registration
  let S1,OU0;
  let OU1,OU2 be OSSubAlgebra of OU0;
  cluster OU1 /\ OU2 -> order-sorted;
end;

:: generally, GenOSAlg can differ from GenMSAlg, example should be given

definition
  let S1,OU0;
  let A be OSSubset of OU0;

  func GenOSAlg(A) -> strict OSSubAlgebra of OU0 means
:: OSALG_2:def 12

  A is OSSubset
  of it & for OU1 be OSSubAlgebra of OU0 st A is OSSubset of OU1 holds it is
  OSSubAlgebra of OU1;
end;

:: this should rather be a definition, but I want to keep
:: compatibility of the definition with MSUALG_2

theorem :: OSALG_2:30
  for A be OSSubset of OU0 holds GenOSAlg(A) = OU0 | OSMSubSort(A)
  & the Sorts of GenOSAlg(A) = OSMSubSort(A);

:: this could simplify some proofs in MSUALG_2, I need it anyway

theorem :: OSALG_2:31
  for S be non void non empty ManySortedSign for U0 be MSAlgebra
  over S for A be MSSubset of U0 holds GenMSAlg(A) = U0 | MSSubSort(A) & the
  Sorts of GenMSAlg(A) = MSSubSort(A);

theorem :: OSALG_2:32
  for A being OSSubset of OU0 holds the Sorts of GenMSAlg(A) c=
  the Sorts of GenOSAlg(A);

theorem :: OSALG_2:33
  for A being OSSubset of OU0 holds GenMSAlg(A) is MSSubAlgebra of
  GenOSAlg(A);

theorem :: OSALG_2:34
  for OU0 being strict OSAlgebra of S1 for B being OSSubset of OU0
  st B = the Sorts of OU0 holds GenOSAlg(B) = OU0;

theorem :: OSALG_2:35
  for OU1 being strict OSSubAlgebra of OU0, B being OSSubset of
  OU0 st B = the Sorts of OU1 holds GenOSAlg(B) = OU1;

theorem :: OSALG_2:36
  for U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0
  holds GenOSAlg(OSConstants(U0)) /\ U1 = GenOSAlg(OSConstants(U0));

definition
  let S1;
  let U0 be non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of U0;
  func U1 "\/"_os U2 -> strict OSSubAlgebra of U0 means
:: OSALG_2:def 13

  for A be
  OSSubset of U0 st A = (the Sorts of U1) (\/) (the Sorts of U2) holds it =
  GenOSAlg(A);
end;

theorem :: OSALG_2:37
  for U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0, A
,B be OSSubset of U0 st B = A (\/) the Sorts of U1
  holds GenOSAlg(A) "\/"_os U1 = GenOSAlg(B);

theorem :: OSALG_2:38
  for U0 be non-empty OSAlgebra of S1, U1 be OSSubAlgebra of U0, B
  be OSSubset of U0 st B = the Sorts of U0 holds GenOSAlg(B) "\/"_os U1 =
  GenOSAlg(B);

theorem :: OSALG_2:39
  for U0 being non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of
  U0 holds U1 "\/"_os U2 = U2 "\/"_os U1;

theorem :: OSALG_2:40
  for U0 be non-empty OSAlgebra of S1, U1,U2 be strict
  OSSubAlgebra of U0 holds U1 /\ (U1"\/"_os U2) = U1;

theorem :: OSALG_2:41
  for U0 be non-empty OSAlgebra of S1, U1,U2 be strict
  OSSubAlgebra of U0 holds (U1 /\ U2) "\/"_os U2 = U2;

begin :: The Lattice of SubAlgebras of an Order Sorted Algebra.
:: ossub, ossubalgebra

definition
  let S1,OU0;
  func OSSub(OU0) -> set means
:: OSALG_2:def 14

  for x being object holds x in it iff x is strict OSSubAlgebra of OU0;
end;

theorem :: OSALG_2:42
  OSSub(OU0) c= MSSub(OU0);

registration
  let S be OrderSortedSign, U0 be OSAlgebra of S;
  cluster OSSub(U0) -> non empty;
end;

definition
  let S1,OU0;
  redefine func OSSub(OU0) -> Subset of MSSub(OU0);
end;

:: maybe show that e.g. for TrivialOSA(S,z,z1), OSSub(U0) is
:: proper subset of MSSub(U0), to have some counterexamples

definition
  let S1;
  let U0 be non-empty OSAlgebra of S1;
  func OSAlg_join(U0) -> BinOp of (OSSub(U0)) means
:: OSALG_2:def 15

  for x,y be Element
  of OSSub(U0) holds for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2
  holds it.(x,y) = U1 "\/"_os U2;
end;

definition
  let S1;
  let U0 be non-empty OSAlgebra of S1;
  func OSAlg_meet(U0) -> BinOp of (OSSub(U0)) means
:: OSALG_2:def 16

  for x,y be Element
  of OSSub(U0) holds for U1,U2 be strict OSSubAlgebra of U0 st x = U1 & y = U2
  holds it.(x,y) = U1 /\ U2;
end;

theorem :: OSALG_2:43
  for U0 being non-empty OSAlgebra of S1 for x,y being Element of
  OSSub(U0) holds (OSAlg_meet(U0)).(x,y) = (MSAlg_meet(U0)).(x,y);

reserve U0 for non-empty OSAlgebra of S1;

theorem :: OSALG_2:44
  OSAlg_join(U0) is commutative;

theorem :: OSALG_2:45
  OSAlg_join(U0) is associative;

theorem :: OSALG_2:46
  OSAlg_meet(U0) is commutative;

theorem :: OSALG_2:47
  OSAlg_meet(U0) is associative;

definition
  let S1;
  let U0 be non-empty OSAlgebra of S1;
  func OSSubAlLattice(U0) -> strict Lattice equals
:: OSALG_2:def 17
  LattStr (# OSSub(U0),
    OSAlg_join(U0), OSAlg_meet(U0) #);
end;

theorem :: OSALG_2:48
  for U0 be non-empty OSAlgebra of S1 holds OSSubAlLattice(U0) is bounded;

registration
  let S1;
  let U0 be non-empty OSAlgebra of S1;
  cluster OSSubAlLattice(U0) -> bounded;
end;

theorem :: OSALG_2:49
  for U0 be non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice(U0))
  = GenOSAlg(OSConstants(U0));

theorem :: OSALG_2:50
  for U0 be non-empty OSAlgebra of S1, B be OSSubset of U0 st B =
  the Sorts of U0 holds Top (OSSubAlLattice(U0)) = GenOSAlg(B);

theorem :: OSALG_2:51
  for U0 be strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice(
  U0)) = U0;