The abstract of the Mizar article:

Subalgebras of Many Sorted Algebra. Lattice of Subalgebras

by

Ewa Burakowska

Received April 25, 1994

MML identifier: MSUALG_2

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, PBOOLE, ZF_REFLE, BOOLE, CARD_3, AMI_1, MSUALG_1,
      UNIALG_2, FINSEQ_1, TDGROUP, QC_LANG1, FINSEQ_4, PRALG_1, FUNCT_2,
      PROB_1, TARSKI, SETFAM_1, LATTICES, BINOP_1, MSUALG_2;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, STRUCT_0, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, SETFAM_1, FINSEQ_2, LATTICES, BINOP_1, PROB_1, CARD_3,
      PBOOLE, PRALG_1, MSUALG_1;
 constructors LATTICES, BINOP_1, PRALG_1, MSUALG_1, PROB_1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, LATTICES, PBOOLE, PRALG_1, MSUALG_1, RELAT_1, RELSET_1,
      STRUCT_0, RLSUB_2, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0;
 requirements BOOLE, SUBSET;


begin
::
:: Auxiliary facts about Many Sorted Sets.
::

reserve x,y for set;

scheme LambdaB {D()->non empty set, F(set)->set}:
ex f be Function st dom f = D() & for d be Element of D() holds f.d = F(d);

definition
  let I be set, X be ManySortedSet of I, Y be non-empty ManySortedSet of I;
  cluster X \/ Y -> non-empty;
  cluster Y \/ X -> non-empty;
end;

canceled;

theorem :: MSUALG_2:2
for I be non empty set, X, Y be ManySortedSet of I, i be Element of I*
holds product ((X /\ Y)*i) = product(X * i) /\ product(Y * i);

definition let I be set,
               M be ManySortedSet of I;
mode ManySortedSubset of M -> ManySortedSet of I means
:: MSUALG_2:def 1
 it c= M;
end;

definition let I be set,
               M be non-empty ManySortedSet of I;
cluster non-empty ManySortedSubset of M;
end;

begin
::
::  Constants of a Many Sorted Algebra.
::

reserve S for non void non empty ManySortedSign,
        o for OperSymbol of S,
        U0,U1,U2 for MSAlgebra over S;

definition let S be non empty ManySortedSign,
              U0 be MSAlgebra over S;
mode MSSubset of U0 is ManySortedSubset of the Sorts of U0;
end;

definition let S be non empty ManySortedSign;
 let IT be SortSymbol of S;
attr IT is with_const_op means
:: MSUALG_2:def 2
 ex o be OperSymbol of S st
 (the Arity of S).o = {} & (the ResultSort of S).o = IT;
end;

definition let IT be non empty ManySortedSign;
attr IT is all-with_const_op means
:: MSUALG_2:def 3
 for s be SortSymbol of IT holds s is with_const_op;
end;

definition let A be non empty set, B be set,
 a be Function of B,A*, r be Function of B,A;
 cluster ManySortedSign(#A,B,a,r#) -> non empty;
end;

definition
cluster non void all-with_const_op strict (non empty ManySortedSign);
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               s be SortSymbol of S;
func Constants(U0,s) -> Subset of (the Sorts of U0).s means
:: MSUALG_2:def 4
 ex A being non empty set st A =(the Sorts of U0).s &
 it = { a where a is Element of A :
       ex o be OperSymbol of S st (the Arity of S).o = {} &
       (the ResultSort of S).o = s & a in rng Den(o,U0)}
        if (the Sorts of U0).s <> {}
  otherwise it = {};
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
func Constants (U0) -> MSSubset of U0 means
:: MSUALG_2:def 5
 for s be SortSymbol of S holds it.s = Constants(U0,s);
end;

definition let S be all-with_const_op non void (non empty ManySortedSign),
               U0 be non-empty MSAlgebra over S,
               s be SortSymbol of S;
cluster Constants(U0,s) -> non empty;
end;

definition let S be non void all-with_const_op (non empty ManySortedSign),
               U0 be non-empty MSAlgebra over S;
cluster Constants(U0) -> non-empty;
end;

begin
::
::   Subalgebras of a Many Sorted Algebra.
::

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               o be OperSymbol of S,
               A be MSSubset of U0;
pred A is_closed_on o means
:: MSUALG_2:def 6
 rng ((Den(o,U0))|((A# * the Arity of S).o)) c= (A * the ResultSort of S).o;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
attr A is opers_closed means
:: MSUALG_2:def 7
 for o be OperSymbol of S holds A is_closed_on o;
end;

theorem :: MSUALG_2:3
for S be non void non empty ManySortedSign, o be OperSymbol of S,
U0 be MSAlgebra over S, B0, B1 be MSSubset of U0 st B0 c= B1 holds
((B0# * the Arity of S).o) c= ((B1# * the Arity of S).o);

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               o be OperSymbol of S,
               A be MSSubset of U0;
assume  A is_closed_on o;
func o/.A ->Function of (A# * the Arity of S).o, (A * the ResultSort of S).o
 equals
:: MSUALG_2:def 8
  (Den(o,U0)) | ((A# * the Arity of S).o);
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
func Opers(U0,A) -> ManySortedFunction of
                 (A# * the Arity of S),(A * the ResultSort of S) means
:: MSUALG_2:def 9
 for o be OperSymbol of S holds it.o = o/.A;
end;

theorem :: MSUALG_2:4
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B=the Sorts of U0 holds
 B is opers_closed & for o holds o/.B = Den(o,U0);

theorem :: MSUALG_2:5
for B being MSSubset of U0 st B=the Sorts of U0 holds
Opers(U0,B) = the Charact of U0;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
mode MSSubAlgebra of U0 -> MSAlgebra over S means
:: MSUALG_2:def 10
  the Sorts of it is MSSubset of U0 &
  for B be MSSubset of U0 st B = the Sorts of it holds
  B is opers_closed & the Charact of it = Opers(U0,B);
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
cluster strict MSSubAlgebra of U0;
end;

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S;
  cluster MSAlgebra (#the Sorts of U0,the Charact of U0#) -> non-empty;
end;

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S;
cluster non-empty strict MSSubAlgebra of U0;
end;

theorem :: MSUALG_2:6
  U0 is MSSubAlgebra of U0;

theorem :: MSUALG_2:7
  U0 is MSSubAlgebra of U1 & U1 is MSSubAlgebra of U2 implies
U0 is MSSubAlgebra of U2;

theorem :: MSUALG_2:8
U1 is strict MSSubAlgebra of U2 & U2 is strict MSSubAlgebra of U1 implies
U1 = U2;

theorem :: MSUALG_2:9
for U1,U2 be MSSubAlgebra of U0
  st the Sorts of U1 c= the Sorts of U2
holds U1 is MSSubAlgebra of U2;

theorem :: MSUALG_2:10
for U1,U2 be strict MSSubAlgebra of U0
 st the Sorts of U1 = the Sorts of U2
holds U1 = U2;

theorem :: MSUALG_2:11
for S be non void non empty ManySortedSign, U0 be MSAlgebra over S,
U1 be MSSubAlgebra of U0 holds Constants(U0) is MSSubset of U1;

theorem :: MSUALG_2:12
 for S be non void all-with_const_op (non empty ManySortedSign),
U0 be non-empty MSAlgebra over S, U1 be non-empty MSSubAlgebra of U0 holds
Constants(U0) is non-empty MSSubset of U1;

theorem :: MSUALG_2:13
  for S be non void all-with_const_op (non empty ManySortedSign),
U0 be non-empty MSAlgebra over S, U1,U2 be non-empty MSSubAlgebra of U0 holds
(the Sorts of U1) /\ (the Sorts of U2) is non-empty;

begin
::
::  Many Sorted Subsets of a Many Sorted Algebra.
::

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
func SubSort(A) -> set means
:: MSUALG_2:def 11
 for x be set holds
 x in it iff x in Funcs(the carrier of S, bool (Union (the Sorts of U0))) &
 x is MSSubset of U0 & for B be MSSubset of U0 st
 B = x holds B is opers_closed & Constants(U0) c= B & A c= B;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
  cluster SubSort(A) -> non empty;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
func SubSort(U0) -> set means
:: MSUALG_2:def 12
 for x be set holds
 x in it iff x in Funcs(the carrier of S, bool Union the Sorts of U0) &
 x is MSSubset of U0 & for B be MSSubset of U0 st
 B = x holds B is opers_closed;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
cluster SubSort(U0) -> non empty;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               e be Element of SubSort(U0);
func @e -> MSSubset of U0 equals
:: MSUALG_2:def 13
 e;
end;

theorem :: MSUALG_2:14
for A,B be MSSubset of U0 holds
B in SubSort(A) iff B is opers_closed & Constants(U0) c= B & A c= B;

theorem :: MSUALG_2:15
for B be MSSubset of U0 holds B in SubSort(U0) iff B is opers_closed;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0,
               s be SortSymbol of S;
func SubSort(A,s) -> set means
:: MSUALG_2:def 14
for x be set holds
 x in it iff ex B be MSSubset of U0 st B in SubSort(A) & x = B.s;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0,
               s be SortSymbol of S;
cluster SubSort(A,s) -> non empty;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
func MSSubSort(A) -> MSSubset of U0 means
:: MSUALG_2:def 15
for s be SortSymbol of S holds it.s = meet (SubSort(A,s));
end;

theorem :: MSUALG_2:16
for A be MSSubset of U0 holds Constants(U0) \/ A c= MSSubSort(A);

theorem :: MSUALG_2:17
for A be MSSubset of U0 st Constants(U0) \/ A is non-empty holds
MSSubSort(A) is non-empty;

theorem :: MSUALG_2:18
for A be MSSubset of U0
for B be MSSubset of U0 st B in SubSort(A) holds
 ((MSSubSort A)# * (the Arity of S)).o c= (B# * (the Arity of S)).o;

theorem :: MSUALG_2:19
for A be MSSubset of U0
for B be MSSubset of U0 st B in SubSort(A) holds
 rng (Den(o,U0)|(((MSSubSort A)# * (the Arity of S)).o)) c=
 (B * (the ResultSort of S)).o;

theorem :: MSUALG_2:20
for A be MSSubset of U0 holds
rng ((Den(o,U0))|(((MSSubSort A)# * (the Arity of S)).o)) c=
 ((MSSubSort A) * (the ResultSort of S)).o;

theorem :: MSUALG_2:21
for A be MSSubset of U0 holds
MSSubSort(A) is opers_closed & A c= MSSubSort(A);

begin
::
::  Operations on Subalgebras of a Many Sorted Algebra.
::

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
assume  A is opers_closed;
func U0|A -> strict MSSubAlgebra of U0 equals
:: MSUALG_2:def 16
  MSAlgebra (#A , Opers(U0,A) qua ManySortedFunction of
                      (A# * the Arity of S),(A * the ResultSort of S)#);
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               U1,U2 be MSSubAlgebra of U0;
func U1 /\ U2 -> strict MSSubAlgebra of U0 means
:: MSUALG_2:def 17
 the Sorts of it = (the Sorts of U1) /\ (the Sorts of U2) &
for B be MSSubset of U0 st B=the Sorts of it holds
B is opers_closed & the Charact of it = Opers(U0,B);
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S,
               A be MSSubset of U0;
func GenMSAlg(A) -> strict MSSubAlgebra of U0 means
:: MSUALG_2:def 18
 A is MSSubset of it &
 for U1 be MSSubAlgebra of U0 st A is MSSubset of U1 holds
       it is MSSubAlgebra of U1;
end;

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S,
               A be non-empty MSSubset of U0;
 cluster GenMSAlg(A) -> non-empty;
end;

theorem :: MSUALG_2:22
for S be non void non empty ManySortedSign,
    U0 be strict MSAlgebra over S, B be MSSubset of U0 st B = the Sorts of U0
holds GenMSAlg(B) = U0;

theorem :: MSUALG_2:23
for S be non void non empty ManySortedSign, U0 be MSAlgebra over S,
U1 be strict MSSubAlgebra of U0,
B be MSSubset of U0 st B = the Sorts of U1 holds GenMSAlg(B) = U1;

theorem :: MSUALG_2:24
for S be non void non empty ManySortedSign,
 U0 be non-empty MSAlgebra over S,
 U1 be MSSubAlgebra of U0 holds
GenMSAlg(Constants(U0)) /\ U1 = GenMSAlg(Constants(U0));

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S,
               U1,U2 be MSSubAlgebra of U0;
func U1 "\/" U2 -> strict MSSubAlgebra of U0 means
:: MSUALG_2:def 19
 for A be MSSubset of U0 st
  A = (the Sorts of U1) \/ (the Sorts of U2) holds it = GenMSAlg(A);
end;

theorem :: MSUALG_2:25
for S be non void non empty ManySortedSign,U0 be non-empty MSAlgebra over S,
U1 be MSSubAlgebra of U0, A,B be MSSubset of U0 st B = A \/ the Sorts of U1
 holds GenMSAlg(A) "\/" U1 = GenMSAlg(B);

theorem :: MSUALG_2:26
for S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S,
U1 be MSSubAlgebra of U0, B be MSSubset of U0 st B = the Sorts of U0
 holds GenMSAlg(B) "\/" U1 = GenMSAlg(B);

theorem :: MSUALG_2:27
for S be non void non empty ManySortedSign,U0 be non-empty MSAlgebra over S,
U1,U2 be MSSubAlgebra of U0 holds
U1 "\/" U2 = U2 "\/" U1;

theorem :: MSUALG_2:28
for S be non void non empty ManySortedSign,
 U0 be non-empty MSAlgebra over S,
 U1,U2 be strict MSSubAlgebra of U0 holds
  U1 /\ (U1"\/"U2) = U1;

theorem :: MSUALG_2:29
for S be non void non empty ManySortedSign,
 U0 be non-empty MSAlgebra over S,
 U1,U2 be strict MSSubAlgebra of U0
holds (U1 /\ U2)"\/"U2 = U2;

begin
::
::  The Lattice of SubAlgebras of a Many Sorted Algebra.
::

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
func MSSub(U0) -> set means
:: MSUALG_2:def 20
for x holds x in it iff x is strict MSSubAlgebra of U0;
end;

definition let S be non void non empty ManySortedSign,
               U0 be MSAlgebra over S;
cluster MSSub(U0) -> non empty;
end;

definition let S be non void non empty ManySortedSign,
                U0 be non-empty MSAlgebra over S;
func MSAlg_join(U0) -> BinOp of (MSSub(U0)) means
:: MSUALG_2:def 21
for x,y be Element of MSSub(U0) holds
 for U1,U2 be strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
  it.(x,y) = U1 "\/" U2;
end;

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S;
func MSAlg_meet(U0) -> BinOp of (MSSub(U0)) means
:: MSUALG_2:def 22
for x,y be Element of MSSub(U0) holds
  for U1,U2 be strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
  it.(x,y) = U1 /\ U2;
end;

reserve U0 for non-empty MSAlgebra over S;

theorem :: MSUALG_2:30
MSAlg_join(U0) is commutative;

theorem :: MSUALG_2:31
MSAlg_join(U0) is associative;

theorem :: MSUALG_2:32
for S be non void non empty ManySortedSign,
 U0 be non-empty MSAlgebra over S
holds MSAlg_meet(U0) is commutative;

theorem :: MSUALG_2:33
for S be non void non empty ManySortedSign,
    U0 be non-empty MSAlgebra over S
holds MSAlg_meet(U0) is associative;

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S;
func MSSubAlLattice(U0) -> strict Lattice equals
:: MSUALG_2:def 23
  LattStr (# MSSub(U0), MSAlg_join(U0), MSAlg_meet(U0) #);
end;

theorem :: MSUALG_2:34
for S be non void non empty ManySortedSign,
    U0 be non-empty MSAlgebra over S
holds MSSubAlLattice(U0) is bounded;

definition let S be non void non empty ManySortedSign,
               U0 be non-empty MSAlgebra over S;
cluster MSSubAlLattice(U0) -> bounded;
end;

theorem :: MSUALG_2:35
  for S be non void non empty ManySortedSign,
    U0 be non-empty MSAlgebra over S
holds Bottom (MSSubAlLattice(U0)) = GenMSAlg(Constants(U0));

theorem :: MSUALG_2:36
for S be non void non empty ManySortedSign,
    U0 be non-empty MSAlgebra over S,
B be MSSubset of U0 st B = the Sorts of U0 holds
 Top (MSSubAlLattice(U0)) = GenMSAlg(B);

theorem :: MSUALG_2:37
  for S be non void non empty ManySortedSign,
U0 be strict non-empty MSAlgebra over S holds Top (MSSubAlLattice(U0)) = U0;

theorem :: MSUALG_2:38
    for S being non void non empty ManySortedSign,
      U0 being MSAlgebra over S holds
 MSAlgebra (#the Sorts of U0,the Charact of U0#) is MSSubAlgebra of U0;

theorem :: MSUALG_2:39
    for S being non void non empty ManySortedSign,
  U0 being non-empty MSAlgebra over S holds
  MSAlgebra (#the Sorts of U0,the Charact of U0#) is non-empty;

theorem :: MSUALG_2:40
    for S being non void non empty ManySortedSign,
  U0 being MSAlgebra over S,
  A being MSSubset of U0 holds
  the Sorts of U0 in SubSort(A);

theorem :: MSUALG_2:41
    for S being non void non empty ManySortedSign,
      U0 being MSAlgebra over S,
      A being MSSubset of U0 holds
  SubSort(A) c= SubSort(U0);