src/HOL/Data_Structures/AVL_Set.thy
changeset 68342 b80734daf7ed
parent 68313 56c57e91edf9
child 68413 b56ed5010e69
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Wed May 30 13:44:53 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Jun 01 13:32:44 2018 +0200
     1.3 @@ -455,7 +455,7 @@
     1.4  
     1.5  subsection \<open>Height-Size Relation\<close>
     1.6  
     1.7 -text \<open>By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
     1.8 +text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
     1.9  
    1.10  lemma height_invers: 
    1.11    "(height t = 0) = (t = Leaf)"
    1.12 @@ -529,19 +529,36 @@
    1.13  
    1.14  text \<open>The size of an AVL tree is (at least) exponential in its height:\<close>
    1.15  
    1.16 -lemma avl_lowerbound:
    1.17 +lemma avl_size_lowerbound:
    1.18    defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
    1.19    assumes "avl t"
    1.20 -  shows   "real (size1 t) \<ge> \<phi> ^ (height t)"
    1.21 +  shows   "\<phi> ^ (height t) \<le> size1 t"
    1.22  proof -
    1.23    have "\<phi> > 0" by(simp add: \<phi>_def add_pos_nonneg)
    1.24    hence "\<phi> ^ height t = (1 / \<phi> ^ 2) * \<phi> ^ (height t + 2)"
    1.25      by(simp add: field_simps power2_eq_square)
    1.26 -  also have "\<dots> \<le> real (fib (height t + 2))"
    1.27 +  also have "\<dots> \<le> fib (height t + 2)"
    1.28      using fib_lowerbound[of "height t + 2"] by(simp add: \<phi>_def)
    1.29 -  also have "\<dots> \<le> real (size1 t)"
    1.30 +  also have "\<dots> \<le> size1 t"
    1.31      using avl_fib_bound[of t "height t"] assms by simp
    1.32    finally show ?thesis .
    1.33  qed
    1.34  
    1.35 +text \<open>The height of an AVL tree is most @{term "(1/log 2 \<phi>)"} \<open>\<approx> 1.44\<close> times worse
    1.36 +than @{term "log 2 (size1 t)"}:\<close>
    1.37 +
    1.38 +lemma  avl_height_upperbound:
    1.39 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
    1.40 +  assumes "avl t"
    1.41 +  shows   "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)"
    1.42 +proof -
    1.43 +  have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
    1.44 +  hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
    1.45 +  also have "\<dots> \<le> log \<phi> (size1 t)"
    1.46 +    using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>  by simp
    1.47 +  also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
    1.48 +    by(simp add: log_base_change[of 2 \<phi>])
    1.49 +  finally show ?thesis .
    1.50 +qed
    1.51 +
    1.52  end