:: On Defining Functions on Binary Trees
:: by Grzegorz Bancerek and Piotr Rudnicki
::
:: Received December 30, 1993
:: Copyright (c) 1993-2011 Association of Mizar Users


begin

definition
let D be non empty set ;
let t be DecoratedTree of D;
func root-label t -> Element of D equals :: BINTREE1:def 1
t . {};
coherence
t . {} is Element of D
proof end;
end;

:: deftheorem defines root-label BINTREE1:def 1 :
for D being non empty set
for t being DecoratedTree of D holds root-label t = t . {};

theorem :: BINTREE1:1
for D being non empty set
for t being DecoratedTree of D holds roots <*t*> = <*(root-label t)*> by DTCONSTR:4;

theorem :: BINTREE1:2
for D being non empty set
for t1, t2 being DecoratedTree of D holds roots <*t1,t2*> = <*(root-label t1),(root-label t2)*> by DTCONSTR:6;

definition
let IT be Tree;
attr IT is binary means :Def2: :: BINTREE1:def 2
 for t being Element of IT st not t in Leaves IT holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)};
end;

:: deftheorem Def2 defines binary BINTREE1:def 2 :
for IT being Tree holds
( IT is binary iff for t being Element of IT st not t in Leaves IT holds
succ t = {(t ^ <*0*>),(t ^ <*1*>)} );

theorem :: BINTREE1:3
canceled;

theorem :: BINTREE1:4
canceled;

theorem :: BINTREE1:5
for T being Tree
for t being Element of T holds
( succ t = {} iff t in Leaves T )
proof end;

registration
cluster elementary_tree 0 -> binary ;
coherence
elementary_tree 0 is binary
proof end;
cluster elementary_tree 2 -> binary ;
coherence
elementary_tree 2 is binary
proof end;
end;

theorem :: BINTREE1:6
elementary_tree 0 is binary ;

theorem :: BINTREE1:7
elementary_tree 2 is binary ;

registration
cluster non empty finite Tree-like binary set ;
existence
ex b1 being Tree st
( b1 is binary & b1 is finite )
proof end;
end;

definition
let IT be DecoratedTree;
attr IT is binary means :Def3: :: BINTREE1:def 3
 dom IT is binary ;
end;

:: deftheorem Def3 defines binary BINTREE1:def 3 :
for IT being DecoratedTree holds
( IT is binary iff dom IT is binary );

registration
let D be non empty set ;
cluster Relation-like D -valued Function-like finite DecoratedTree-like binary set ;
existence
ex b1 being DecoratedTree of D st
( b1 is binary & b1 is finite )
proof end;
end;

registration
cluster Relation-like Function-like finite DecoratedTree-like binary set ;
existence
ex b1 being DecoratedTree st
( b1 is binary & b1 is finite )
proof end;
end;

registration
cluster non empty Tree-like binary -> finite-order set ;
coherence
for b1 being Tree st b1 is binary holds
b1 is finite-order
proof end;
end;

theorem Th8: :: BINTREE1:8
for T0, T1 being Tree
for t being Element of tree (T0,T1) holds
( ( for p being Element of T0 st t = <*0*> ^ p holds
( t in Leaves (tree (T0,T1)) iff p in Leaves T0 ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
( t in Leaves (tree (T0,T1)) iff p in Leaves T1 ) ) )
proof end;

theorem Th9: :: BINTREE1:9
for T0, T1 being Tree
for t being Element of tree (T0,T1) holds
( ( t = {} implies succ t = {(t ^ <*0*>),(t ^ <*1*>)} ) & ( for p being Element of T0 st t = <*0*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*0*> ^ sp in succ t ) ) & ( for p being Element of T1 st t = <*1*> ^ p holds
for sp being FinSequence holds
( sp in succ p iff <*1*> ^ sp in succ t ) ) )
proof end;

theorem Th10: :: BINTREE1:10
for T1, T2 being Tree holds
( ( T1 is binary & T2 is binary ) iff tree (T1,T2) is binary )
proof end;

theorem Th11: :: BINTREE1:11
for T1, T2 being DecoratedTree
for x being set holds
( ( T1 is binary & T2 is binary ) iff x -tree (T1,T2) is binary )
proof end;

registration
let D be non empty set ;
let x be Element of D;
let T1, T2 be finite binary DecoratedTree of D;
cluster x -tree (T1,T2) -> D -valued finite binary ;
coherence
( x -tree (T1,T2) is binary & x -tree (T1,T2) is finite & x -tree (T1,T2) is D -valued )
proof end;
end;

definition
let IT be non empty DTConstrStr ;
attr IT is binary means :Def4: :: BINTREE1:def 4
 for s being Symbol of IT
for p being FinSequence st s ==> p holds
ex x1, x2 being Symbol of IT st p = <*x1,x2*>;
end;

:: deftheorem Def4 defines binary BINTREE1:def 4 :
for IT being non empty DTConstrStr holds
( IT is binary iff for s being Symbol of IT
for p being FinSequence st s ==> p holds
ex x1, x2 being Symbol of IT st p = <*x1,x2*> );

registration
cluster non empty strict with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr ;
existence
ex b1 being non empty DTConstrStr st
( b1 is binary & b1 is with_terminals & b1 is with_nonterminals & b1 is with_useful_nonterminals & b1 is strict )
proof end;
end;

scheme :: BINTREE1:sch 1
BinDTConstrStrEx{ F1() -> non empty set , P1[ set , set , set ] } :
ex G being non empty strict binary DTConstrStr st
( the carrier of G = F1() & ( for x, y, z being Symbol of G holds
( x ==> <*y,z*> iff P1[x,y,z] ) ) )
proof end;

theorem Th12: :: BINTREE1:12
for G being non empty with_terminals with_nonterminals binary DTConstrStr
for ts being FinSequence of TS G
for nt being Symbol of G st nt ==> roots ts holds
( nt is NonTerminal of G & dom ts = {1,2} & 1 in dom ts & 2 in dom ts & ex tl, tr being Element of TS G st
( roots ts = <*(root-label tl),(root-label tr)*> & tl = ts . 1 & tr = ts . 2 & nt -tree ts = nt -tree (tl,tr) & tl in rng ts & tr in rng ts ) )
proof end;

scheme :: BINTREE1:sch 2
BinDTConstrInd{ F1() -> non empty with_terminals with_nonterminals binary DTConstrStr , P1[ set ] } :
for t being Element of TS F1() holds P1[t]
provided
A1: for s being Terminal of F1() holds P1[ root-tree s] and
A2: for nt being NonTerminal of F1()
for tl, tr being Element of TS F1() st nt ==> <*(root-label tl),(root-label tr)*> & P1[tl] & P1[tr] holds
P1[nt -tree (tl,tr)]
proof end;

scheme :: BINTREE1:sch 3
BinDTConstrIndDef{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3( set ) -> Element of F2(), F4( set , set , set , set , set ) -> Element of F2() } :
ex f being Function of (TS F1()),F2() st
( ( for t being Terminal of F1() holds f . (root-tree t) = F3(t) ) & ( for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = F4(nt,rtl,rtr,xl,xr) ) )
proof end;

scheme :: BINTREE1:sch 4
BinDTConstrUniqDef{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3() -> Function of (TS F1()),F2(), F4() -> Function of (TS F1()),F2(), F5( set ) -> Element of F2(), F6( set , set , set , set , set ) -> Element of F2() } :
F3() = F4()
provided
A1: ( ( for t being Terminal of F1() holds F3() . (root-tree t) = F5(t) ) & ( for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = F3() . tl & xr = F3() . tr holds
F3() . (nt -tree (tl,tr)) = F6(nt,rtl,rtr,xl,xr) ) ) and
A2: ( ( for t being Terminal of F1() holds F4() . (root-tree t) = F5(t) ) & ( for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of F2() st xl = F4() . tl & xr = F4() . tr holds
F4() . (nt -tree (tl,tr)) = F6(nt,rtl,rtr,xl,xr) ) )
proof end;

definition
let A, B, C be non empty set ;
let a be Element of A;
let b be Element of B;
let c be Element of C;
:: original: [
redefine func [a,b,c] -> Element of [:A,B,C:];
coherence
[a,b,c] is Element of [:A,B,C:] by MCART_1:73;
end;

scheme :: BINTREE1:sch 5
BinDTCDefLambda{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F3(), F5( set , set , set , set ) -> Element of F3() } :
ex f being Function of (TS F1()),(Funcs (F2(),F3())) st
( ( for t being Terminal of F1() ex g being Function of F2(),F3() st
( g = f . (root-tree t) & ( for a being Element of F2() holds g . a = F4(t,a) ) ) ) & ( for nt being NonTerminal of F1()
for t1, t2 being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for a being Element of F2() holds g . a = F5(nt,f1,f2,a) ) ) ) )
proof end;

scheme :: BINTREE1:sch 6
BinDTCDefLambdaUniq{ F1() -> non empty with_terminals with_nonterminals with_useful_nonterminals binary DTConstrStr , F2() -> non empty set , F3() -> non empty set , F4() -> Function of (TS F1()),(Funcs (F2(),F3())), F5() -> Function of (TS F1()),(Funcs (F2(),F3())), F6( set , set ) -> Element of F3(), F7( set , set , set , set ) -> Element of F3() } :
F4() = F5()
provided
A1: ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st
( g = F4() . (root-tree t) & ( for a being Element of F2() holds g . a = F6(t,a) ) ) ) & ( for nt being NonTerminal of F1()
for t1, t2 being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = F4() . (nt -tree (t1,t2)) & f1 = F4() . t1 & f2 = F4() . t2 & ( for a being Element of F2() holds g . a = F7(nt,f1,f2,a) ) ) ) ) and
A2: ( ( for t being Terminal of F1() ex g being Function of F2(),F3() st
( g = F5() . (root-tree t) & ( for a being Element of F2() holds g . a = F6(t,a) ) ) ) & ( for nt being NonTerminal of F1()
for t1, t2 being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of F2(),F3() st
( g = F5() . (nt -tree (t1,t2)) & f1 = F5() . t1 & f2 = F5() . t2 & ( for a being Element of F2() holds g . a = F7(nt,f1,f2,a) ) ) ) )
proof end;

registration
let G be non empty with_terminals with_nonterminals binary DTConstrStr ;
cluster -> binary Element of TS G;
coherence
for b1 being Element of TS G holds b1 is binary
proof end;
end;