431 |
470 |
432 lemma word_less_def [code]: |
471 lemma word_less_def [code]: |
433 "a < b \<longleftrightarrow> uint a < uint b" |
472 "a < b \<longleftrightarrow> uint a < uint b" |
434 by transfer rule |
473 by transfer rule |
435 |
474 |
|
475 lemma word_greater_zero_iff: |
|
476 \<open>a > 0 \<longleftrightarrow> a \<noteq> 0\<close> for a :: \<open>'a::len0 word\<close> |
|
477 by transfer (simp add: less_le) |
|
478 |
|
479 lemma of_nat_word_eq_iff: |
|
480 \<open>of_nat m = (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m = take_bit LENGTH('a) n\<close> |
|
481 by transfer (simp add: take_bit_of_nat) |
|
482 |
|
483 lemma of_nat_word_less_eq_iff: |
|
484 \<open>of_nat m \<le> (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m \<le> take_bit LENGTH('a) n\<close> |
|
485 by transfer (simp add: take_bit_of_nat) |
|
486 |
|
487 lemma of_nat_word_less_iff: |
|
488 \<open>of_nat m < (of_nat n :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) m < take_bit LENGTH('a) n\<close> |
|
489 by transfer (simp add: take_bit_of_nat) |
|
490 |
|
491 lemma of_nat_word_eq_0_iff: |
|
492 \<open>of_nat n = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd n\<close> |
|
493 using of_nat_word_eq_iff [where ?'a = 'a, of n 0] by (simp add: take_bit_eq_0_iff) |
|
494 |
|
495 lemma of_int_word_eq_iff: |
|
496 \<open>of_int k = (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k = take_bit LENGTH('a) l\<close> |
|
497 by transfer rule |
|
498 |
|
499 lemma of_int_word_less_eq_iff: |
|
500 \<open>of_int k \<le> (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k \<le> take_bit LENGTH('a) l\<close> |
|
501 by transfer rule |
|
502 |
|
503 lemma of_int_word_less_iff: |
|
504 \<open>of_int k < (of_int l :: 'a::len word) \<longleftrightarrow> take_bit LENGTH('a) k < take_bit LENGTH('a) l\<close> |
|
505 by transfer rule |
|
506 |
|
507 lemma of_int_word_eq_0_iff: |
|
508 \<open>of_int k = (0 :: 'a::len word) \<longleftrightarrow> 2 ^ LENGTH('a) dvd k\<close> |
|
509 using of_int_word_eq_iff [where ?'a = 'a, of k 0] by (simp add: take_bit_eq_0_iff) |
|
510 |
436 definition word_sle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <=s _)" [50, 51] 50) |
511 definition word_sle :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <=s _)" [50, 51] 50) |
437 where "a <=s b \<longleftrightarrow> sint a \<le> sint b" |
512 where "a <=s b \<longleftrightarrow> sint a \<le> sint b" |
438 |
513 |
439 definition word_sless :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <s _)" [50, 51] 50) |
514 definition word_sless :: "'a::len word \<Rightarrow> 'a word \<Rightarrow> bool" ("(_/ <s _)" [50, 51] 50) |
440 where "x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y" |
515 where "x <s y \<longleftrightarrow> x <=s y \<and> x \<noteq> y" |
441 |
516 |
442 |
517 |
443 subsection \<open>Bit-wise operations\<close> |
518 subsection \<open>Bit-wise operations\<close> |
|
519 |
|
520 lemma word_bit_induct [case_names zero even odd]: |
|
521 \<open>P a\<close> if word_zero: \<open>P 0\<close> |
|
522 and word_even: \<open>\<And>a. P a \<Longrightarrow> 0 < a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (2 * a)\<close> |
|
523 and word_odd: \<open>\<And>a. P a \<Longrightarrow> a < 2 ^ (LENGTH('a) - 1) \<Longrightarrow> P (1 + 2 * a)\<close> |
|
524 for P and a :: \<open>'a::len word\<close> |
|
525 proof - |
|
526 define m :: nat where \<open>m = LENGTH('a) - 1\<close> |
|
527 then have l: \<open>LENGTH('a) = Suc m\<close> |
|
528 by simp |
|
529 define n :: nat where \<open>n = unat a\<close> |
|
530 then have \<open>n < 2 ^ LENGTH('a)\<close> |
|
531 by (unfold unat_def) (transfer, simp add: take_bit_eq_mod) |
|
532 then have \<open>n < 2 * 2 ^ m\<close> |
|
533 by (simp add: l) |
|
534 then have \<open>P (of_nat n)\<close> |
|
535 proof (induction n rule: nat_bit_induct) |
|
536 case zero |
|
537 show ?case |
|
538 by simp (rule word_zero) |
|
539 next |
|
540 case (even n) |
|
541 then have \<open>n < 2 ^ m\<close> |
|
542 by simp |
|
543 with even.IH have \<open>P (of_nat n)\<close> |
|
544 by simp |
|
545 moreover from \<open>n < 2 ^ m\<close> even.hyps have \<open>0 < (of_nat n :: 'a word)\<close> |
|
546 by (auto simp add: word_greater_zero_iff of_nat_word_eq_0_iff l) |
|
547 moreover from \<open>n < 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close> |
|
548 using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] |
|
549 by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l) |
|
550 ultimately have \<open>P (2 * of_nat n)\<close> |
|
551 by (rule word_even) |
|
552 then show ?case |
|
553 by simp |
|
554 next |
|
555 case (odd n) |
|
556 then have \<open>Suc n \<le> 2 ^ m\<close> |
|
557 by simp |
|
558 with odd.IH have \<open>P (of_nat n)\<close> |
|
559 by simp |
|
560 moreover from \<open>Suc n \<le> 2 ^ m\<close> have \<open>(of_nat n :: 'a word) < 2 ^ (LENGTH('a) - 1)\<close> |
|
561 using of_nat_word_less_iff [where ?'a = 'a, of n \<open>2 ^ m\<close>] |
|
562 by (cases \<open>m = 0\<close>) (simp_all add: not_less take_bit_eq_self ac_simps l) |
|
563 ultimately have \<open>P (1 + 2 * of_nat n)\<close> |
|
564 by (rule word_odd) |
|
565 then show ?case |
|
566 by simp |
|
567 qed |
|
568 moreover have \<open>of_nat (nat (uint a)) = a\<close> |
|
569 by transfer simp |
|
570 ultimately show ?thesis |
|
571 by (simp add: n_def unat_def) |
|
572 qed |
|
573 |
|
574 lemma bit_word_half_eq: |
|
575 \<open>(of_bool b + a * 2) div 2 = a\<close> |
|
576 if \<open>a < 2 ^ (LENGTH('a) - Suc 0)\<close> |
|
577 for a :: \<open>'a::len word\<close> |
|
578 proof (cases \<open>2 \<le> LENGTH('a::len)\<close>) |
|
579 case False |
|
580 have \<open>of_bool (odd k) < (1 :: int) \<longleftrightarrow> even k\<close> for k :: int |
|
581 by auto |
|
582 with False that show ?thesis |
|
583 by transfer (simp add: eq_iff) |
|
584 next |
|
585 case True |
|
586 obtain n where length: \<open>LENGTH('a) = Suc n\<close> |
|
587 by (cases \<open>LENGTH('a)\<close>) simp_all |
|
588 show ?thesis proof (cases b) |
|
589 case False |
|
590 moreover have \<open>a * 2 div 2 = a\<close> |
|
591 using that proof transfer |
|
592 fix k :: int |
|
593 from length have \<open>k * 2 mod 2 ^ LENGTH('a) = (k mod 2 ^ n) * 2\<close> |
|
594 by simp |
|
595 moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close> |
|
596 with \<open>LENGTH('a) = Suc n\<close> |
|
597 have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close> |
|
598 by (simp add: take_bit_eq_mod divmod_digit_0) |
|
599 ultimately have \<open>take_bit LENGTH('a) (k * 2) = take_bit LENGTH('a) k * 2\<close> |
|
600 by (simp add: take_bit_eq_mod) |
|
601 with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (k * 2) div take_bit LENGTH('a) 2) |
|
602 = take_bit LENGTH('a) k\<close> |
|
603 by simp |
|
604 qed |
|
605 ultimately show ?thesis |
|
606 by simp |
|
607 next |
|
608 case True |
|
609 moreover have \<open>(1 + a * 2) div 2 = a\<close> |
|
610 using that proof transfer |
|
611 fix k :: int |
|
612 from length have \<open>(1 + k * 2) mod 2 ^ LENGTH('a) = 1 + (k mod 2 ^ n) * 2\<close> |
|
613 using pos_zmod_mult_2 [of \<open>2 ^ n\<close> k] by (simp add: ac_simps) |
|
614 moreover assume \<open>take_bit LENGTH('a) k < take_bit LENGTH('a) (2 ^ (LENGTH('a) - Suc 0))\<close> |
|
615 with \<open>LENGTH('a) = Suc n\<close> |
|
616 have \<open>k mod 2 ^ LENGTH('a) = k mod 2 ^ n\<close> |
|
617 by (simp add: take_bit_eq_mod divmod_digit_0) |
|
618 ultimately have \<open>take_bit LENGTH('a) (1 + k * 2) = 1 + take_bit LENGTH('a) k * 2\<close> |
|
619 by (simp add: take_bit_eq_mod) |
|
620 with True show \<open>take_bit LENGTH('a) (take_bit LENGTH('a) (1 + k * 2) div take_bit LENGTH('a) 2) |
|
621 = take_bit LENGTH('a) k\<close> |
|
622 by (auto simp add: take_bit_Suc) |
|
623 qed |
|
624 ultimately show ?thesis |
|
625 by simp |
|
626 qed |
|
627 qed |
|
628 |
|
629 lemma even_mult_exp_div_word_iff: |
|
630 \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> \<not> ( |
|
631 m \<le> n \<and> |
|
632 n < LENGTH('a) \<and> odd (a div 2 ^ (n - m)))\<close> for a :: \<open>'a::len word\<close> |
|
633 by transfer |
|
634 (auto simp flip: drop_bit_eq_div simp add: even_drop_bit_iff_not_bit bit_take_bit_iff, |
|
635 simp_all flip: push_bit_eq_mult add: bit_push_bit_iff_int) |
|
636 |
|
637 instance word :: (len) semiring_bits |
|
638 proof |
|
639 show \<open>P a\<close> if stable: \<open>\<And>a. a div 2 = a \<Longrightarrow> P a\<close> |
|
640 and rec: \<open>\<And>a b. P a \<Longrightarrow> (of_bool b + 2 * a) div 2 = a \<Longrightarrow> P (of_bool b + 2 * a)\<close> |
|
641 for P and a :: \<open>'a word\<close> |
|
642 proof (induction a rule: word_bit_induct) |
|
643 case zero |
|
644 have \<open>0 div 2 = (0::'a word)\<close> |
|
645 by transfer simp |
|
646 with stable [of 0] show ?case |
|
647 by simp |
|
648 next |
|
649 case (even a) |
|
650 with rec [of a False] show ?case |
|
651 using bit_word_half_eq [of a False] by (simp add: ac_simps) |
|
652 next |
|
653 case (odd a) |
|
654 with rec [of a True] show ?case |
|
655 using bit_word_half_eq [of a True] by (simp add: ac_simps) |
|
656 qed |
|
657 show \<open>0 div a = 0\<close> |
|
658 for a :: \<open>'a word\<close> |
|
659 by transfer simp |
|
660 show \<open>a div 1 = a\<close> |
|
661 for a :: \<open>'a word\<close> |
|
662 by transfer simp |
|
663 show \<open>a mod b div b = 0\<close> |
|
664 for a b :: \<open>'a word\<close> |
|
665 apply transfer |
|
666 apply (simp add: take_bit_eq_mod) |
|
667 apply (subst (3) mod_pos_pos_trivial [of _ \<open>2 ^ LENGTH('a)\<close>]) |
|
668 apply simp_all |
|
669 apply (metis le_less mod_by_0 pos_mod_conj zero_less_numeral zero_less_power) |
|
670 using pos_mod_bound [of \<open>2 ^ LENGTH('a)\<close>] apply simp |
|
671 proof - |
|
672 fix aa :: int and ba :: int |
|
673 have f1: "\<And>i n. (i::int) mod 2 ^ n = 0 \<or> 0 < i mod 2 ^ n" |
|
674 by (metis le_less take_bit_eq_mod take_bit_nonnegative) |
|
675 have "(0::int) < 2 ^ len_of (TYPE('a)::'a itself) \<and> ba mod 2 ^ len_of (TYPE('a)::'a itself) \<noteq> 0 \<or> aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" |
|
676 by (metis (no_types) mod_by_0 unique_euclidean_semiring_numeral_class.pos_mod_bound zero_less_numeral zero_less_power) |
|
677 then show "aa mod 2 ^ len_of (TYPE('a)::'a itself) mod (ba mod 2 ^ len_of (TYPE('a)::'a itself)) < 2 ^ len_of (TYPE('a)::'a itself)" |
|
678 using f1 by (meson le_less less_le_trans unique_euclidean_semiring_numeral_class.pos_mod_bound) |
|
679 qed |
|
680 show \<open>(1 + a) div 2 = a div 2\<close> |
|
681 if \<open>even a\<close> |
|
682 for a :: \<open>'a word\<close> |
|
683 using that by transfer (auto dest: le_Suc_ex simp add: take_bit_Suc) |
|
684 show \<open>(2 :: 'a word) ^ m div 2 ^ n = of_bool ((2 :: 'a word) ^ m \<noteq> 0 \<and> n \<le> m) * 2 ^ (m - n)\<close> |
|
685 for m n :: nat |
|
686 by transfer (simp, simp add: exp_div_exp_eq) |
|
687 show "a div 2 ^ m div 2 ^ n = a div 2 ^ (m + n)" |
|
688 for a :: "'a word" and m n :: nat |
|
689 apply transfer |
|
690 apply (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: drop_bit_eq_div) |
|
691 apply (simp add: drop_bit_take_bit) |
|
692 done |
|
693 show "a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n" |
|
694 for a :: "'a word" and m n :: nat |
|
695 by transfer (auto simp flip: take_bit_eq_mod simp add: ac_simps) |
|
696 show \<open>a * 2 ^ m mod 2 ^ n = a mod 2 ^ (n - m) * 2 ^ m\<close> |
|
697 if \<open>m \<le> n\<close> for a :: "'a word" and m n :: nat |
|
698 using that apply transfer |
|
699 apply (auto simp flip: take_bit_eq_mod) |
|
700 apply (auto simp flip: push_bit_eq_mult simp add: push_bit_take_bit split: split_min_lin) |
|
701 done |
|
702 show \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close> |
|
703 for a :: "'a word" and m n :: nat |
|
704 by transfer (auto simp add: not_less take_bit_drop_bit ac_simps simp flip: take_bit_eq_mod drop_bit_eq_div split: split_min_lin) |
|
705 show \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close> |
|
706 for m n :: nat |
|
707 by transfer (auto simp add: take_bit_of_mask even_mask_div_iff) |
|
708 show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n - m))\<close> |
|
709 for a :: \<open>'a word\<close> and m n :: nat |
|
710 proof transfer |
|
711 show \<open>even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \<longleftrightarrow> |
|
712 n < m |
|
713 \<or> take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0 |
|
714 \<or> (m \<le> n \<and> even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\<close> |
|
715 for m n :: nat and k l :: int |
|
716 by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult |
|
717 simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m]) |
|
718 qed |
|
719 qed |
|
720 |
|
721 context |
|
722 includes lifting_syntax |
|
723 begin |
|
724 |
|
725 lemma transfer_rule_bit_word [transfer_rule]: |
|
726 \<open>((pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool) ===> (=)) (\<lambda>k n. n < LENGTH('a) \<and> bit k n) bit\<close> |
|
727 proof - |
|
728 let ?t = \<open>\<lambda>a n. odd (take_bit LENGTH('a) a div take_bit LENGTH('a) ((2::int) ^ n))\<close> |
|
729 have \<open>((pcr_word :: int \<Rightarrow> 'a word \<Rightarrow> bool) ===> (=)) ?t bit\<close> |
|
730 by (unfold bit_def) transfer_prover |
|
731 also have \<open>?t = (\<lambda>k n. n < LENGTH('a) \<and> bit k n)\<close> |
|
732 by (simp add: fun_eq_iff bit_take_bit_iff flip: bit_def) |
|
733 finally show ?thesis . |
|
734 qed |
|
735 |
|
736 end |
444 |
737 |
445 definition shiftl1 :: "'a::len0 word \<Rightarrow> 'a word" |
738 definition shiftl1 :: "'a::len0 word \<Rightarrow> 'a word" |
446 where "shiftl1 w = word_of_int (uint w BIT False)" |
739 where "shiftl1 w = word_of_int (uint w BIT False)" |
447 |
740 |
448 definition shiftr1 :: "'a::len0 word \<Rightarrow> 'a word" |
741 definition shiftr1 :: "'a::len0 word \<Rightarrow> 'a word" |