6 theory Bit_Operations |
6 theory Bit_Operations |
7 imports |
7 imports |
8 "HOL-Library.Boolean_Algebra" |
8 "HOL-Library.Boolean_Algebra" |
9 Main |
9 Main |
10 begin |
10 begin |
11 |
|
12 lemma nat_take_bit_eq: |
|
13 \<open>nat (take_bit n k) = take_bit n (nat k)\<close> |
|
14 if \<open>k \<ge> 0\<close> |
|
15 using that by (simp add: take_bit_eq_mod nat_mod_distrib nat_power_eq) |
|
16 |
|
17 lemma take_bit_eq_self: |
|
18 \<open>take_bit m n = n\<close> if \<open>n < 2 ^ m\<close> for n :: nat |
|
19 using that by (simp add: take_bit_eq_mod) |
|
20 |
|
21 lemma horner_sum_of_bool_2_less: |
|
22 \<open>(horner_sum of_bool 2 bs :: int) < 2 ^ length bs\<close> |
|
23 proof - |
|
24 have \<open>(\<Sum>n = 0..<length bs. of_bool (bs ! n) * (2::int) ^ n) \<le> (\<Sum>n = 0..<length bs. 2 ^ n)\<close> |
|
25 by (rule sum_mono) simp |
|
26 also have \<open>\<dots> = 2 ^ length bs - 1\<close> |
|
27 by (induction bs) simp_all |
|
28 finally show ?thesis |
|
29 by (simp add: horner_sum_eq_sum) |
|
30 qed |
|
31 |
|
32 |
11 |
33 subsection \<open>Bit operations\<close> |
12 subsection \<open>Bit operations\<close> |
34 |
13 |
35 class semiring_bit_operations = semiring_bit_shifts + |
14 class semiring_bit_operations = semiring_bit_shifts + |
36 fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>AND\<close> 64) |
15 fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infixr \<open>AND\<close> 64) |
837 by (cases n) (simp_all add: signed_take_bit_Suc) |
816 by (cases n) (simp_all add: signed_take_bit_Suc) |
838 |
817 |
839 lemma bit_signed_take_bit_iff: |
818 lemma bit_signed_take_bit_iff: |
840 \<open>bit (signed_take_bit m k) n = bit k (min m n)\<close> |
819 \<open>bit (signed_take_bit m k) n = bit k (min m n)\<close> |
841 by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def) |
820 by (simp add: signed_take_bit_def bit_or_iff bit_concat_bit_iff bit_not_iff bit_mask_iff min_def) |
|
821 |
|
822 lemma signed_take_bit_of_0 [simp]: |
|
823 \<open>signed_take_bit n 0 = 0\<close> |
|
824 by (simp add: signed_take_bit_def) |
|
825 |
|
826 lemma signed_take_bit_of_minus_1 [simp]: |
|
827 \<open>signed_take_bit n (- 1) = - 1\<close> |
|
828 by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask) |
|
829 |
|
830 lemma signed_take_bit_signed_take_bit [simp]: |
|
831 \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close> |
|
832 by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff) |
|
833 |
|
834 lemma signed_take_bit_eq_iff_take_bit_eq: |
|
835 \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close> |
|
836 proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>) |
|
837 case True |
|
838 moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close> |
|
839 for k :: int |
|
840 by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask) |
|
841 ultimately show ?thesis |
|
842 by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq) |
|
843 next |
|
844 case False |
|
845 then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close> |
|
846 by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def) |
|
847 then show ?thesis |
|
848 by simp |
|
849 qed |
|
850 |
|
851 lemma take_bit_signed_take_bit: |
|
852 \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close> |
|
853 using that by (rule le_SucE; intro bit_eqI) |
|
854 (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) |
|
855 |
|
856 lemma signed_take_bit_add: |
|
857 \<open>signed_take_bit n (signed_take_bit n k + signed_take_bit n l) = signed_take_bit n (k + l)\<close> |
|
858 proof - |
|
859 have \<open>take_bit (Suc n) |
|
860 (take_bit (Suc n) (signed_take_bit n k) + |
|
861 take_bit (Suc n) (signed_take_bit n l)) = |
|
862 take_bit (Suc n) (k + l)\<close> |
|
863 by (simp add: take_bit_signed_take_bit take_bit_add) |
|
864 then show ?thesis |
|
865 by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_add) |
|
866 qed |
|
867 |
|
868 lemma signed_take_bit_diff: |
|
869 \<open>signed_take_bit n (signed_take_bit n k - signed_take_bit n l) = signed_take_bit n (k - l)\<close> |
|
870 proof - |
|
871 have \<open>take_bit (Suc n) |
|
872 (take_bit (Suc n) (signed_take_bit n k) - |
|
873 take_bit (Suc n) (signed_take_bit n l)) = |
|
874 take_bit (Suc n) (k - l)\<close> |
|
875 by (simp add: take_bit_signed_take_bit take_bit_diff) |
|
876 then show ?thesis |
|
877 by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_diff) |
|
878 qed |
|
879 |
|
880 lemma signed_take_bit_minus: |
|
881 \<open>signed_take_bit n (- signed_take_bit n k) = signed_take_bit n (- k)\<close> |
|
882 proof - |
|
883 have \<open>take_bit (Suc n) |
|
884 (- take_bit (Suc n) (signed_take_bit n k)) = |
|
885 take_bit (Suc n) (- k)\<close> |
|
886 by (simp add: take_bit_signed_take_bit take_bit_minus) |
|
887 then show ?thesis |
|
888 by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_minus) |
|
889 qed |
|
890 |
|
891 lemma signed_take_bit_mult: |
|
892 \<open>signed_take_bit n (signed_take_bit n k * signed_take_bit n l) = signed_take_bit n (k * l)\<close> |
|
893 proof - |
|
894 have \<open>take_bit (Suc n) |
|
895 (take_bit (Suc n) (signed_take_bit n k) * |
|
896 take_bit (Suc n) (signed_take_bit n l)) = |
|
897 take_bit (Suc n) (k * l)\<close> |
|
898 by (simp add: take_bit_signed_take_bit take_bit_mult) |
|
899 then show ?thesis |
|
900 by (simp only: signed_take_bit_eq_iff_take_bit_eq take_bit_mult) |
|
901 qed |
842 |
902 |
843 text \<open>Modulus centered around 0\<close> |
903 text \<open>Modulus centered around 0\<close> |
844 |
904 |
845 lemma signed_take_bit_eq_take_bit_minus: |
905 lemma signed_take_bit_eq_take_bit_minus: |
846 \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close> |
906 \<open>signed_take_bit n k = take_bit (Suc n) k - 2 ^ Suc n * of_bool (bit k n)\<close> |
883 using * ** |
943 using * ** |
884 by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps) |
944 by (simp add: signed_take_bit_def concat_bit_Suc min_def ac_simps) |
885 (simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps) |
945 (simp add: concat_bit_def take_bit_eq_mask push_bit_minus_one_eq_not_mask ac_simps) |
886 qed |
946 qed |
887 |
947 |
888 lemma signed_take_bit_of_0 [simp]: |
|
889 \<open>signed_take_bit n 0 = 0\<close> |
|
890 by (simp add: signed_take_bit_def) |
|
891 |
|
892 lemma signed_take_bit_of_minus_1 [simp]: |
|
893 \<open>signed_take_bit n (- 1) = - 1\<close> |
|
894 by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask take_bit_minus_one_eq_mask) |
|
895 |
|
896 lemma signed_take_bit_eq_iff_take_bit_eq: |
|
897 \<open>signed_take_bit n k = signed_take_bit n l \<longleftrightarrow> take_bit (Suc n) k = take_bit (Suc n) l\<close> |
|
898 proof (cases \<open>bit k n \<longleftrightarrow> bit l n\<close>) |
|
899 case True |
|
900 moreover have \<open>take_bit n k OR NOT (mask n) = take_bit n k - 2 ^ n\<close> |
|
901 for k :: int |
|
902 by (auto simp add: disjunctive_add [symmetric] bit_not_iff bit_mask_iff bit_take_bit_iff minus_exp_eq_not_mask) |
|
903 ultimately show ?thesis |
|
904 by (simp add: signed_take_bit_def take_bit_Suc_from_most concat_bit_eq) |
|
905 next |
|
906 case False |
|
907 then have \<open>signed_take_bit n k \<noteq> signed_take_bit n l\<close> and \<open>take_bit (Suc n) k \<noteq> take_bit (Suc n) l\<close> |
|
908 by (auto simp add: bit_eq_iff bit_take_bit_iff bit_signed_take_bit_iff min_def) |
|
909 then show ?thesis |
|
910 by simp |
|
911 qed |
|
912 |
|
913 lemma signed_take_bit_signed_take_bit [simp]: |
|
914 \<open>signed_take_bit m (signed_take_bit n k) = signed_take_bit (min m n) k\<close> |
|
915 by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_or_iff bit_not_iff bit_mask_iff bit_take_bit_iff) |
|
916 |
|
917 lemma take_bit_signed_take_bit: |
|
918 \<open>take_bit m (signed_take_bit n k) = take_bit m k\<close> if \<open>m \<le> Suc n\<close> |
|
919 using that by (rule le_SucE; intro bit_eqI) |
|
920 (auto simp add: bit_take_bit_iff bit_signed_take_bit_iff min_def less_Suc_eq) |
|
921 |
|
922 lemma signed_take_bit_take_bit: |
948 lemma signed_take_bit_take_bit: |
923 \<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close> |
949 \<open>signed_take_bit m (take_bit n k) = (if n \<le> m then take_bit n else signed_take_bit m) k\<close> |
924 by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff) |
950 by (rule bit_eqI) (auto simp add: bit_signed_take_bit_iff min_def bit_take_bit_iff) |
925 |
951 |
926 lemma signed_take_bit_nonnegative_iff [simp]: |
952 lemma signed_take_bit_nonnegative_iff [simp]: |
938 |
964 |
939 lemma signed_take_bit_less_eq: |
965 lemma signed_take_bit_less_eq: |
940 \<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close> |
966 \<open>signed_take_bit n k \<le> k - 2 ^ Suc n\<close> if \<open>k \<ge> 2 ^ n\<close> |
941 using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>] |
967 using that take_bit_less_eq [of \<open>Suc n\<close> \<open>k + 2 ^ n\<close>] |
942 by (simp add: signed_take_bit_eq_take_bit_shift) |
968 by (simp add: signed_take_bit_eq_take_bit_shift) |
|
969 |
|
970 lemma signed_take_bit_eq_self: |
|
971 \<open>signed_take_bit n k = k\<close> if \<open>- (2 ^ n) \<le> k\<close> \<open>k < 2 ^ n\<close> |
|
972 using that by (simp add: signed_take_bit_eq_take_bit_shift take_bit_int_eq_self) |
943 |
973 |
944 lemma signed_take_bit_Suc_1 [simp]: |
974 lemma signed_take_bit_Suc_1 [simp]: |
945 \<open>signed_take_bit (Suc n) 1 = 1\<close> |
975 \<open>signed_take_bit (Suc n) 1 = 1\<close> |
946 by (simp add: signed_take_bit_Suc) |
976 by (simp add: signed_take_bit_Suc) |
947 |
977 |