equal
deleted
inserted
replaced
151 qed |
151 qed |
152 |
152 |
153 lemma mask_numeral: |
153 lemma mask_numeral: |
154 \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close> |
154 \<open>mask (numeral n) = 1 + 2 * mask (pred_numeral n)\<close> |
155 by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps) |
155 by (simp add: numeral_eq_Suc mask_Suc_double one_or_eq ac_simps) |
|
156 |
|
157 lemma take_bit_mask [simp]: |
|
158 \<open>take_bit m (mask n) = mask (min m n)\<close> |
|
159 by (rule bit_eqI) (simp add: bit_simps) |
156 |
160 |
157 lemma take_bit_eq_mask: |
161 lemma take_bit_eq_mask: |
158 \<open>take_bit n a = a AND mask n\<close> |
162 \<open>take_bit n a = a AND mask n\<close> |
159 by (rule bit_eqI) |
163 by (rule bit_eqI) |
160 (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff) |
164 (auto simp add: bit_take_bit_iff bit_and_iff bit_mask_iff) |
964 apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff) |
968 apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff) |
965 done |
969 done |
966 qed |
970 qed |
967 qed |
971 qed |
968 |
972 |
|
973 lemma take_bit_eq_mask_iff: |
|
974 \<open>take_bit n k = mask n \<longleftrightarrow> take_bit n (k + 1) = 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) |
|
975 for k :: int |
|
976 proof |
|
977 assume ?P |
|
978 then have \<open>take_bit n (take_bit n k + take_bit n 1) = 0\<close> |
|
979 by (simp add: mask_eq_exp_minus_1) |
|
980 then show ?Q |
|
981 by (simp only: take_bit_add) |
|
982 next |
|
983 assume ?Q |
|
984 then have \<open>take_bit n (k + 1) - 1 = - 1\<close> |
|
985 by simp |
|
986 then have \<open>take_bit n (take_bit n (k + 1) - 1) = take_bit n (- 1)\<close> |
|
987 by simp |
|
988 moreover have \<open>take_bit n (take_bit n (k + 1) - 1) = take_bit n k\<close> |
|
989 by (simp add: take_bit_eq_mod mod_simps) |
|
990 ultimately show ?P |
|
991 by (simp add: take_bit_minus_one_eq_mask) |
|
992 qed |
|
993 |
|
994 lemma take_bit_eq_mask_iff_exp_dvd: |
|
995 \<open>take_bit n k = mask n \<longleftrightarrow> 2 ^ n dvd k + 1\<close> |
|
996 for k :: int |
|
997 by (simp add: take_bit_eq_mask_iff flip: take_bit_eq_0_iff) |
|
998 |
969 context ring_bit_operations |
999 context ring_bit_operations |
970 begin |
1000 begin |
971 |
1001 |
972 lemma even_of_int_iff: |
1002 lemma even_of_int_iff: |
973 \<open>even (of_int k) \<longleftrightarrow> even k\<close> |
1003 \<open>even (of_int k) \<longleftrightarrow> even k\<close> |
1629 \<open>of_nat (mask n) = mask n\<close> |
1659 \<open>of_nat (mask n) = mask n\<close> |
1630 by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq) |
1660 by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq) |
1631 |
1661 |
1632 end |
1662 end |
1633 |
1663 |
|
1664 lemma Suc_mask_eq_exp: |
|
1665 \<open>Suc (mask n) = 2 ^ n\<close> |
|
1666 by (simp add: mask_eq_exp_minus_1) |
|
1667 |
|
1668 lemma less_eq_mask: |
|
1669 \<open>n \<le> mask n\<close> |
|
1670 by (simp add: mask_eq_exp_minus_1 le_diff_conv2) |
|
1671 (metis Suc_mask_eq_exp diff_Suc_1 diff_le_diff_pow diff_zero le_refl not_less_eq_eq power_0) |
|
1672 |
|
1673 lemma less_mask: |
|
1674 \<open>n < mask n\<close> if \<open>Suc 0 < n\<close> |
|
1675 proof - |
|
1676 define m where \<open>m = n - 2\<close> |
|
1677 with that have *: \<open>n = m + 2\<close> |
|
1678 by simp |
|
1679 have \<open>Suc (Suc (Suc m)) < 4 * 2 ^ m\<close> |
|
1680 by (induction m) simp_all |
|
1681 then have \<open>Suc (m + 2) < Suc (mask (m + 2))\<close> |
|
1682 by (simp add: Suc_mask_eq_exp) |
|
1683 then have \<open>m + 2 < mask (m + 2)\<close> |
|
1684 by (simp add: less_le) |
|
1685 with * show ?thesis |
|
1686 by simp |
|
1687 qed |
|
1688 |
1634 |
1689 |
1635 subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close> |
1690 subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close> |
1636 |
1691 |
1637 unbundle integer.lifting natural.lifting |
1692 unbundle integer.lifting natural.lifting |
1638 |
1693 |