:: Introduction to Trees
:: by Grzegorz Bancerek
::
:: Received October 25, 1989
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, SUBSET_1, FUNCT_1, FINSEQ_1, TARSKI, RELAT_1,
NAT_1, ORDINAL4, ARYTM_3, FINSET_1, CARD_1, XXREAL_0, ORDINAL1, TREES_1,
AMISTD_3, FINSEQ_2;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, XCMPLX_0, ORDINAL1,
NAT_1, NUMBERS, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FUNCT_2, FINSET_1,
XXREAL_0;
constructors ENUMSET1, WELLORD2, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, FINSEQ_2,
FUNCOP_1, FUNCT_2, RELSET_1, NUMBERS;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FINSET_1, XXREAL_0,
XREAL_0, NAT_1, FINSEQ_1, CARD_1, RELSET_1, FINSEQ_2;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
begin
reserve:: D for non empty set,
X,x,y,z for set,
k,n,m for Nat ,
f for Function,
p,q,r for FinSequence of NAT;
::
:: Relations "is a prefix of", "is a proper prefix of" and
:: "are comparable" of finite sequences
::
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 is_a_prefix_of q means
:: TREES_1:def 1
ex n st p = q|Seg n;
end;
theorem :: TREES_1:1
for p,q being FinSequence holds p is_a_prefix_of q iff
ex r being FinSequence st q = p^r;
::$CT
theorem :: TREES_1:3
<*x*> is_a_prefix_of <*y*> implies x = y;
notation
let p,q be FinSequence;
synonym p is_a_proper_prefix_of q for p c< q;
end;
theorem :: TREES_1:4
for p,q being finite set st p,q are_c=-comparable & card p = card q holds
p = q;
reserve p1,p2,p3 for FinSequence;
theorem :: TREES_1:5
<*x*>,<*y*> are_c=-comparable implies x = y;
theorem :: TREES_1:6
for p,q being finite set st p c< q holds card p < card q;
theorem :: TREES_1:7
p1^<*x*> is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2;
theorem :: TREES_1:8
p1 is_a_prefix_of p2 implies p1 is_a_proper_prefix_of p2^<*x*>;
theorem :: TREES_1:9
p1 is_a_proper_prefix_of p2^<*x*> implies p1 is_a_prefix_of p2;
theorem :: TREES_1:10
{} is_a_proper_prefix_of p2 or {} <> p2 implies
p1 is_a_proper_prefix_of p1^p2;
::
:: The set of proper prefixes of a finite sequence
::
definition
let p be FinSequence;
func ProperPrefixes p -> set means
:: 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;
end;
theorem :: TREES_1:11
for p being FinSequence st x in ProperPrefixes p holds x is FinSequence;
theorem :: TREES_1:12
for p,q being FinSequence holds
p in ProperPrefixes q iff p is_a_proper_prefix_of q;
theorem :: TREES_1:13
for p,q being FinSequence st p in ProperPrefixes q holds len p < len q;
theorem :: TREES_1:14
for p,q,r being FinSequence st q^r in ProperPrefixes p holds
q in ProperPrefixes p;
theorem :: TREES_1:15
ProperPrefixes {} = {};
theorem :: TREES_1:16
ProperPrefixes <*x*> = { {} };
theorem :: TREES_1:17
for p,q being FinSequence st p is_a_prefix_of q holds
ProperPrefixes p c= ProperPrefixes q;
theorem :: TREES_1:18
for p,q,r being FinSequence st
q in ProperPrefixes p & r in ProperPrefixes p holds q,r are_c=-comparable;
::
:: Trees and their properties
::
definition
let X;
attr X is Tree-like means
:: TREES_1:def 3
X c= NAT* & (for p st p in X holds ProperPrefixes p c= X) &
for p,k,n st p^<*k*> in X & n <= k holds p^<*n*> in X;
end;
registration
cluster { {} } -> Tree-like;
end;
registration
cluster non empty Tree-like for set;
end;
definition
mode Tree is Tree-like non empty set;
end;
reserve T,T1 for Tree;
theorem :: TREES_1:19
x in T implies x is FinSequence of NAT;
definition
let T;
redefine mode Element of T -> FinSequence of NAT;
end;
theorem :: TREES_1:20
for p,q being FinSequence st p in T & q is_a_prefix_of p holds q in T;
theorem :: TREES_1:21
for r being FinSequence st q^r in T holds q in T;
theorem :: TREES_1:22
{} in T & <*> NAT in T;
theorem :: TREES_1:23
{ {} } is Tree;
registration
let T,T1;
cluster T \/ T1 -> Tree-like;
cluster T /\ T1 -> Tree-like non empty;
end;
theorem :: TREES_1:24
T \/ T1 is Tree;
theorem :: TREES_1:25
T /\ T1 is Tree;
::
:: Finite trees and their properties
::
registration
cluster finite for Tree;
end;
reserve fT,fT1 for finite Tree;
theorem :: TREES_1:26
fT \/ fT1 is finite Tree;
theorem :: TREES_1:27
fT /\ T is finite Tree;
::
:: Elementary trees
::
definition
let n;
func elementary_tree n -> Tree equals
:: TREES_1:def 4
{ <*k*> : k < n } \/ { {} };
end;
registration
let n;
cluster elementary_tree n -> finite;
end;
theorem :: TREES_1:28
k < n implies <*k*> in elementary_tree n;
theorem :: TREES_1:29
elementary_tree 0 = { {} };
theorem :: TREES_1:30
p in elementary_tree n implies p = {} or ex k st k < n & p = <*k*>;
::
:: Leaves and subtrees
::
definition
let T;
func Leaves T -> Subset of T means
:: TREES_1:def 5
p in it iff p in T & not ex q st q in T & p is_a_proper_prefix_of q;
let p such that
p in T;
func T|p -> Tree means
:: TREES_1:def 6 :: subtree of T, which root is in p
q in it iff p^q in T;
end;
theorem :: TREES_1:31
T|(<*> NAT) = T;
registration
let T be finite Tree;
let p be Element of T;
cluster T|p -> finite;
end;
definition
let T;
assume
Leaves T <> {};
mode Leaf of T -> Element of T means
:: TREES_1:def 7
it in Leaves T;
end;
definition
let T;
mode Subtree of T -> Tree means
:: TREES_1:def 8
ex p being Element of T st it = T|p;
end;
reserve t for Element of T;
definition
let T,p,T1;
assume
p in T;
func T with-replacement (p,T1) -> Tree means
:: TREES_1:def 9
q in it iff q in T & not p is_a_proper_prefix_of q or
ex r st r in T1 & q = p^r;
end;
theorem :: TREES_1:32
p in T implies T with-replacement (p,T1) =
{ t1 where t1 is Element of T : not p is_a_proper_prefix_of t1 } \/
the set of all p^s where s is Element of T1;
theorem :: TREES_1:33
p in T implies T1 = T with-replacement (p,T1)|p;
registration
let T be finite Tree, t be Element of T;
let T1 be finite Tree;
cluster T with-replacement (t,T1) -> finite;
end;
reserve w for FinSequence;
theorem :: TREES_1:34
for p being FinSequence holds ProperPrefixes p,dom p are_equipotent;
registration
let p be FinSequence;
cluster ProperPrefixes p -> finite;
end;
theorem :: TREES_1:35
for p being FinSequence holds card ProperPrefixes p = len p;
::
:: Height and width of finite trees
::
definition
let IT be set;
attr IT is AntiChain_of_Prefixes-like means
:: TREES_1:def 10
(for x st x in IT holds x is FinSequence) &
for p1,p2 st p1 in IT & p2 in IT & p1 <> p2 holds
not p1,p2 are_c=-comparable;
end;
registration
cluster AntiChain_of_Prefixes-like for set;
end;
definition
mode AntiChain_of_Prefixes is AntiChain_of_Prefixes-like set;
end;
theorem :: TREES_1:36
{ w } is AntiChain_of_Prefixes-like;
theorem :: TREES_1:37
not p1,p2 are_c=-comparable implies { p1,p2 } is AntiChain_of_Prefixes-like;
definition
let T;
mode AntiChain_of_Prefixes of T -> AntiChain_of_Prefixes means
:: TREES_1:def 11
it c= T;
end;
reserve t1,t2 for Element of T;
theorem :: TREES_1:38
{} is AntiChain_of_Prefixes of T & { {} } is AntiChain_of_Prefixes of T;
theorem :: TREES_1:39
{ t } is AntiChain_of_Prefixes of T;
theorem :: TREES_1:40
not t1,t2 are_c=-comparable implies { t1,t2 } is AntiChain_of_Prefixes of T;
registration
let T be finite Tree;
cluster -> finite for AntiChain_of_Prefixes of T;
end;
definition
let T be finite Tree;
func height T -> Nat means
:: TREES_1:def 12
(ex p st p in T & len p = it) & for p st p in T holds len p <= it;
func width T -> Nat means
:: TREES_1:def 13
ex X being AntiChain_of_Prefixes of T st it = card X &
for Y being AntiChain_of_Prefixes of T holds card Y <= card X;
end;
theorem :: TREES_1:41
1 <= width fT;
theorem :: TREES_1:42
height elementary_tree 0 = 0;
theorem :: TREES_1:43
height fT = 0 implies fT = elementary_tree 0;
theorem :: TREES_1:44
height elementary_tree(n+1) = 1;
theorem :: TREES_1:45
width elementary_tree 0 = 1;
theorem :: TREES_1:46
width elementary_tree(n+1) = n+1;
theorem :: TREES_1:47
for t being Element of fT holds height(fT|t) <= height fT;
theorem :: TREES_1:48
for t being Element of fT st t <> {} holds height(fT|t) < height fT;
scheme :: TREES_1:sch 1
TreeInd { P[Tree] }: for fT holds P[fT]
provided
for fT st
for n being Element of NAT st <*n*> in fT holds P[fT|<*n*>]
holds P[fT];
begin :: Addenda
:: from MODAL_1, 2007.03.14, A.T.
reserve s,t for FinSequence;
theorem :: TREES_1:49
w^t is_a_proper_prefix_of w^s implies t is_a_proper_prefix_of s;
theorem :: TREES_1:50
n <> m implies not <*n*> is_a_prefix_of <*m*>^s;
theorem :: TREES_1:51
elementary_tree 1 = {{},<*0*>};
theorem :: TREES_1:52
not <*n*> is_a_proper_prefix_of <*m*>;
theorem :: TREES_1:53
elementary_tree 2 = {{},<*0*>,<*1*>};
:: from BINTREE1
theorem :: TREES_1:54
for T being Tree, t being Element of T holds
t in Leaves T iff not t^<*0*> in T;
theorem :: TREES_1:55
for T being Tree, t being Element of T holds
t in Leaves T iff not ex n being Nat st t^<*n*> in T;
definition
func TrivialInfiniteTree -> set equals
:: TREES_1:def 14
the set of all k |-> 0 where k is Nat;
end;
registration
cluster TrivialInfiniteTree -> non empty Tree-like;
end;
theorem :: TREES_1:56
NAT,TrivialInfiniteTree are_equipotent;
registration
cluster TrivialInfiniteTree -> infinite;
end;