:: 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;