The abstract of the Mizar article:

Many Sorted Algebras

by

Andrzej Trybulec

Received April 21, 1994

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#);