author | wenzelm |
Sat, 26 Jun 2021 20:55:43 +0200 | |
changeset 73884 | 0a12ca4f3e8d |
parent 73526 | a3cc9fa1295d |
child 76063 | 24c9f56aa035 |
permissions | -rw-r--r-- |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
1 |
(* Author: Tobias Nipkow, Daniel Stüwe *) |
61784 | 2 |
|
62130 | 3 |
section \<open>1-2 Brother Tree Implementation of Sets\<close> |
61784 | 4 |
|
5 |
theory Brother12_Set |
|
6 |
imports |
|
7 |
Cmp |
|
67965 | 8 |
Set_Specs |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63411
diff
changeset
|
9 |
"HOL-Number_Theory.Fib" |
61784 | 10 |
begin |
11 |
||
12 |
subsection \<open>Data Type and Operations\<close> |
|
13 |
||
14 |
datatype 'a bro = |
|
15 |
N0 | |
|
16 |
N1 "'a bro" | |
|
17 |
N2 "'a bro" 'a "'a bro" | |
|
18 |
(* auxiliary constructors: *) |
|
19 |
L2 'a | |
|
20 |
N3 "'a bro" 'a "'a bro" 'a "'a bro" |
|
21 |
||
68431 | 22 |
definition empty :: "'a bro" where |
23 |
"empty = N0" |
|
24 |
||
61784 | 25 |
fun inorder :: "'a bro \<Rightarrow> 'a list" where |
26 |
"inorder N0 = []" | |
|
27 |
"inorder (N1 t) = inorder t" | |
|
28 |
"inorder (N2 l a r) = inorder l @ a # inorder r" | |
|
29 |
"inorder (L2 a) = [a]" | |
|
30 |
"inorder (N3 t1 a1 t2 a2 t3) = inorder t1 @ a1 # inorder t2 @ a2 # inorder t3" |
|
31 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
32 |
fun isin :: "'a bro \<Rightarrow> 'a::linorder \<Rightarrow> bool" where |
61784 | 33 |
"isin N0 x = False" | |
34 |
"isin (N1 t) x = isin t x" | |
|
35 |
"isin (N2 l a r) x = |
|
36 |
(case cmp x a of |
|
37 |
LT \<Rightarrow> isin l x | |
|
38 |
EQ \<Rightarrow> True | |
|
39 |
GT \<Rightarrow> isin r x)" |
|
40 |
||
41 |
fun n1 :: "'a bro \<Rightarrow> 'a bro" where |
|
42 |
"n1 (L2 a) = N2 N0 a N0" | |
|
43 |
"n1 (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | |
|
44 |
"n1 t = N1 t" |
|
45 |
||
46 |
hide_const (open) insert |
|
47 |
||
48 |
locale insert |
|
49 |
begin |
|
50 |
||
51 |
fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where |
|
52 |
"n2 (L2 a1) a2 t = N3 N0 a1 N0 a2 t" | |
|
53 |
"n2 (N3 t1 a1 t2 a2 t3) a3 (N1 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" | |
|
54 |
"n2 (N3 t1 a1 t2 a2 t3) a3 t4 = N3 (N2 t1 a1 t2) a2 (N1 t3) a3 t4" | |
|
55 |
"n2 t1 a1 (L2 a2) = N3 t1 a1 N0 a2 N0" | |
|
56 |
"n2 (N1 t1) a1 (N3 t2 a2 t3 a3 t4) = N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)" | |
|
57 |
"n2 t1 a1 (N3 t2 a2 t3 a3 t4) = N3 t1 a1 (N1 t2) a2 (N2 t3 a3 t4)" | |
|
58 |
"n2 t1 a t2 = N2 t1 a t2" |
|
59 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
60 |
fun ins :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where |
61789 | 61 |
"ins x N0 = L2 x" | |
62 |
"ins x (N1 t) = n1 (ins x t)" | |
|
63 |
"ins x (N2 l a r) = |
|
64 |
(case cmp x a of |
|
65 |
LT \<Rightarrow> n2 (ins x l) a r | |
|
66 |
EQ \<Rightarrow> N2 l a r | |
|
67 |
GT \<Rightarrow> n2 l a (ins x r))" |
|
61784 | 68 |
|
69 |
fun tree :: "'a bro \<Rightarrow> 'a bro" where |
|
70 |
"tree (L2 a) = N2 N0 a N0" | |
|
71 |
"tree (N3 t1 a1 t2 a2 t3) = N2 (N2 t1 a1 t2) a2 (N1 t3)" | |
|
72 |
"tree t = t" |
|
73 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
74 |
definition insert :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where |
61784 | 75 |
"insert x t = tree(ins x t)" |
76 |
||
77 |
end |
|
78 |
||
79 |
locale delete |
|
80 |
begin |
|
81 |
||
82 |
fun n2 :: "'a bro \<Rightarrow> 'a \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where |
|
83 |
"n2 (N1 t1) a1 (N1 t2) = N1 (N2 t1 a1 t2)" | |
|
84 |
"n2 (N1 (N1 t1)) a1 (N2 (N1 t2) a2 (N2 t3 a3 t4)) = |
|
85 |
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | |
|
86 |
"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N1 t4)) = |
|
87 |
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | |
|
88 |
"n2 (N1 (N1 t1)) a1 (N2 (N2 t2 a2 t3) a3 (N2 t4 a4 t5)) = |
|
89 |
N2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N2 t4 a4 t5))" | |
|
90 |
"n2 (N2 (N1 t1) a1 (N2 t2 a2 t3)) a3 (N1 (N1 t4)) = |
|
91 |
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | |
|
92 |
"n2 (N2 (N2 t1 a1 t2) a2 (N1 t3)) a3 (N1 (N1 t4)) = |
|
93 |
N1 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4))" | |
|
94 |
"n2 (N2 (N2 t1 a1 t2) a2 (N2 t3 a3 t4)) a5 (N1 (N1 t5)) = |
|
95 |
N2 (N1 (N2 t1 a1 t2)) a2 (N2 (N2 t3 a3 t4) a5 (N1 t5))" | |
|
96 |
"n2 t1 a1 t2 = N2 t1 a1 t2" |
|
97 |
||
68020 | 98 |
fun split_min :: "'a bro \<Rightarrow> ('a \<times> 'a bro) option" where |
99 |
"split_min N0 = None" | |
|
100 |
"split_min (N1 t) = |
|
101 |
(case split_min t of |
|
61784 | 102 |
None \<Rightarrow> None | |
103 |
Some (a, t') \<Rightarrow> Some (a, N1 t'))" | |
|
68020 | 104 |
"split_min (N2 t1 a t2) = |
105 |
(case split_min t1 of |
|
61784 | 106 |
None \<Rightarrow> Some (a, N1 t2) | |
107 |
Some (b, t1') \<Rightarrow> Some (b, n2 t1' a t2))" |
|
108 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
109 |
fun del :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where |
61784 | 110 |
"del _ N0 = N0" | |
111 |
"del x (N1 t) = N1 (del x t)" | |
|
112 |
"del x (N2 l a r) = |
|
113 |
(case cmp x a of |
|
114 |
LT \<Rightarrow> n2 (del x l) a r | |
|
115 |
GT \<Rightarrow> n2 l a (del x r) | |
|
68020 | 116 |
EQ \<Rightarrow> (case split_min r of |
61784 | 117 |
None \<Rightarrow> N1 l | |
118 |
Some (b, r') \<Rightarrow> n2 l b r'))" |
|
119 |
||
120 |
fun tree :: "'a bro \<Rightarrow> 'a bro" where |
|
121 |
"tree (N1 t) = t" | |
|
122 |
"tree t = t" |
|
123 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
124 |
definition delete :: "'a::linorder \<Rightarrow> 'a bro \<Rightarrow> 'a bro" where |
61784 | 125 |
"delete a t = tree (del a t)" |
126 |
||
127 |
end |
|
128 |
||
129 |
subsection \<open>Invariants\<close> |
|
130 |
||
131 |
fun B :: "nat \<Rightarrow> 'a bro set" |
|
132 |
and U :: "nat \<Rightarrow> 'a bro set" where |
|
133 |
"B 0 = {N0}" | |
|
134 |
"B (Suc h) = { N2 t1 a t2 | t1 a t2. |
|
135 |
t1 \<in> B h \<union> U h \<and> t2 \<in> B h \<or> t1 \<in> B h \<and> t2 \<in> B h \<union> U h}" | |
|
136 |
"U 0 = {}" | |
|
137 |
"U (Suc h) = N1 ` B h" |
|
138 |
||
139 |
abbreviation "T h \<equiv> B h \<union> U h" |
|
140 |
||
141 |
fun Bp :: "nat \<Rightarrow> 'a bro set" where |
|
142 |
"Bp 0 = B 0 \<union> L2 ` UNIV" | |
|
143 |
"Bp (Suc 0) = B (Suc 0) \<union> {N3 N0 a N0 b N0|a b. True}" | |
|
144 |
"Bp (Suc(Suc h)) = B (Suc(Suc h)) \<union> |
|
145 |
{N3 t1 a t2 b t3 | t1 a t2 b t3. t1 \<in> B (Suc h) \<and> t2 \<in> U (Suc h) \<and> t3 \<in> B (Suc h)}" |
|
146 |
||
147 |
fun Um :: "nat \<Rightarrow> 'a bro set" where |
|
148 |
"Um 0 = {}" | |
|
149 |
"Um (Suc h) = N1 ` T h" |
|
150 |
||
151 |
||
152 |
subsection "Functional Correctness Proofs" |
|
153 |
||
154 |
subsubsection "Proofs for isin" |
|
155 |
||
67929 | 156 |
lemma isin_set: |
157 |
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set(inorder t))" |
|
158 |
by(induction h arbitrary: t) (fastforce simp: isin_simps split: if_splits)+ |
|
61784 | 159 |
|
160 |
subsubsection "Proofs for insertion" |
|
161 |
||
162 |
lemma inorder_n1: "inorder(n1 t) = inorder t" |
|
62526 | 163 |
by(cases t rule: n1.cases) (auto simp: sorted_lems) |
61784 | 164 |
|
165 |
context insert |
|
166 |
begin |
|
167 |
||
168 |
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r" |
|
169 |
by(cases "(l,a,r)" rule: n2.cases) (auto simp: sorted_lems) |
|
170 |
||
171 |
lemma inorder_tree: "inorder(tree t) = inorder t" |
|
172 |
by(cases t) auto |
|
173 |
||
174 |
lemma inorder_ins: "t \<in> T h \<Longrightarrow> |
|
175 |
sorted(inorder t) \<Longrightarrow> inorder(ins a t) = ins_list a (inorder t)" |
|
176 |
by(induction h arbitrary: t) (auto simp: ins_list_simps inorder_n1 inorder_n2) |
|
177 |
||
178 |
lemma inorder_insert: "t \<in> T h \<Longrightarrow> |
|
179 |
sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)" |
|
180 |
by(simp add: insert_def inorder_ins inorder_tree) |
|
181 |
||
182 |
end |
|
183 |
||
184 |
subsubsection \<open>Proofs for deletion\<close> |
|
185 |
||
186 |
context delete |
|
187 |
begin |
|
188 |
||
189 |
lemma inorder_tree: "inorder(tree t) = inorder t" |
|
190 |
by(cases t) auto |
|
191 |
||
192 |
lemma inorder_n2: "inorder(n2 l a r) = inorder l @ a # inorder r" |
|
62526 | 193 |
by(cases "(l,a,r)" rule: n2.cases) (auto) |
61784 | 194 |
|
68020 | 195 |
lemma inorder_split_min: |
196 |
"t \<in> T h \<Longrightarrow> (split_min t = None \<longleftrightarrow> inorder t = []) \<and> |
|
197 |
(split_min t = Some(a,t') \<longrightarrow> inorder t = a # inorder t')" |
|
61784 | 198 |
by(induction h arbitrary: t a t') (auto simp: inorder_n2 split: option.splits) |
199 |
||
200 |
lemma inorder_del: |
|
61792 | 201 |
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)" |
73526
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
68431
diff
changeset
|
202 |
apply (induction h arbitrary: t) |
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
68431
diff
changeset
|
203 |
apply (auto simp: del_list_simps inorder_n2 split: option.splits) |
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
68431
diff
changeset
|
204 |
apply (auto simp: del_list_simps inorder_n2 |
68020 | 205 |
inorder_split_min[OF UnI1] inorder_split_min[OF UnI2] split: option.splits) |
73526
a3cc9fa1295d
new automatic order prover: stateless, complete, verified
nipkow
parents:
68431
diff
changeset
|
206 |
done |
61792 | 207 |
|
208 |
lemma inorder_delete: |
|
209 |
"t \<in> T h \<Longrightarrow> sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)" |
|
210 |
by(simp add: delete_def inorder_del inorder_tree) |
|
61784 | 211 |
|
212 |
end |
|
213 |
||
214 |
||
215 |
subsection \<open>Invariant Proofs\<close> |
|
216 |
||
61789 | 217 |
subsubsection \<open>Proofs for insertion\<close> |
61784 | 218 |
|
219 |
lemma n1_type: "t \<in> Bp h \<Longrightarrow> n1 t \<in> T (Suc h)" |
|
220 |
by(cases h rule: Bp.cases) auto |
|
221 |
||
222 |
context insert |
|
223 |
begin |
|
224 |
||
61809 | 225 |
lemma tree_type: "t \<in> Bp h \<Longrightarrow> tree t \<in> B h \<union> B (Suc h)" |
61784 | 226 |
by(cases h rule: Bp.cases) auto |
227 |
||
228 |
lemma n2_type: |
|
229 |
"(t1 \<in> Bp h \<and> t2 \<in> T h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h)) \<and> |
|
230 |
(t1 \<in> T h \<and> t2 \<in> Bp h \<longrightarrow> n2 t1 a t2 \<in> Bp (Suc h))" |
|
231 |
apply(cases h rule: Bp.cases) |
|
232 |
apply (auto)[2] |
|
233 |
apply(rule conjI impI | erule conjE exE imageE | simp | erule disjE)+ |
|
234 |
done |
|
235 |
||
236 |
lemma Bp_if_B: "t \<in> B h \<Longrightarrow> t \<in> Bp h" |
|
237 |
by (cases h rule: Bp.cases) simp_all |
|
238 |
||
67406 | 239 |
text\<open>An automatic proof:\<close> |
61784 | 240 |
|
241 |
lemma |
|
242 |
"(t \<in> B h \<longrightarrow> ins x t \<in> Bp h) \<and> (t \<in> U h \<longrightarrow> ins x t \<in> T h)" |
|
243 |
apply(induction h arbitrary: t) |
|
244 |
apply (simp) |
|
245 |
apply (fastforce simp: Bp_if_B n2_type dest: n1_type) |
|
246 |
done |
|
247 |
||
67406 | 248 |
text\<open>A detailed proof:\<close> |
61784 | 249 |
|
250 |
lemma ins_type: |
|
251 |
shows "t \<in> B h \<Longrightarrow> ins x t \<in> Bp h" and "t \<in> U h \<Longrightarrow> ins x t \<in> T h" |
|
252 |
proof(induction h arbitrary: t) |
|
253 |
case 0 |
|
254 |
{ case 1 thus ?case by simp |
|
255 |
next |
|
256 |
case 2 thus ?case by simp } |
|
257 |
next |
|
258 |
case (Suc h) |
|
259 |
{ case 1 |
|
260 |
then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and |
|
261 |
t1: "t1 \<in> T h" and t2: "t2 \<in> T h" and t12: "t1 \<in> B h \<or> t2 \<in> B h" |
|
262 |
by auto |
|
67040 | 263 |
have ?case if "x < a" |
264 |
proof - |
|
265 |
have "n2 (ins x t1) a t2 \<in> Bp (Suc h)" |
|
61784 | 266 |
proof cases |
267 |
assume "t1 \<in> B h" |
|
268 |
with t2 show ?thesis by (simp add: Suc.IH(1) n2_type) |
|
269 |
next |
|
270 |
assume "t1 \<notin> B h" |
|
271 |
hence 1: "t1 \<in> U h" and 2: "t2 \<in> B h" using t1 t12 by auto |
|
272 |
show ?thesis by (metis Suc.IH(2)[OF 1] Bp_if_B[OF 2] n2_type) |
|
273 |
qed |
|
67406 | 274 |
with \<open>x < a\<close> show ?case by simp |
67040 | 275 |
qed |
61784 | 276 |
moreover |
67040 | 277 |
have ?case if "a < x" |
278 |
proof - |
|
279 |
have "n2 t1 a (ins x t2) \<in> Bp (Suc h)" |
|
61784 | 280 |
proof cases |
281 |
assume "t2 \<in> B h" |
|
282 |
with t1 show ?thesis by (simp add: Suc.IH(1) n2_type) |
|
283 |
next |
|
284 |
assume "t2 \<notin> B h" |
|
285 |
hence 1: "t1 \<in> B h" and 2: "t2 \<in> U h" using t2 t12 by auto |
|
286 |
show ?thesis by (metis Bp_if_B[OF 1] Suc.IH(2)[OF 2] n2_type) |
|
287 |
qed |
|
67406 | 288 |
with \<open>a < x\<close> show ?case by simp |
67040 | 289 |
qed |
290 |
moreover |
|
291 |
have ?case if "x = a" |
|
292 |
proof - |
|
61784 | 293 |
from 1 have "t \<in> Bp (Suc h)" by(rule Bp_if_B) |
67406 | 294 |
thus "?case" using \<open>x = a\<close> by simp |
67040 | 295 |
qed |
61784 | 296 |
ultimately show ?case by auto |
297 |
next |
|
298 |
case 2 thus ?case using Suc(1) n1_type by fastforce } |
|
299 |
qed |
|
300 |
||
301 |
lemma insert_type: |
|
61809 | 302 |
"t \<in> B h \<Longrightarrow> insert x t \<in> B h \<union> B (Suc h)" |
303 |
unfolding insert_def by (metis ins_type(1) tree_type) |
|
61784 | 304 |
|
305 |
end |
|
306 |
||
61789 | 307 |
subsubsection "Proofs for deletion" |
61784 | 308 |
|
309 |
lemma B_simps[simp]: |
|
310 |
"N1 t \<in> B h = False" |
|
311 |
"L2 y \<in> B h = False" |
|
312 |
"(N3 t1 a1 t2 a2 t3) \<in> B h = False" |
|
313 |
"N0 \<in> B h \<longleftrightarrow> h = 0" |
|
314 |
by (cases h, auto)+ |
|
315 |
||
316 |
context delete |
|
317 |
begin |
|
318 |
||
319 |
lemma n2_type1: |
|
320 |
"\<lbrakk>t1 \<in> Um h; t2 \<in> B h\<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)" |
|
321 |
apply(cases h rule: Bp.cases) |
|
322 |
apply auto[2] |
|
323 |
apply(erule exE bexE conjE imageE | simp | erule disjE)+ |
|
324 |
done |
|
325 |
||
326 |
lemma n2_type2: |
|
327 |
"\<lbrakk>t1 \<in> B h ; t2 \<in> Um h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)" |
|
328 |
apply(cases h rule: Bp.cases) |
|
329 |
apply auto[2] |
|
330 |
apply(erule exE bexE conjE imageE | simp | erule disjE)+ |
|
331 |
done |
|
332 |
||
333 |
lemma n2_type3: |
|
334 |
"\<lbrakk>t1 \<in> T h ; t2 \<in> T h \<rbrakk> \<Longrightarrow> n2 t1 a t2 \<in> T (Suc h)" |
|
335 |
apply(cases h rule: Bp.cases) |
|
336 |
apply auto[2] |
|
337 |
apply(erule exE bexE conjE imageE | simp | erule disjE)+ |
|
338 |
done |
|
339 |
||
68020 | 340 |
lemma split_minNoneN0: "\<lbrakk>t \<in> B h; split_min t = None\<rbrakk> \<Longrightarrow> t = N0" |
61784 | 341 |
by (cases t) (auto split: option.splits) |
342 |
||
68020 | 343 |
lemma split_minNoneN1 : "\<lbrakk>t \<in> U h; split_min t = None\<rbrakk> \<Longrightarrow> t = N1 N0" |
344 |
by (cases h) (auto simp: split_minNoneN0 split: option.splits) |
|
61784 | 345 |
|
68020 | 346 |
lemma split_min_type: |
347 |
"t \<in> B h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> T h" |
|
348 |
"t \<in> U h \<Longrightarrow> split_min t = Some (a, t') \<Longrightarrow> t' \<in> Um h" |
|
61784 | 349 |
proof (induction h arbitrary: t a t') |
350 |
case (Suc h) |
|
351 |
{ case 1 |
|
352 |
then obtain t1 a t2 where [simp]: "t = N2 t1 a t2" and |
|
353 |
t12: "t1 \<in> T h" "t2 \<in> T h" "t1 \<in> B h \<or> t2 \<in> B h" |
|
354 |
by auto |
|
355 |
show ?case |
|
68020 | 356 |
proof (cases "split_min t1") |
61784 | 357 |
case None |
358 |
show ?thesis |
|
359 |
proof cases |
|
360 |
assume "t1 \<in> B h" |
|
68020 | 361 |
with split_minNoneN0[OF this None] 1 show ?thesis by(auto) |
61784 | 362 |
next |
363 |
assume "t1 \<notin> B h" |
|
364 |
thus ?thesis using 1 None by (auto) |
|
365 |
qed |
|
366 |
next |
|
367 |
case [simp]: (Some bt') |
|
368 |
obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce |
|
369 |
show ?thesis |
|
370 |
proof cases |
|
371 |
assume "t1 \<in> B h" |
|
372 |
from Suc.IH(1)[OF this] 1 have "t1' \<in> T h" by simp |
|
373 |
from n2_type3[OF this t12(2)] 1 show ?thesis by auto |
|
374 |
next |
|
375 |
assume "t1 \<notin> B h" |
|
376 |
hence t1: "t1 \<in> U h" and t2: "t2 \<in> B h" using t12 by auto |
|
377 |
from Suc.IH(2)[OF t1] have "t1' \<in> Um h" by simp |
|
378 |
from n2_type1[OF this t2] 1 show ?thesis by auto |
|
379 |
qed |
|
380 |
qed |
|
381 |
} |
|
382 |
{ case 2 |
|
383 |
then obtain t1 where [simp]: "t = N1 t1" and t1: "t1 \<in> B h" by auto |
|
384 |
show ?case |
|
68020 | 385 |
proof (cases "split_min t1") |
61784 | 386 |
case None |
68020 | 387 |
with split_minNoneN0[OF t1 None] 2 show ?thesis by(auto) |
61784 | 388 |
next |
389 |
case [simp]: (Some bt') |
|
390 |
obtain b t1' where [simp]: "bt' = (b,t1')" by fastforce |
|
391 |
from Suc.IH(1)[OF t1] have "t1' \<in> T h" by simp |
|
392 |
thus ?thesis using 2 by auto |
|
393 |
qed |
|
394 |
} |
|
395 |
qed auto |
|
396 |
||
397 |
lemma del_type: |
|
398 |
"t \<in> B h \<Longrightarrow> del x t \<in> T h" |
|
399 |
"t \<in> U h \<Longrightarrow> del x t \<in> Um h" |
|
400 |
proof (induction h arbitrary: x t) |
|
401 |
case (Suc h) |
|
402 |
{ case 1 |
|
403 |
then obtain l a r where [simp]: "t = N2 l a r" and |
|
404 |
lr: "l \<in> T h" "r \<in> T h" "l \<in> B h \<or> r \<in> B h" by auto |
|
67040 | 405 |
have ?case if "x < a" |
406 |
proof cases |
|
407 |
assume "l \<in> B h" |
|
408 |
from n2_type3[OF Suc.IH(1)[OF this] lr(2)] |
|
67406 | 409 |
show ?thesis using \<open>x<a\<close> by(simp) |
67040 | 410 |
next |
411 |
assume "l \<notin> B h" |
|
412 |
hence "l \<in> U h" "r \<in> B h" using lr by auto |
|
413 |
from n2_type1[OF Suc.IH(2)[OF this(1)] this(2)] |
|
67406 | 414 |
show ?thesis using \<open>x<a\<close> by(simp) |
67040 | 415 |
qed |
416 |
moreover |
|
417 |
have ?case if "x > a" |
|
418 |
proof cases |
|
419 |
assume "r \<in> B h" |
|
420 |
from n2_type3[OF lr(1) Suc.IH(1)[OF this]] |
|
67406 | 421 |
show ?thesis using \<open>x>a\<close> by(simp) |
67040 | 422 |
next |
423 |
assume "r \<notin> B h" |
|
424 |
hence "l \<in> B h" "r \<in> U h" using lr by auto |
|
425 |
from n2_type2[OF this(1) Suc.IH(2)[OF this(2)]] |
|
67406 | 426 |
show ?thesis using \<open>x>a\<close> by(simp) |
67040 | 427 |
qed |
428 |
moreover |
|
429 |
have ?case if [simp]: "x=a" |
|
68020 | 430 |
proof (cases "split_min r") |
67040 | 431 |
case None |
432 |
show ?thesis |
|
61784 | 433 |
proof cases |
434 |
assume "r \<in> B h" |
|
68020 | 435 |
with split_minNoneN0[OF this None] lr show ?thesis by(simp) |
61784 | 436 |
next |
437 |
assume "r \<notin> B h" |
|
67040 | 438 |
hence "r \<in> U h" using lr by auto |
68020 | 439 |
with split_minNoneN1[OF this None] lr(3) show ?thesis by (simp) |
61784 | 440 |
qed |
67040 | 441 |
next |
442 |
case [simp]: (Some br') |
|
443 |
obtain b r' where [simp]: "br' = (b,r')" by fastforce |
|
444 |
show ?thesis |
|
445 |
proof cases |
|
446 |
assume "r \<in> B h" |
|
68020 | 447 |
from split_min_type(1)[OF this] n2_type3[OF lr(1)] |
67040 | 448 |
show ?thesis by simp |
61784 | 449 |
next |
67040 | 450 |
assume "r \<notin> B h" |
451 |
hence "l \<in> B h" and "r \<in> U h" using lr by auto |
|
68020 | 452 |
from split_min_type(2)[OF this(2)] n2_type2[OF this(1)] |
67040 | 453 |
show ?thesis by simp |
61784 | 454 |
qed |
67040 | 455 |
qed |
456 |
ultimately show ?case by auto |
|
61784 | 457 |
} |
458 |
{ case 2 with Suc.IH(1) show ?case by auto } |
|
459 |
qed auto |
|
460 |
||
67613 | 461 |
lemma tree_type: "t \<in> T (h+1) \<Longrightarrow> tree t \<in> B (h+1) \<union> B h" |
61784 | 462 |
by(auto) |
463 |
||
61809 | 464 |
lemma delete_type: "t \<in> B h \<Longrightarrow> delete x t \<in> B h \<union> B(h-1)" |
61784 | 465 |
unfolding delete_def |
61809 | 466 |
by (cases h) (simp, metis del_type(1) tree_type Suc_eq_plus1 diff_Suc_1) |
61784 | 467 |
|
468 |
end |
|
469 |
||
61789 | 470 |
|
61784 | 471 |
subsection "Overall correctness" |
472 |
||
473 |
interpretation Set_by_Ordered |
|
68431 | 474 |
where empty = empty and isin = isin and insert = insert.insert |
61809 | 475 |
and delete = delete.delete and inorder = inorder and inv = "\<lambda>t. \<exists>h. t \<in> B h" |
61784 | 476 |
proof (standard, goal_cases) |
477 |
case 2 thus ?case by(auto intro!: isin_set) |
|
478 |
next |
|
479 |
case 3 thus ?case by(auto intro!: insert.inorder_insert) |
|
480 |
next |
|
61792 | 481 |
case 4 thus ?case by(auto intro!: delete.inorder_delete) |
61784 | 482 |
next |
483 |
case 6 thus ?case using insert.insert_type by blast |
|
484 |
next |
|
485 |
case 7 thus ?case using delete.delete_type by blast |
|
68431 | 486 |
qed (auto simp: empty_def) |
61784 | 487 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
488 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
489 |
subsection \<open>Height-Size Relation\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
490 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
491 |
text \<open>By Daniel St\"uwe\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
492 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
493 |
fun fib_tree :: "nat \<Rightarrow> unit bro" where |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
494 |
"fib_tree 0 = N0" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
495 |
| "fib_tree (Suc 0) = N2 N0 () N0" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
496 |
| "fib_tree (Suc(Suc h)) = N2 (fib_tree (h+1)) () (N1 (fib_tree h))" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
497 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
498 |
fun fib' :: "nat \<Rightarrow> nat" where |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
499 |
"fib' 0 = 0" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
500 |
| "fib' (Suc 0) = 1" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
501 |
| "fib' (Suc(Suc h)) = 1 + fib' (Suc h) + fib' h" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
502 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
503 |
fun size :: "'a bro \<Rightarrow> nat" where |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
504 |
"size N0 = 0" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
505 |
| "size (N1 t) = size t" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
506 |
| "size (N2 t1 _ t2) = 1 + size t1 + size t2" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
507 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
508 |
lemma fib_tree_B: "fib_tree h \<in> B h" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
509 |
by (induction h rule: fib_tree.induct) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
510 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
511 |
declare [[names_short]] |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
512 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
513 |
lemma size_fib': "size (fib_tree h) = fib' h" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
514 |
by (induction h rule: fib_tree.induct) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
515 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
516 |
lemma fibfib: "fib' h + 1 = fib (Suc(Suc h))" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
517 |
by (induction h rule: fib_tree.induct) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
518 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
519 |
lemma B_N2_cases[consumes 1]: |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
520 |
assumes "N2 t1 a t2 \<in> B (Suc n)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
521 |
obtains |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
522 |
(BB) "t1 \<in> B n" and "t2 \<in> B n" | |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
523 |
(UB) "t1 \<in> U n" and "t2 \<in> B n" | |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
524 |
(BU) "t1 \<in> B n" and "t2 \<in> U n" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
525 |
using assms by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
526 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
527 |
lemma size_bounded: "t \<in> B h \<Longrightarrow> size t \<ge> size (fib_tree h)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
528 |
unfolding size_fib' proof (induction h arbitrary: t rule: fib'.induct) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
529 |
case (3 h t') |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
530 |
note main = 3 |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
531 |
then obtain t1 a t2 where t': "t' = N2 t1 a t2" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
532 |
with main have "N2 t1 a t2 \<in> B (Suc (Suc h))" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
533 |
thus ?case proof (cases rule: B_N2_cases) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
534 |
case BB |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
535 |
then obtain x y z where t2: "t2 = N2 x y z \<or> t2 = N2 z y x" "x \<in> B h" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
536 |
show ?thesis unfolding t' using main(1)[OF BB(1)] main(2)[OF t2(2)] t2(1) by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
537 |
next |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
538 |
case UB |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
539 |
then obtain t11 where t1: "t1 = N1 t11" "t11 \<in> B h" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
540 |
show ?thesis unfolding t' t1(1) using main(2)[OF t1(2)] main(1)[OF UB(2)] by simp |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
541 |
next |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
542 |
case BU |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
543 |
then obtain t22 where t2: "t2 = N1 t22" "t22 \<in> B h" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
544 |
show ?thesis unfolding t' t2(1) using main(2)[OF t2(2)] main(1)[OF BU(1)] by simp |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
545 |
qed |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
546 |
qed auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
547 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
548 |
theorem "t \<in> B h \<Longrightarrow> fib (h + 2) \<le> size t + 1" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
549 |
using size_bounded |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
550 |
by (simp add: size_fib' fibfib[symmetric] del: fib.simps) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
551 |
|
61784 | 552 |
end |