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;