TREES_1: Introduction to Trees

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

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 :: TREES_1:def 1
ex n being Nat st p = q | (Seg n);

compatibility

proof end;

end;

:: deftheorem defines is_a_prefix_of TREES_1:def 1 :

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 )

proof end;

theorem :: TREES_1:2

canceled;

::$CT

theorem Th2: :: TREES_1:3

for x, y being set st <*x*> is_a_prefix_of <*y*> holds
x = y

proof end;

notation

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

end;

theorem Th3: :: TREES_1:4

for p, q being finite set st p,q are_c=-comparable & card p = card q holds
p = q by CARD_2:102;

theorem Th4: :: TREES_1:5

for x, y being set st <*x*>,<*y*> are_c=-comparable holds
x = y

proof end;

theorem Th5: :: TREES_1:6

for p, q being finite set st p c< q holds
card p < card q

proof end;

theorem Th6: :: 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

proof end;

theorem Th7: :: 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*>

proof end;

theorem Th8: :: 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

proof end;

theorem :: TREES_1:10

for p1, p2 being FinSequence st ( {} is_a_proper_prefix_of p2 or {} <> p2 ) holds
p1 is_a_proper_prefix_of p1 ^ p2

proof end;

::
:: 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 object holds
( x in it iff ex q being FinSequence st
( x = q & q is_a_proper_prefix_of p ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines ProperPrefixes TREES_1:def 2 :

theorem Th10: :: TREES_1:11

for x being set
for p being FinSequence st x in ProperPrefixes p holds
x is FinSequence

proof end;

theorem Th11: :: TREES_1:12

for p, q being FinSequence holds
( p in ProperPrefixes q iff p is_a_proper_prefix_of q )

proof end;

theorem Th12: :: TREES_1:13

for p, q being FinSequence st p in ProperPrefixes q holds
len p < len q by Th11, Th5;

theorem :: TREES_1:14

for p, q, r being FinSequence st q ^ r in ProperPrefixes p holds
q in ProperPrefixes p

proof end;

theorem Th14: :: TREES_1:15

ProperPrefixes {} = {}

proof end;

set D = {{}};

theorem Th15: :: TREES_1:16

for x being set holds ProperPrefixes <*x*> = {{}}

proof end;

theorem :: TREES_1:17

for p, q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q

proof end;

theorem Th17: :: TREES_1:18

for p, q, r being FinSequence st q in ProperPrefixes p & r in ProperPrefixes p holds
q,r are_c=-comparable

proof end;

::
:: Trees and their properties
::

definition

let X be set ;

attr X is Tree-like means :Def3: :: TREES_1:def 3
( X c= NAT * & ( for p being FinSequence of NAT st p in X holds
ProperPrefixes p c= X ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in X & n <= k holds
p ^ <*n*> in X ) );

end;

:: deftheorem Def3 defines Tree-like TREES_1:def 3 :

registration

cluster {{}} -> Tree-like ;

coherence

proof end;

end;

registration

cluster non empty Tree-like for set ;

existence

proof end;

end;

definition

mode Tree is non empty Tree-like set ;

end;

theorem Th18: :: TREES_1:19

for x being set
for T being Tree st x in T holds
x is FinSequence of NAT

proof end;

definition

let T be Tree;
:: original: Element
redefine mode Element of T -> FinSequence of NAT ;
coherence by Th18;

end;

theorem Th19: :: TREES_1:20

for T being Tree
for p, q being FinSequence st p in T & q is_a_prefix_of p holds
q in T

proof end;

theorem Th20: :: 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

proof end;

theorem Th21: :: TREES_1:22

for T being Tree holds
( {} in T & <*> NAT in T )

proof end;

theorem :: TREES_1:23

{{}} is Tree ;

registration

let T, T1 be Tree;

cluster T \/ T1 -> Tree-like ;

coherence

proof end;

cluster T /\ T1 -> non empty Tree-like ;

coherence

proof end;

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

proof end;

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 Nat;

func elementary_tree n -> Tree equals :: TREES_1:def 4
{ <*k*> where k is Nat : k < n } \/ {{}};

correctness

proof end;

end;

:: deftheorem defines elementary_tree TREES_1:def 4 :

registration

let n be Nat;

cluster elementary_tree n -> finite ;

coherence

proof end;

end;

theorem Th27: :: TREES_1:28

for k, n being Nat st k < n holds
<*k*> in elementary_tree n

proof end;

theorem Th28: :: TREES_1:29

elementary_tree 0 = {{}}

proof end;

theorem :: TREES_1:30

for n being Nat
for p being FinSequence of NAT holds
( not p in elementary_tree n or p = {} or ex k being Nat st
( k < n & p = <*k*> ) )

proof end;

::
:: 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 & ( for q being FinSequence of NAT holds
( not q in T or not p is_a_proper_prefix_of q ) ) ) );

existence

proof end;

uniqueness

proof end;

let p be FinSequence of NAT ;
assume A11: p in T ;

func T | p -> Tree means :Def6: :: TREES_1:def 6
for q being FinSequence of NAT holds
( q in it iff p ^ q in T );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines Leaves TREES_1:def 5 :

:: deftheorem Def6 defines | TREES_1:def 6 :

theorem :: TREES_1:31

for T being Tree holds T | (<*> NAT) = T

proof end;

registration

let T be finite Tree;
let p be Element of T;

cluster T | p -> finite ;

coherence

proof end;

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

proof end;

end;

:: deftheorem defines Leaf TREES_1:def 7 :

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

proof end;

end;

:: deftheorem defines Subtree TREES_1:def 8 :

definition

let T be Tree;
let p be FinSequence of NAT ;
let T1 be Tree;
assume A1: p in T ;

func T 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 & not p is_a_proper_prefix_of q ) or ex r being FinSequence of NAT st
( r in T1 & q = p ^ r ) ) );

existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines with-replacement TREES_1:def 9 :

theorem Th31: :: 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 : verum }

proof end;

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

proof end;

registration

let T be finite Tree;
let t be Element of T;
let T1 be finite Tree;

cluster T with-replacement (t,T1) -> finite ;

coherence

proof end;

end;

theorem Th33: :: TREES_1:34

for p being FinSequence holds ProperPrefixes p, dom p are_equipotent

proof end;

registration

let p be FinSequence;

cluster ProperPrefixes p -> finite ;

coherence

proof end;

end;

theorem :: TREES_1:35

for p being FinSequence holds card (ProperPrefixes p) = len p

proof end;

::
:: Height and width of finite trees
::

definition

let IT be set ;

attr IT is AntiChain_of_Prefixes-like means :Def10: :: TREES_1:def 10
( ( for x being set st x in IT holds
x is FinSequence ) & ( for p1, p2 being FinSequence st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable ) );

end;

:: deftheorem Def10 defines AntiChain_of_Prefixes-like TREES_1:def 10 :

registration

cluster AntiChain_of_Prefixes-like for set ;

existence

proof end;

end;

definition

mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set ;

end;

theorem Th35: :: TREES_1:36

for w being FinSequence holds {w} is AntiChain_of_Prefixes-like

proof end;

theorem Th36: :: TREES_1:37

for p1, p2 being FinSequence st not p1,p2 are_c=-comparable holds
{p1,p2} is AntiChain_of_Prefixes-like

proof end;

definition

let T be Tree;

mode AntiChain_of_Prefixes of T -> AntiChain_of_Prefixes means :Def11: :: TREES_1:def 11
it c= T;

existence

proof end;

end;

:: deftheorem Def11 defines AntiChain_of_Prefixes TREES_1:def 11 :

theorem Th37: :: TREES_1:38

for T being Tree holds
( {} is AntiChain_of_Prefixes of T & {{}} is AntiChain_of_Prefixes of T )

proof end;

theorem :: TREES_1:39

for T being Tree
for t being Element of T holds {t} is AntiChain_of_Prefixes of T

proof end;

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

proof end;

registration

let T be finite Tree;

cluster -> finite for AntiChain_of_Prefixes of T;

coherence

proof end;

end;

definition

let T be finite Tree;

func height T -> Nat means :Def12: :: TREES_1:def 12
( ex p being FinSequence of NAT st
( p in T & len p = it ) & ( for p being FinSequence of NAT st p in T holds
len p <= it ) );