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
|
|
275 |
"diff Leaf 0 = 0" |
|
|
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 |
|
69943
|
282 |
lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = size t - n"
|
69941
|
283 |
by(induction t arbitrary: n) auto
|
|
284 |
|
|
285 |
lemma size_fast: "braun t \<Longrightarrow> size_fast t = size t"
|
|
286 |
by(induction t) (auto simp add: Let_def diff)
|
|
287 |
|
|
288 |
|
69232
|
289 |
subsubsection \<open>Initialization with 1 element\<close>
|
|
290 |
|
69206
|
291 |
fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
|
|
292 |
"braun_of_naive x n = (if n=0 then Leaf
|
69145
|
293 |
else let m = (n-1) div 2
|
69206
|
294 |
in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
|
|
295 |
else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
|
69145
|
296 |
|
|
297 |
fun braun2_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree * 'a tree" where
|
|
298 |
"braun2_of x n = (if n = 0 then (Leaf, Node Leaf x Leaf)
|
|
299 |
else let (s,t) = braun2_of x ((n-1) div 2)
|
|
300 |
in if odd n then (Node s x s, Node t x s) else (Node t x s, Node t x t))"
|
|
301 |
|
|
302 |
definition braun_of :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
|
|
303 |
"braun_of x n = fst (braun2_of x n)"
|
|
304 |
|
|
305 |
declare braun2_of.simps [simp del]
|
|
306 |
|
|
307 |
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"
|
|
308 |
proof(induction x n arbitrary: s t rule: braun2_of.induct)
|
|
309 |
case (1 x n)
|
|
310 |
then show ?case
|
|
311 |
by (auto simp: braun2_of.simps[of x n] split: prod.splits if_splits) presburger+
|
|
312 |
qed
|
|
313 |
|
|
314 |
lemma braun2_of_replicate:
|
|
315 |
"braun2_of x n = (s,t) \<Longrightarrow> list s = replicate n x \<and> list t = replicate (n+1) x"
|
|
316 |
proof(induction x n arbitrary: s t rule: braun2_of.induct)
|
|
317 |
case (1 x n)
|
|
318 |
have "x # replicate m x = replicate (m+1) x" for m by simp
|
|
319 |
with 1 show ?case
|
|
320 |
apply (auto simp: braun2_of.simps[of x n] replicate.simps(2)[of 0 x]
|
|
321 |
simp del: replicate.simps(2) split: prod.splits if_splits)
|
|
322 |
by presburger+
|
|
323 |
qed
|
|
324 |
|
|
325 |
corollary braun_braun_of: "braun(braun_of x n)"
|
|
326 |
unfolding braun_of_def by (metis eq_fst_iff braun2_of_size_braun)
|
|
327 |
|
|
328 |
corollary list_braun_of: "list(braun_of x n) = replicate n x"
|
|
329 |
unfolding braun_of_def by (metis eq_fst_iff braun2_of_replicate)
|
|
330 |
|
69232
|
331 |
|
|
332 |
subsubsection "Proof Infrastructure"
|
|
333 |
|
|
334 |
text \<open>Originally due to Thomas Sewell.\<close>
|
|
335 |
|
|
336 |
paragraph \<open>\<open>take_nths\<close>\<close>
|
|
337 |
|
|
338 |
fun take_nths :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" where
|
|
339 |
"take_nths i k [] = []" |
|
|
340 |
"take_nths i k (x # xs) = (if i = 0 then x # take_nths (2^k - 1) k xs
|
|
341 |
else take_nths (i - 1) k xs)"
|
|
342 |
|
|
343 |
lemma take_nths_drop:
|
|
344 |
"take_nths i k (drop j xs) = take_nths (i + j) k xs"
|
|
345 |
by (induct xs arbitrary: i j; simp add: drop_Cons split: nat.split)
|
|
346 |
|
|
347 |
lemma take_nths_00:
|
|
348 |
"take_nths 0 0 xs = xs"
|
|
349 |
by (induct xs; simp)
|
|
350 |
|
|
351 |
lemma splice_take_nths:
|
|
352 |
"splice (take_nths 0 (Suc 0) xs) (take_nths (Suc 0) (Suc 0) xs) = xs"
|
|
353 |
by (induct xs; simp)
|
|
354 |
|
|
355 |
lemma take_nths_take_nths:
|
|
356 |
"take_nths i m (take_nths j n xs) = take_nths ((i * 2^n) + j) (m + n) xs"
|
|
357 |
by (induct xs arbitrary: i j; simp add: algebra_simps power_add)
|
|
358 |
|
|
359 |
lemma take_nths_empty:
|
|
360 |
"(take_nths i k xs = []) = (length xs \<le> i)"
|
|
361 |
by (induction xs arbitrary: i k) auto
|
|
362 |
|
|
363 |
lemma hd_take_nths:
|
|
364 |
"i < length xs \<Longrightarrow> hd(take_nths i k xs) = xs ! i"
|
|
365 |
by (induction xs arbitrary: i k) auto
|
|
366 |
|
|
367 |
lemma take_nths_01_splice:
|
|
368 |
"\<lbrakk> length xs = length ys \<or> length xs = length ys + 1 \<rbrakk> \<Longrightarrow>
|
|
369 |
take_nths 0 (Suc 0) (splice xs ys) = xs \<and>
|
|
370 |
take_nths (Suc 0) (Suc 0) (splice xs ys) = ys"
|
|
371 |
by (induct xs arbitrary: ys; case_tac ys; simp)
|
|
372 |
|
|
373 |
lemma length_take_nths_00:
|
|
374 |
"length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) \<or>
|
|
375 |
length (take_nths 0 (Suc 0) xs) = length (take_nths (Suc 0) (Suc 0) xs) + 1"
|
|
376 |
by (induct xs) auto
|
|
377 |
|
|
378 |
|
|
379 |
paragraph \<open>\<open>braun_list\<close>\<close>
|
|
380 |
|
|
381 |
fun braun_list :: "'a tree \<Rightarrow> 'a list \<Rightarrow> bool" where
|
|
382 |
"braun_list Leaf xs = (xs = [])" |
|
|
383 |
"braun_list (Node l x r) xs = (xs \<noteq> [] \<and> x = hd xs \<and>
|
|
384 |
braun_list l (take_nths 1 1 xs) \<and>
|
|
385 |
braun_list r (take_nths 2 1 xs))"
|
|
386 |
|
|
387 |
lemma braun_list_eq:
|
|
388 |
"braun_list t xs = (braun t \<and> xs = list t)"
|
|
389 |
proof (induct t arbitrary: xs)
|
|
390 |
case Leaf
|
|
391 |
show ?case by simp
|
|
392 |
next
|
|
393 |
case Node
|
|
394 |
show ?case
|
|
395 |
using length_take_nths_00[of xs] splice_take_nths[of xs]
|
|
396 |
by (auto simp: neq_Nil_conv Node.hyps size_list[symmetric] take_nths_01_splice)
|
|
397 |
qed
|
|
398 |
|
|
399 |
|
|
400 |
subsubsection \<open>Converting a list of elements into a Braun tree\<close>
|
|
401 |
|
|
402 |
fun nodes :: "'a tree list \<Rightarrow> 'a list \<Rightarrow> 'a tree list \<Rightarrow> 'a tree list" where
|
|
403 |
"nodes (l#ls) (x#xs) (r#rs) = Node l x r # nodes ls xs rs" |
|
|
404 |
"nodes (l#ls) (x#xs) [] = Node l x Leaf # nodes ls xs []" |
|
|
405 |
"nodes [] (x#xs) (r#rs) = Node Leaf x r # nodes [] xs rs" |
|
|
406 |
"nodes [] (x#xs) [] = Node Leaf x Leaf # nodes [] xs []" |
|
|
407 |
"nodes ls [] rs = []"
|
|
408 |
|
|
409 |
fun brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree list" where
|
|
410 |
"brauns k xs = (if xs = [] then [] else
|
|
411 |
let ys = take (2^k) xs;
|
|
412 |
zs = drop (2^k) xs;
|
|
413 |
ts = brauns (k+1) zs
|
|
414 |
in nodes ts ys (drop (2^k) ts))"
|
|
415 |
|
|
416 |
declare brauns.simps[simp del]
|
|
417 |
|
|
418 |
definition brauns1 :: "'a list \<Rightarrow> 'a tree" where
|
|
419 |
"brauns1 xs = (if xs = [] then Leaf else brauns 0 xs ! 0)"
|
|
420 |
|
|
421 |
fun t_brauns :: "nat \<Rightarrow> 'a list \<Rightarrow> nat" where
|
|
422 |
"t_brauns k xs = (if xs = [] then 0 else
|
|
423 |
let ys = take (2^k) xs;
|
|
424 |
zs = drop (2^k) xs;
|
|
425 |
ts = brauns (k+1) zs
|
|
426 |
in 4 * min (2^k) (length xs) + t_brauns (k+1) zs)"
|
|
427 |
|
|
428 |
|
|
429 |
paragraph "Functional correctness"
|
|
430 |
|
|
431 |
text \<open>The proof is originally due to Thomas Sewell.\<close>
|
|
432 |
|
|
433 |
lemma length_nodes:
|
|
434 |
"length (nodes ls xs rs) = length xs"
|
|
435 |
by (induct ls xs rs rule: nodes.induct; simp)
|
|
436 |
|
|
437 |
lemma nth_nodes:
|
|
438 |
"i < length xs \<Longrightarrow> nodes ls xs rs ! i =
|
|
439 |
Node (if i < length ls then ls ! i else Leaf) (xs ! i)
|
|
440 |
(if i < length rs then rs ! i else Leaf)"
|
|
441 |
by (induct ls xs rs arbitrary: i rule: nodes.induct;
|
|
442 |
simp add: nth_Cons split: nat.split)
|
|
443 |
|
|
444 |
theorem length_brauns:
|
|
445 |
"length (brauns k xs) = min (length xs) (2 ^ k)"
|
|
446 |
proof (induct xs arbitrary: k rule: measure_induct_rule[where f=length])
|
|
447 |
case (less xs) thus ?case by (simp add: brauns.simps[of k xs] Let_def length_nodes)
|
|
448 |
qed
|
|
449 |
|
|
450 |
theorem brauns_correct:
|
|
451 |
"i < min (length xs) (2 ^ k) \<Longrightarrow> braun_list (brauns k xs ! i) (take_nths i k xs)"
|
|
452 |
proof (induct xs arbitrary: i k rule: measure_induct_rule[where f=length])
|
|
453 |
case (less xs)
|
|
454 |
have "xs \<noteq> []" using less.prems by auto
|
|
455 |
let ?zs = "drop (2^k) xs"
|
|
456 |
let ?ts = "brauns (Suc k) ?zs"
|
|
457 |
from less.hyps[of ?zs _ "Suc k"]
|
|
458 |
have IH: "\<lbrakk> j = i + 2 ^ k; i < min (length ?zs) (2 ^ (k+1)) \<rbrakk> \<Longrightarrow>
|
|
459 |
braun_list (?ts ! i) (take_nths j (Suc k) xs)" for i j
|
|
460 |
using \<open>xs \<noteq> []\<close> by (simp add: take_nths_drop)
|
|
461 |
let ?xs' = "take_nths i k xs"
|
|
462 |
let ?ts' = "drop (2^k) ?ts"
|
|
463 |
show ?case
|
|
464 |
proof (cases "i < length ?ts \<and> \<not> i < length ?ts'")
|
|
465 |
case True
|
|
466 |
have "braun_list (brauns k xs ! i) ?xs' \<longleftrightarrow>
|
|
467 |
braun_list (nodes ?ts (take (2^k) xs) ?ts' ! i) ?xs'"
|
|
468 |
using \<open>xs \<noteq> []\<close> by (simp add: brauns.simps[of k xs] Let_def)
|
|
469 |
also have "\<dots> \<longleftrightarrow> braun_list (?ts ! i) (take_nths (2^k + i) (k+1) xs)
|
|
470 |
\<and> braun_list Leaf (take_nths (2^(k+1) + i) (k+1) xs)"
|
|
471 |
using less.prems True
|
|
472 |
by (clarsimp simp: nth_nodes take_nths_take_nths take_nths_empty hd_take_nths)
|
|
473 |
also have "\<dots>" using less.prems True by (auto simp: IH take_nths_empty length_brauns)
|
|
474 |
finally show ?thesis .
|
|
475 |
next
|
|
476 |
case False
|
|
477 |
thus ?thesis using less.prems
|
|
478 |
by (auto simp: brauns.simps[of k xs] Let_def nth_nodes take_nths_take_nths
|
|
479 |
IH take_nths_empty hd_take_nths length_brauns)
|
|
480 |
qed
|
|
481 |
qed
|
|
482 |
|
|
483 |
corollary brauns1_correct:
|
|
484 |
"braun (brauns1 xs) \<and> list (brauns1 xs) = xs"
|
|
485 |
using brauns_correct[of 0 xs 0]
|
|
486 |
by (simp add: brauns1_def braun_list_eq take_nths_00)
|
|
487 |
|
|
488 |
|
|
489 |
paragraph "Running Time Analysis"
|
|
490 |
|
|
491 |
theorem t_brauns:
|
|
492 |
"t_brauns k xs = 4 * length xs"
|
|
493 |
proof (induction xs arbitrary: k rule: measure_induct_rule[where f = length])
|
|
494 |
case (less xs)
|
|
495 |
show ?case
|
|
496 |
proof cases
|
|
497 |
assume "xs = []"
|
|
498 |
thus ?thesis by(simp add: Let_def)
|
|
499 |
next
|
|
500 |
assume "xs \<noteq> []"
|
|
501 |
let ?zs = "drop (2^k) xs"
|
|
502 |
have "t_brauns k xs = t_brauns (k+1) ?zs + 4 * min (2^k) (length xs)"
|
|
503 |
using \<open>xs \<noteq> []\<close> by(simp add: Let_def)
|
|
504 |
also have "\<dots> = 4 * length ?zs + 4 * min (2^k) (length xs)"
|
|
505 |
using less[of ?zs "k+1"] \<open>xs \<noteq> []\<close>
|
|
506 |
by (simp)
|
|
507 |
also have "\<dots> = 4 * length xs"
|
|
508 |
by(simp)
|
|
509 |
finally show ?case .
|
|
510 |
qed
|
|
511 |
qed
|
|
512 |
|
|
513 |
|
|
514 |
subsubsection \<open>Converting a Braun Tree into a List of Elements\<close>
|
|
515 |
|
|
516 |
text \<open>The code and the proof are originally due to Thomas Sewell (except running time).\<close>
|
|
517 |
|
|
518 |
function list_fast_rec :: "'a tree list \<Rightarrow> 'a list" where
|
|
519 |
"list_fast_rec ts = (if ts = [] then [] else
|
|
520 |
let us = filter (\<lambda>t. t \<noteq> Leaf) ts
|
69655
|
521 |
in map value us @ list_fast_rec (map left us @ map right us))"
|
69232
|
522 |
by (pat_completeness, auto)
|
|
523 |
|
|
524 |
lemma list_fast_rec_term: "\<lbrakk> ts \<noteq> []; us = filter (\<lambda>t. t \<noteq> \<langle>\<rangle>) ts \<rbrakk> \<Longrightarrow>
|
|
525 |
(map left us @ map right us, ts) \<in> measure (sum_list \<circ> map (\<lambda>t. 2 * size t + 1))"
|
|
526 |
apply (clarsimp simp: sum_list_addf[symmetric] sum_list_map_filter')
|
|
527 |
apply (rule sum_list_strict_mono; simp)
|
|
528 |
apply (case_tac x; simp)
|
|
529 |
done
|
|
530 |
|
|
531 |
termination
|
|
532 |
apply (relation "measure (sum_list o map (\<lambda>t. 2 * size t + 1))")
|
|
533 |
apply simp
|
|
534 |
using list_fast_rec_term by auto
|
|
535 |
|
|
536 |
declare list_fast_rec.simps[simp del]
|
|
537 |
|
|
538 |
definition list_fast :: "'a tree \<Rightarrow> 'a list" where
|
|
539 |
"list_fast t = list_fast_rec [t]"
|
|
540 |
|
|
541 |
function t_list_fast_rec :: "'a tree list \<Rightarrow> nat" where
|
|
542 |
"t_list_fast_rec ts = (if ts = [] then 0 else
|
|
543 |
let us = filter (\<lambda>t. t \<noteq> Leaf) ts
|
|
544 |
in length ts + 5 * length us + t_list_fast_rec (map left us @ map right us))"
|
|
545 |
by (pat_completeness, auto)
|
|
546 |
|
|
547 |
termination
|
|
548 |
apply (relation "measure (sum_list o map (\<lambda>t. 2 * size t + 1))")
|
|
549 |
apply simp
|
|
550 |
using list_fast_rec_term by auto
|
|
551 |
|
|
552 |
declare t_list_fast_rec.simps[simp del]
|
|
553 |
|
|
554 |
|
|
555 |
paragraph "Functional Correctness"
|
|
556 |
|
|
557 |
lemma list_fast_rec_all_Leaf:
|
|
558 |
"\<forall>t \<in> set ts. t = Leaf \<Longrightarrow> list_fast_rec ts = []"
|
|
559 |
by (simp add: filter_empty_conv list_fast_rec.simps)
|
|
560 |
|
|
561 |
lemma take_nths_eq_single:
|
|
562 |
"length xs - i < 2^n \<Longrightarrow> take_nths i n xs = take 1 (drop i xs)"
|
|
563 |
by (induction xs arbitrary: i n; simp add: drop_Cons')
|
|
564 |
|
|
565 |
lemma braun_list_Nil:
|
|
566 |
"braun_list t [] = (t = Leaf)"
|
|
567 |
by (cases t; simp)
|
|
568 |
|
|
569 |
lemma braun_list_not_Nil: "xs \<noteq> [] \<Longrightarrow>
|
|
570 |
braun_list t xs =
|
|
571 |
(\<exists>l x r. t = Node l x r \<and> x = hd xs \<and>
|
|
572 |
braun_list l (take_nths 1 1 xs) \<and>
|
|
573 |
braun_list r (take_nths 2 1 xs))"
|
|
574 |
by(cases t; simp)
|
|
575 |
|
|
576 |
theorem list_fast_rec_correct:
|
|
577 |
"\<lbrakk> length ts = 2 ^ k; \<forall>i < 2 ^ k. braun_list (ts ! i) (take_nths i k xs) \<rbrakk>
|
|
578 |
\<Longrightarrow> list_fast_rec ts = xs"
|
|
579 |
proof (induct xs arbitrary: k ts rule: measure_induct_rule[where f=length])
|
|
580 |
case (less xs)
|
|
581 |
show ?case
|
|
582 |
proof (cases "length xs < 2 ^ k")
|
|
583 |
case True
|
|
584 |
from less.prems True have filter:
|
|
585 |
"\<exists>n. ts = map (\<lambda>x. Node Leaf x Leaf) xs @ replicate n Leaf"
|
|
586 |
apply (rule_tac x="length ts - length xs" in exI)
|
|
587 |
apply (clarsimp simp: list_eq_iff_nth_eq)
|
|
588 |
apply(auto simp: nth_append braun_list_not_Nil take_nths_eq_single braun_list_Nil hd_drop_conv_nth)
|
|
589 |
done
|
|
590 |
thus ?thesis
|
|
591 |
by (clarsimp simp: list_fast_rec.simps[of ts] o_def list_fast_rec_all_Leaf)
|
|
592 |
next
|
|
593 |
case False
|
|
594 |
with less.prems(2) have *:
|
|
595 |
"\<forall>i < 2 ^ k. ts ! i \<noteq> Leaf
|
69655
|
596 |
\<and> value (ts ! i) = xs ! i
|
69232
|
597 |
\<and> braun_list (left (ts ! i)) (take_nths (i + 2 ^ k) (Suc k) xs)
|
|
598 |
\<and> (\<forall>ys. ys = take_nths (i + 2 * 2 ^ k) (Suc k) xs
|
|
599 |
\<longrightarrow> braun_list (right (ts ! i)) ys)"
|
|
600 |
by (auto simp: take_nths_empty hd_take_nths braun_list_not_Nil take_nths_take_nths
|
|
601 |
algebra_simps)
|
69655
|
602 |
have 1: "map value ts = take (2 ^ k) xs"
|
69232
|
603 |
using less.prems(1) False by (simp add: list_eq_iff_nth_eq *)
|
|
604 |
have 2: "list_fast_rec (map left ts @ map right ts) = drop (2 ^ k) xs"
|
|
605 |
using less.prems(1) False
|
|
606 |
by (auto intro!: Nat.diff_less less.hyps[where k= "Suc k"]
|
|
607 |
simp: nth_append * take_nths_drop algebra_simps)
|
|
608 |
from less.prems(1) False show ?thesis
|
|
609 |
by (auto simp: list_fast_rec.simps[of ts] 1 2 Let_def * all_set_conv_all_nth)
|
|
610 |
qed
|
|
611 |
qed
|
|
612 |
|
|
613 |
corollary list_fast_correct:
|
|
614 |
"braun t \<Longrightarrow> list_fast t = list t"
|
|
615 |
by (simp add: list_fast_def take_nths_00 braun_list_eq list_fast_rec_correct[where k=0])
|
|
616 |
|
|
617 |
|
|
618 |
paragraph "Running Time Analysis"
|
|
619 |
|
|
620 |
lemma sum_tree_list_children: "\<forall>t \<in> set ts. t \<noteq> Leaf \<Longrightarrow>
|
|
621 |
(\<Sum>t\<leftarrow>ts. k * size t) = (\<Sum>t \<leftarrow> map left ts @ map right ts. k * size t) + k * length ts"
|
|
622 |
by(induction ts)(auto simp add: neq_Leaf_iff algebra_simps)
|
|
623 |
|
|
624 |
theorem t_list_fast_rec_ub:
|
|
625 |
"t_list_fast_rec ts \<le> sum_list (map (\<lambda>t. 7*size t + 1) ts)"
|
|
626 |
proof (induction ts rule: measure_induct_rule[where f="sum_list o map (\<lambda>t. 2*size t + 1)"])
|
|
627 |
case (less ts)
|
|
628 |
show ?case
|
|
629 |
proof cases
|
|
630 |
assume "ts = []"
|
|
631 |
thus ?thesis using t_list_fast_rec.simps[of ts] by(simp add: Let_def)
|
|
632 |
next
|
|
633 |
assume "ts \<noteq> []"
|
|
634 |
let ?us = "filter (\<lambda>t. t \<noteq> Leaf) ts"
|
|
635 |
let ?children = "map left ?us @ map right ?us"
|
|
636 |
have "t_list_fast_rec ts = t_list_fast_rec ?children + 5 * length ?us + length ts"
|
|
637 |
using \<open>ts \<noteq> []\<close> t_list_fast_rec.simps[of ts] by(simp add: Let_def)
|
|
638 |
also have "\<dots> \<le> (\<Sum>t\<leftarrow>?children. 7 * size t + 1) + 5 * length ?us + length ts"
|
|
639 |
using less[of "map left ?us @ map right ?us"]
|
|
640 |
list_fast_rec_term[of ts, OF \<open>ts \<noteq> []\<close>]
|
|
641 |
by (simp)
|
|
642 |
also have "\<dots> = (\<Sum>t\<leftarrow>?children. 7*size t) + 7 * length ?us + length ts"
|
|
643 |
by(simp add: sum_list_Suc o_def)
|
|
644 |
also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts"
|
|
645 |
by(simp add: sum_tree_list_children)
|
|
646 |
also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts"
|
|
647 |
by(simp add: sum_list_filter_le_nat)
|
|
648 |
also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)"
|
|
649 |
by(simp add: sum_list_Suc)
|
|
650 |
finally show ?case .
|
|
651 |
qed
|
|
652 |
qed
|
|
653 |
|
69145
|
654 |
end |