:: Many Sorted Algebras
:: by Andrzej Trybulec
::
:: Received April 21, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users


begin

begin

definition
attrc1 is strict ;
struct ManySortedSign  ->  2-sorted ;
aggrManySortedSign(# carrier, carrier', Arity, ResultSort #) ->  ManySortedSign ;
sel Arity c1 ->  Function of the carrier' of c1,( the carrier of c1 *);
sel ResultSort c1 ->  Function of the carrier' of c1, the carrier of c1;
end;

registration
cluster non empty void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is void & b1 is strict & not b1 is empty )
proofend;
cluster non empty non void strict for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( not b1 is void & b1 is strict & not b1 is empty )
proofend;
end;

definition
let S be non empty ManySortedSign ;
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 empty non void 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;
coherence
 the Arity of S . o is Element of the carrier of S * ;
func the_result_sort_of o ->  Element of S equals :: MSUALG_1:def 2
 the ResultSort of S . o;
coherence
 the ResultSort of S . o is Element of S ;
end;

:: deftheorem  defines the_arity_of MSUALG_1:def_1_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S holds the_arity_of o = the Arity of S . o;

:: deftheorem  defines the_result_sort_of MSUALG_1:def_2_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S holds the_result_sort_of o = the ResultSort of S . o;

begin

definition
let S be 1-sorted ;
attrc2 is strict ;
struct many-sorted over S -> ;
aggrmany-sorted(# Sorts #) ->  many-sorted over S;
sel Sorts c2 ->  ManySortedSet of the carrier of S;
end;

definition
let S be non empty ManySortedSign ;
attrc2 is strict ;
struct MSAlgebra over S ->  many-sorted over S;
aggrMSAlgebra(# Sorts, Charact #) ->  MSAlgebra over S;
sel Charact c2 ->  ManySortedFunction of ( the Sorts of c2 #) * the Arity of S, the Sorts of c2 * the ResultSort of S;
end;

definition
let S be 1-sorted ;
let A be many-sorted over S;
attrA is non-empty  means :Def3: :: MSUALG_1:def 3
 the Sorts of A is V5();
end;

:: deftheorem Def3 defines non-empty MSUALG_1:def_3_:_
 for S being 1-sorted
for A being many-sorted over S holds
( A is non-empty iff the Sorts of A is V5() );

registration
let S be non empty ManySortedSign ;
cluster strict non-empty for MSAlgebra over S;
existence
 ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty )
proofend;
end;

registration
let S be 1-sorted ;
cluster strict non-empty for many-sorted over S;
existence
 ex b1 being many-sorted over S st
( b1 is strict & b1 is non-empty )
proofend;
end;

registration
let S be 1-sorted ;
let A be non-empty many-sorted over S;
cluster the Sorts of A -> V5() ;
coherence
 the Sorts of A is non-empty by Def3;
end;

registration
let S be non empty ManySortedSign ;
let A be non-empty MSAlgebra over S;
cluster  ->  non empty for Element of rng the Sorts of A;
coherence
 for b1 being Component of the Sorts of A holds not b1 is empty
proofend;
cluster  ->  non empty for Element of rng ( the Sorts of A #);
coherence
 for b1 being Component of ( the Sorts of A #) holds not b1 is empty
proofend;
end;

definition
let S be non empty non void 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;
coherence
 (( the Sorts of A #) * the Arity of S) . o is Component of ( the Sorts of A #)
proofend;
correctness
;
func Result (o,A) ->  Component of the Sorts of A equals :: MSUALG_1:def 5
( the Sorts of A * the ResultSort of S) . o;
coherence
 ( the Sorts of A * the ResultSort of S) . o is Component of the Sorts of A
proofend;
correctness
;
end;

:: deftheorem  defines Args MSUALG_1:def_4_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds Args (o,A) = (( the Sorts of A #) * the Arity of S) . o;

:: deftheorem  defines Result MSUALG_1:def_5_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds Result (o,A) = ( the Sorts of A * the ResultSort of S) . o;

definition
let S be non empty non void 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;
coherence
 the Charact of A . o is Function of (Args (o,A)),(Result (o,A)) by PBOOLE:def_15;
end;

:: deftheorem  defines Den MSUALG_1:def_6_:_
 for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being MSAlgebra over S holds Den (o,A) = the Charact of A . o;

theorem :: MSUALG_1:1
for S being non empty non void ManySortedSign
for o being OperSymbol of S
for A being non-empty MSAlgebra over S holds not Den (o,A) is empty ;

begin

Lm1:  for D being non empty set
for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D
proofend;

theorem Th2: :: MSUALG_1:2
for C being set
for A, B being non empty set
for F being PartFunc of C,A
for G being Function of A,B holds G * F is Function of (dom F),B
proofend;

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

theorem Th4: :: MSUALG_1:4
for A being Universal_Algebra holds not signature A is empty
proofend;

begin

definition
let IT be ManySortedSign ;
attrIT is segmental  means :Def7: :: MSUALG_1:def 7
 ex n being Nat st the carrier' of IT = Seg n;
end;

:: deftheorem Def7 defines segmental MSUALG_1:def_7_:_
 for IT being ManySortedSign holds
( IT is segmental iff ex n being Nat st the carrier' of IT = Seg n );

theorem Th5: :: MSUALG_1:5
for S being non empty ManySortedSign st S is trivial holds
for A being MSAlgebra over S
for c1, c2 being Component of the Sorts of A holds c1 = c2
proofend;

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 & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )
proofend;

registration
cluster non void 1 -element strict segmental for ManySortedSign ;
existence
 ex b1 being ManySortedSign st
( b1 is segmental & not b1 is void & b1 is strict & b1 is 1 -element )
proofend;
end;

definition
let A be Universal_Algebra;
func MSSign A ->  trivial non void strict segmental ManySortedSign  means :Def8: :: 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 );
correctness
existence
ex b1 being trivial non void strict segmental ManySortedSign st
( the carrier of b1 = {0} & the carrier' of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 );
uniqueness
for b1, b2 being trivial non void strict segmental ManySortedSign st the carrier of b1 = {0} & the carrier' of b1 = dom (signature A) & the Arity of b1 = (*--> 0) * (signature A) & the ResultSort of b1 = (dom (signature A)) --> 0 & the carrier of b2 = {0} & the carrier' of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 holds
b1 = b2;
proofend;
end;

:: deftheorem Def8 defines MSSign MSUALG_1:def_8_:_
 for A being Universal_Algebra
for b2 being trivial non void strict segmental ManySortedSign holds
( b2 = MSSign A iff ( the carrier of b2 = {0} & the carrier' of b2 = dom (signature A) & the Arity of b2 = (*--> 0) * (signature A) & the ResultSort of b2 = (dom (signature A)) --> 0 ) );

registration
let A be Universal_Algebra;
cluster MSSign A ->  trivial non void 1 -element strict segmental ;
coherence
 MSSign A is 1 -element
proofend;
end;

definition
let A be Universal_Algebra;
func MSSorts A ->  V5() ManySortedSet of the carrier of (MSSign A) equals :: MSUALG_1:def 9
0 .--> the carrier of A;
coherence
 0 .--> the carrier of A is V5() ManySortedSet of the carrier of (MSSign A)
proofend;
correctness
;
end;

:: deftheorem  defines MSSorts MSUALG_1:def_9_:_
 for A being Universal_Algebra holds MSSorts A = 0 .--> the carrier of A;

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;
coherence
 the charact of A is ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A)
proofend;
correctness
;
end;

:: deftheorem  defines MSCharact MSUALG_1:def_10_:_
 for A being Universal_Algebra holds MSCharact A = the charact of A;

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

:: deftheorem  defines MSAlg MSUALG_1:def_11_:_
 for A being Universal_Algebra holds MSAlg A = MSAlgebra(# (MSSorts A),(MSCharact A) #);

registration
let A be Universal_Algebra;
cluster MSAlg A ->  strict non-empty ;
coherence
 MSAlg A is non-empty
proofend;
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: :: MSUALG_1:def 12
it is Component of the Sorts of A;
existence
 ex b1 being set st b1 is Component of the Sorts of A
proofend;
uniqueness
 for b1, b2 being set st b1 is Component of the Sorts of A & b2 is Component of the Sorts of A holds
b1 = b2 by Th5;
end;

:: deftheorem Def12 defines the_sort_of MSUALG_1:def_12_:_
 for MS being 1 -element ManySortedSign
for A being MSAlgebra over MS
for b3 being set holds
( b3 = the_sort_of A iff b3 is Component of the Sorts of A );

registration
let MS be 1 -element ManySortedSign ;
let A be non-empty MSAlgebra over MS;
cluster the_sort_of A ->  non empty ;
coherence
 not the_sort_of A is empty
proofend;
end;

theorem Th6: :: MSUALG_1:6
for MS being non void 1 -element segmental ManySortedSign
for i being OperSymbol of MS
for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)
proofend;

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

theorem Th8: :: MSUALG_1:8
for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))
proofend;

definition
let MS be non void 1 -element segmental 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;
coherence
 the Charact of A is PFuncFinSequence of (the_sort_of A) by Th8;
end;

:: deftheorem  defines the_charact_of MSUALG_1:def_13_:_
 for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds the_charact_of A = the Charact of A;

definition
let MS be non void 1 -element segmental ManySortedSign ;
let A be non-empty MSAlgebra over MS;
func 1-Alg A ->  strict Universal_Algebra equals :: MSUALG_1:def 14
 UAStr(# (the_sort_of A),(the_charact_of A) #);
coherence
 UAStr(# (the_sort_of A),(the_charact_of A) #) is strict Universal_Algebra
proofend;
correctness
;
end;

:: deftheorem  defines 1-Alg MSUALG_1:def_14_:_
 for MS being non void 1 -element segmental ManySortedSign
for A being non-empty MSAlgebra over MS holds 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #);

theorem :: MSUALG_1:9
for A being strict Universal_Algebra holds A = 1-Alg (MSAlg A)
proofend;

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