author  wenzelm 
Fri, 07 Aug 2020 11:46:14 +0200  
changeset 72110  16fab31feadc 
parent 71818  986d5abbe77c 
permissions  rwrr 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

1 
(* Author: Tobias Nipkow *) 
61232  2 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

3 
subsection \<open>Invariant\<close> 
61232  4 

5 
theory AVL_Set 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

6 
imports 
71795  7 
AVL_Set_Code 
66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
63411
diff
changeset

8 
"HOLNumber_Theory.Fib" 
61232  9 
begin 
10 

71818  11 
fun avl :: "'a tree_ht \<Rightarrow> bool" where 
61232  12 
"avl Leaf = True"  
71466  13 
"avl (Node l (a,n) r) = 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

14 
(abs(int(height l)  int(height r)) \<le> 1 \<and> 
71466  15 
n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" 
61232  16 

67406  17 
subsubsection \<open>Insertion maintains AVL balance\<close> 
61232  18 

19 
declare Let_def [simp] 

20 

70571  21 
lemma ht_height[simp]: "avl t \<Longrightarrow> ht t = height t" 
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset

22 
by (cases t rule: tree2_cases) simp_all 
61232  23 

71635  24 
text \<open>First, a fast but relatively manual proof with many lemmas:\<close> 
25 

61581  26 
lemma height_balL: 
71722  27 
"\<lbrakk> avl l; avl r; height l = height r + 2 \<rbrakk> \<Longrightarrow> 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

28 
height (balL l a r) \<in> {height r + 2, height r + 3}" 
71818  29 
by (auto simp:node_def balL_def split:tree.split) 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

30 

61581  31 
lemma height_balR: 
71722  32 
"\<lbrakk> avl l; avl r; height r = height l + 2 \<rbrakk> \<Longrightarrow> 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

33 
height (balR l a r) : {height l + 2, height l + 3}" 
71818  34 
by(auto simp add:node_def balR_def split:tree.split) 
61232  35 

70571  36 
lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1" 
61232  37 
by (simp add: node_def) 
38 

61581  39 
lemma height_balL2: 
61232  40 
"\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow> 
71722  41 
height (balL l a r) = 1 + max (height l) (height r)" 
71817  42 
by (simp_all add: balL_def) 
61232  43 

61581  44 
lemma height_balR2: 
61232  45 
"\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow> 
71722  46 
height (balR l a r) = 1 + max (height l) (height r)" 
71817  47 
by (simp_all add: balR_def) 
61232  48 

61581  49 
lemma avl_balL: 
71722  50 
"\<lbrakk> avl l; avl r; height r  1 \<le> height l \<and> height l \<le> height r + 2 \<rbrakk> \<Longrightarrow> avl(balL l a r)" 
71817  51 
by(auto simp: balL_def node_def split!: if_split tree.split) 
61232  52 

61581  53 
lemma avl_balR: 
71722  54 
"\<lbrakk> avl l; avl r; height l  1 \<le> height r \<and> height r \<le> height l + 2 \<rbrakk> \<Longrightarrow> avl(balR l a r)" 
71817  55 
by(auto simp: balR_def node_def split!: if_split tree.split) 
61232  56 

71635  57 
text\<open>Insertion maintains the AVL property. Requires simultaneous proof.\<close> 
61232  58 

68422  59 
theorem avl_insert: 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

60 
"avl t \<Longrightarrow> avl(insert x t)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

61 
"avl t \<Longrightarrow> height (insert x t) \<in> {height t, height t + 1}" 
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset

62 
proof (induction t rule: tree2_induct) 
71466  63 
case (Node l a _ r) 
61232  64 
case 1 
68422  65 
show ?case 
61232  66 
proof(cases "x = a") 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

67 
case True with 1 show ?thesis by simp 
61232  68 
next 
69 
case False 

68422  70 
show ?thesis 
61232  71 
proof(cases "x<a") 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

72 
case True with 1 Node(1,2) show ?thesis by (auto intro!:avl_balL) 
61232  73 
next 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

74 
case False with 1 Node(3,4) \<open>x\<noteq>a\<close> show ?thesis by (auto intro!:avl_balR) 
61232  75 
qed 
76 
qed 

77 
case 2 

68422  78 
show ?case 
61232  79 
proof(cases "x = a") 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

80 
case True with 2 show ?thesis by simp 
61232  81 
next 
82 
case False 

68422  83 
show ?thesis 
84 
proof(cases "x<a") 

61232  85 
case True 
68422  86 
show ?thesis 
61232  87 
proof(cases "height (insert x l) = height r + 2") 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

88 
case False with 2 Node(1,2) \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) 
61232  89 
next 
90 
case True 

61581  91 
hence "(height (balL (insert x l) a r) = height r + 2) \<or> 
92 
(height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B") 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

93 
using 2 Node(1,2) height_balL[OF _ _ True] by simp 
61232  94 
thus ?thesis 
95 
proof 

68422  96 
assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto) 
61232  97 
next 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

98 
assume ?B with 2 Node(2) True \<open>x < a\<close> show ?thesis by (simp) arith 
61232  99 
qed 
100 
qed 

101 
next 

102 
case False 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

103 
show ?thesis 
61232  104 
proof(cases "height (insert x r) = height l + 2") 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

105 
case False with 2 Node(3,4) \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) 
61232  106 
next 
107 
case True 

61581  108 
hence "(height (balR l a (insert x r)) = height l + 2) \<or> 
109 
(height (balR l a (insert x r)) = height l + 3)" (is "?A \<or> ?B") 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

110 
using 2 Node(3) height_balR[OF _ _ True] by simp 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

111 
thus ?thesis 
61232  112 
proof 
68422  113 
assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) 
61232  114 
next 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

115 
assume ?B with 2 Node(4) True \<open>\<not>x < a\<close> show ?thesis by (simp) arith 
61232  116 
qed 
117 
qed 

118 
qed 

119 
qed 

120 
qed simp_all 

121 

71635  122 
text \<open>Now an automatic proof without lemmas:\<close> 
123 

124 
theorem avl_insert_auto: "avl t \<Longrightarrow> 

125 
avl(insert x t) \<and> height (insert x t) \<in> {height t, height t + 1}" 

126 
apply (induction t rule: tree2_induct) 

71722  127 
(* if you want to save a few secs: apply (auto split!: if_split) *) 
128 
apply (auto simp: balL_def balR_def node_def max_absorb2 split!: if_split tree.split) 

71635  129 
done 
130 

61232  131 

67406  132 
subsubsection \<open>Deletion maintains AVL balance\<close> 
61232  133 

68023  134 
lemma avl_split_max: 
71722  135 
"\<lbrakk> avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> 
136 
avl (fst (split_max t)) \<and> 

137 
height t \<in> {height(fst (split_max t)), height(fst (split_max t)) + 1}" 

138 
by(induct t rule: split_max_induct) 

139 
(auto simp: balL_def node_def max_absorb2 split!: prod.split if_split tree.split) 

61232  140 

67406  141 
text\<open>Deletion maintains the AVL property:\<close> 
61232  142 

68422  143 
theorem avl_delete: 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

144 
"avl t \<Longrightarrow> avl(delete x t)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

145 
"avl t \<Longrightarrow> height t \<in> {height (delete x t), height (delete x t) + 1}" 
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset

146 
proof (induct t rule: tree2_induct) 
71466  147 
case (Node l a n r) 
61232  148 
case 1 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

149 
show ?case 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

150 
proof(cases "x = a") 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

151 
case True thus ?thesis 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

152 
using 1 avl_split_max[of l] by (auto intro!: avl_balR split: prod.split) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

153 
next 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

154 
case False thus ?thesis 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

155 
using Node 1 by (auto intro!: avl_balL avl_balR) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

156 
qed 
61232  157 
case 2 
68422  158 
show ?case 
71466  159 
proof(cases "x = a") 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

160 
case True thus ?thesis using 2 avl_split_max[of l] 
71636  161 
by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split) 
61232  162 
next 
163 
case False 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

164 
show ?thesis 
71466  165 
proof(cases "x<a") 
61232  166 
case True 
167 
show ?thesis 

168 
proof(cases "height r = height (delete x l) + 2") 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

169 
case False 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

170 
thus ?thesis using 2 Node(1,2) \<open>x < a\<close> by(auto simp: balR_def) 
61232  171 
next 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

172 
case True 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

173 
thus ?thesis using height_balR[OF _ _ True, of a] 2 Node(1,2) \<open>x < a\<close> by simp linarith 
61232  174 
qed 
175 
next 

176 
case False 

177 
show ?thesis 

178 
proof(cases "height l = height (delete x r) + 2") 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

179 
case False 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

180 
thus ?thesis using 2 Node(3,4) \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by(auto simp: balL_def) 
61232  181 
next 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

182 
case True 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

183 
thus ?thesis 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

184 
using height_balL[OF _ _ True, of a] 2 Node(3,4) \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> by simp linarith 
61232  185 
qed 
186 
qed 

187 
qed 

188 
qed simp_all 

189 

71722  190 
text \<open>A more automatic proof. 
191 
Complete automation as for insertion seems hard due to resource requirements.\<close> 

192 

193 
theorem avl_delete_auto: 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

194 
"avl t \<Longrightarrow> avl(delete x t)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

195 
"avl t \<Longrightarrow> height t \<in> {height (delete x t), height (delete x t) + 1}" 
71722  196 
proof (induct t rule: tree2_induct) 
197 
case (Node l a n r) 

198 
case 1 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

199 
thus ?case 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

200 
using Node avl_split_max[of l] by (auto intro!: avl_balL avl_balR split: prod.split) 
71722  201 
case 2 
202 
show ?case 

71817  203 
using 2 Node avl_split_max[of l] 
204 
by auto 

205 
(auto simp: balL_def balR_def max_absorb1 max_absorb2 split!: tree.splits prod.splits if_splits) 

71722  206 
qed simp_all 
207 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

208 

68422  209 
subsection "Overall correctness" 
210 

68440  211 
interpretation S: Set_by_Ordered 
68431  212 
where empty = empty and isin = isin and insert = insert and delete = delete 
68422  213 
and inorder = inorder and inv = avl 
214 
proof (standard, goal_cases) 

68431  215 
case 1 show ?case by (simp add: empty_def) 
68422  216 
next 
217 
case 2 thus ?case by(simp add: isin_set_inorder) 

218 
next 

219 
case 3 thus ?case by(simp add: inorder_insert) 

220 
next 

221 
case 4 thus ?case by(simp add: inorder_delete) 

222 
next 

68431  223 
case 5 thus ?case by (simp add: empty_def) 
68422  224 
next 
225 
case 6 thus ?case by (simp add: avl_insert(1)) 

226 
next 

227 
case 7 thus ?case by (simp add: avl_delete(1)) 

228 
qed 

229 

230 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

231 
subsection \<open>HeightSize Relation\<close> 
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

232 

71466  233 
text \<open>Any AVL tree of height \<open>n\<close> has at least \<open>fib (n+2)\<close> leaves:\<close> 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

234 

71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

235 
theorem avl_fib_bound: 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

236 
"avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

237 
proof (induction rule: tree2_induct) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

238 
case (Node l a h r) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

239 
have 1: "height l + 1 \<le> height r + 2" and 2: "height r + 1 \<le> height l + 2" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

240 
using Node.prems by auto 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

241 
have "fib (max (height l) (height r) + 3) \<le> size1 l + size1 r" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

242 
proof cases 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

243 
assume "height l \<ge> height r" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

244 
hence "fib (max (height l) (height r) + 3) = fib (height l + 3)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

245 
by(simp add: max_absorb1) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

246 
also have "\<dots> = fib (height l + 2) + fib (height l + 1)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

247 
by (simp add: numeral_eq_Suc) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

248 
also have "\<dots> \<le> size1 l + fib (height l + 1)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

249 
using Node by (simp) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

250 
also have "\<dots> \<le> size1 r + size1 l" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

251 
using Node fib_mono[OF 1] by auto 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

252 
also have "\<dots> = size1 (Node l (a,h) r)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

253 
by simp 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

254 
finally show ?thesis 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

255 
by (simp) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

256 
next 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

257 
assume "\<not> height l \<ge> height r" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

258 
hence "fib (max (height l) (height r) + 3) = fib (height r + 3)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

259 
by(simp add: max_absorb1) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

260 
also have "\<dots> = fib (height r + 2) + fib (height r + 1)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

261 
by (simp add: numeral_eq_Suc) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

262 
also have "\<dots> \<le> size1 r + fib (height r + 1)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

263 
using Node by (simp) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

264 
also have "\<dots> \<le> size1 r + size1 l" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

265 
using Node fib_mono[OF 2] by auto 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

266 
also have "\<dots> = size1 (Node l (a,h) r)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

267 
by simp 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

268 
finally show ?thesis 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

269 
by (simp) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

270 
qed 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

271 
also have "\<dots> = size1 (Node l (a,h) r)" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

272 
by simp 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

273 
finally show ?case by (simp del: fib.simps add: numeral_eq_Suc) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

274 
qed auto 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

275 

884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

276 
lemma avl_fib_bound_auto: "avl t \<Longrightarrow> fib (height t + 2) \<le> size1 t" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

277 
proof (induction t rule: tree2_induct) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

278 
case Leaf thus ?case by (simp) 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

279 
next 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

280 
case (Node l a h r) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

281 
have 1: "height l + 1 \<le> height r + 2" and 2: "height r + 1 \<le> height l + 2" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

282 
using Node.prems by auto 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

283 
have left: "height l \<ge> height r \<Longrightarrow> ?case" (is "?asm \<Longrightarrow> _") 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

284 
using Node fib_mono[OF 1] by (simp add: max.absorb1) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

285 
have right: "height l \<le> height r \<Longrightarrow> ?case" 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

286 
using Node fib_mono[OF 2] by (simp add: max.absorb2) 
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

287 
show ?case using left right using Node.prems by simp linarith 
68313  288 
qed 
289 

69597  290 
text \<open>An exponential lower bound for \<^const>\<open>fib\<close>:\<close> 
63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

291 

68313  292 
lemma fib_lowerbound: 
293 
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" 

71486  294 
shows "real (fib(n+2)) \<ge> \<phi> ^ n" 
295 
proof (induction n rule: fib.induct) 

296 
case 1 

297 
then show ?case by simp 

298 
next 

299 
case 2 

300 
then show ?case by (simp add: \<phi>_def real_le_lsqrt) 

301 
next 

72110
16fab31feadc
avoid failure of "isabelle build o skip_proofs";
wenzelm
parents:
71818
diff
changeset

302 
case (3 n) 
71486  303 
have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n" 
304 
by (simp add: field_simps power2_eq_square) 

305 
also have "\<dots> = (\<phi> + 1) * \<phi> ^ n" 

306 
by (simp_all add: \<phi>_def power2_eq_square field_simps) 

307 
also have "\<dots> = \<phi> ^ Suc n + \<phi> ^ n" 

68313  308 
by (simp add: field_simps) 
71486  309 
also have "\<dots> \<le> real (fib (Suc n + 2)) + real (fib (n + 2))" 
310 
by (intro add_mono "3.IH") 

311 
finally show ?case by simp 

68313  312 
qed 
313 

314 
text \<open>The size of an AVL tree is (at least) exponential in its height:\<close> 

315 

68342  316 
lemma avl_size_lowerbound: 
68313  317 
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" 
318 
assumes "avl t" 

68342  319 
shows "\<phi> ^ (height t) \<le> size1 t" 
68313  320 
proof  
71486  321 
have "\<phi> ^ height t \<le> fib (height t + 2)" 
322 
unfolding \<phi>_def by(rule fib_lowerbound) 

68342  323 
also have "\<dots> \<le> size1 t" 
71806
884c6c0bc99a
use abs(h l  h r) instead of 3 cases, tuned proofs
nipkow
parents:
71801
diff
changeset

324 
using avl_fib_bound[of t] assms by simp 
68313  325 
finally show ?thesis . 
326 
qed 

63411
e051eea34990
got rid of class cmp; added heightsize proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset

327 

69597  328 
text \<open>The height of an AVL tree is most \<^term>\<open>(1/log 2 \<phi>)\<close> \<open>\<approx> 1.44\<close> times worse 
329 
than \<^term>\<open>log 2 (size1 t)\<close>:\<close> 

68342  330 

331 
lemma avl_height_upperbound: 

332 
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" 

333 
assumes "avl t" 

334 
shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)" 

335 
proof  

336 
have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict) 

337 
hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power) 

338 
also have "\<dots> \<le> log \<phi> (size1 t)" 

70350  339 
using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> 
340 
by (simp add: le_log_of_power) 

68342  341 
also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)" 
342 
by(simp add: log_base_change[of 2 \<phi>]) 

343 
finally show ?thesis . 

344 
qed 

345 

61232  346 
end 