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