MSAFREE: Free Many Sorted Universal Algebra

:: Free Many Sorted Universal Algebra
:: by Beata Perkowska
::
:: Received April 27, 1994
:: Copyright (c) 1994-2012 Association of Mizar Users

begin

::
:: Preliminaries
::

theorem Th1: :: MSAFREE:1

for I being set
for J being non empty set
for f being Function of I,(J *)
for X being ManySortedSet of J
for p being Element of J *
for x being set st x in I & p = f . x holds
((X #) * f) . x = product (X * p)

proof end;

definition

let I be set ;
let A, B be ManySortedSet of I;
let C be ManySortedSubset of A;
let F be ManySortedFunction of A,B;

func F || C -> ManySortedFunction of C,B means :Def1: :: MSAFREE:def 1
for i being set st i in I holds
for f being Function of (A . i),(B . i) st f = F . i holds
it . i = f | (C . i);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines || MSAFREE:def 1 :

definition

let I be set ;
let X be ManySortedSet of I;
let i be set ;
assume A1: i in I ;

func coprod (i,X) -> set means :Def2: :: MSAFREE:def 2
for x being set holds
( x in it iff ex a being set st
( a in X . i & x = [a,i] ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines coprod MSAFREE:def 2 :

notation

let I be set ;
let X be ManySortedSet of I;
synonym coprod X for disjoin I;

end;

registration

let I be set ;
let X be ManySortedSet of I;

cluster coprod -> I -defined ;

coherence

proof end;

end;

registration

let I be set ;
let X be ManySortedSet of I;

cluster coprod -> total ;

coherence

proof end;

end;

definition

let I be set ;
let X be ManySortedSet of I;

:: original: coprod
redefine func coprod X -> set means :Def3: :: MSAFREE:def 3
( dom it = I & ( for i being set st i in I holds
it . i = coprod (i,X) ) );

compatibility

proof end;

end;

:: deftheorem Def3 defines coprod MSAFREE:def 3 :

registration

let I be non empty set ;
let X be V16() ManySortedSet of I;

cluster coprod -> V16() ;

coherence

proof end;

end;

registration

let I be non empty set ;
let X be V16() ManySortedSet of I;

cluster Union X -> non empty ;

coherence

proof end;

end;

theorem :: MSAFREE:2

for I being set
for X being ManySortedSet of I
for i being set st i in I holds
( X . i <> {} iff (coprod X) . i <> {} )

proof end;

begin

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;

mode GeneratorSet of U0 -> MSSubset of U0 means :Def4: :: MSAFREE:def 4
the Sorts of (GenMSAlg it) = the Sorts of U0;

existence

proof end;

end;

:: deftheorem Def4 defines GeneratorSet MSAFREE:def 4 :

theorem :: MSAFREE:3

for S being non empty non void ManySortedSign
for U0 being strict non-empty MSAlgebra over S
for A being MSSubset of U0 holds
( A is GeneratorSet of U0 iff GenMSAlg A = U0 )

proof end;

definition

let S be non empty non void ManySortedSign ;
let U0 be MSAlgebra over S;
let IT be GeneratorSet of U0;

attr IT is free means :Def5: :: MSAFREE:def 5
for U1 being non-empty MSAlgebra over S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h || IT = f );

end;

:: deftheorem Def5 defines free MSAFREE:def 5 :

definition

let S be non empty non void ManySortedSign ;
let IT be MSAlgebra over S;

attr IT is free means :Def6: :: MSAFREE:def 6
ex G being GeneratorSet of IT st G is free ;

end;

:: deftheorem Def6 defines free MSAFREE:def 6 :

theorem Th4: :: MSAFREE:4

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds Union (coprod X) misses [: the carrier' of S,{ the carrier of S}:]

proof end;

begin

::
:: Construction of Free Many Sorted Algebras for Given Signature
::

definition

let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;

func REL X -> Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) means :Def7: :: MSAFREE:def 7
for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines REL MSAFREE:def 7 :

theorem Th5: :: MSAFREE:5

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for o being OperSymbol of S
for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o, the carrier of S],b] in REL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds
the_result_sort_of o1 = (the_arity_of o) . x ) & ( b . x in Union (coprod X) implies b . x in coprod (((the_arity_of o) . x),X) ) ) ) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;

func DTConMSA X -> DTConstrStr equals :: MSAFREE:def 8
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(REL X) #);

correctness ;

end;

:: deftheorem defines DTConMSA MSAFREE:def 8 :

registration

let S be non empty non void ManySortedSign ;
let X be ManySortedSet of the carrier of S;

cluster DTConMSA X -> non empty strict ;

coherence ;

end;

theorem Th6: :: MSAFREE:6

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S holds
( NonTerminals (DTConMSA X) c= [: the carrier' of S,{ the carrier of S}:] & Union (coprod X) c= Terminals (DTConMSA X) & ( X is V16() implies ( NonTerminals (DTConMSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConMSA X) = Union (coprod X) ) ) )

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

cluster DTConMSA X -> with_terminals with_nonterminals with_useful_nonterminals ;

coherence

proof end;

end;

theorem Th7: :: MSAFREE:7

for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for t being set holds
( ( t in Terminals (DTConMSA X) & X is V16() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;

func Sym (o,X) -> Symbol of (DTConMSA X) equals :: MSAFREE:def 9
[o, the carrier of S];

coherence

proof end;

end;

:: deftheorem defines Sym MSAFREE:def 9 :

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;

func FreeSort (X,s) -> Subset of (TS (DTConMSA X)) equals :: MSAFREE:def 10
{ a where a is Element of TS (DTConMSA X) : ( ex x being set st
( x in X . s & a = root-tree [x,s] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} & the_result_sort_of o = s ) ) } ;

coherence

proof end;

end;

:: deftheorem defines FreeSort MSAFREE:def 10 :

registration

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;

cluster FreeSort (X,s) -> non empty ;

coherence

proof end;

end;

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

func FreeSort X -> ManySortedSet of the carrier of S means :Def11: :: MSAFREE:def 11
for s being SortSymbol of S holds it . s = FreeSort (X,s);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines FreeSort MSAFREE:def 11 :

registration

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

cluster FreeSort X -> V16() ;

coherence

proof end;

end;

theorem Th8: :: MSAFREE:8

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for x being set st x in (((FreeSort X) #) * the Arity of S) . o holds
x is FinSequence of TS (DTConMSA X)

proof end;

theorem Th9: :: MSAFREE:9

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( p in (((FreeSort X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in FreeSort (X,((the_arity_of o) /. n)) ) ) )

proof end;

theorem Th10: :: MSAFREE:10

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConMSA X) holds
( Sym (o,X) ==> roots p iff p in (((FreeSort X) #) * the Arity of S) . o )

proof end;

theorem Th11: :: MSAFREE:11

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeSort X)) = TS (DTConMSA X)

proof end;

theorem Th12: :: MSAFREE:12

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s1, s2 being SortSymbol of S st s1 <> s2 holds
(FreeSort X) . s1 misses (FreeSort X) . s2

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let o be OperSymbol of S;

func DenOp (o,X) -> Function of ((((FreeSort X) #) * the Arity of S) . o),(((FreeSort X) * the ResultSort of S) . o) means :Def12: :: MSAFREE:def 12
for p being FinSequence of TS (DTConMSA X) st Sym (o,X) ==> roots p holds
it . p = (Sym (o,X)) -tree p;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines DenOp MSAFREE:def 12 :

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

func FreeOper X -> ManySortedFunction of ((FreeSort X) #) * the Arity of S,(FreeSort X) * the ResultSort of S means :Def13: :: MSAFREE:def 13
for o being OperSymbol of S holds it . o = DenOp (o,X);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines FreeOper MSAFREE:def 13 :

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

func FreeMSA X -> MSAlgebra over S equals :: MSAFREE:def 14
MSAlgebra(# (FreeSort X),(FreeOper X) #);

coherence ;

end;

:: deftheorem defines FreeMSA MSAFREE:def 14 :

registration

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

cluster FreeMSA X -> strict non-empty ;

coherence by MSUALG_1:def 3;

end;

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;

func FreeGen (s,X) -> Subset of ((FreeSort X) . s) means :Def15: :: MSAFREE:def 15
for x being set holds
( x in it iff ex a being set st
( a in X . s & x = root-tree [a,s] ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines FreeGen MSAFREE:def 15 :

registration

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;

cluster FreeGen (s,X) -> non empty ;

coherence

proof end;

end;

theorem Th13: :: MSAFREE:13

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S
for s being SortSymbol of S holds FreeGen (s,X) = { (root-tree t) where t is Symbol of (DTConMSA X) : ( t in Terminals (DTConMSA X) & t `2 = s ) }

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

func FreeGen X -> GeneratorSet of FreeMSA X means :Def16: :: MSAFREE:def 16
for s being SortSymbol of S holds it . s = FreeGen (s,X);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines FreeGen MSAFREE:def 16 :

theorem :: MSAFREE:14

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeGen X is V16()

proof end;

theorem :: MSAFREE:15

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds union (rng (FreeGen X)) = { (root-tree t) where t is Symbol of (DTConMSA X) : t in Terminals (DTConMSA X) }

proof end;

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let s be SortSymbol of S;

func Reverse (s,X) -> Function of (FreeGen (s,X)),(X . s) means :Def17: :: MSAFREE:def 17
for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
it . (root-tree t) = t `1 ;

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines Reverse MSAFREE:def 17 :

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;

func Reverse X -> ManySortedFunction of FreeGen X,X means :Def18: :: MSAFREE:def 18
for s being SortSymbol of S holds it . s = Reverse (s,X);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def18 defines Reverse MSAFREE:def 18 :

definition

let S be non empty non void ManySortedSign ;
let X, A be V16() ManySortedSet of the carrier of S;
let F be ManySortedFunction of FreeGen X,A;
let t be Symbol of (DTConMSA X);
assume A1: t in Terminals (DTConMSA X) ;

func pi (F,A,t) -> Element of Union A means :Def19: :: MSAFREE:def 19
for f being Function st f = F . (t `2) holds
it = f . (root-tree t);

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def19 defines pi MSAFREE:def 19 :

definition

let S be non empty non void ManySortedSign ;
let X be V16() ManySortedSet of the carrier of S;
let t be Symbol of (DTConMSA X);
assume A1: ex p being FinSequence st t ==> p ;

func @ (X,t) -> OperSymbol of S means :Def20: :: MSAFREE:def 20
[it, the carrier of S] = t;

existence

proof end;

uniqueness by XTUPLE_0:1;

end;

:: deftheorem Def20 defines @ MSAFREE:def 20 :

definition

let S be non empty non void ManySortedSign ;
let U0 be non-empty MSAlgebra over S;
let o be OperSymbol of S;
let p be FinSequence;
assume A1: p in Args (o,U0) ;

func pi (o,U0,p) -> Element of Union the Sorts of U0 equals :Def21: :: MSAFREE:def 21
(Den (o,U0)) . p;

coherence

proof end;

end;

:: deftheorem Def21 defines pi MSAFREE:def 21 :

theorem Th16: :: MSAFREE:16

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeGen X is free

proof end;

theorem Th17: :: MSAFREE:17

for S being non empty non void ManySortedSign
for X being V16() ManySortedSet of the carrier of S holds FreeMSA X is free

proof end;

registration

let S be non empty non void ManySortedSign ;

cluster strict non-empty free for MSAlgebra over S;

existence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let U0 be free MSAlgebra over S;

cluster non empty Relation-like the carrier of S -defined Function-like total free for GeneratorSet of U0;

existence by Def6;

end;

theorem Th18: :: MSAFREE:18

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1

proof end;

theorem :: MSAFREE:19

for S being non empty non void ManySortedSign
for U1 being strict non-empty MSAlgebra over S ex U0 being strict non-empty free MSAlgebra over S ex F being ManySortedFunction of U0,U1 st
( F is_epimorphism U0,U1 & Image F = U1 )

proof end;