FREEALG: Free Universal Algebra Construction

:: Free Universal Algebra Construction
:: by Beata Perkowska
::
:: Received October 20, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users

begin

definition

let IT be set ;
attr IT is disjoint_with_NAT means :Def1: :: FREEALG:def 1
IT misses NAT ;

end;

:: deftheorem Def1 defines disjoint_with_NAT FREEALG:def 1 :

registration

cluster non empty disjoint_with_NAT set ;
existence

proof end;

end;

Lm1: ( not 0 in rng <*1*> & 0 in rng <*0*> )

proof end;

notation

let IT be Relation;
antonym with_zero IT for non-empty ;
synonym without_zero IT for non-empty ;

end;

definition

let IT be Relation;
redefine attr IT is non-empty means :Def2: :: FREEALG:def 2
not 0 in rng IT;
compatibility by RELAT_1:def 9;

end;

:: deftheorem Def2 defines with_zero FREEALG:def 2 :

registration

cluster non empty Relation-like with_zero NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of NAT ;
existence

proof end;

cluster non empty Relation-like without_zero NAT -defined NAT -valued Function-like V31() FinSequence-like FinSubsequence-like FinSequence of NAT ;
existence

proof end;

end;

begin

definition

let U1 be Universal_Algebra;
let n be Element of NAT ;
assume A1: n in dom the charact of U1 ;
canceled;
func oper (n,U1) -> operation of U1 equals :Def4: :: FREEALG:def 4
the charact of U1 . n;
coherence by A1, FUNCT_1:def 5;

end;

:: deftheorem FREEALG:def 3 :

:: deftheorem Def4 defines oper FREEALG:def 4 :

definition

let U0 be Universal_Algebra;
mode GeneratorSet of U0 -> Subset of U0 means :: FREEALG:def 5
for A being Subset of U0 st A is opers_closed & it c= A holds
A = the carrier of U0;
existence

proof end;

end;

:: deftheorem defines GeneratorSet FREEALG:def 5 :

Lm2: for A being Universal_Algebra
for B being Subset of A st B is opers_closed holds
Constants A c= B

proof end;

Lm3: for A being Universal_Algebra
for B being Subset of A st ( B <> {} or Constants A <> {} ) holds
( B is GeneratorSet of A iff the carrier of (GenUnivAlg B) = the carrier of A )

proof end;

definition

let U0 be Universal_Algebra;
let IT be GeneratorSet of U0;
attr IT is free means :Def6: :: FREEALG:def 6
for U1 being Universal_Algebra st U0,U1 are_similar holds
for f being Function of IT, the carrier of U1 ex h being Function of U0,U1 st
( h is_homomorphism U0,U1 & h | IT = f );

end;

:: deftheorem Def6 defines free FREEALG:def 6 :

definition

let IT be Universal_Algebra;
attr IT is free means :Def7: :: FREEALG:def 7
ex G being GeneratorSet of IT st G is free ;

end;

:: deftheorem Def7 defines free FREEALG:def 7 :

registration

cluster non empty strict V106() quasi_total non-empty free UAStr ;
existence

proof end;

end;

registration

let U0 be free Universal_Algebra;
cluster free GeneratorSet of U0;
existence by Def7;

end;

theorem :: FREEALG:1

for U0 being strict Universal_Algebra
for A being Subset of U0 st ( Constants U0 <> {} or A <> {} ) holds
( A is GeneratorSet of U0 iff GenUnivAlg A = U0 )

proof end;

begin

definition

let f be non empty FinSequence of NAT ;
let X be set ;
func REL (f,X) -> Relation of ((dom f) \/ X),(((dom f) \/ X) *) means :Def8: :: FREEALG:def 8
for a being Element of (dom f) \/ X
for b being Element of ((dom f) \/ X) * holds
( [a,b] in it iff ( a in dom f & f . a = len b ) );
existence

proof end;

proof end;

end;

:: deftheorem Def8 defines REL FREEALG:def 8 :

definition

let f be non empty FinSequence of NAT ;
let X be set ;
func DTConUA (f,X) -> strict DTConstrStr equals :: FREEALG:def 9
DTConstrStr(# ((dom f) \/ X),(REL (f,X)) #);
correctness ;

end;

:: deftheorem defines DTConUA FREEALG:def 9 :

registration

let f be non empty FinSequence of NAT ;
let X be set ;
cluster DTConUA (f,X) -> non empty strict ;
coherence ;

end;

theorem Th2: :: FREEALG:2

for f being non empty FinSequence of NAT
for X being set holds
( Terminals (DTConUA (f,X)) c= X & NonTerminals (DTConUA (f,X)) = dom f )

proof end;

theorem Th3: :: FREEALG:3

for f being non empty FinSequence of NAT
for X being disjoint_with_NAT set holds Terminals (DTConUA (f,X)) = X

proof end;

registration

let f be non empty FinSequence of NAT ;
let X be set ;
cluster DTConUA (f,X) -> strict with_nonterminals ;
coherence

proof end;

end;

registration

let f be non empty with_zero FinSequence of NAT ;
let X be set ;
cluster DTConUA (f,X) -> strict with_nonterminals with_useful_nonterminals ;
coherence

proof end;

end;

registration

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
cluster DTConUA (f,D) -> strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence

proof end;

end;

definition

let f be non empty FinSequence of NAT ;
let X be set ;
let n be Nat;
assume A1: n in dom f ;
func Sym (n,f,X) -> Symbol of (DTConUA (f,X)) equals :Def10: :: FREEALG:def 10
n;
coherence by A1, XBOOLE_0:def 3;

end;

:: deftheorem Def10 defines Sym FREEALG:def 10 :

begin

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
let n be Nat;
assume A1: n in dom f ;
func FreeOpNSG (n,f,D) -> non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def11: :: FREEALG:def 11
( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds
it . p = (Sym (n,f,D)) -tree p ) );
existence

proof end;

proof end;

end;

:: deftheorem Def11 defines FreeOpNSG FREEALG:def 11 :

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
func FreeOpSeqNSG (f,D) -> PFuncFinSequence of (TS (DTConUA (f,D))) means :Def12: :: FREEALG:def 12
( len it = len f & ( for n being Element of NAT st n in dom it holds
it . n = FreeOpNSG (n,f,D) ) );
existence

proof end;

proof end;

end;

:: deftheorem Def12 defines FreeOpSeqNSG FREEALG:def 12 :

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
func FreeUnivAlgNSG (f,D) -> strict Universal_Algebra equals :: FREEALG:def 13
UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqNSG (f,D)) #);
coherence

proof end;

end;

:: deftheorem defines FreeUnivAlgNSG FREEALG:def 13 :

theorem Th4: :: FREEALG:4

for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds signature (FreeUnivAlgNSG (f,D)) = f

proof end;

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
func FreeGenSetNSG (f,D) -> Subset of (FreeUnivAlgNSG (f,D)) equals :: FREEALG:def 14
{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;
coherence

proof end;

end;

:: deftheorem defines FreeGenSetNSG FREEALG:def 14 :

theorem Th5: :: FREEALG:5

for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds not FreeGenSetNSG (f,D) is empty

proof end;

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
:: original: FreeGenSetNSG
redefine func FreeGenSetNSG (f,D) -> GeneratorSet of FreeUnivAlgNSG (f,D);
coherence

proof end;

end;

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
let C be non empty set ;
let s be Symbol of (DTConUA (f,D));
let F be Function of (FreeGenSetNSG (f,D)),C;
assume A1: s in Terminals (DTConUA (f,D)) ;
func pi (F,s) -> Element of C equals :Def15: :: FREEALG:def 15
F . (root-tree s);
coherence

proof end;

end;

:: deftheorem Def15 defines pi FREEALG:def 15 :

definition

let f be non empty FinSequence of NAT ;
let D be set ;
let s be Symbol of (DTConUA (f,D));
given p being FinSequence such that A1: s ==> p ;
func @ s -> Element of NAT equals :Def16: :: FREEALG:def 16
s;
coherence

proof end;

end;

:: deftheorem Def16 defines @ FREEALG:def 16 :

theorem Th6: :: FREEALG:6

for f being non empty FinSequence of NAT
for D being non empty disjoint_with_NAT set holds FreeGenSetNSG (f,D) is free

proof end;

registration

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
cluster FreeUnivAlgNSG (f,D) -> strict free ;
coherence

proof end;

end;

definition

let f be non empty FinSequence of NAT ;
let D be non empty disjoint_with_NAT set ;
:: original: FreeGenSetNSG
redefine func FreeGenSetNSG (f,D) -> free GeneratorSet of FreeUnivAlgNSG (f,D);
coherence by Th6;

end;

begin

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
let n be Nat;
assume A1: n in dom f ;
func FreeOpZAO (n,f,D) -> non empty homogeneous quasi_total PartFunc of ((TS (DTConUA (f,D))) *),(TS (DTConUA (f,D))) means :Def17: :: FREEALG:def 17
( dom it = (f /. n) -tuples_on (TS (DTConUA (f,D))) & ( for p being FinSequence of TS (DTConUA (f,D)) st p in dom it holds
it . p = (Sym (n,f,D)) -tree p ) );
existence

proof end;

proof end;

end;

:: deftheorem Def17 defines FreeOpZAO FREEALG:def 17 :

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
func FreeOpSeqZAO (f,D) -> PFuncFinSequence of (TS (DTConUA (f,D))) means :Def18: :: FREEALG:def 18
( len it = len f & ( for n being Element of NAT st n in dom it holds
it . n = FreeOpZAO (n,f,D) ) );
existence

proof end;

proof end;

end;

:: deftheorem Def18 defines FreeOpSeqZAO FREEALG:def 18 :

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
func FreeUnivAlgZAO (f,D) -> strict Universal_Algebra equals :: FREEALG:def 19
UAStr(# (TS (DTConUA (f,D))),(FreeOpSeqZAO (f,D)) #);
coherence

proof end;

end;

:: deftheorem defines FreeUnivAlgZAO FREEALG:def 19 :

theorem Th7: :: FREEALG:7

for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds signature (FreeUnivAlgZAO (f,D)) = f

proof end;

theorem Th8: :: FREEALG:8

for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeUnivAlgZAO (f,D) is with_const_op

proof end;

theorem Th9: :: FREEALG:9

for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds Constants (FreeUnivAlgZAO (f,D)) <> {}

proof end;

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
func FreeGenSetZAO (f,D) -> Subset of (FreeUnivAlgZAO (f,D)) equals :: FREEALG:def 20
{ (root-tree s) where s is Symbol of (DTConUA (f,D)) : s in Terminals (DTConUA (f,D)) } ;
coherence

proof end;

end;

:: deftheorem defines FreeGenSetZAO FREEALG:def 20 :

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
:: original: FreeGenSetZAO
redefine func FreeGenSetZAO (f,D) -> GeneratorSet of FreeUnivAlgZAO (f,D);
coherence

proof end;

end;

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
let C be non empty set ;
let s be Symbol of (DTConUA (f,D));
let F be Function of (FreeGenSetZAO (f,D)),C;
assume A1: s in Terminals (DTConUA (f,D)) ;
func pi (F,s) -> Element of C equals :Def21: :: FREEALG:def 21
F . (root-tree s);
coherence

proof end;

end;

:: deftheorem Def21 defines pi FREEALG:def 21 :

theorem Th10: :: FREEALG:10

for f being non empty with_zero FinSequence of NAT
for D being disjoint_with_NAT set holds FreeGenSetZAO (f,D) is free

proof end;

registration

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
cluster FreeUnivAlgZAO (f,D) -> strict free ;
coherence

proof end;

end;

definition

let f be non empty with_zero FinSequence of NAT ;
let D be disjoint_with_NAT set ;
:: original: FreeGenSetZAO
redefine func FreeGenSetZAO (f,D) -> free GeneratorSet of FreeUnivAlgZAO (f,D);
coherence by Th10;

end;

registration

cluster non empty strict V106() quasi_total non-empty with_const_op free UAStr ;
existence

proof end;

end;