author | wenzelm |
Fri, 07 Aug 2020 11:46:14 +0200 | |
changeset 72110 | 16fab31feadc |
parent 71818 | 986d5abbe77c |
permissions | -rw-r--r-- |
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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
6 |
imports |
71795 | 7 |
AVL_Set_Code |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63411
diff
changeset
|
8 |
"HOL-Number_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 height-size 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 height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
231 |
subsection \<open>Height-Size Relation\<close> |
e051eea34990
got rid of class cmp; added height-size 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 height-size 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 height-size 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 height-size 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 height-size 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 |