Journal of Formalized Mathematics
Volume 6, 1994
University of Bialystok
Copyright (c) 1994 Association of Mizar Users

### Many Sorted Algebras

by
Andrzej Trybulec

MML identifier: MSUALG_1
[ Mizar article, MML identifier index ]

```environ

vocabulary ZF_REFLE, PBOOLE, BOOLE, RELAT_1, FUNCT_1, PRALG_1, TDGROUP,
CARD_3, FINSEQ_2, FINSEQ_1, FUNCOP_1, FUNCT_2, AMI_1, QC_LANG1, UNIALG_1,
PARTFUN1, REALSET1, MSUALG_1;
notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1,
FUNCT_2, FINSEQ_1, STRUCT_0, FUNCOP_1, PARTFUN1, FINSEQ_2, CARD_3,
PBOOLE, REALSET1, PRALG_1, UNIALG_1;
constructors REALSET1, PRALG_1, MEMBERED, XBOOLE_0;
clusters FUNCT_1, PBOOLE, UNIALG_1, TEX_2, PRALG_1, RELSET_1, STRUCT_0,
FINSEQ_2, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS,
ORDINAL2;
requirements BOOLE, SUBSET;

begin :: Preliminaries

reserve i,j for set,
I for set;

theorem :: MSUALG_1:1
not ex M being non-empty ManySortedSet of I st {} in rng M;

scheme MSSEx { I() -> set, P[set,set] }:
ex f being ManySortedSet of I() st
for i st i in I() holds P[i,f.i]
provided  for i st i in I() ex j st P[i,j];

scheme MSSLambda { I() -> set, F(set) -> set }:
ex f being ManySortedSet of I() st
for i st i in I() holds f.i = F(i);

definition let I be set; let M be ManySortedSet of I;
mode Component of M is Element of rng M;
end;

theorem :: MSUALG_1:2
for I being non empty set
for M being ManySortedSet of I, A being Component of M
ex i st i in I & A = M.i;

theorem :: MSUALG_1:3
for M being ManySortedSet of I, i st i in I holds M.i is Component of M;

definition let I; let B be ManySortedSet of I;
mode Element of B -> ManySortedSet of I means
:: MSUALG_1:def 1
for i st i in I holds it.i is Element of B.i;
end;

begin :: Many Sorted Functions

definition let I;
let A be ManySortedSet of I, B be ManySortedSet of I;
mode ManySortedFunction of A,B -> ManySortedSet of I means
:: MSUALG_1:def 2
for i st i in I holds it.i is Function of A.i, B.i;
end;

definition let I;
let A be ManySortedSet of I, B be ManySortedSet of I;
cluster ->Function-yielding ManySortedFunction of A,B;
end;

definition let I be set; let M be ManySortedSet of I;
func M# -> ManySortedSet of I* means
:: MSUALG_1:def 3
for i being Element of I* holds it.i = product(M*i);
end;

definition let I be set; let M be non-empty ManySortedSet of I;
cluster M# -> non-empty;
end;

definition let I; let J be non empty set;
let O be Function of I,J;
let F be ManySortedSet of J;
redefine func F*O -> ManySortedSet of I;
end;

definition let I; let J be non empty set;
let O be Function of I,J;
let F be non-empty ManySortedSet of J;
redefine func F*O -> non-empty ManySortedSet of I;
end;

definition let a be set;
func *-->a -> Function of NAT,{a}* means
:: MSUALG_1:def 4
for n being Nat holds it.n = n |-> a;
end;

reserve D for non empty set,
n for Nat;

theorem :: MSUALG_1:4
for a,b being set holds ({a} --> b)*(n|->a) = n |-> b;

theorem :: MSUALG_1:5
for a being set
for M being ManySortedSet of {a} st M = {a} --> D
holds (M#**-->a).n = Funcs(Seg n, D);

definition let I,i;
redefine func I --> i -> Function of I,{i};
end;

begin :: Many Sorted Signatures

definition
struct(1-sorted) ManySortedSign
(# carrier -> set,
OperSymbols -> set,
Arity -> Function of the OperSymbols, the carrier*,
ResultSort -> Function of the OperSymbols, the carrier
#);
end;

definition let IT be ManySortedSign;
attr IT is void means
:: MSUALG_1:def 5
the OperSymbols of IT = {};
end;

definition
cluster void strict non empty ManySortedSign;
cluster non void strict non empty ManySortedSign;
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 OperSymbols 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
:: MSUALG_1:def 6
(the Arity of S).o;
func the_result_sort_of o -> Element of S equals
:: MSUALG_1:def 7
(the ResultSort of S).o;
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
:: MSUALG_1:def 8
the Sorts of A is non-empty;
end;

definition let S;
cluster strict non-empty MSAlgebra over S;
end;

definition let S be 1-sorted;
cluster strict non-empty many-sorted over S;
end;

definition let S be 1-sorted; let A be non-empty many-sorted over S;
cluster the Sorts of A -> non-empty;
end;

definition let S; let A be non-empty MSAlgebra over S;
cluster -> non empty Component of the Sorts of A;
cluster -> non empty Component of (the Sorts of A)#;
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
:: MSUALG_1:def 9
((the Sorts of A)# * the Arity of S).o;
func Result(o,A) -> Component of the Sorts of A equals
:: MSUALG_1:def 10
((the Sorts of A) * the ResultSort of S).o;
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
:: MSUALG_1:def 11
(the Charact of A).o;
end;

theorem :: MSUALG_1:6
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

theorem :: MSUALG_1:7
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;

theorem :: MSUALG_1:8
for h being homogeneous quasi_total non empty PartFunc of D*,D
holds dom h = Funcs(Seg(arity h),D);

theorem :: MSUALG_1:9
for A being Universal_Algebra holds signature A is non empty;

begin :: Relationship to one sorted algebras

definition let A be Universal_Algebra;
redefine func signature A -> FinSequence of NAT;
end;

definition let IT be ManySortedSign;
attr IT is segmental means
:: MSUALG_1:def 12
ex n st the OperSymbols of IT = Seg n;
end;

theorem :: MSUALG_1:10
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;

definition
cluster segmental trivial non void strict non empty ManySortedSign;
end;

definition let A be Universal_Algebra;
func MSSign A -> non void strict segmental trivial ManySortedSign means
:: MSUALG_1:def 13

the carrier of it = {0} &
the OperSymbols of it = dom signature A &
the Arity of it = (*-->0)*signature A &
the ResultSort of it = dom signature(A)-->0;
end;

definition let A be Universal_Algebra;
cluster MSSign A -> non empty;
end;

definition let A be Universal_Algebra;
func MSSorts A -> non-empty ManySortedSet of the carrier of MSSign A equals
:: MSUALG_1:def 14
{0}-->the carrier of A;
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
:: MSUALG_1:def 15
the charact of A;
end;

definition let A be Universal_Algebra;
func MSAlg A -> strict MSAlgebra over MSSign A equals
:: MSUALG_1:def 16
MSAlgebra(#MSSorts A,MSCharact A#);
end;

definition let A be Universal_Algebra;
cluster MSAlg A -> non-empty;
end;

:: Manysorted Algebras with 1 Sort Only

definition let MS be trivial non empty ManySortedSign;
let A be MSAlgebra over MS;
func the_sort_of A -> set means
:: MSUALG_1:def 17
ex c being Component of the Sorts of A st it = c;
end;

definition let MS be trivial non empty ManySortedSign;
let A be non-empty MSAlgebra over MS;
cluster the_sort_of A -> non empty;
end;

theorem :: MSUALG_1:11
for MS being segmental trivial non void non empty 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;

theorem :: MSUALG_1:12
for A being non empty set, n holds n-tuples_on A c= A*;

theorem :: MSUALG_1:13
for MS being segmental trivial non void non empty ManySortedSign,
i being OperSymbol of MS,
A being non-empty MSAlgebra over MS holds Args(i,A) c= (the_sort_of A)*;

theorem :: MSUALG_1:14
for MS being segmental trivial non void non empty 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);

definition let MS be segmental trivial non void non empty ManySortedSign;
let A be non-empty MSAlgebra over MS;
func the_charact_of A -> PFuncFinSequence of the_sort_of A equals
:: MSUALG_1:def 18
the Charact of A;
end;

reserve MS for segmental trivial non void non empty 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
:: MSUALG_1:def 19
UAStr(#the_sort_of A, the_charact_of A#);
end;

theorem :: MSUALG_1:15
for A being strict Universal_Algebra holds
A = 1-Alg MSAlg A;

theorem :: MSUALG_1:16
for A being Universal_Algebra
for f being Function of dom signature A, {0}*
st f = (*-->0)*signature A
holds MSSign A = ManySortedSign(#{0},dom signature A,f,dom signature(A)-->0#);
```