src/HOL/Data_Structures/AVL_Set.thy
changeset 68313 56c57e91edf9
parent 68023 75130777ece4
child 68342 b80734daf7ed
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Tue May 29 14:05:59 2018 +0200
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Tue May 29 20:01:50 2018 +0200
     1.3 @@ -455,80 +455,93 @@
     1.4  
     1.5  subsection \<open>Height-Size Relation\<close>
     1.6  
     1.7 -text \<open>By Daniel St\"uwe\<close>
     1.8 -
     1.9 -fun fib_tree :: "nat \<Rightarrow> unit avl_tree" where
    1.10 -"fib_tree 0 = Leaf" |
    1.11 -"fib_tree (Suc 0) = Node 1 Leaf () Leaf" |
    1.12 -"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)"
    1.13 -
    1.14 -lemma [simp]: "ht (fib_tree h) = h"
    1.15 -by (induction h rule: "fib_tree.induct") auto
    1.16 +text \<open>By Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close>
    1.17  
    1.18 -lemma [simp]: "height (fib_tree h) = h"
    1.19 -by (induction h rule: "fib_tree.induct") auto
    1.20 -
    1.21 -lemma "avl(fib_tree h)"          
    1.22 -by (induction h rule: "fib_tree.induct") auto
    1.23 -
    1.24 -lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)"
    1.25 -by (induction h rule: fib_tree.induct) auto
    1.26 -
    1.27 -lemma height_invers[simp]: 
    1.28 +lemma height_invers: 
    1.29    "(height t = 0) = (t = Leaf)"
    1.30    "avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)"
    1.31  by (induction t) auto
    1.32  
    1.33 -lemma fib_Suc_lt: "fib n \<le> fib (Suc n)"
    1.34 -by (induction n rule: fib.induct) auto
    1.35 +text \<open>Any AVL tree of height \<open>h\<close> has at least \<open>fib (h+2)\<close> leaves:\<close>
    1.36  
    1.37 -lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> fib m"
    1.38 -proof (induction n arbitrary: m rule: fib.induct )
    1.39 -  case (2 m)
    1.40 -  thus ?case using fib_neq_0_nat[of m] by auto
    1.41 +lemma avl_fib_bound: "avl t \<Longrightarrow> height t = h \<Longrightarrow> fib (h+2) \<le> size1 t"
    1.42 +proof (induction h arbitrary: t rule: fib.induct)
    1.43 +  case 1 thus ?case by (simp add: height_invers)
    1.44  next
    1.45 -  case (3 n m)
    1.46 -  from 3 obtain m' where "m = Suc (Suc m')"
    1.47 -    by (metis le_Suc_ex plus_nat.simps(2)) 
    1.48 -  thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto
    1.49 -qed simp
    1.50 -
    1.51 -lemma size1_fib_tree_mono:
    1.52 -  assumes "n \<le> m"
    1.53 -  shows   "size1 (fib_tree n) \<le> size1 (fib_tree m)"
    1.54 -using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce 
    1.55 -
    1.56 -lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t"
    1.57 -proof (induction "ht t" arbitrary: t rule: fib_tree.induct)
    1.58 -  case (2 t)
    1.59 -  from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto
    1.60 -  with 2 show ?case by auto
    1.61 +  case 2 thus ?case by (cases t) (auto simp: height_invers)
    1.62  next
    1.63 -  case (3 h t)
    1.64 -  note [simp] = 3(3)[symmetric] 
    1.65 -  from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto
    1.66 -  show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) 
    1.67 -    case equal
    1.68 -    with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto
    1.69 -    with 3 have "size1 (fib_tree (ht l)) \<le> size1 l" by auto moreover
    1.70 -    from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> size1 r" by auto ultimately
    1.71 -    show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto
    1.72 -  next
    1.73 -    case greater
    1.74 -    with 3(3,4) have ht: "ht l = Suc h"  "ht r = h" by auto
    1.75 -    from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \<le> size1 l" by auto moreover
    1.76 -    from ht 3(1,2,4) have "size1 (fib_tree h) \<le> size1 r" by auto ultimately
    1.77 -    show ?thesis by auto
    1.78 -  next
    1.79 -    case less (* analogously *)
    1.80 -    with 3 have ht: "ht l = h"  "Suc h = ht r" by auto
    1.81 -    from ht 3 have "size1 (fib_tree h) \<le> size1 l" by auto moreover
    1.82 -    from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately
    1.83 -    show ?thesis by auto
    1.84 -  qed
    1.85 -qed auto
    1.86 +  case (3 h)
    1.87 +  from "3.prems" obtain l a r where
    1.88 +    [simp]: "t = Node (Suc(Suc h)) l a r" "avl l" "avl r"
    1.89 +    and C: "
    1.90 +      height r = Suc h \<and> height l = Suc h
    1.91 +    \<or> height r = Suc h \<and> height l = h
    1.92 +    \<or> height r = h \<and> height l = Suc h" (is "?C1 \<or> ?C2 \<or> ?C3")
    1.93 +    by (cases t) (simp, fastforce)
    1.94 +  {
    1.95 +    assume ?C1
    1.96 +    with "3.IH"(1)
    1.97 +    have "fib (h + 3) \<le> size1 l" "fib (h + 3) \<le> size1 r"
    1.98 +      by (simp_all add: eval_nat_numeral)
    1.99 +    hence ?case by (auto simp: eval_nat_numeral)
   1.100 +  } moreover {
   1.101 +    assume ?C2
   1.102 +    hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto
   1.103 +  } moreover {
   1.104 +    assume ?C3
   1.105 +    hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto
   1.106 +  } ultimately show ?case using C by blast
   1.107 +qed
   1.108 +
   1.109 +lemma fib_alt_induct [consumes 1, case_names 1 2 rec]:
   1.110 +  assumes "n > 0" "P 1" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))"
   1.111 +  shows   "P n"
   1.112 +  using assms(1)
   1.113 +proof (induction n rule: fib.induct)
   1.114 +  case (3 n)
   1.115 +  thus ?case using assms by (cases n) (auto simp: eval_nat_numeral)
   1.116 +qed (insert assms, auto)
   1.117 +
   1.118 +text \<open>An exponential lower bound for @{const fib}:\<close>
   1.119  
   1.120 -theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t" 
   1.121 -using fib_tree_minimal fib_tree_size1 by fastforce
   1.122 +lemma fib_lowerbound:
   1.123 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   1.124 +  defines "c \<equiv> 1 / \<phi> ^ 2"
   1.125 +  assumes "n > 0"
   1.126 +  shows   "real (fib n) \<ge> c * \<phi> ^ n"
   1.127 +proof -
   1.128 +  have "\<phi> > 1" by (simp add: \<phi>_def)
   1.129 +  hence "c > 0" by (simp add: c_def)
   1.130 +  from \<open>n > 0\<close> show ?thesis
   1.131 +  proof (induction n rule: fib_alt_induct)
   1.132 +    case (rec n)
   1.133 +    have "c * \<phi> ^ Suc (Suc n) = \<phi> ^ 2 * (c * \<phi> ^ n)"
   1.134 +      by (simp add: field_simps power2_eq_square)
   1.135 +    also have "\<dots> \<le> (\<phi> + 1) * (c * \<phi> ^ n)"
   1.136 +      by (rule mult_right_mono) (insert \<open>c > 0\<close>, simp_all add: \<phi>_def power2_eq_square field_simps)
   1.137 +    also have "\<dots> = c * \<phi> ^ Suc n + c * \<phi> ^ n"
   1.138 +      by (simp add: field_simps)
   1.139 +    also have "\<dots> \<le> real (fib (Suc n)) + real (fib n)"
   1.140 +      by (intro add_mono rec.IH)
   1.141 +    finally show ?case by simp
   1.142 +  qed (insert \<open>\<phi> > 1\<close>, simp_all add: c_def power2_eq_square eval_nat_numeral)
   1.143 +qed
   1.144 +
   1.145 +text \<open>The size of an AVL tree is (at least) exponential in its height:\<close>
   1.146 +
   1.147 +lemma avl_lowerbound:
   1.148 +  defines "\<phi> \<equiv> (1 + sqrt 5) / 2"
   1.149 +  assumes "avl t"
   1.150 +  shows   "real (size1 t) \<ge> \<phi> ^ (height t)"
   1.151 +proof -
   1.152 +  have "\<phi> > 0" by(simp add: \<phi>_def add_pos_nonneg)
   1.153 +  hence "\<phi> ^ height t = (1 / \<phi> ^ 2) * \<phi> ^ (height t + 2)"
   1.154 +    by(simp add: field_simps power2_eq_square)
   1.155 +  also have "\<dots> \<le> real (fib (height t + 2))"
   1.156 +    using fib_lowerbound[of "height t + 2"] by(simp add: \<phi>_def)
   1.157 +  also have "\<dots> \<le> real (size1 t)"
   1.158 +    using avl_fib_bound[of t "height t"] assms by simp
   1.159 +  finally show ?thesis .
   1.160 +qed
   1.161  
   1.162  end