:: Introduction to Trees
:: by Grzegorz Bancerek
::
:: Received October 25, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

notation
let p, q be FinSequence;
synonym p is_a_prefix_of q for p c= q;
end;

definition
let p, q be FinSequence;
redefine pred p c= q means :Def1: :: TREES_1:def 1
 ex n being Element of NAT st p = q | (Seg n);
compatibility
 ( p is_a_prefix_of q iff ex n being Element of NAT st p = q | (Seg n) )
proofend;
end;

:: deftheorem Def1 defines is_a_prefix_of TREES_1:def_1_:_
 for p, q being FinSequence holds
( p is_a_prefix_of q iff ex n being Element of NAT st p = q | (Seg n) );

theorem Th1: :: TREES_1:1
for p, q being FinSequence holds
( p is_a_prefix_of q iff ex r being FinSequence st q = p ^ r )
proofend;

theorem Th2: :: TREES_1:2
for p, q being FinSequence st p is_a_prefix_of q & len p = len q holds
p = q
proofend;

theorem Th3: :: TREES_1:3
for x, y being set holds
( <*x*> is_a_prefix_of <*y*> iff x = y )
proofend;

notation
let p, q be FinSequence;
synonym p is_a_proper_prefix_of q for p c< q;
end;

Lm1:  for A, B being finite set st A c= B &amp; card A = card B holds
A = B
proofend;

theorem Th4: :: TREES_1:4
for p, q being finite set st p,q are_c=-comparable &amp; card p = card q holds
p = q
proofend;

theorem Th5: :: TREES_1:5
for x, y being set st <*x*>,<*y*> are_c=-comparable holds
x = y
proofend;

theorem Th6: :: TREES_1:6
for p, q being finite set st p c< q holds
card p < card q
proofend;

theorem Th7: :: TREES_1:7
for x being set
for p1, p2 being FinSequence st p1 ^ <*x*> is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2
proofend;

theorem Th8: :: TREES_1:8
for x being set
for p1, p2 being FinSequence st p1 is_a_prefix_of p2 holds
p1 is_a_proper_prefix_of p2 ^ <*x*>
proofend;

theorem Th9: :: TREES_1:9
for x being set
for p1, p2 being FinSequence st p1 is_a_proper_prefix_of p2 ^ <*x*> holds
p1 is_a_prefix_of p2
proofend;

theorem :: TREES_1:10
for p2, p1 being FinSequence st ( {} is_a_proper_prefix_of p2 or {} <> p2 ) holds
p1 is_a_proper_prefix_of p1 ^ p2
proofend;

::
:: The set of proper prefixes of a finite sequence
::
definition
let p be FinSequence;
func ProperPrefixes p ->  set  means :Def2: :: TREES_1:def 2
 for x being set holds
( x in it iff ex q being FinSequence st
( x = q &amp; q is_a_proper_prefix_of p ) );
existence
 ex b1 being set st
for x being set holds
( x in b1 iff ex q being FinSequence st
( x = q &amp; q is_a_proper_prefix_of p ) )
proofend;
uniqueness
 for b1, b2 being set st ( for x being set holds
( x in b1 iff ex q being FinSequence st
( x = q &amp; q is_a_proper_prefix_of p ) ) ) &amp; ( for x being set holds
( x in b2 iff ex q being FinSequence st
( x = q &amp; q is_a_proper_prefix_of p ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines ProperPrefixes TREES_1:def_2_:_
 for p being FinSequence
for b2 being set holds
( b2 = ProperPrefixes p iff for x being set holds
( x in b2 iff ex q being FinSequence st
( x = q &amp; q is_a_proper_prefix_of p ) ) );

theorem Th11: :: TREES_1:11
for x being set
for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence
proofend;

theorem Th12: :: TREES_1:12
for p, q being FinSequence holds
( p in ProperPrefixes q iff p is_a_proper_prefix_of q )
proofend;

theorem Th13: :: TREES_1:13
for p, q being FinSequence st p in ProperPrefixes q holds
len p < len q
proofend;

theorem :: TREES_1:14
for p, q, r being FinSequence st q ^ r in ProperPrefixes p holds
q in ProperPrefixes p
proofend;

theorem Th15: :: TREES_1:15
ProperPrefixes {} = {}
proofend;

set D = {{}};

theorem Th16: :: TREES_1:16
for x being set holds ProperPrefixes <*x*> = {{}}
proofend;

theorem :: TREES_1:17
for p, q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q
proofend;

theorem Th18: :: TREES_1:18
for p, q, r being FinSequence st q in ProperPrefixes p &amp; r in ProperPrefixes p holds
q,r are_c=-comparable
proofend;

::
:: Trees and their properties
::
definition
let X be set ;
attrX is Tree-like  means :Def3: :: TREES_1:def 3
( X c= NAT * &amp; ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) &amp; ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in X &amp; n <= k holds
p ^ <*n*> in X ) );
end;

:: deftheorem Def3 defines Tree-like TREES_1:def_3_:_
 for X being set holds
( X is Tree-like iff ( X c= NAT * &amp; ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) &amp; ( for p being FinSequence of NAT
for k, n being Element of NAT st p ^ <*k*> in X &amp; n <= k holds
p ^ <*n*> in X ) ) );

registration
cluster{{}} ->  Tree-like ;
coherence
 {{}} is Tree-like
proofend;
end;

registration
cluster non empty Tree-like for set ;
existence
 ex b1 being set st
( not b1 is empty &amp; b1 is Tree-like )
proofend;
end;

definition
mode Tree is non empty Tree-like set ;
end;

theorem Th19: :: TREES_1:19
for x being set
for T being Tree st x in T holds
x is FinSequence of NAT
proofend;

definition
let T be Tree;
:: original:Element
redefine mode Element of T ->  FinSequence of NAT ;
coherence
 for b1 being Element of T holds b1 is FinSequence of NAT by Th19;
end;

theorem Th20: :: TREES_1:20
for T being Tree
for p, q being FinSequence st p in T &amp; q is_a_prefix_of p holds
q in T
proofend;

theorem Th21: :: TREES_1:21
for q being FinSequence of NAT
for T being Tree
for r being FinSequence st q ^ r in T holds
q in T
proofend;

theorem Th22: :: TREES_1:22
for T being Tree holds
( {} in T &amp; <*> NAT in T )
proofend;

theorem :: TREES_1:23
{{}} is Tree ;

registration
let T, T1 be Tree;
clusterT \/ T1 ->  Tree-like ;
coherence
 T \/ T1 is Tree-like
proofend;
clusterT /\ T1 ->  non empty Tree-like ;
coherence
 ( T /\ T1 is Tree-like &amp; not T /\ T1 is empty )
proofend;
end;

theorem :: TREES_1:24
for T, T1 being Tree holds T \/ T1 is Tree ;

theorem :: TREES_1:25
for T, T1 being Tree holds T /\ T1 is Tree ;

::
:: Finite trees and their properties
::
registration
cluster non empty finite Tree-like for set ;
existence
 ex b1 being Tree st b1 is finite
proofend;
end;

theorem :: TREES_1:26
for fT, fT1 being finite Tree holds fT \/ fT1 is finite Tree ;

theorem :: TREES_1:27
for T being Tree
for fT being finite Tree holds fT /\ T is finite Tree ;

::
:: Elementary trees
::
definition
let n be Element of NAT ;
func elementary_tree n ->  Tree equals :: TREES_1:def 4
 {  <*k*> where k is Element of NAT : k < n  }  \/ {{}};
correctness
coherence
{  <*k*> where k is Element of NAT : k < n  }  \/ {{}} is Tree;
proofend;
end;

:: deftheorem  defines elementary_tree TREES_1:def_4_:_
 for n being Element of NAT holds elementary_tree n =  {  <*k*> where k is Element of NAT : k < n  }  \/ {{}};

registration
let n be Element of NAT ;
cluster elementary_tree n ->  finite ;
coherence
 elementary_tree n is finite
proofend;
end;

theorem Th28: :: TREES_1:28
for k, n being Element of NAT st k < n holds
<*k*> in elementary_tree n
proofend;

theorem Th29: :: TREES_1:29
elementary_tree 0 = {{}}
proofend;

theorem :: TREES_1:30
for n being Element of NAT
for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Element of NAT st
( k < n &amp; p = <*k*> ) )
proofend;

::
:: Leaves and subtrees
::
definition
let T be Tree;
func Leaves T ->  Subset of T means :Def5: :: TREES_1:def 5
 for p being FinSequence of NAT holds
( p in it iff ( p in T &amp; ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) );
existence
 ex b1 being Subset of T st
for p being FinSequence of NAT holds
( p in b1 iff ( p in T &amp; ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) )
proofend;
uniqueness
 for b1, b2 being Subset of T st ( for p being FinSequence of NAT holds
( p in b1 iff ( p in T &amp; ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) &amp; ( for p being FinSequence of NAT holds
( p in b2 iff ( p in T &amp; ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) ) holds
b1 = b2
proofend;
let p be FinSequence of NAT ;
assume B11: p in T ;
funcT | p ->  Tree means :Def6: :: TREES_1:def 6
 for q being FinSequence of NAT holds
( q in it iff p ^ q in T );
existence
 ex b1 being Tree st
for q being FinSequence of NAT holds
( q in b1 iff p ^ q in T )
proofend;
uniqueness
 for b1, b2 being Tree st ( for q being FinSequence of NAT holds
( q in b1 iff p ^ q in T ) ) &amp; ( for q being FinSequence of NAT holds
( q in b2 iff p ^ q in T ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines Leaves TREES_1:def_5_:_
 for T being Tree
for b2 being Subset of T holds
( b2 = Leaves T iff for p being FinSequence of NAT holds
( p in b2 iff ( p in T &amp; ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) ) );

:: deftheorem Def6 defines | TREES_1:def_6_:_
 for T being Tree
for p being FinSequence of NAT st p in T holds
for b3 being Tree holds
( b3 = T | p iff for q being FinSequence of NAT holds
( q in b3 iff p ^ q in T ) );

theorem :: TREES_1:31
for T being Tree holds T | (<*> NAT) = T
proofend;

registration
let T be finite Tree;
let p be Element of T;
clusterT | p ->  finite ;
coherence
 T | p is finite
proofend;
end;

definition
let T be Tree;
assume A1: Leaves T <> {} ;
mode Leaf of T ->  Element of T means :: TREES_1:def 7
it in Leaves T;
existence
 ex b1 being Element of T st b1 in Leaves T
proofend;
end;

:: deftheorem  defines Leaf TREES_1:def_7_:_
 for T being Tree st Leaves T <> {} holds
for b2 being Element of T holds
( b2 is Leaf of T iff b2 in Leaves T );

definition
let T be Tree;
mode Subtree of T ->  Tree means :: TREES_1:def 8
 ex p being Element of T st it = T | p;
existence
 ex b1 being Tree ex p being Element of T st b1 = T | p
proofend;
end;

:: deftheorem  defines Subtree TREES_1:def_8_:_
 for T, b2 being Tree holds
( b2 is Subtree of T iff ex p being Element of T st b2 = T | p );

definition
let T be Tree;
let p be FinSequence of NAT ;
let T1 be Tree;
assume A1: p in T ;
funcT with-replacement (p,T1) ->  Tree means :Def9: :: TREES_1:def 9
 for q being FinSequence of NAT holds
( q in it iff ( ( q in T &amp; not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 &amp; q = p ^ r ) ) );
existence
 ex b1 being Tree st
for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T &amp; not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 &amp; q = p ^ r ) ) )
proofend;
uniqueness
 for b1, b2 being Tree st ( for q being FinSequence of NAT holds
( q in b1 iff ( ( q in T &amp; not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 &amp; q = p ^ r ) ) ) ) &amp; ( for q being FinSequence of NAT holds
( q in b2 iff ( ( q in T &amp; not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 &amp; q = p ^ r ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines with-replacement TREES_1:def_9_:_
 for T being Tree
for p being FinSequence of NAT
for T1 being Tree st p in T holds
for b4 being Tree holds
( b4 = T with-replacement (p,T1) iff for q being FinSequence of NAT holds
( q in b4 iff ( ( q in T &amp; not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 &amp; q = p ^ r ) ) ) );

theorem Th32: :: TREES_1:32
for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T with-replacement (p,T1) =  {  t1 where t1 is Element of T : not p is_a_proper_prefix_of t1  }  \/  {  (p ^ s) where s is Element of T1 : s = s  }
proofend;

theorem :: TREES_1:33
for p being FinSequence of NAT
for T, T1 being Tree st p in T holds
T1 = (T with-replacement (p,T1)) | p
proofend;

registration
let T be finite Tree;
let t be Element of T;
let T1 be finite Tree;
clusterT with-replacement (t,T1) ->  finite ;
coherence
 T with-replacement (t,T1) is finite
proofend;
end;

theorem Th34: :: TREES_1:34
for p being FinSequence holds ProperPrefixes p, dom p are_equipotent
proofend;

registration
let p be FinSequence;
cluster ProperPrefixes p ->  finite ;
coherence
 ProperPrefixes p is finite
proofend;
end;

theorem :: TREES_1:35
for p being FinSequence holds card (ProperPrefixes p) = len p
proofend;

::
:: Height and width of finite trees
::
definition
let IT be set ;
attrIT is AntiChain_of_Prefixes-like  means :Def10: :: TREES_1:def 10
( ( for x being set st x in IT holds
x is FinSequence ) &amp; ( for p1, p2 being FinSequence st p1 in IT &amp; p2 in IT &amp; p1 <> p2 holds
not p1,p2 are_c=-comparable ) );
end;

:: deftheorem Def10 defines AntiChain_of_Prefixes-like TREES_1:def_10_:_
 for IT being set holds
( IT is AntiChain_of_Prefixes-like iff ( ( for x being set st x in IT holds
x is FinSequence ) &amp; ( for p1, p2 being FinSequence st p1 in IT &amp; p2 in IT &amp; p1 <> p2 holds
not p1,p2 are_c=-comparable ) ) );

registration
cluster AntiChain_of_Prefixes-like for set ;
existence
 ex b1 being set st b1 is AntiChain_of_Prefixes-like
proofend;
end;

definition
mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set ;
end;

theorem Th36: :: TREES_1:36
for w being FinSequence holds {w} is AntiChain_of_Prefixes-like
proofend;

theorem Th37: :: TREES_1:37
for p1, p2 being FinSequence st not p1,p2 are_c=-comparable holds
{p1,p2} is AntiChain_of_Prefixes-like
proofend;

definition
let T be Tree;
mode AntiChain_of_Prefixes of T ->  AntiChain_of_Prefixes means :Def11: :: TREES_1:def 11
it c= T;
existence
 ex b1 being AntiChain_of_Prefixes st b1 c= T
proofend;
end;

:: deftheorem Def11 defines AntiChain_of_Prefixes TREES_1:def_11_:_
 for T being Tree
for b2 being AntiChain_of_Prefixes holds
( b2 is AntiChain_of_Prefixes of T iff b2 c= T );

theorem Th38: :: TREES_1:38
for T being Tree holds
( {} is AntiChain_of_Prefixes of T &amp; {{}} is AntiChain_of_Prefixes of T )
proofend;

theorem :: TREES_1:39
for T being Tree
for t being Element of T holds {t} is AntiChain_of_Prefixes of T
proofend;

theorem :: TREES_1:40
for T being Tree
for t1, t2 being Element of T st not t1,t2 are_c=-comparable holds
{t1,t2} is AntiChain_of_Prefixes of T
proofend;

registration
let T be finite Tree;
cluster  ->  finite for AntiChain_of_Prefixes of T;
coherence
 for b1 being AntiChain_of_Prefixes of T holds b1 is finite
proofend;
end;

definition
let T be finite Tree;
func height T ->  Element of NAT  means :Def12: :: TREES_1:def 12
( ex p being FinSequence of NAT st
( p in T &amp; len p = it ) &amp; ( for p being FinSequence of NAT st p in T holds
len p <= it ) );
existence
 ex b1 being Element of NAT st
( ex p being FinSequence of NAT st
( p in T &amp; len p = b1 ) &amp; ( for p being FinSequence of NAT st p in T holds
len p <= b1 ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex p being FinSequence of NAT st
( p in T &amp; len p = b1 ) &amp; ( for p being FinSequence of NAT st p in T holds
len p <= b1 ) &amp; ex p being FinSequence of NAT st
( p in T &amp; len p = b2 ) &amp; ( for p being FinSequence of NAT st p in T holds
len p <= b2 ) holds
b1 = b2
proofend;
func width T ->  Element of NAT  means :Def13: :: TREES_1:def 13
 ex X being AntiChain_of_Prefixes of T st
( it = card X &amp; ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) );
existence
 ex b1 being Element of NAT ex X being AntiChain_of_Prefixes of T st
( b1 = card X &amp; ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) )
proofend;
uniqueness
 for b1, b2 being Element of NAT st ex X being AntiChain_of_Prefixes of T st
( b1 = card X &amp; ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) &amp; ex X being AntiChain_of_Prefixes of T st
( b2 = card X &amp; ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines height TREES_1:def_12_:_
 for T being finite Tree
for b2 being Element of NAT holds
( b2 = height T iff ( ex p being FinSequence of NAT st
( p in T &amp; len p = b2 ) &amp; ( for p being FinSequence of NAT st p in T holds
len p <= b2 ) ) );

:: deftheorem Def13 defines width TREES_1:def_13_:_
 for T being finite Tree
for b2 being Element of NAT holds
( b2 = width T iff ex X being AntiChain_of_Prefixes of T st
( b2 = card X &amp; ( for Y being AntiChain_of_Prefixes of T holds card Y <= card X ) ) );

theorem :: TREES_1:41
for fT being finite Tree holds 1 <= width fT
proofend;

theorem :: TREES_1:42
height (elementary_tree 0) = 0
proofend;

theorem :: TREES_1:43
for fT being finite Tree st height fT = 0 holds
fT = elementary_tree 0
proofend;

theorem :: TREES_1:44
for n being Element of NAT holds height (elementary_tree (n + 1)) = 1
proofend;

theorem :: TREES_1:45
width (elementary_tree 0) = 1
proofend;

theorem :: TREES_1:46
for n being Element of NAT holds width (elementary_tree (n + 1)) = n + 1
proofend;

theorem :: TREES_1:47
for fT being finite Tree
for t being Element of fT holds height (fT | t) <= height fT
proofend;

theorem Th48: :: TREES_1:48
for fT being finite Tree
for t being Element of fT st t <> {} holds
height (fT | t) < height fT
proofend;

scheme :: TREES_1:sch 1
TreeInd{ P1[ Tree] } :
 for fT being finite Tree holds P1[fT]
provided
A1: for fT being finite Tree st ( for n being Element of NAT st <*n*> in fT holds
P1[fT | <*n*>] ) holds
P1[fT]
proofend;

begin

theorem :: TREES_1:49
for w, t, s being FinSequence st w ^ t is_a_proper_prefix_of w ^ s holds
t is_a_proper_prefix_of s
proofend;

theorem :: TREES_1:50
for n, m being Element of NAT
for s being FinSequence st n <> m holds
not <*n*> is_a_prefix_of <*m*> ^ s
proofend;

theorem :: TREES_1:51
elementary_tree 1 = {{},<*0*>}
proofend;

theorem :: TREES_1:52
for n, m being Element of NAT holds not <*n*> is_a_proper_prefix_of <*m*>
proofend;

theorem :: TREES_1:53
elementary_tree 2 = {{},<*0*>,<*1*>}
proofend;

:: from BINTREE1
theorem :: TREES_1:54
for T being Tree
for t being Element of T holds
( t in Leaves T iff not t ^ <*0*> in T )
proofend;

theorem :: TREES_1:55
for T being Tree
for t being Element of T holds
( t in Leaves T iff for n being Element of NAT holds not t ^ <*n*> in T )
proofend;

definition
func TrivialInfiniteTree  ->  set  equals :: TREES_1:def 14
 {  (k |-> 0) where k is Element of NAT : verum  }  ;
coherence
  {  (k |-> 0) where k is Element of NAT : verum  }  is set ;
end;

:: deftheorem  defines TrivialInfiniteTree TREES_1:def_14_:_
 TrivialInfiniteTree =  {  (k |-> 0) where k is Element of NAT : verum  }  ;

registration
cluster TrivialInfiniteTree  ->  non empty Tree-like ;
coherence
 ( not TrivialInfiniteTree is empty &amp; TrivialInfiniteTree is Tree-like )
proofend;
end;

theorem Th56: :: TREES_1:56
NAT , TrivialInfiniteTree are_equipotent
proofend;

registration
cluster TrivialInfiniteTree  ->  infinite ;
coherence
 not TrivialInfiniteTree is finite by Th56, CARD_1:38;
end;