:: Many Sorted Algebras
:: by Andrzej Trybulec
::
:: Received April 21, 1994
:: Copyright (c) 1994-2017 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;
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;
cluster non void strict non empty for 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 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
:: MSUALG_1:def 1
(the Arity of S).o;
func the_result_sort_of o -> Element of S equals
:: MSUALG_1:def 2
(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 3
the Sorts of A is non-empty;
end;
registration
let S;
cluster strict non-empty for MSAlgebra over S;
end;
registration
let S be 1-sorted;
cluster strict non-empty for many-sorted over S;
end;
registration
let S be 1-sorted;
let A be non-empty many-sorted over S;
cluster the Sorts of A -> non-empty;
end;
registration
let S;
let A be non-empty MSAlgebra over S;
cluster -> non empty for Component of the Sorts of A;
cluster -> non empty for 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 4
((the Sorts of A)# *
the Arity of S).o;
func Result(o,A) -> Component of the Sorts of A equals
:: MSUALG_1:def 5
((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 6
(the Charact of A
).o;
end;
theorem :: MSUALG_1:1
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;
theorem :: MSUALG_1:2
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:3
for h being homogeneous quasi_total non empty PartFunc of D*,D
holds dom h = Funcs(Seg(arity h),D);
theorem :: MSUALG_1:4
for A being Universal_Algebra holds signature A is non empty;
begin :: Relationship to one sorted algebras
definition
let IT be ManySortedSign;
attr IT is segmental means
:: MSUALG_1:def 7
ex n st the carrier' of IT = Seg n;
end;
theorem :: MSUALG_1:5
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;
registration
cluster segmental non void strict 1-element for ManySortedSign;
end;
definition
let A be Universal_Algebra;
func MSSign A -> non void strict segmental trivial ManySortedSign means
:: MSUALG_1:def 8
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;
end;
registration
let A be Universal_Algebra;
cluster MSSign A -> 1-element;
end;
definition
let A be Universal_Algebra;
func MSSorts A -> non-empty ManySortedSet of the carrier of MSSign A equals
:: MSUALG_1:def 9
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 10
the charact of A;
end;
definition
let A be Universal_Algebra;
func MSAlg A -> strict MSAlgebra over MSSign A equals
:: MSUALG_1:def 11
MSAlgebra(#MSSorts A, MSCharact A#);
end;
registration
let A be Universal_Algebra;
cluster MSAlg A -> non-empty;
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
:: MSUALG_1:def 12
it is Component of the Sorts of A;
end;
registration
let MS be 1-element ManySortedSign;
let A be non-empty MSAlgebra over MS;
cluster the_sort_of A -> non empty;
end;
theorem :: MSUALG_1:6
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;
theorem :: MSUALG_1:7
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)*;
theorem :: MSUALG_1:8
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);
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
:: MSUALG_1:def 13
the
Charact of A;
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
:: MSUALG_1:def 14
UAStr(#the_sort_of
A, the_charact_of A#);
end;
theorem :: MSUALG_1:9
for A being strict Universal_Algebra holds A = 1-Alg MSAlg A;
theorem :: MSUALG_1:10
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#);