Volume 6, 1994

University of Bialystok

Copyright (c) 1994 Association of Mizar Users

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

Back to top