Volume 14, 2002

University of Bialystok

Copyright (c) 2002 Association of Mizar Users

### The abstract of the Mizar article:

### Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras

**by****Josef Urban**- Received September 19, 2002
- MML identifier: OSALG_2

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, BOOLE, CARD_3, AMI_1, MSUALG_1, UNIALG_2, TDGROUP, QC_LANG1, PRALG_1, PROB_1, TARSKI, SETFAM_1, LATTICES, BINOP_1, MSUALG_2, OSALG_1, ORDERS_1, SEQM_3, OSALG_2; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1, SETFAM_1, LATTICES, BINOP_1, PROB_1, CARD_3, MBOOLEAN, PBOOLE, MSUALG_1, ORDERS_1, MSUALG_2, YELLOW18, OSALG_1; constructors MBOOLEAN, PROB_1, ORDERS_3, OSALG_1, YELLOW18, MSUALG_2; clusters FUNCT_1, LATTICES, MSUALG_1, RELSET_1, STRUCT_0, RLSUB_2, SUBSET_1, ORDERS_3, OSALG_1, MSUALG_2, MSAFREE, XBOOLE_0; 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; definition let R be non empty Poset, M be non-empty OrderSortedSet of R; cluster non-empty 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 definition let S be OrderSortedSign; cluster monotone strict non-empty OSAlgebra of S; end; definition let S be OrderSortedSign, U0 be non-empty OSAlgebra of S; cluster non-empty 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; definition cluster all-with_const_op strict 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; definition let S be OrderSortedSign, U0 be OSAlgebra of S; :: can't for ms! cluster order-sorted 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; definition let S be OrderSortedSign, U0 be OSAlgebra of S; cluster strict OSSubAlgebra of U0; end; definition let S be OrderSortedSign, U0 be non-empty OSAlgebra of S; cluster non-empty strict 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); canceled 5; theorem :: OSALG_2:11 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:12 for M being ManySortedSet of the carrier of S1 holds M c= OSCl M; theorem :: OSALG_2:13 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:14 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:15 Constants(OU0) c= OSConstants(OU0); theorem :: OSALG_2:16 for A being OSSubset of OU0 holds Constants(OU0) c= A implies OSConstants(OU0) c= A; theorem :: OSALG_2:17 for A being OSSubset of OU0 holds OSConstants(OU0) = OSCl Constants(OU0); theorem :: OSALG_2:18 for OU1 being OSSubAlgebra of OU0 holds OSConstants(OU0) is OSSubset of OU1; theorem :: OSALG_2:19 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:20 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:21 for A being OSSubset of OU0 holds OSSubSort(A) c= SubSort(A); theorem :: OSALG_2:22 for A being OSSubset of OU0 holds the Sorts of OU0 in OSSubSort(A); definition 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:23 for A being OSSubset of OU0 holds OSSubSort(A) c= OSSubSort(OU0); definition 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:24 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:25 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 set holds x in it iff ex B be OSSubset of OU0 st B in OSSubSort(A) & x = B.s; end; theorem :: OSALG_2:26 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:27 for A being OSSubset of OU0, s being SortSymbol of S1 holds OSSubSort(A,s) c= SubSort(A,s); theorem :: OSALG_2:28 for A being OSSubset of OU0, s being SortSymbol of S1 holds (the Sorts of OU0).s in OSSubSort(A,s); definition 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; definition let S1,OU0; canceled; cluster opers_closed OSSubset of OU0; end; theorem :: OSALG_2:29 for A be OSSubset of OU0 holds OSConstants(OU0) \/ A c= OSMSubSort(A); theorem :: OSALG_2:30 for A be OSSubset of OU0 st OSConstants(OU0) \/ A is non-empty holds OSMSubSort(A) is non-empty; theorem :: OSALG_2:31 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:32 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:33 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:34 for A be OSSubset of OU0 holds OSMSubSort(A) is opers_closed & A c= OSMSubSort(A); definition let S1,OU0; let A be OSSubset of OU0; cluster OSMSubSort(A) -> opers_closed; end; begin :: Operations on Subalgebras of an Order Sorted Algebra. definition let S1,OU0; let A be opers_closed OSSubset of OU0; cluster OU0|A -> order-sorted; end; definition 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 13 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:35 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:36 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:37 for A being OSSubset of OU0 holds the Sorts of GenMSAlg(A) c= the Sorts of GenOSAlg(A); theorem :: OSALG_2:38 for A being OSSubset of OU0 holds GenMSAlg(A) is MSSubAlgebra of GenOSAlg(A); theorem :: OSALG_2:39 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:40 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:41 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 14 for A be OSSubset of U0 st A = (the Sorts of U1) \/ (the Sorts of U2) holds it = GenOSAlg(A); end; theorem :: OSALG_2:42 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:43 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:44 for U0 being non-empty OSAlgebra of S1, U1,U2 be OSSubAlgebra of U0 holds U1 "\/"_os U2 = U2 "\/"_os U1; theorem :: OSALG_2:45 for U0 be non-empty OSAlgebra of S1, U1,U2 be strict OSSubAlgebra of U0 holds U1 /\ (U1"\/"_os U2) = U1; theorem :: OSALG_2:46 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 15 for x holds x in it iff x is strict OSSubAlgebra of OU0; end; theorem :: OSALG_2:47 OSSub(OU0) c= MSSub(OU0); definition 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 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 "\/"_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 17 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:48 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:49 OSAlg_join(U0) is commutative; theorem :: OSALG_2:50 OSAlg_join(U0) is associative; theorem :: OSALG_2:51 OSAlg_meet(U0) is commutative; theorem :: OSALG_2:52 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 18 LattStr (# OSSub(U0), OSAlg_join(U0), OSAlg_meet(U0) #); end; theorem :: OSALG_2:53 for U0 be non-empty OSAlgebra of S1 holds OSSubAlLattice(U0) is bounded; definition let S1; let U0 be non-empty OSAlgebra of S1; cluster OSSubAlLattice(U0) -> bounded; end; theorem :: OSALG_2:54 for U0 be non-empty OSAlgebra of S1 holds Bottom (OSSubAlLattice(U0)) = GenOSAlg(OSConstants(U0)); theorem :: OSALG_2:55 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:56 for U0 be strict non-empty OSAlgebra of S1 holds Top (OSSubAlLattice(U0)) = U0;

Back to top