363 apply (case_tac [!] bit) |
363 apply (case_tac [!] bit) |
364 apply (auto simp: le_Bits) |
364 apply (auto simp: le_Bits) |
365 done |
365 done |
366 |
366 |
367 lemmas int_and_le = |
367 lemmas int_and_le = |
368 xtr3 [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] |
368 xtrans(3) [OF bbw_ao_absorbs (2) [THEN conjunct2, symmetric] le_int_or] |
369 |
369 |
370 lemma add_BIT_simps [simp]: (* FIXME: move *) |
370 lemma add_BIT_simps [simp]: (* FIXME: move *) |
371 "x BIT 0 + y BIT 0 = (x + y) BIT 0" |
371 "x BIT 0 + y BIT 0 = (x + y) BIT 0" |
372 "x BIT 0 + y BIT 1 = (x + y) BIT 1" |
372 "x BIT 0 + y BIT 1 = (x + y) BIT 1" |
373 "x BIT 1 + y BIT 0 = (x + y) BIT 1" |
373 "x BIT 1 + y BIT 0 = (x + y) BIT 1" |
551 "bin_split n c = (a, b) ==> |
551 "bin_split n c = (a, b) ==> |
552 (ALL k. bin_nth a k = bin_nth c (n + k)) & |
552 (ALL k. bin_nth a k = bin_nth c (n + k)) & |
553 (ALL k. bin_nth b k = (k < n & bin_nth c k))" |
553 (ALL k. bin_nth b k = (k < n & bin_nth c k))" |
554 apply (induct n arbitrary: b c) |
554 apply (induct n arbitrary: b c) |
555 apply clarsimp |
555 apply clarsimp |
556 apply (clarsimp simp: Let_def split: ls_splits) |
556 apply (clarsimp simp: Let_def split: prod.split_asm) |
557 apply (case_tac k) |
557 apply (case_tac k) |
558 apply auto |
558 apply auto |
559 done |
559 done |
560 |
560 |
561 lemma bin_cat_assoc: |
561 lemma bin_cat_assoc: |
587 "bin_cat a n (bintrunc n b) = bin_cat a n b" |
587 "bin_cat a n (bintrunc n b) = bin_cat a n b" |
588 by (induct n arbitrary: b) auto |
588 by (induct n arbitrary: b) auto |
589 |
589 |
590 lemma split_bintrunc: |
590 lemma split_bintrunc: |
591 "bin_split n c = (a, b) ==> b = bintrunc n c" |
591 "bin_split n c = (a, b) ==> b = bintrunc n c" |
592 by (induct n arbitrary: b c) (auto simp: Let_def split: ls_splits) |
592 by (induct n arbitrary: b c) (auto simp: Let_def split: prod.split_asm) |
593 |
593 |
594 lemma bin_cat_split: |
594 lemma bin_cat_split: |
595 "bin_split n w = (u, v) ==> w = bin_cat u n v" |
595 "bin_split n w = (u, v) ==> w = bin_cat u n v" |
596 by (induct n arbitrary: v w) (auto simp: Let_def split: ls_splits) |
596 by (induct n arbitrary: v w) (auto simp: Let_def split: prod.split_asm) |
597 |
597 |
598 lemma bin_split_cat: |
598 lemma bin_split_cat: |
599 "bin_split n (bin_cat v n w) = (v, bintrunc n w)" |
599 "bin_split n (bin_cat v n w) = (v, bintrunc n w)" |
600 by (induct n arbitrary: w) auto |
600 by (induct n arbitrary: w) auto |
601 |
601 |
608 |
608 |
609 lemma bin_split_trunc: |
609 lemma bin_split_trunc: |
610 "bin_split (min m n) c = (a, b) ==> |
610 "bin_split (min m n) c = (a, b) ==> |
611 bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" |
611 bin_split n (bintrunc m c) = (bintrunc (m - n) a, b)" |
612 apply (induct n arbitrary: m b c, clarsimp) |
612 apply (induct n arbitrary: m b c, clarsimp) |
613 apply (simp add: bin_rest_trunc Let_def split: ls_splits) |
613 apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) |
614 apply (case_tac m) |
614 apply (case_tac m) |
615 apply (auto simp: Let_def split: ls_splits) |
615 apply (auto simp: Let_def split: prod.split_asm) |
616 done |
616 done |
617 |
617 |
618 lemma bin_split_trunc1: |
618 lemma bin_split_trunc1: |
619 "bin_split n c = (a, b) ==> |
619 "bin_split n c = (a, b) ==> |
620 bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" |
620 bin_split n (bintrunc m c) = (bintrunc (m - n) a, bintrunc m b)" |
621 apply (induct n arbitrary: m b c, clarsimp) |
621 apply (induct n arbitrary: m b c, clarsimp) |
622 apply (simp add: bin_rest_trunc Let_def split: ls_splits) |
622 apply (simp add: bin_rest_trunc Let_def split: prod.split_asm) |
623 apply (case_tac m) |
623 apply (case_tac m) |
624 apply (auto simp: Let_def split: ls_splits) |
624 apply (auto simp: Let_def split: prod.split_asm) |
625 done |
625 done |
626 |
626 |
627 lemma bin_cat_num: |
627 lemma bin_cat_num: |
628 "bin_cat a n b = a * 2 ^ n + bintrunc n b" |
628 "bin_cat a n b = a * 2 ^ n + bintrunc n b" |
629 apply (induct n arbitrary: b, clarsimp) |
629 apply (induct n arbitrary: b, clarsimp) |