equal
deleted
inserted
replaced
750 next |
750 next |
751 assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast |
751 assume ?rhs then obtain q1 q2 where q12: "x + n * q1 = y + n * q2" by blast |
752 hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp |
752 hence "(x + n * q1) mod n = (y + n * q2) mod n" by simp |
753 thus ?lhs by simp |
753 thus ?lhs by simp |
754 qed |
754 qed |
|
755 |
|
756 lemma take_bit_greater_eq: |
|
757 \<open>k + 2 ^ n \<le> take_bit n k\<close> if \<open>k < 0\<close> for k :: int |
|
758 proof - |
|
759 have \<open>k + 2 ^ n \<le> take_bit n (k + 2 ^ n)\<close> |
|
760 proof (cases \<open>k > - (2 ^ n)\<close>) |
|
761 case False |
|
762 then have \<open>k + 2 ^ n \<le> 0\<close> |
|
763 by simp |
|
764 also note take_bit_nonnegative |
|
765 finally show ?thesis . |
|
766 next |
|
767 case True |
|
768 with that have \<open>0 \<le> k + 2 ^ n\<close> and \<open>k + 2 ^ n < 2 ^ n\<close> |
|
769 by simp_all |
|
770 then show ?thesis |
|
771 by (simp only: take_bit_eq_mod mod_pos_pos_trivial) |
|
772 qed |
|
773 then show ?thesis |
|
774 by (simp add: take_bit_eq_mod) |
|
775 qed |
|
776 |
|
777 lemma take_bit_less_eq: |
|
778 \<open>take_bit n k \<le> k - 2 ^ n\<close> if \<open>2 ^ n \<le> k\<close> and \<open>n > 0\<close> for k :: int |
|
779 using that zmod_le_nonneg_dividend [of \<open>k - 2 ^ n\<close> \<open>2 ^ n\<close>] |
|
780 by (simp add: take_bit_eq_mod) |
755 |
781 |
756 |
782 |
757 subsection \<open>Numeral division with a pragmatic type class\<close> |
783 subsection \<open>Numeral division with a pragmatic type class\<close> |
758 |
784 |
759 text \<open> |
785 text \<open> |