:: Introduction to Trees :: by Grzegorz Bancerek :: :: Received October 25, 1989 :: Copyright (c) 1990-2018 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;