equal
deleted
inserted
replaced
265 case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits) |
265 case 8 thus ?case by (simp add: braun_del_hi list_del_hi flip: size_list split: prod.splits) |
266 qed |
266 qed |
267 |
267 |
268 |
268 |
269 subsection "Faster" |
269 subsection "Faster" |
|
270 |
|
271 |
|
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 |
|
282 lemma diff: "braun t \<Longrightarrow> size t : {n, n + 1} \<Longrightarrow> diff t n = (if size t = n then 0 else 1)" |
|
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) |
270 |
287 |
271 |
288 |
272 subsubsection \<open>Initialization with 1 element\<close> |
289 subsubsection \<open>Initialization with 1 element\<close> |
273 |
290 |
274 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where |
291 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where |