:: Free Many Sorted Universal Algebra :: by Beata Perkowska :: :: Received April 27, 1994 :: Copyright (c) 1994-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, FUNCT_1, RELAT_1, PBOOLE, SUBSET_1, CARD_3, REALSET1, TARSKI, ZFMISC_1, PARTFUN1, STRUCT_0, MSUALG_1, MSUALG_2, PRELAMB, MSUALG_3, FINSEQ_1, MARGREL1, LANG1, TDGROUP, DTCONSTR, TREES_3, TREES_4, NAT_1, TREES_2, MCART_1, UNIALG_2, QC_LANG1, GROUP_6, MSAFREE; notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1, NAT_1, RELAT_1, RELSET_1, STRUCT_0, FUNCT_1, PARTFUN1, MCART_1, FUNCT_2, FINSEQ_1, PBOOLE, TREES_2, FINSEQ_2, CARD_3, LANG1, TREES_4, DTCONSTR, MSUALG_1, MSUALG_2, MSUALG_3; constructors XXREAL_0, NAT_1, NAT_D, CARD_3, FINSEQOP, DTCONSTR, MSUALG_3, RELSET_1, PBOOLE, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, FINSEQ_1, PBOOLE, TREES_2, TREES_3, STRUCT_0, DTCONSTR, MSUALG_1, MSUALG_3, FUNCT_2, RELSET_1, XTUPLE_0; requirements BOOLE, SUBSET; begin :: :: Preliminaries :: theorem :: MSAFREE:1 for I be set, J be non empty set, f be Function of I,J*, X be ManySortedSet of J, p be Element of J*, x be set st x in I & p = f.x holds (X# * f).x = product (X * p); definition let I be set, A,B be ManySortedSet of I, C be ManySortedSubset of A; let F be ManySortedFunction of A,B; func F || C -> ManySortedFunction of C,B means :: MSAFREE:def 1 for i be set st i in I holds it.i = (F.i) | (C.i); end; definition let I be set, X be ManySortedSet of I, i be object; assume i in I; func coprod(i,X) -> set means :: MSAFREE:def 2 for x be set holds x in it iff ex a be set st a in X.i & x = [a,i]; end; notation let I be set, X be ManySortedSet of I; synonym coprod X for disjoin X; end; registration let I be set, X be ManySortedSet of I; cluster coprod X -> I-defined; end; registration let I be set, X be ManySortedSet of I; cluster coprod X -> total; end; definition let I be set, X be ManySortedSet of I; redefine func coprod X means :: MSAFREE:def 3 dom it = I & for i be set st i in I holds it.i = coprod(i,X); end; registration let I be set, X be non-empty ManySortedSet of I; cluster coprod X -> non-empty; end; registration let I be non empty set, X be non-empty ManySortedSet of I; cluster Union X -> non empty; end; theorem :: MSAFREE:2 for I be set, X be ManySortedSet of I, i be set st i in I holds X.i <> {} iff (coprod X).i <> {}; begin :: :: Free Many Sorted Universal Algebra - General Notions :: reserve S for non void non empty ManySortedSign, U0 for MSAlgebra over S; definition let S be non void non empty ManySortedSign, U0 be MSAlgebra over S; mode GeneratorSet of U0 -> MSSubset of U0 means :: MSAFREE:def 4 the Sorts of GenMSAlg (it) = the Sorts of U0; end; theorem :: MSAFREE:3 for S be non void non empty ManySortedSign, U0 be strict non-empty MSAlgebra over S, A be MSSubset of U0 holds A is GeneratorSet of U0 iff GenMSAlg(A) = U0; definition let S,U0; let IT be GeneratorSet of U0; attr IT is free means :: MSAFREE:def 5 for U1 be non-empty MSAlgebra over S for f be ManySortedFunction of IT,the Sorts of U1 ex h be ManySortedFunction of U0,U1 st h is_homomorphism U0,U1 & h || IT = f; end; definition let S be non void non empty ManySortedSign; let IT be MSAlgebra over S; attr IT is free means :: MSAFREE:def 6 ex G being GeneratorSet of IT st G is free; end; theorem :: MSAFREE:4 for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S holds Union coprod X misses [:the carrier' of S,{the carrier of S}:]; begin :: :: Construction of Free Many Sorted Algebras for Given Signature :: definition let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; func REL(X) -> Relation of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X)), (([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))*) means :: MSAFREE:def 7 for a be Element of [:the carrier' of S,{the carrier of S}:] \/ Union (coprod X), b be Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))* holds [a,b] in it iff a in [:the carrier' of S,{the carrier of S}:] & for o be OperSymbol of S st [o,the carrier of S] = a holds len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union (coprod X) implies b.x in coprod((the_arity_of o).x,X)); end; reserve S for non void non empty ManySortedSign, X for ManySortedSet of the carrier of S, o for OperSymbol of S, b for Element of ([:the carrier' of S,{the carrier of S}:] \/ Union (coprod X))*; theorem :: MSAFREE:5 [[o,the carrier of S],b] in REL(X) iff len b = len (the_arity_of o) & for x be set st x in dom b holds (b.x in [:the carrier' of S,{the carrier of S}:] implies for o1 be OperSymbol of S st [o1,the carrier of S] = b.x holds the_result_sort_of o1 = (the_arity_of o).x) & (b.x in Union (coprod X) implies b.x in coprod((the_arity_of o).x,X)); definition let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; func DTConMSA(X) -> DTConstrStr equals :: MSAFREE:def 8 DTConstrStr (# [:the carrier' of S,{ the carrier of S}:] \/ Union (coprod X), REL(X) #); end; registration let S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S; cluster DTConMSA(X) -> strict non empty; end; theorem :: MSAFREE:6 for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S holds NonTerminals(DTConMSA(X))c= [:the carrier' of S,{the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA(X)) & (X is non-empty implies NonTerminals(DTConMSA(X)) = [:the carrier' of S,{the carrier of S}:] & Terminals (DTConMSA(X)) = Union (coprod X)); reserve x for set; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster DTConMSA(X) -> with_terminals with_nonterminals with_useful_nonterminals; end; theorem :: MSAFREE:7 for S be non void non empty ManySortedSign, X be ManySortedSet of the carrier of S, t be set holds (t in Terminals DTConMSA(X) & X is non-empty implies ex s be SortSymbol of S, x be set st x in X.s & t = [x,s]) & for s be SortSymbol of S, x be set st x in X.s holds [x,s] in Terminals DTConMSA(X); definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S; func Sym(o,X) ->Symbol of DTConMSA(X) equals :: MSAFREE:def 9 [o,the carrier of S]; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; func FreeSort(X,s) -> Subset of TS(DTConMSA(X)) equals :: MSAFREE:def 10 {a where a is Element of TS(DTConMSA(X)): (ex x be set st x in X.s & a = root-tree [x,s]) or ex o be OperSymbol of S st [o,the carrier of S] = a.{} & the_result_sort_of o = s}; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; cluster FreeSort(X,s) -> non empty; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeSort(X) -> ManySortedSet of the carrier of S means :: MSAFREE:def 11 for s be SortSymbol of S holds it.s = FreeSort(X,s); end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeSort(X) -> non-empty; end; theorem :: MSAFREE:8 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, x be set st x in (( FreeSort X)# * (the Arity of S)).o holds x is FinSequence of TS(DTConMSA(X)); theorem :: MSAFREE:9 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS (DTConMSA(X)) holds p in ((FreeSort X)# * (the Arity of S)).o iff dom p = dom ( the_arity_of o) & for n be Nat st n in dom p holds p.n in FreeSort(X,( the_arity_of o)/.n); theorem :: MSAFREE:10 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S, p be FinSequence of TS (DTConMSA(X)) holds Sym(o,X) ==> roots p iff p in ((FreeSort X)# * (the Arity of S)).o; theorem :: MSAFREE:11 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds union rng (FreeSort X) = TS (DTConMSA(X )); theorem :: MSAFREE:12 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s1,s2 be SortSymbol of S st s1 <> s2 holds ( FreeSort X).s1 misses (FreeSort X).s2; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, o be OperSymbol of S; func DenOp(o,X) -> Function of ((FreeSort X)# * (the Arity of S)).o, (( FreeSort X) * (the ResultSort of S)).o means :: MSAFREE:def 12 for p be FinSequence of TS (DTConMSA(X)) st Sym(o,X) ==> roots p holds it.p = (Sym(o,X))-tree p; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeOper(X) -> ManySortedFunction of (FreeSort X)# * (the Arity of S), (FreeSort X) * (the ResultSort of S) means :: MSAFREE:def 13 for o be OperSymbol of S holds it.o = DenOp(o,X); end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeMSA(X) -> MSAlgebra over S equals :: MSAFREE:def 14 MSAlgebra (# FreeSort(X), FreeOper(X) #); end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; cluster FreeMSA(X) -> strict non-empty; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; func FreeGen(s,X) -> Subset of (FreeSort(X)).s means :: MSAFREE:def 15 for x be set holds x in it iff ex a be set st a in X.s & x = root-tree [a,s]; end; registration let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; cluster FreeGen(s,X) -> non empty; end; theorem :: MSAFREE:13 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S holds FreeGen(s,X) = { root-tree t where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X) & t`2 = s}; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func FreeGen(X) -> GeneratorSet of FreeMSA(X) means :: MSAFREE:def 16 for s be SortSymbol of S holds it.s = FreeGen(s,X); end; theorem :: MSAFREE:14 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds FreeGen(X)is non-empty; theorem :: MSAFREE:15 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds union rng FreeGen(X) = {root-tree t where t is Symbol of DTConMSA(X): t in Terminals DTConMSA(X)}; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, s be SortSymbol of S; func Reverse(s,X) -> Function of FreeGen(s,X),X.s means :: MSAFREE:def 17 for t be Symbol of DTConMSA(X) st root-tree t in FreeGen(s,X) holds it.(root-tree t) = t `1; end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S; func Reverse(X) -> ManySortedFunction of FreeGen(X),X means :: MSAFREE:def 18 for s be SortSymbol of S holds it.s = Reverse(s,X); end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, A be non-empty ManySortedSet of the carrier of S, F be ManySortedFunction of FreeGen(X), A, t be Symbol of DTConMSA(X); assume t in Terminals (DTConMSA(X)); func pi(F,A,t) -> Element of Union A means :: MSAFREE:def 19 for f be Function st f = F.(t`2) holds it = f.(root-tree t); end; definition let S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S, t be Symbol of DTConMSA(X); assume ex p be FinSequence st t ==> p; func @(X,t) -> OperSymbol of S means :: MSAFREE:def 20 [it,the carrier of S] = t; end; definition let S be non void non empty ManySortedSign, U0 be non-empty MSAlgebra over S , o be OperSymbol of S, p be FinSequence; assume p in Args(o,U0); func pi(o,U0,p) -> Element of Union (the Sorts of U0) equals :: MSAFREE:def 21 Den(o, U0).p; end; theorem :: MSAFREE:16 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds FreeGen(X) is free; theorem :: MSAFREE:17 for S be non void non empty ManySortedSign, X be non-empty ManySortedSet of the carrier of S holds FreeMSA(X) is free; registration let S be non void non empty ManySortedSign; cluster free strict for non-empty MSAlgebra over S; end; registration let S be non void non empty ManySortedSign, U0 be free MSAlgebra over S; cluster free for GeneratorSet of U0; end; theorem :: MSAFREE:18 for S be non void non empty ManySortedSign, U1 be non-empty MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be ManySortedFunction of U0,U1 st F is_epimorphism U0,U1; theorem :: MSAFREE:19 for S be non void non empty ManySortedSign, U1 be strict non-empty MSAlgebra over S ex U0 be strict free non-empty MSAlgebra over S, F be ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 & Image F = U1;