Journal of Formalized Mathematics
Volume 14, 2002
University of Bialystok
Copyright (c) 2002 Association of Mizar Users

Subalgebras of an Order Sorted Algebra. Lattice of Subalgebras

by
Josef Urban

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;

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;