:: Many Sorted Algebras
:: by Andrzej Trybulec
::
:: Received April 21, 1994
:: Copyright (c) 1994-2026 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 STRUCT_0, FUNCT_1, RELAT_1, XBOOLE_0, FUNCOP_1, SUBSET_1,
MARGREL1, PBOOLE, CARD_1, NAT_1, UNIALG_1, FUNCT_2, PARTFUN1, FINSEQ_2,
TARSKI, FINSEQ_1, NUMBERS, ZFMISC_1, CARD_3, MSUALG_1;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, NAT_1,
RELAT_1, FUNCT_1, FUNCT_2, FINSEQ_1, STRUCT_0, PARTFUN1, FINSEQ_2,
CARD_3, FUNCOP_1, PBOOLE, MARGREL1, UNIALG_1;
constructors CARD_3, PBOOLE, REALSET2, UNIALG_1, RELSET_1, MARGREL1;
registrations FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSEQ_2, RELAT_1,
PBOOLE, STRUCT_0, UNIALG_1, FUNCT_2, CARD_1, ZFMISC_1, MARGREL1,
FINSEQ_1;
requirements BOOLE, SUBSET, NUMERALS;
definitions TARSKI, FINSEQ_1, FUNCT_1, PBOOLE, XBOOLE_0, MARGREL1;
equalities XBOOLE_0, FUNCOP_1;
expansions STRUCT_0;
theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, UNIALG_1, PBOOLE,
FUNCT_2, CARD_3, FINSEQ_3, FINSEQ_2, RELAT_1, RELSET_1, ORDINAL1,
MARGREL1, CARD_1;
begin
reserve i for object;
begin :: Many Sorted Signatures
definition
struct(2-sorted) ManySortedSign (# carrier,carrier' -> set, Arity ->
Function of the carrier', the carrier*, ResultSort -> Function of the carrier',
the carrier #);
end;
registration
cluster void strict non empty for ManySortedSign;
existence
proof
reconsider g = {}-->{} as Function of {},{{}};
reconsider f = {}-->{} as Function of {},{{}}*;
take ManySortedSign(#{{}},{},f,g#);
thus thesis;
end;
cluster non void strict non empty for ManySortedSign;
existence
proof
{} in {{}}* by FINSEQ_1:49;
then reconsider f = {{}}-->{} as Function of {{}},{{}}* by FUNCOP_1:46;
reconsider g = {{}}-->{} as Function of {{}},{{}};
take ManySortedSign(#{{}},{{}},f,g#);
thus thesis;
end;
end;
reserve S for non empty ManySortedSign;
definition
let S;
mode SortSymbol of S is Element of S;
mode OperSymbol of S is Element of the carrier' of S;
end;
definition
let S be non void non empty ManySortedSign;
let o be OperSymbol of S;
func the_arity_of o -> Element of (the carrier of S)* equals
(the Arity of S).o;
coherence;
func the_result_sort_of o -> Element of S equals
(the ResultSort of S).o;
coherence;
end;
begin :: Many Sorted Algebras
definition
let S be 1-sorted;
struct many-sorted over S (# Sorts -> ManySortedSet of the carrier of S #);
end;
definition
let S;
struct(many-sorted over S) MSAlgebra over S
(# Sorts -> ManySortedSet of the carrier of S,
Charact -> ManySortedFunction of
((the Sorts)# * the Arity of S), the Sorts * the ResultSort of S#);
end;
definition
let S be 1-sorted;
let A be many-sorted over S;
attr A is non-empty means
:Def3:
the Sorts of A is non-empty;
end;
registration
let S;
cluster strict non-empty for MSAlgebra over S;
existence
proof
reconsider s = (the carrier of S) --> {0} as ManySortedSet of the carrier
of S;
set o = the ManySortedFunction of s# * the Arity of S, s * the ResultSort of S;
take MSAlgebra(#s,o#);
thus MSAlgebra(#s,o#) is strict;
let i be object;
assume i in the carrier of S;
hence thesis;
end;
end;
registration
let S be 1-sorted;
cluster strict non-empty for many-sorted over S;
existence
proof
reconsider s = (the carrier of S) --> {0} as ManySortedSet of the carrier
of S;
take many-sorted(#s#);
thus many-sorted (#s#) is strict;
let i be object;
assume i in the carrier of S;
hence thesis;
end;
end;
registration
let S be 1-sorted;
let A be non-empty many-sorted over S;
cluster the Sorts of A -> non-empty;
coherence by Def3;
end;
registration
let S;
let A be non-empty MSAlgebra over S;
cluster -> non empty for Component of the Sorts of A;
coherence
proof
let C be Component of the Sorts of A;
ex i being object st i in the carrier of S & C = (the Sorts of A).i
by PBOOLE:138;
hence thesis;
end;
cluster -> non empty for Component of (the Sorts of A)#;
coherence
proof
let C be Component of (the Sorts of A)#;
ex i being object st i in (the carrier of S)* & C = (the Sorts of A)#.i
by PBOOLE:138;
hence thesis;
end;
end;
definition
let S be non void non empty ManySortedSign;
let o be OperSymbol of S;
let A be MSAlgebra over S;
func Args(o,A) -> Component of (the Sorts of A)# equals
((the Sorts of A)# *
the Arity of S).o;
coherence
proof
o in the carrier' of S;
then o in dom((the Sorts of A)# * the Arity of S) by PARTFUN1:def 2;
then
((the Sorts of A)# * the Arity of S).o in rng((the Sorts of A)# * the
Arity of S) by FUNCT_1:def 3;
hence thesis by FUNCT_1:14;
end;
correctness;
func Result(o,A) -> Component of the Sorts of A equals
((the Sorts of A) *
the ResultSort of S).o;
coherence
proof
o in the carrier' of S;
then o in dom((the Sorts of A) * the ResultSort of S) by PARTFUN1:def 2;
then ((the Sorts of A) * the ResultSort of S).o in rng((the Sorts of A) *
the ResultSort of S) by FUNCT_1:def 3;
hence thesis by FUNCT_1:14;
end;
correctness;
end;
definition
let S be non void non empty ManySortedSign;
let o be OperSymbol of S;
let A be MSAlgebra over S;
func Den(o,A) -> Function of Args(o,A), Result(o,A) equals
(the Charact of A
).o;
coherence by PBOOLE:def 15;
end;
theorem
for S being non void non empty ManySortedSign, o being OperSymbol of S
, A being non-empty MSAlgebra over S holds Den(o,A) is non empty;
begin :: On the one-sorted algebras
reserve D for non empty set,
n for Nat;
Lm1: for h being homogeneous quasi_total non empty PartFunc of D*,D holds dom
h = (arity h)-tuples_on D
proof
let h be homogeneous quasi_total non empty PartFunc of D*,D;
set x0 = the Element of dom h;
A1: x0 in dom h;
A2: dom h c= D* by RELAT_1:def 18;
then reconsider x0 as FinSequence of D by A1,FINSEQ_1:def 11;
thus dom h c= (arity h)-tuples_on D
proof
let x be object;
assume
A3: x in dom h;
then reconsider f = x as FinSequence of D by A2,FINSEQ_1:def 11;
A4: f is Element of (len f)-tuples_on D by FINSEQ_2:92;
len f = arity h by A3,MARGREL1:def 25;
hence thesis by A4;
end;
let x be object;
assume x in (arity h)-tuples_on D;
then reconsider f = x as Element of (arity h)-tuples_on D;
len x0 = arity h by MARGREL1:def 25
.= len f by CARD_1:def 7;
hence thesis by MARGREL1:def 22;
end;
theorem Th2:
for C being set, A,B being non empty set, F being PartFunc of C,A
, G being Function of A,B holds G*F is Function of dom F,B
proof
let C be set;
let A,B be non empty set;
let F be PartFunc of C,A;
let G be Function of A,B;
dom G = A by FUNCT_2:def 1;
then rng F c= dom G by RELAT_1:def 19;
then
A1: dom(G*F) = dom F by RELAT_1:27;
rng(G*F) c= B by RELAT_1:def 19;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
theorem Th3:
for h being homogeneous quasi_total non empty PartFunc of D*,D
holds dom h = Funcs(Seg(arity h),D)
proof
let h be homogeneous quasi_total non empty PartFunc of D*,D;
thus dom h = (arity h)-tuples_on D by Lm1
.= Funcs(Seg(arity h),D) by FINSEQ_2:93;
end;
theorem Th4:
for A being Universal_Algebra holds signature A is non empty
proof
let A be Universal_Algebra;
len(the charact of A) <> 0;
then len(signature A) <> 0 by UNIALG_1:def 4;
hence thesis;
end;
begin :: Relationship to one sorted algebras
definition
let IT be ManySortedSign;
attr IT is segmental means
:Def7:
ex n st the carrier' of IT = Seg n;
end;
theorem Th5:
for S being non empty ManySortedSign st S is trivial for A being
MSAlgebra over S, c1,c2 being Component of the Sorts of A holds c1 = c2
proof
let S be non empty ManySortedSign such that
A1: S is trivial;
let A be MSAlgebra over S, c1,c2 be Component of the Sorts of A;
(ex i1 being object st i1 in the carrier of S & c1 = (the Sorts of A).i1 )&
ex i2 being object st i2 in the carrier of S & c2 = (the Sorts of A).i2
by
PBOOLE:138;
hence thesis by A1;
end;
reconsider z = 0 as Element of {0} by TARSKI:def 1;
Lm2: for A being Universal_Algebra for f being Function of dom signature A, {0
}* holds ManySortedSign (#{0},dom signature(A),f,dom signature(A)-->z#) is
segmental 1-element non void strict
proof
let A be Universal_Algebra;
let f be Function of dom signature A, {0}*;
set S = ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->z#);
A1: S is segmental
proof
take len signature(A);
thus thesis by FINSEQ_1:def 3;
end;
signature A <> {} by Th4;
hence thesis by A1;
end;
registration
cluster segmental non void strict 1-element for ManySortedSign;
existence
proof
set A = the Universal_Algebra;
reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}*
by Th2;
ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->z#) is
segmental non void strict 1-element by Lm2;
hence thesis;
end;
end;
definition
let A be Universal_Algebra;
func MSSign A -> non void strict segmental trivial ManySortedSign means
:Def8: the carrier of it = {0} & the carrier' of it = dom signature A & the
Arity of it = (*-->0)*signature A &
the ResultSort of it = dom signature(A)-->0;
correctness
proof
reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}*
by Th2;
ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->z#) is
segmental trivial non void strict by Lm2;
hence thesis;
end;
end;
registration
let A be Universal_Algebra;
cluster MSSign A -> 1-element;
coherence
by Def8;
end;
definition
let A be Universal_Algebra;
func MSSorts A -> non-empty ManySortedSet of the carrier of MSSign A equals
0.-->the carrier of A;
coherence
proof
set M = {0}-->the carrier of A;
the carrier of MSSign A = {0} by Def8;
then reconsider M as ManySortedSet of the carrier of MSSign A;
M is non-empty;
hence thesis;
end;
correctness;
end;
definition
let A be Universal_Algebra;
func MSCharact A -> ManySortedFunction of (MSSorts A)# * the Arity of MSSign
A, (MSSorts A)* the ResultSort of MSSign A equals
the charact of A;
coherence
proof
A1: the ResultSort of MSSign A = dom signature(A)-->0 by Def8;
reconsider OS = the carrier' of MSSign A as non empty set;
reconsider DO = (MSSorts A)# * the Arity of MSSign A, RO = (MSSorts A)*
the ResultSort of MSSign A as ManySortedSet of OS;
A2: the carrier' of MSSign A = dom signature A by Def8;
len signature A = len the charact of A by UNIALG_1:def 4;
then
A3: dom the charact of A = OS by A2,FINSEQ_3:29;
then reconsider O = the charact of A as ManySortedSet of OS by
PARTFUN1:def 2,RELAT_1:def 18;
A4: the Arity of MSSign A = (*-->0)*signature A by Def8;
reconsider O as ManySortedFunction of OS;
A5: the carrier of MSSign A = {0} by Def8;
O is ManySortedFunction of DO,RO
proof
set D = the carrier of A;
let i;
reconsider M = 0.-->D as ManySortedSet of {0};
A6: 0 in {0} by TARSKI:def 1;
assume
A7: i in OS;
then reconsider n = i as Nat by A2;
reconsider h = O.n as homogeneous quasi_total non empty PartFunc of D*,D
by A3,A7,MARGREL1:def 24,UNIALG_1:1;
n in dom(dom signature(A)-->0) by A2,A7;
then RO.i = (MSSorts A).((dom signature(A)-->0).n) by A1,FUNCT_1:13
.= ({0}-->the carrier of A).0 by A2,A7,FUNCOP_1:7
.= the carrier of A by A6,FUNCOP_1:7;
then
A8: rng h c= RO.i by RELAT_1:def 19;
reconsider o = i as Element of OS by A7;
DO.i = ((MSSorts A)#*(*-->0)*signature A).n by A4,RELAT_1:36
.= (M#*(*-->0)).((signature A).n) by A5,A2,A7,FUNCT_1:13
.= (M#*(*-->0)).arity h by A2,A7,UNIALG_1:def 4
.= Funcs(Seg arity h,D) by FINSEQ_2:145
.= dom(O.o) by Th3;
hence thesis by A8,FUNCT_2:def 1,RELSET_1:4;
end;
hence thesis;
end;
correctness;
end;
definition
let A be Universal_Algebra;
func MSAlg A -> strict MSAlgebra over MSSign A equals
MSAlgebra(#MSSorts A, MSCharact A#);
correctness;
end;
registration
let A be Universal_Algebra;
cluster MSAlg A -> non-empty;
coherence;
end;
:: Manysorted Algebras with 1 Sort Only
definition
let MS be 1-element ManySortedSign;
let A be MSAlgebra over MS;
func the_sort_of A -> set means
:Def12:
it is Component of the Sorts of A;
existence
proof
set c = the Component of the Sorts of A;
take c;
thus thesis;
end;
uniqueness by Th5;
end;
registration
let MS be 1-element ManySortedSign;
let A be non-empty MSAlgebra over MS;
cluster the_sort_of A -> non empty;
coherence
proof
the_sort_of A is Component of the Sorts of A by Def12;
hence thesis;
end;
end;
theorem Th6:
for MS being segmental non void 1-element ManySortedSign
, i being OperSymbol of MS, A being non-empty MSAlgebra over MS holds Args(i,A)
= (len the_arity_of i)-tuples_on the_sort_of A
proof
let MS be segmental non void 1-element ManySortedSign, i be
OperSymbol of MS, A be non-empty MSAlgebra over MS;
set m = len the_arity_of i;
dom(the Arity of MS) = the carrier' of MS by FUNCT_2:def 1;
then
A1: Args(i,A) = (the Sorts of A)# .((the Arity of MS).i) by FUNCT_1:13
.= product((the Sorts of A)*the_arity_of i) by FINSEQ_2:def 5;
A2: rng the_arity_of i c= the carrier of MS by FINSEQ_1:def 4;
then rng the_arity_of i c= dom the Sorts of A by PARTFUN1:def 2;
then
A3: dom((the Sorts of A)*the_arity_of i) = dom the_arity_of i by RELAT_1:27;
A4: ex n being Nat st dom the_arity_of i = Seg n by FINSEQ_1:def 2;
thus Args(i,A) c= m-tuples_on the_sort_of A
proof
let x be object;
assume x in Args(i,A);
then consider g being Function such that
A5: x = g and
A6: dom g = dom((the Sorts of A)*the_arity_of i) and
A7: for j being object st j in dom((the Sorts of A)*the_arity_of i)
holds g.j in ((the Sorts of A)*the_arity_of i).j by A1,CARD_3:def 5;
reconsider p = g as FinSequence by A4,A3,A6,FINSEQ_1:def 2;
rng p c= the_sort_of A
proof
let j be object;
assume j in rng p;
then consider u being object such that
A8: u in dom g and
A9: p.u = j by FUNCT_1:def 3;
(the_arity_of i).u in rng the_arity_of i by A3,A6,A8,FUNCT_1:def 3;
then
A10: (the Sorts of A).((the_arity_of i).u) is Component of the Sorts of
A by A2,PBOOLE:139;
g.u in ((the Sorts of A)*the_arity_of i).u by A6,A7,A8;
then g.u in (the Sorts of A).((the_arity_of i).u) by A3,A6,A8,FUNCT_1:13;
hence thesis by A9,A10,Def12;
end;
then
A11: p is FinSequence of the_sort_of A by FINSEQ_1:def 4;
len p = m by A3,A6,FINSEQ_3:29;
then x is Element of m-tuples_on the_sort_of A by A5,A11,FINSEQ_2:92;
hence thesis;
end;
let x be object;
assume x in m-tuples_on the_sort_of A;
then x in Funcs(Seg m, the_sort_of A) by FINSEQ_2:93;
then consider g being Function such that
A12: x = g and
A13: dom g = Seg m and
A14: rng g c= the_sort_of A by FUNCT_2:def 2;
A15: dom g = dom((the Sorts of A)*the_arity_of i) by A3,A13,FINSEQ_1:def 3;
now
let x be object;
assume
A16: x in dom((the Sorts of A)*the_arity_of i);
then (the_arity_of i).x in rng the_arity_of i by A3,FUNCT_1:def 3;
then
A17: (the Sorts of A).((the_arity_of i).x) is Component of the Sorts of A
by A2,PBOOLE:139;
g.x in rng g by A15,A16,FUNCT_1:def 3;
then g.x in the_sort_of A by A14;
then g.x in (the Sorts of A).((the_arity_of i).x) by A17,Def12;
hence g.x in ((the Sorts of A)*the_arity_of i).x by A3,A16,FUNCT_1:13;
end;
hence thesis by A1,A12,A15,CARD_3:9;
end;
theorem Th7:
for MS being segmental non void 1-element ManySortedSign
, i being OperSymbol of MS, A being non-empty MSAlgebra over MS holds Args(i,A)
c= (the_sort_of A)*
proof
let MS be segmental non void 1-element ManySortedSign, i be
OperSymbol of MS, A be non-empty MSAlgebra over MS;
Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A by Th6;
hence thesis by FINSEQ_2:142;
end;
theorem Th8:
for MS being segmental non void 1-element ManySortedSign
, A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of
PFuncs((the_sort_of A)*,the_sort_of A)
proof
let MS be segmental non void 1-element ManySortedSign, A be
non-empty MSAlgebra over MS;
A1: dom the Charact of A = the carrier' of MS by PARTFUN1:def 2;
ex n being Element of NAT st the carrier' of MS = Seg n
proof
consider n such that
A2: the carrier' of MS = Seg n by Def7;
n in NAT by ORDINAL1:def 12;
hence thesis by A2;
end;
then reconsider f = the Charact of A as FinSequence by A1,FINSEQ_1:def 2;
f is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A)
proof
let x be object;
assume x in rng f;
then consider i being object such that
A3: i in the carrier' of MS and
A4: f.i = x by A1,FUNCT_1:def 3;
reconsider i as OperSymbol of MS by A3;
A5: (the Sorts of A).((the ResultSort of MS).i) is Component of the Sorts
of A by PBOOLE:139;
dom(the ResultSort of MS) = the carrier' of MS by FUNCT_2:def 1;
then ((the Sorts of A)*the ResultSort of MS).i = (the Sorts of A).((the
ResultSort of MS).i) by FUNCT_1:13
.= the_sort_of A by A5,Def12;
then
A6: x is Function of Args(i,A),the_sort_of A by A4,PBOOLE:def 15;
Args(i,A) c= (the_sort_of A)* by Th7;
then x is PartFunc of (the_sort_of A)*,the_sort_of A by A6,RELSET_1:7;
hence thesis by PARTFUN1:45;
end;
hence thesis;
end;
definition
let MS be segmental non void 1-element ManySortedSign;
let A be non-empty MSAlgebra over MS;
func the_charact_of A -> PFuncFinSequence of the_sort_of A equals
the
Charact of A;
coherence by Th8;
end;
reserve MS for segmental non void 1-element ManySortedSign,
A for non-empty MSAlgebra over MS,
h for PartFunc of (the_sort_of A)*,(the_sort_of A) ,
x,y for FinSequence of the_sort_of A;
definition
let MS,A;
func 1-Alg A -> non-empty strict Universal_Algebra equals
UAStr(#the_sort_of
A, the_charact_of A#);
coherence
proof
A1: the_charact_of A is quasi_total
proof
let n,h such that
A2: n in dom(the_charact_of A) and
A3: h = (the_charact_of A).n;
reconsider o = n as OperSymbol of MS by A2,PARTFUN1:def 2;
let x,y such that
A4: len x = len y and
A5: x in dom h;
A6: ((the Sorts of A)# * the Arity of MS).o = Args(o,A);
h is Function of ((the Sorts of A)# * the Arity of MS).o, ((the
Sorts of A) * the ResultSort of MS).o by A3,PBOOLE:def 15;
then
A7: dom h = ((the Sorts of A)# * the Arity of MS).o by FUNCT_2:def 1
.= (len the_arity_of o)-tuples_on the_sort_of A by A6,Th6;
then len y = len the_arity_of o by A4,A5,CARD_1:def 7;
then y is Element of dom h by A7,FINSEQ_2:92;
hence thesis by A5;
end;
A8: the_charact_of A is homogeneous
proof
let n,h such that
A9: n in dom(the_charact_of A) and
A10: h = (the_charact_of A).n;
reconsider o = n as OperSymbol of MS by A9,PARTFUN1:def 2;
thus dom h is with_common_domain
proof
let x,y being FinSequence such that
A11: x in dom h and
A12: y in dom h;
A13: ((the Sorts of A)# * the Arity of MS).o = Args(o,A);
h is Function of ((the Sorts of A)# * the Arity of MS).o, ((the
Sorts of A) * the ResultSort of MS).o by A10,PBOOLE:def 15;
then
A14: dom h = ((the Sorts of A)# * the Arity of MS).o by FUNCT_2:def 1
.= (len the_arity_of o)-tuples_on the_sort_of A by A13,Th6;
hence len x = len the_arity_of o by A11,CARD_1:def 7
.= len y by A12,A14,CARD_1:def 7;
end;
end;
the_charact_of A is non-empty
proof
let n be object;
assume n in dom the_charact_of A;
then reconsider o = n as OperSymbol of MS by PARTFUN1:def 2;
set h = (the_charact_of A).n;
h = Den(o,A);
hence thesis;
end;
hence thesis by A1,A8,UNIALG_1:def 1,def 2,def 3;
end;
correctness;
end;
theorem
for A being strict Universal_Algebra holds A = 1-Alg MSAlg A
proof
let A be strict Universal_Algebra;
the carrier of A in {the carrier of A} by TARSKI:def 1;
then the carrier of A in rng the Sorts of MSAlg A by FUNCOP_1:8;
hence thesis by Def12;
end;
theorem
for A being Universal_Algebra for f being Function of dom signature A,
{0}* for z being Element of {0} st f = (*-->0)*signature A holds MSSign A =
ManySortedSign(#{0},dom signature A,f,dom signature(A)-->z#)
proof
let A be Universal_Algebra;
let f be Function of dom signature A, {0}*;
let z be Element of {0};
A1: the carrier' of MSSign A = dom signature A & the Arity of MSSign A = (
*-->0) *signature A by Def8;
z = 0 & the carrier of MSSign A = {0} by Def8,TARSKI:def 1;
hence thesis by A1,Def8;
end;