author | blanchet |
Fri, 06 Nov 2020 12:48:31 +0100 | |
changeset 72550 | 1d0ae7e578a0 |
parent 71846 | 1a884605a08b |
child 78653 | 7ed1759fe1bd |
permissions | -rw-r--r-- |
69232 | 1 |
(* Author: Tobias Nipkow, with contributions by Thomas Sewell *) |
2 |
||
69145 | 3 |
section "Arrays via Braun Trees" |
4 |
||
5 |
theory Array_Braun |
|
6 |
imports |
|
7 |
Array_Specs |
|
8 |
Braun_Tree |
|
9 |
begin |
|
10 |
||
11 |
subsection "Array" |
|
12 |
||
13 |
fun lookup1 :: "'a tree \<Rightarrow> nat \<Rightarrow> 'a" where |
|
14 |
"lookup1 (Node l x r) n = (if n=1 then x else lookup1 (if even n then l else r) (n div 2))" |
|
15 |
||
16 |
fun update1 :: "nat \<Rightarrow> 'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
17 |
"update1 n x Leaf = Node Leaf x Leaf" | |
|
18 |
"update1 n x (Node l a r) = |
|
19 |
(if n=1 then Node l x r else |
|
20 |
if even n then Node (update1 (n div 2) x l) a r |
|
21 |
else Node l a (update1 (n div 2) x r))" |
|
22 |
||
23 |
fun adds :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
24 |
"adds [] n t = t" | |
|
25 |
"adds (x#xs) n t = adds xs (n+1) (update1 (n+1) x t)" |
|
26 |
||
27 |
fun list :: "'a tree \<Rightarrow> 'a list" where |
|
28 |
"list Leaf = []" | |
|
29 |
"list (Node l x r) = x # splice (list l) (list r)" |
|
30 |
||
31 |
||
32 |
subsubsection "Functional Correctness" |
|
33 |
||
34 |
lemma size_list: "size(list t) = size t" |
|
35 |
by(induction t)(auto) |
|
36 |
||
37 |
lemma minus1_div2: "(n - Suc 0) div 2 = (if odd n then n div 2 else n div 2 - 1)" |
|
38 |
by auto arith |
|
39 |
||
40 |
lemma nth_splice: "\<lbrakk> n < size xs + size ys; size ys \<le> size xs; size xs \<le> size ys + 1 \<rbrakk> |
|
41 |
\<Longrightarrow> splice xs ys ! n = (if even n then xs else ys) ! (n div 2)" |
|
42 |
apply(induction xs ys arbitrary: n rule: splice.induct) |
|
43 |
apply (auto simp: nth_Cons' minus1_div2) |
|
44 |
done |
|
45 |
||
46 |
lemma div2_in_bounds: |
|
47 |
"\<lbrakk> braun (Node l x r); n \<in> {1..size(Node l x r)}; n > 1 \<rbrakk> \<Longrightarrow> |
|
48 |
(odd n \<longrightarrow> n div 2 \<in> {1..size r}) \<and> (even n \<longrightarrow> n div 2 \<in> {1..size l})" |
|
49 |
by auto arith |
|
50 |
||
51 |
declare upt_Suc[simp del] |
|
52 |
||
53 |
||
69597 | 54 |
paragraph \<open>\<^const>\<open>lookup1\<close>\<close> |
69145 | 55 |
|
56 |
lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)" |
|
57 |
proof(induction t arbitrary: i) |
|
58 |
case Leaf thus ?case by simp |
|
59 |
next |
|
60 |
case Node |
|
61 |
thus ?case using div2_in_bounds[OF Node.prems(1), of "i+1"] |
|
62 |
by (auto simp: nth_splice minus1_div2 size_list) |
|
63 |
qed |
|
64 |
||
65 |
lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]" |
|
66 |
by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1) |
|
67 |
||
68 |
||
69597 | 69 |
paragraph \<open>\<^const>\<open>update1\<close>\<close> |
69145 | 70 |
|
71 |
lemma size_update1: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t" |
|
72 |
proof(induction t arbitrary: n) |
|
73 |
case Leaf thus ?case by simp |
|
74 |
next |
|
75 |
case Node thus ?case using div2_in_bounds[OF Node.prems] by simp |
|
76 |
qed |
|
77 |
||
78 |
lemma braun_update1: "\<lbrakk>braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> braun(update1 n x t)" |
|
79 |
proof(induction t arbitrary: n) |
|
80 |
case Leaf thus ?case by simp |
|
81 |
next |
|
82 |
case Node thus ?case |
|
83 |
using div2_in_bounds[OF Node.prems] by (simp add: size_update1) |
|
84 |
qed |
|
85 |
||
86 |
lemma lookup1_update1: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> |
|
87 |
lookup1 (update1 n x t) m = (if n=m then x else lookup1 t m)" |
|
88 |
proof(induction t arbitrary: m n) |
|
89 |
case Leaf |
|
90 |
then show ?case by simp |
|
91 |
next |
|
92 |
have aux: "\<lbrakk> odd n; odd m \<rbrakk> \<Longrightarrow> n div 2 = (m::nat) div 2 \<longleftrightarrow> m=n" for m n |
|
93 |
using odd_two_times_div_two_succ by fastforce |
|
94 |
case Node |
|
95 |
thus ?case using div2_in_bounds[OF Node.prems] by (auto simp: aux) |
|
96 |
qed |
|
97 |
||
98 |
lemma list_update1: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]" |
|
99 |
by(auto simp add: list_eq_map_lookup1 list_eq_iff_nth_eq lookup1_update1 size_update1 braun_update1) |
|
100 |
||
101 |
text \<open>A second proof of @{thm list_update1}:\<close> |
|
102 |
||
103 |
lemma diff1_eq_iff: "n > 0 \<Longrightarrow> n - Suc 0 = m \<longleftrightarrow> n = m+1" |
|
104 |
by arith |
|
105 |
||
106 |
lemma list_update_splice: |
|
107 |
"\<lbrakk> n < size xs + size ys; size ys \<le> size xs; size xs \<le> size ys + 1 \<rbrakk> \<Longrightarrow> |
|
108 |
(splice xs ys) [n := x] = |
|
109 |
(if even n then splice (xs[n div 2 := x]) ys else splice xs (ys[n div 2 := x]))" |
|
110 |
by(induction xs ys arbitrary: n rule: splice.induct) (auto split: nat.split) |
|
111 |
||
112 |
lemma list_update2: "\<lbrakk> braun t; n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> list(update1 n x t) = (list t)[n-1 := x]" |
|
113 |
proof(induction t arbitrary: n) |
|
114 |
case Leaf thus ?case by simp |
|
115 |
next |
|
116 |
case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems] |
|
117 |
by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split) |
|
118 |
qed |
|
119 |
||
120 |
||
69597 | 121 |
paragraph \<open>\<^const>\<open>adds\<close>\<close> |
69145 | 122 |
|
123 |
lemma splice_last: shows |
|
124 |
"size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]" |
|
125 |
and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]" |
|
126 |
by(induction xs ys arbitrary: x y rule: splice.induct) (auto) |
|
127 |
||
128 |
lemma list_add_hi: "braun t \<Longrightarrow> list(update1 (Suc(size t)) x t) = list t @ [x]" |
|
129 |
by(induction t)(auto simp: splice_last size_list) |
|
130 |
||
131 |
lemma size_add_hi: "braun t \<Longrightarrow> m = size t \<Longrightarrow> size(update1 (Suc m) x t) = size t + 1" |
|
132 |
by(induction t arbitrary: m)(auto) |
|
133 |
||
134 |
lemma braun_add_hi: "braun t \<Longrightarrow> braun(update1 (Suc(size t)) x t)" |
|
135 |
by(induction t)(auto simp: size_add_hi) |
|
136 |
||
137 |
lemma size_braun_adds: |
|
138 |
"\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> size(adds xs n t) = size t + length xs \<and> braun (adds xs n t)" |
|
139 |
by(induction xs arbitrary: t n)(auto simp: braun_add_hi size_add_hi) |
|
140 |
||
141 |
lemma list_adds: "\<lbrakk> braun t; size t = n \<rbrakk> \<Longrightarrow> list(adds xs n t) = list t @ xs" |
|
142 |
by(induction xs arbitrary: t n)(auto simp: size_braun_adds list_add_hi size_add_hi braun_add_hi) |
|
143 |
||
144 |
||
145 |
subsubsection "Array Implementation" |
|
146 |
||
147 |
interpretation A: Array |
|
148 |
where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)" |
|
149 |
and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)" |
|
150 |
and len = "\<lambda>(t,l). l" |
|
151 |
and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)" |
|
152 |
and invar = "\<lambda>(t,l). braun t \<and> l = size t" |
|
153 |
and list = "\<lambda>(t,l). list t" |
|
154 |
proof (standard, goal_cases) |
|
155 |
case 1 thus ?case by (simp add: nth_list_lookup1 split: prod.splits) |
|
156 |
next |
|
157 |
case 2 thus ?case by (simp add: list_update1 split: prod.splits) |
|
158 |
next |
|
159 |
case 3 thus ?case by (simp add: size_list split: prod.splits) |
|
160 |
next |
|
161 |
case 4 thus ?case by (simp add: list_adds) |
|
162 |
next |
|
163 |
case 5 thus ?case by (simp add: braun_update1 size_update1 split: prod.splits) |
|
164 |
next |
|
165 |
case 6 thus ?case by (simp add: size_braun_adds split: prod.splits) |
|
166 |
qed |
|
167 |
||
168 |
||
169 |
subsection "Flexible Array" |
|
170 |
||
171 |
fun add_lo where |
|
172 |
"add_lo x Leaf = Node Leaf x Leaf" | |
|
173 |
"add_lo x (Node l a r) = Node (add_lo a r) x l" |
|
174 |
||
175 |
fun merge where |
|
176 |
"merge Leaf r = r" | |
|
177 |
"merge (Node l a r) rr = Node rr a (merge l r)" |
|
178 |
||
179 |
fun del_lo where |
|
180 |
"del_lo Leaf = Leaf" | |
|
181 |
"del_lo (Node l a r) = merge l r" |
|
182 |
||
183 |
fun del_hi :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
184 |
"del_hi n Leaf = Leaf" | |
|
185 |
"del_hi n (Node l x r) = |
|
69752 | 186 |
(if n = 1 then Leaf |
187 |
else if even n |
|
188 |
then Node (del_hi (n div 2) l) x r |
|
189 |
else Node l x (del_hi (n div 2) r))" |
|
69145 | 190 |
|
191 |
||
192 |
subsubsection "Functional Correctness" |
|
193 |
||
194 |
||
69597 | 195 |
paragraph \<open>\<^const>\<open>add_lo\<close>\<close> |
69145 | 196 |
|
197 |
lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t" |
|
198 |
by(induction t arbitrary: a) auto |
|
199 |
||
200 |
lemma braun_add_lo: "braun t \<Longrightarrow> braun(add_lo x t)" |
|
201 |
by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list) |
|
202 |
||
203 |
||
69597 | 204 |
paragraph \<open>\<^const>\<open>del_lo\<close>\<close> |
69145 | 205 |
|
206 |
lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)" |
|
207 |
by (induction l r rule: merge.induct) auto |
|
208 |
||
209 |
lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)" |
|
210 |
by (induction l r rule: merge.induct)(auto simp add: list_merge simp flip: size_list) |
|
211 |
||
212 |
lemma list_del_lo: "braun t \<Longrightarrow> list(del_lo t) = tl (list t)" |
|
213 |
by (cases t) (simp_all add: list_merge) |
|
214 |
||
215 |
lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)" |
|
216 |
by (cases t) (simp_all add: braun_merge) |
|
217 |
||
218 |
||
69597 | 219 |
paragraph \<open>\<^const>\<open>del_hi\<close>\<close> |
69145 | 220 |
|
221 |
lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf" |
|
222 |
by(cases t) simp_all |
|
223 |
||
224 |
lemma butlast_splice: "butlast (splice xs ys) = |
|
225 |
(if size xs > size ys then splice (butlast xs) ys else splice xs (butlast ys))" |
|
226 |
by(induction xs ys rule: splice.induct) (auto) |
|
227 |
||
228 |
lemma list_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> list(del_hi st t) = butlast(list t)" |
|
229 |
apply(induction t arbitrary: st) |
|
230 |
by(auto simp: list_Nil_iff size_list butlast_splice) |
|
231 |
||
232 |
lemma braun_del_hi: "braun t \<Longrightarrow> size t = st \<Longrightarrow> braun(del_hi st t)" |
|
233 |
apply(induction t arbitrary: st) |
|
234 |
by(auto simp: list_del_hi simp flip: size_list) |
|
235 |
||
236 |
||
237 |
subsubsection "Flexible Array Implementation" |
|
238 |
||
239 |
interpretation AF: Array_Flex |
|
240 |
where lookup = "\<lambda>(t,l) n. lookup1 t (n+1)" |
|
241 |
and update = "\<lambda>n x (t,l). (update1 (n+1) x t, l)" |
|
242 |
and len = "\<lambda>(t,l). l" |
|
243 |
and array = "\<lambda>xs. (adds xs 0 Leaf, length xs)" |
|
244 |
and invar = "\<lambda>(t,l). braun t \<and> l = size t" |
|
245 |
and list = "\<lambda>(t,l). list t" |
|
246 |
and add_lo = "\<lambda>x (t,l). (add_lo x t, l+1)" |
|
247 |
and del_lo = "\<lambda>(t,l). (del_lo t, l-1)" |
|
248 |
and add_hi = "\<lambda>x (t,l). (update1 (Suc l) x t, l+1)" |
|
249 |
and del_hi = "\<lambda>(t,l). (del_hi l t, l-1)" |
|
250 |
proof (standard, goal_cases) |
|
251 |
case 1 thus ?case by (simp add: list_add_lo split: prod.splits) |
|
252 |
next |
|
253 |
case 2 thus ?case by (simp add: list_del_lo split: prod.splits) |
|
254 |
next |
|
255 |
case 3 thus ?case by (simp add: list_add_hi braun_add_hi split: prod.splits) |
|
256 |
next |
|
257 |
case 4 thus ?case by (simp add: list_del_hi split: prod.splits) |
|
258 |
next |
|
259 |
case 5 thus ?case by (simp add: braun_add_lo list_add_lo flip: size_list split: prod.splits) |
|
260 |
next |
|
261 |
case 6 thus ?case by (simp add: braun_del_lo list_del_lo flip: size_list split: prod.splits) |
|
262 |
next |
|
263 |
case 7 thus ?case by (simp add: size_add_hi braun_add_hi split: prod.splits) |
|
264 |
next |
|
265 |
case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits) |
|
266 |
qed |
|
267 |
||
268 |
||
269 |
subsection "Faster" |
|
270 |
||
69232 | 271 |
|
69941 | 272 |
subsubsection \<open>Size\<close> |
273 |
||
274 |
fun diff :: "'a tree \<Rightarrow> nat \<Rightarrow> nat" where |
|
71345 | 275 |
"diff Leaf _ = 0" | |
69941 | 276 |
"diff (Node l x r) n = (if n=0 then 1 else if even n then diff r (n div 2 - 1) else diff l (n div 2))" |
277 |
||
278 |
fun size_fast :: "'a tree \<Rightarrow> nat" where |
|
279 |
"size_fast Leaf = 0" | |
|
280 |
"size_fast (Node l x r) = (let n = size_fast r in 1 + 2*n + diff l n)" |
|
281 |
||
71846 | 282 |
declare Let_def[simp] |
283 |
||
69943 | 284 |
lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n" |
69941 | 285 |
by(induction t arbitrary: n) auto |
286 |
||
287 |
lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t" |
|
71846 | 288 |
by(induction t) (auto simp add: diff) |
69941 | 289 |
|
290 |
||
69232 | 291 |
subsubsection \<open>Initialization with 1 element\<close> |
292 |
||
69206 | 293 |
fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where |
294 |
"braun_of_naive x n = (if n=0 then Leaf |
|
69145 | 295 |
else let m = (n-1) div 2 |
69206 | 296 |
in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m) |
297 |
else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))" |
|
69145 | 298 |
|
299 |
fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where |
|
300 |
"braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf) |
|
301 |
else let (s,t) = braun2_of x ((n-1) div 2) |
|
302 |
in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))" |
|
303 |
||
304 |
definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where |
|
305 |
"braun_of x n = fst (braun2_of x n)" |
|
306 |
||
307 |
declare braun2_of.simps [simp del] |
|
308 |
||
309 |
lemma braun2_of_size_braun: "braun2_of x n = (s,t) \<Longrightarrow> size s = n \<and> size t = n+1 \<and> braun s \<and> braun t" |
|
310 |
proof(induction x n arbitrary: s t rule: braun2_of.induct) |
|
311 |
case (1 x n) |
|
312 |
then show ?case |
|
313 |
by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+ |
|
314 |
qed |
|
315 |
||
316 |
lemma braun2_of_replicate: |
|
317 |
"braun2_of x n = (s,t) \<Longrightarrow> list s = replicate n x \<and> list t = replicate (n+1) x" |
|
318 |
proof(induction x n arbitrary: s t rule: braun2_of.induct) |
|
319 |
case (1 x n) |
|
320 |
have "x # replicate m x = replicate (m+1) x" for m by simp |
|
321 |
with 1 show ?case |
|
322 |
apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x] |
|
323 |
simp del: replicate.simps(2) split: prod.splits if_splits) |
|
324 |
by presburger+ |
|
325 |
qed |
|
326 |
||
327 |
corollary braun_braun_of: "braun(braun_of x n)" |
|
328 |
unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun) |
|
329 |
||
330 |
corollary list_braun_of: "list(braun_of x n) = replicate n x" |
|
331 |
unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate) |
|
332 |
||
69232 | 333 |
|
334 |
subsubsection "Proof Infrastructure" |
|
335 |
||
336 |
text \<open>Originally due to Thomas Sewell.\<close> |
|
337 |
||
338 |
paragraph \<open>\<open>take_nths\<close>\<close> |
|
339 |
||
340 |
fun take_nths :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where |
|
341 |
"take_nths i k [] = []" | |
|
342 |
"take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs |
|
343 |
else take_nths (i - 1) k xs)" |
|
344 |
||
71399 | 345 |
text \<open>This is the more concise definition but seems to complicate the proofs:\<close> |
346 |
||
347 |
lemma take_nths_eq_nths: "take_nths i k xs = nths xs (\<Union>n. {n*2^k + i})" |
|
348 |
proof(induction xs arbitrary: i) |
|
349 |
case Nil |
|
350 |
then show ?case by simp |
|
351 |
next |
|
352 |
case (Cons x xs) |
|
353 |
show ?case |
|
354 |
proof cases |
|
355 |
assume [simp]: "i = 0" |
|
356 |
have "(\<Union>n. {(n+1) * 2 ^ k - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k}" |
|
357 |
apply (auto simp del: mult_Suc) |
|
358 |
by (metis diff_Suc_Suc diff_zero mult_eq_0_iff not0_implies_Suc) |
|
359 |
thus ?thesis by (simp add: Cons.IH ac_simps nths_Cons) |
|
360 |
next |
|
361 |
assume [arith]: "i \<noteq> 0" |
|
362 |
have "(\<Union>n. {n * 2 ^ k + i - 1}) = {m. \<exists>n. Suc m = n * 2 ^ k + i}" |
|
363 |
apply auto |
|
364 |
by (metis diff_Suc_Suc diff_zero) |
|
365 |
thus ?thesis by (simp add: Cons.IH nths_Cons) |
|
366 |
qed |
|
367 |
qed |
|
368 |
||
69232 | 369 |
lemma take_nths_drop: |
370 |
"take_nths i k (drop j xs) = take_nths (i + j) k xs" |
|
371 |
by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split) |
|
372 |
||
373 |
lemma take_nths_00: |
|
374 |
"take_nths 0 0 xs = xs" |
|
375 |
by (induct xs; simp) |
|
376 |
||
377 |
lemma splice_take_nths: |
|
378 |
"splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs" |
|
379 |
by (induct xs; simp) |
|
380 |
||
381 |
lemma take_nths_take_nths: |
|
382 |
"take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs" |
|
383 |
by (induct xs arbitrary: i j; simp add: algebra_simps power_add) |
|
384 |
||
385 |
lemma take_nths_empty: |
|
386 |
"(take_nths i k xs = []) = (length xs \<le> i)" |
|
387 |
by (induction xs arbitrary: i k) auto |
|
388 |
||
389 |
lemma hd_take_nths: |
|
390 |
"i < length xs \<Longrightarrow> hd(take_nths i k xs) = xs ! i" |
|
391 |
by (induction xs arbitrary: i k) auto |
|
392 |
||
393 |
lemma take_nths_01_splice: |
|
394 |
"\<lbrakk> length xs = length ys \<or> length xs = length ys + 1 \<rbrakk> \<Longrightarrow> |
|
395 |
take_nths 0 (Suc 0) (splice xs ys) = xs \<and> |
|
396 |
take_nths (Suc 0) (Suc 0) (splice xs ys) = ys" |
|
397 |
by (induct xs arbitrary: ys; case_tac ys; simp) |
|
398 |
||
399 |
lemma length_take_nths_00: |
|
400 |
"length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \<or> |
|
401 |
length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1" |
|
402 |
by (induct xs) auto |
|
403 |
||
404 |
||
405 |
paragraph \<open>\<open>braun_list\<close>\<close> |
|
406 |
||
407 |
fun braun_list :: "'a tree \<Rightarrow> 'a list \<Rightarrow> bool" where |
|
408 |
"braun_list Leaf xs = (xs = [])" | |
|
409 |
"braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and> |
|
410 |
braun_list l (take_nths 1 1 xs) \<and> |
|
411 |
braun_list r (take_nths 2 1 xs))" |
|
412 |
||
413 |
lemma braun_list_eq: |
|
414 |
"braun_list t xs = (braun t \<and> xs = list t)" |
|
415 |
proof (induct t arbitrary: xs) |
|
416 |
case Leaf |
|
417 |
show ?case by simp |
|
418 |
next |
|
419 |
case Node |
|
420 |
show ?case |
|
421 |
using length_take_nths_00[of xs] splice_take_nths[of xs] |
|
422 |
by (auto simp: neq_Nil_conv Node.hyps size_list[symmetric] take_nths_01_splice) |
|
423 |
qed |
|
424 |
||
425 |
||
426 |
subsubsection \<open>Converting a list of elements into a Braun tree\<close> |
|
427 |
||
428 |
fun nodes :: "'a tree list \<Rightarrow> 'a list \<Rightarrow> 'a tree list \<Rightarrow> 'a tree list" where |
|
429 |
"nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" | |
|
430 |
"nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" | |
|
431 |
"nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" | |
|
432 |
"nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" | |
|
433 |
"nodes ls [] rs = []" |
|
434 |
||
435 |
fun brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree list" where |
|
436 |
"brauns k xs = (if xs = [] then [] else |
|
437 |
let ys = take (2^k) xs; |
|
438 |
zs = drop (2^k) xs; |
|
439 |
ts = brauns (k+1) zs |
|
440 |
in nodes ts ys (drop (2^k) ts))" |
|
441 |
||
442 |
declare brauns.simps[simp del] |
|
443 |
||
444 |
definition brauns1 :: "'a list \<Rightarrow> 'a tree" where |
|
445 |
"brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)" |
|
446 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
447 |
fun T_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
448 |
"T_brauns k xs = (if xs = [] then 0 else |
69232 | 449 |
let ys = take (2^k) xs; |
450 |
zs = drop (2^k) xs; |
|
451 |
ts = brauns (k+1) zs |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
452 |
in 4 * min (2^k) (length xs) + T_brauns (k+1) zs)" |
69232 | 453 |
|
454 |
||
455 |
paragraph "Functional correctness" |
|
456 |
||
457 |
text \<open>The proof is originally due to Thomas Sewell.\<close> |
|
458 |
||
459 |
lemma length_nodes: |
|
460 |
"length (nodes ls xs rs) = length xs" |
|
461 |
by (induct ls xs rs rule: nodes.induct; simp) |
|
462 |
||
463 |
lemma nth_nodes: |
|
464 |
"i < length xs \<Longrightarrow> nodes ls xs rs ! i = |
|
465 |
Node (if i < length ls then ls ! i else Leaf) (xs ! i) |
|
466 |
(if i < length rs then rs ! i else Leaf)" |
|
467 |
by (induct ls xs rs arbitrary: i rule: nodes.induct; |
|
468 |
simp add: nth_Cons split: nat.split) |
|
469 |
||
470 |
theorem length_brauns: |
|
471 |
"length (brauns k xs) = min (length xs) (2 ^ k)" |
|
472 |
proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length]) |
|
71846 | 473 |
case (less xs) thus ?case by (simp add: brauns.simps[of k xs] length_nodes) |
69232 | 474 |
qed |
475 |
||
476 |
theorem brauns_correct: |
|
477 |
"i < min (length xs) (2 ^ k) \<Longrightarrow> braun_list (brauns k xs ! i) (take_nths i k xs)" |
|
478 |
proof (induct xs arbitrary: i k rule: measure_induct_rule[where f=length]) |
|
479 |
case (less xs) |
|
480 |
have "xs \<noteq> []" using less.prems by auto |
|
481 |
let ?zs = "drop (2^k) xs" |
|
482 |
let ?ts = "brauns (Suc k) ?zs" |
|
483 |
from less.hyps[of ?zs _ "Suc k"] |
|
484 |
have IH: "\<lbrakk> j = i + 2 ^ k; i < min (length ?zs) (2 ^ (k+1)) \<rbrakk> \<Longrightarrow> |
|
485 |
braun_list (?ts ! i) (take_nths j (Suc k) xs)" for i j |
|
486 |
using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop) |
|
487 |
show ?case |
|
71304 | 488 |
using less.prems |
71846 | 489 |
by (auto simp: brauns.simps[of k xs] nth_nodes take_nths_take_nths |
69232 | 490 |
IH take_nths_empty hd_take_nths length_brauns) |
491 |
qed |
|
492 |
||
493 |
corollary brauns1_correct: |
|
494 |
"braun (brauns1 xs) \<and> list (brauns1 xs) = xs" |
|
495 |
using brauns_correct[of 0 xs 0] |
|
496 |
by (simp add: brauns1_def braun_list_eq take_nths_00) |
|
497 |
||
498 |
||
499 |
paragraph "Running Time Analysis" |
|
500 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
501 |
theorem T_brauns: |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
502 |
"T_brauns k xs = 4 * length xs" |
69232 | 503 |
proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length]) |
504 |
case (less xs) |
|
505 |
show ?case |
|
506 |
proof cases |
|
507 |
assume "xs = []" |
|
71846 | 508 |
thus ?thesis by(simp) |
69232 | 509 |
next |
510 |
assume "xs \<noteq> []" |
|
511 |
let ?zs = "drop (2^k) xs" |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
512 |
have "T_brauns k xs = T_brauns (k+1) ?zs + 4 * min (2^k) (length xs)" |
71846 | 513 |
using \<open>xs \<noteq> []\<close> by(simp) |
69232 | 514 |
also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)" |
515 |
using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close> |
|
516 |
by (simp) |
|
517 |
also have "\<dots> = 4 * length xs" |
|
518 |
by(simp) |
|
519 |
finally show ?case . |
|
520 |
qed |
|
521 |
qed |
|
522 |
||
523 |
||
524 |
subsubsection \<open>Converting a Braun Tree into a List of Elements\<close> |
|
525 |
||
526 |
text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close> |
|
527 |
||
528 |
function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where |
|
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
529 |
"list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts in |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
530 |
if us = [] then [] else |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
531 |
map value us @ list_fast_rec (map left us @ map right us))" |
69232 | 532 |
by (pat_completeness, auto) |
533 |
||
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
534 |
lemma list_fast_rec_term1: "ts \<noteq> [] \<Longrightarrow> Leaf \<notin> set ts \<Longrightarrow> |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
535 |
sum_list (map (size o left) ts) + sum_list (map (size o right) ts) < sum_list (map size ts)" |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
536 |
apply (clarsimp simp: sum_list_addf[symmetric] sum_list_map_filter') |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
537 |
apply (rule sum_list_strict_mono; clarsimp?) |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
538 |
apply (case_tac x; simp) |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
539 |
done |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
540 |
|
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
541 |
lemma list_fast_rec_term: "us \<noteq> [] \<Longrightarrow> us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<Longrightarrow> |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
542 |
sum_list (map (size o left) us) + sum_list (map (size o right) us) < sum_list (map size ts)" |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
543 |
apply (rule order_less_le_trans, rule list_fast_rec_term1, simp_all) |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
544 |
apply (rule sum_list_filter_le_nat) |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
545 |
done |
69232 | 546 |
|
547 |
termination |
|
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
548 |
apply (relation "measure (sum_list o map size)") |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
549 |
apply simp |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
550 |
apply (simp add: list_fast_rec_term) |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
551 |
done |
69232 | 552 |
|
553 |
declare list_fast_rec.simps[simp del] |
|
554 |
||
555 |
definition list_fast :: "'a tree \<Rightarrow> 'a list" where |
|
556 |
"list_fast t = list_fast_rec [t]" |
|
557 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
558 |
function T_list_fast_rec :: "'a tree list \<Rightarrow> nat" where |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
559 |
"T_list_fast_rec ts = (let us = filter (\<lambda>t. t \<noteq> Leaf) ts |
69985
8e916ed23d17
follow up on Braun: get timing function right
Thomas Sewell <sewell@chalmers.se>
parents:
69984
diff
changeset
|
560 |
in length ts + (if us = [] then 0 else |
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
561 |
5 * length us + T_list_fast_rec (map left us @ map right us)))" |
69232 | 562 |
by (pat_completeness, auto) |
563 |
||
564 |
termination |
|
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
565 |
apply (relation "measure (sum_list o map size)") |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
566 |
apply simp |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
567 |
apply (simp add: list_fast_rec_term) |
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
568 |
done |
69232 | 569 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
570 |
declare T_list_fast_rec.simps[simp del] |
69232 | 571 |
|
572 |
paragraph "Functional Correctness" |
|
573 |
||
574 |
lemma list_fast_rec_all_Leaf: |
|
575 |
"\<forall>t \<in> set ts. t = Leaf \<Longrightarrow> list_fast_rec ts = []" |
|
576 |
by (simp add: filter_empty_conv list_fast_rec.simps) |
|
577 |
||
578 |
lemma take_nths_eq_single: |
|
579 |
"length xs - i < 2^n \<Longrightarrow> take_nths i n xs = take 1 (drop i xs)" |
|
580 |
by (induction xs arbitrary: i n; simp add: drop_Cons') |
|
581 |
||
582 |
lemma braun_list_Nil: |
|
583 |
"braun_list t [] = (t = Leaf)" |
|
584 |
by (cases t; simp) |
|
585 |
||
586 |
lemma braun_list_not_Nil: "xs \<noteq> [] \<Longrightarrow> |
|
587 |
braun_list t xs = |
|
588 |
(\<exists>l x r. t = Node l x r \<and> x = hd xs \<and> |
|
589 |
braun_list l (take_nths 1 1 xs) \<and> |
|
590 |
braun_list r (take_nths 2 1 xs))" |
|
591 |
by(cases t; simp) |
|
592 |
||
593 |
theorem list_fast_rec_correct: |
|
594 |
"\<lbrakk> length ts = 2 ^ k; \<forall>i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \<rbrakk> |
|
595 |
\<Longrightarrow> list_fast_rec ts = xs" |
|
596 |
proof (induct xs arbitrary: k ts rule: measure_induct_rule[where f=length]) |
|
597 |
case (less xs) |
|
598 |
show ?case |
|
599 |
proof (cases "length xs < 2 ^ k") |
|
600 |
case True |
|
601 |
from less.prems True have filter: |
|
602 |
"\<exists>n. ts = map (\<lambda>x. Node Leaf x Leaf) xs @ replicate n Leaf" |
|
603 |
apply (rule_tac x="length ts - length xs" in exI) |
|
604 |
apply (clarsimp simp: list_eq_iff_nth_eq) |
|
605 |
apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth) |
|
606 |
done |
|
607 |
thus ?thesis |
|
71846 | 608 |
by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf) |
69232 | 609 |
next |
610 |
case False |
|
611 |
with less.prems(2) have *: |
|
612 |
"\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf |
|
69655 | 613 |
\<and> value (ts ! i) = xs ! i |
69232 | 614 |
\<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs) |
615 |
\<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs |
|
616 |
\<longrightarrow> braun_list (right (ts ! i)) ys)" |
|
617 |
by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths |
|
618 |
algebra_simps) |
|
69655 | 619 |
have 1: "map value ts = take (2 ^ k) xs" |
69232 | 620 |
using less.prems(1) False by (simp add: list_eq_iff_nth_eq *) |
621 |
have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs" |
|
622 |
using less.prems(1) False |
|
623 |
by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"] |
|
624 |
simp: nth_append * take_nths_drop algebra_simps) |
|
625 |
from less.prems(1) False show ?thesis |
|
71846 | 626 |
by (auto simp: list_fast_rec.simps[of ts] 1 2 * all_set_conv_all_nth) |
69232 | 627 |
qed |
628 |
qed |
|
629 |
||
630 |
corollary list_fast_correct: |
|
631 |
"braun t \<Longrightarrow> list_fast t = list t" |
|
632 |
by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0]) |
|
633 |
||
634 |
paragraph "Running Time Analysis" |
|
635 |
||
636 |
lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow> |
|
637 |
(\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts" |
|
638 |
by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps) |
|
639 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
640 |
theorem T_list_fast_rec_ub: |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
641 |
"T_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)" |
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
642 |
proof (induction ts rule: measure_induct_rule[where f="sum_list o map size"]) |
69232 | 643 |
case (less ts) |
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
644 |
let ?us = "filter (\<lambda>t. t \<noteq> Leaf) ts" |
69232 | 645 |
show ?case |
646 |
proof cases |
|
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
647 |
assume "?us = []" |
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
648 |
thus ?thesis using T_list_fast_rec.simps[of ts] |
71846 | 649 |
by(simp add: sum_list_Suc) |
69985
8e916ed23d17
follow up on Braun: get timing function right
Thomas Sewell <sewell@chalmers.se>
parents:
69984
diff
changeset
|
650 |
next |
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
651 |
assume "?us \<noteq> []" |
69232 | 652 |
let ?children = "map left ?us @ map right ?us" |
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
653 |
have "T_list_fast_rec ts = T_list_fast_rec ?children + 5 * length ?us + length ts" |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
654 |
using \<open>?us \<noteq> []\<close> T_list_fast_rec.simps[of ts] by(simp) |
69232 | 655 |
also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts" |
69984
3afa3b25b5e7
Tweak Braun tree list_fast_rec recursion.
Thomas Sewell <sewell@chalmers.se>
parents:
69943
diff
changeset
|
656 |
using less[of "?children"] list_fast_rec_term[of "?us"] \<open>?us \<noteq> []\<close> |
69232 | 657 |
by (simp) |
658 |
also have "\<dots> = (\<Sum>t\<leftarrow>?children. 7*size t) + 7 * length ?us + length ts" |
|
659 |
by(simp add: sum_list_Suc o_def) |
|
660 |
also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts" |
|
661 |
by(simp add: sum_tree_list_children) |
|
662 |
also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts" |
|
663 |
by(simp add: sum_list_filter_le_nat) |
|
664 |
also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)" |
|
665 |
by(simp add: sum_list_Suc) |
|
666 |
finally show ?case . |
|
667 |
qed |
|
668 |
qed |
|
669 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
71846
diff
changeset
|
670 |
end |