src/HOL/Data_Structures/Array_Braun.thy
 changeset 69232 2b913054a9cf parent 69206 9660bbf5ce7e child 69597 ff784d5a5bfb
equal inserted replaced
69231:6b90ace5e5eb 69232:2b913054a9cf

1 (* Author: Tobias Nipkow, with contributions by Thomas Sewell *)

2
1 section "Arrays via Braun Trees"
3 section "Arrays via Braun Trees"
2
4
3 theory Array_Braun
5 theory Array_Braun
4 imports
6 imports
5   Array_Specs
7   Array_Specs
47 by auto arith
49 by auto arith
48
50
49 declare upt_Suc[simp del]
51 declare upt_Suc[simp del]
50
52
51
53
52 text \<open>@{const lookup1}\<close>
54 paragraph \<open>@{const lookup1}\<close>
53
55
54 lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"
56 lemma nth_list_lookup1: "\<lbrakk>braun t; i < size t\<rbrakk> \<Longrightarrow> list t ! i = lookup1 t (i+1)"
55 proof(induction t arbitrary: i)
57 proof(induction t arbitrary: i)
56   case Leaf thus ?case by simp
58   case Leaf thus ?case by simp
57 next
59 next
62
64
63 lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"
65 lemma list_eq_map_lookup1: "braun t \<Longrightarrow> list t = map (lookup1 t) [1..<size t + 1]"
64 by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
66 by(auto simp add: list_eq_iff_nth_eq size_list nth_list_lookup1)
65
67
66
68
67 text \<open>@{const update1}\<close>
69 paragraph \<open>@{const update1}\<close>
68
70
69 lemma size_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"
71 lemma size_update1: "\<lbrakk> braun t;  n \<in> {1.. size t} \<rbrakk> \<Longrightarrow> size(update1 n x t) = size t"
70 proof(induction t arbitrary: n)
72 proof(induction t arbitrary: n)
71   case Leaf thus ?case by simp
73   case Leaf thus ?case by simp
72 next
74 next
114   case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]
116   case (Node l a r) thus ?case using div2_in_bounds[OF Node.prems]
115     by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)
117     by(auto simp: list_update_splice diff1_eq_iff size_list split: nat.split)
116 qed
118 qed
117
119
118
120
120
122
121 lemma splice_last: shows
123 lemma splice_last: shows
122   "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
124   "size ys \<le> size xs \<Longrightarrow> splice (xs @ [x]) ys = splice xs ys @ [x]"
123 and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
125 and "size ys+1 \<ge> size xs \<Longrightarrow> splice xs (ys @ [y]) = splice xs ys @ [y]"
124 by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
126 by(induction xs ys arbitrary: x y rule: splice.induct) (auto)
188
190
189
191
190 subsubsection "Functional Correctness"
192 subsubsection "Functional Correctness"
191
193
192
194
194
196
195 lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
197 lemma list_add_lo: "braun t \<Longrightarrow> list (add_lo a t) = a # list t"
196 by(induction t arbitrary: a) auto
198 by(induction t arbitrary: a) auto
197
199
199 by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
201 by(induction t arbitrary: x) (auto simp add: list_add_lo simp flip: size_list)
200
202
201
203
202 text \<open>@{const del_lo}\<close>
204 paragraph \<open>@{const del_lo}\<close>
203
205
204 lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
206 lemma list_merge: "braun (Node l x r) \<Longrightarrow> list(merge l r) = splice (list l) (list r)"
205 by (induction l r rule: merge.induct) auto
207 by (induction l r rule: merge.induct) auto
206
208
207 lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"
209 lemma braun_merge: "braun (Node l x r) \<Longrightarrow> braun(merge l r)"
212
214
213 lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"
215 lemma braun_del_lo: "braun t \<Longrightarrow> braun(del_lo t)"
214 by (cases t) (simp_all add: braun_merge)
216 by (cases t) (simp_all add: braun_merge)
215
217
216
218
217 text \<open>@{const del_hi}\<close>
219 paragraph \<open>@{const del_hi}\<close>
218
220
219 lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
221 lemma list_Nil_iff: "list t = [] \<longleftrightarrow> t = Leaf"
220 by(cases t) simp_all
222 by(cases t) simp_all
221
223
222 lemma butlast_splice: "butlast (splice xs ys) =
224 lemma butlast_splice: "butlast (splice xs ys) =
264 qed
266 qed
265
267
266
268
267 subsection "Faster"
269 subsection "Faster"
268
270

271

272 subsubsection \<open>Initialization with 1 element\<close>

273
269 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
274 fun braun_of_naive :: "'a \<Rightarrow> nat \<Rightarrow> 'a tree" where
270 "braun_of_naive x n = (if n=0 then Leaf
275 "braun_of_naive x n = (if n=0 then Leaf
271   else let m = (n-1) div 2
276   else let m = (n-1) div 2
272        in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
277        in if odd n then Node (braun_of_naive x m) x (braun_of_naive x m)
273        else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
278        else Node (braun_of_naive x (m + 1)) x (braun_of_naive x m))"
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"

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"

627     also have "\<dots> = (\<Sum>t\<leftarrow>?us. 7*size t) + length ts"

629     also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 7*size t) + length ts"

631     also have "\<dots> = (\<Sum>t\<leftarrow>ts. 7 * size t + 1)"