:: Free Many Sorted Universal Algebra
:: by Beata Perkowska
::
:: Received April 27, 1994
:: Copyright (c) 1994-2016 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, PARTFUN1, RELSET_1, XTUPLE_0;
requirements NUMERALS, 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;