merged
authornipkow
Tue Jan 19 11:36:09 2016 +0100 (2016-01-19 ago)
changeset 622036acae6430fcc
parent 62201 eca7b38c8ee5
parent 62202 e5bc7cbb0bcc
child 62204 7f5579b12b0a
merged
     1.1 --- a/src/HOL/Library/Tree.thy	Tue Jan 19 11:19:25 2016 +0100
     1.2 +++ b/src/HOL/Library/Tree.thy	Tue Jan 19 11:36:09 2016 +0100
     1.3 @@ -58,6 +58,27 @@
     1.4  lemma height_map_tree[simp]: "height (map_tree f t) = height t"
     1.5  by (induction t) auto
     1.6  
     1.7 +lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)"
     1.8 +proof(induction t)
     1.9 +  case (Node l a r)
    1.10 +  show ?case
    1.11 +  proof (cases "height l \<le> height r")
    1.12 +    case True
    1.13 +    have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp
    1.14 +    also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1))
    1.15 +    also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2))
    1.16 +    also have "(2::nat) ^ height l \<le> 2 ^ height r" using True by simp
    1.17 +    finally show ?thesis using True by (auto simp: max_def mult_2)
    1.18 +  next
    1.19 +    case False
    1.20 +    have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp
    1.21 +    also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1))
    1.22 +    also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2))
    1.23 +    also have "(2::nat) ^ height r \<le> 2 ^ height l" using False by simp
    1.24 +    finally show ?thesis using False by (auto simp: max_def mult_2)
    1.25 +  qed
    1.26 +qed simp
    1.27 +
    1.28  
    1.29  subsection "The set of subtrees"
    1.30