diff -r 57e4bd1e2e18 -r b80734daf7ed src/HOL/Data_Structures/AVL_Set.thy --- a/src/HOL/Data_Structures/AVL_Set.thy Wed May 30 13:44:53 2018 +0200 +++ b/src/HOL/Data_Structures/AVL_Set.thy Fri Jun 01 13:32:44 2018 +0200 @@ -455,7 +455,7 @@ subsection \Height-Size Relation\ -text \By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\ +text \Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\ lemma height_invers: "(height t = 0) = (t = Leaf)" @@ -529,19 +529,36 @@ text \The size of an AVL tree is (at least) exponential in its height:\ -lemma avl_lowerbound: +lemma avl_size_lowerbound: defines "\ \ (1 + sqrt 5) / 2" assumes "avl t" - shows "real (size1 t) \ \ ^ (height t)" + shows "\ ^ (height t) \ size1 t" proof - have "\ > 0" by(simp add: \_def add_pos_nonneg) hence "\ ^ height t = (1 / \ ^ 2) * \ ^ (height t + 2)" by(simp add: field_simps power2_eq_square) - also have "\ \ real (fib (height t + 2))" + also have "\ \ fib (height t + 2)" using fib_lowerbound[of "height t + 2"] by(simp add: \_def) - also have "\ \ real (size1 t)" + also have "\ \ size1 t" using avl_fib_bound[of t "height t"] assms by simp finally show ?thesis . qed +text \The height of an AVL tree is most @{term "(1/log 2 \)"} \\ 1.44\ times worse +than @{term "log 2 (size1 t)"}:\ + +lemma avl_height_upperbound: + defines "\ \ (1 + sqrt 5) / 2" + assumes "avl t" + shows "height t \ (1/log 2 \) * log 2 (size1 t)" +proof - + have "\ > 0" "\ > 1" by(auto simp: \_def pos_add_strict) + hence "height t = log \ (\ ^ height t)" by(simp add: log_nat_power) + also have "\ \ log \ (size1 t)" + using avl_size_lowerbound[OF assms(2), folded \_def] \1 < \\ by simp + also have "\ = (1/log 2 \) * log 2 (size1 t)" + by(simp add: log_base_change[of 2 \]) + finally show ?thesis . +qed + end