:: Lattice of Substitutions :: by Adam Grabowski :: :: Received May 21, 1997 :: Copyright (c) 1997-2018 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 SUBSET_1, FINSUB_1, PARTFUN1, FINSET_1, TARSKI, XBOOLE_0, NORMFORM, FUNCT_1, ORDINAL4, FUNCT_4, STRUCT_0, LATTICES, BINOP_1, EQREL_1, XXREAL_2, SUBSTLAT; notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, FINSUB_1, BINOP_1, STRUCT_0, FUNCT_1, PARTFUN1, LATTICES, FUNCT_4; constructors BINOP_1, FUNCT_4, FINSUB_1, LATTICES, RELSET_1; registrations XBOOLE_0, RELSET_1, PARTFUN1, FINSET_1, FINSUB_1, LATTICES, FUNCT_1; requirements SUBSET, BOOLE; begin :: Preliminaries reserve V, C for set; definition let V, C; func SubstitutionSet (V, C) -> Subset of Fin PFuncs (V, C) equals :: SUBSTLAT:def 1 { A where A is Element of Fin PFuncs (V,C) : ( for u being set st u in A holds u is finite ) & for s, t being Element of PFuncs (V, C) holds ( s in A & t in A & s c= t implies s = t ) }; end; theorem :: SUBSTLAT:1 {} in SubstitutionSet (V, C); theorem :: SUBSTLAT:2 { {} } in SubstitutionSet (V, C); registration let V, C; cluster SubstitutionSet (V, C) -> non empty; end; definition let V, C; let A, B be Element of SubstitutionSet (V, C); redefine func A \/ B -> Element of Fin PFuncs (V, C); end; registration let V, C; cluster non empty for Element of SubstitutionSet (V, C); end; registration let V, C; cluster -> finite for Element of SubstitutionSet (V, C); end; definition let V, C; let A be Element of Fin PFuncs (V, C); func mi A -> Element of SubstitutionSet (V, C) equals :: SUBSTLAT:def 2 { t where t is Element of PFuncs (V, C) : t is finite & for s being Element of PFuncs (V, C) holds ( s in A & s c= t iff s = t ) }; end; registration let V, C; cluster -> functional for Element of SubstitutionSet(V, C); end; definition let V, C; let A, B be Element of Fin PFuncs (V, C); func A^B -> Element of Fin PFuncs (V, C) equals :: SUBSTLAT:def 3 { s \/ t where s,t is Element of PFuncs (V,C) : s in A & t in B & s tolerates t }; end; reserve A, B, D for Element of Fin PFuncs (V, C); theorem :: SUBSTLAT:3 A^B = B^A; theorem :: SUBSTLAT:4 B = { {} } implies A ^ B = A; theorem :: SUBSTLAT:5 for a, b be set holds B in SubstitutionSet (V, C) & a in B & b in B & a c= b implies a = b; theorem :: SUBSTLAT:6 for a be set holds a in mi B implies a in B & for b be set holds b in B & b c= a implies b = a; reserve s for Element of PFuncs (V,C); registration let V, C; cluster finite for Element of PFuncs (V,C); end; theorem :: SUBSTLAT:7 for a be finite set holds a in B & (for b be finite set st b in B & b c= a holds b = a) implies a in mi B; theorem :: SUBSTLAT:8 mi A c= A; theorem :: SUBSTLAT:9 A = {} implies mi A = {}; theorem :: SUBSTLAT:10 for b be finite set holds b in B implies ex c be set st c c= b & c in mi B; theorem :: SUBSTLAT:11 for K be Element of SubstitutionSet (V, C) holds mi K = K; theorem :: SUBSTLAT:12 mi (A \/ B) c= mi A \/ B; theorem :: SUBSTLAT:13 mi(mi A \/ B) = mi (A \/ B); theorem :: SUBSTLAT:14 A c= B implies A ^ D c= B ^ D; theorem :: SUBSTLAT:15 for a be set holds a in A^B implies ex b,c be set st b in A & c in B & a = b \/ c; theorem :: SUBSTLAT:16 for b, c be Element of PFuncs (V, C) holds b in A & c in B & b tolerates c implies b \/ c in A^B; theorem :: SUBSTLAT:17 mi(A ^ B) c= mi A ^ B; theorem :: SUBSTLAT:18 A c= B implies D ^ A c= D ^ B; theorem :: SUBSTLAT:19 mi(mi A ^ B) = mi (A ^ B); theorem :: SUBSTLAT:20 mi(A ^ mi B) = mi (A ^ B); theorem :: SUBSTLAT:21 for K, L, M being Element of Fin PFuncs (V, C) holds K^(L^M) = K ^L^M; theorem :: SUBSTLAT:22 for K, L, M being Element of Fin PFuncs (V, C) holds K^(L \/ M) = K^L \/ K^M; theorem :: SUBSTLAT:23 B c= B ^ B; theorem :: SUBSTLAT:24 mi (A ^ A) = mi A; theorem :: SUBSTLAT:25 for K be Element of SubstitutionSet (V, C) holds mi (K^K) = K; begin :: Definition of the lattice definition let V, C; func SubstLatt (V, C) -> strict LattStr means :: SUBSTLAT:def 4 the carrier of it = SubstitutionSet (V, C) & for A, B being Element of SubstitutionSet (V, C) holds (the L_join of it).(A,B) = mi (A \/ B) & (the L_meet of it).(A,B) = mi (A^B); end; registration let V, C; cluster SubstLatt (V, C) -> non empty; end; reserve K, L, M for Element of SubstitutionSet (V,C); registration let V, C; cluster SubstLatt (V, C) -> Lattice-like; end; registration let V, C; cluster SubstLatt (V, C) -> distributive bounded; end; theorem :: SUBSTLAT:26 Bottom SubstLatt (V,C) = {}; theorem :: SUBSTLAT:27 Top SubstLatt (V,C) = { {} };