735 apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff) |
735 apply (clarsimp simp add: bit_and_iff bit_not_iff bit_exp_iff) |
736 done |
736 done |
737 qed |
737 qed |
738 qed |
738 qed |
739 |
739 |
|
740 context ring_bit_operations |
|
741 begin |
|
742 |
|
743 lemma even_of_int_iff: |
|
744 \<open>even (of_int k) \<longleftrightarrow> even k\<close> |
|
745 by (induction k rule: int_bit_induct) simp_all |
|
746 |
|
747 lemma bit_of_int_iff: |
|
748 \<open>bit (of_int k) n \<longleftrightarrow> (2::'a) ^ n \<noteq> 0 \<and> bit k n\<close> |
|
749 proof (cases \<open>(2::'a) ^ n = 0\<close>) |
|
750 case True |
|
751 then show ?thesis |
|
752 by (simp add: exp_eq_0_imp_not_bit) |
|
753 next |
|
754 case False |
|
755 then have \<open>bit (of_int k) n \<longleftrightarrow> bit k n\<close> |
|
756 proof (induction k arbitrary: n rule: int_bit_induct) |
|
757 case zero |
|
758 then show ?case |
|
759 by simp |
|
760 next |
|
761 case minus |
|
762 then show ?case |
|
763 by simp |
|
764 next |
|
765 case (even k) |
|
766 then show ?case |
|
767 using bit_double_iff [of \<open>of_int k\<close> n] Parity.bit_double_iff [of k n] |
|
768 by (cases n) (auto simp add: ac_simps dest: mult_not_zero) |
|
769 next |
|
770 case (odd k) |
|
771 then show ?case |
|
772 using bit_double_iff [of \<open>of_int k\<close> n] |
|
773 by (cases n) (auto simp add: ac_simps bit_double_iff even_bit_succ_iff Parity.bit_Suc dest: mult_not_zero) |
|
774 qed |
|
775 with False show ?thesis |
|
776 by simp |
|
777 qed |
|
778 |
|
779 lemma push_bit_of_int: |
|
780 \<open>push_bit n (of_int k) = of_int (push_bit n k)\<close> |
|
781 by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult) |
|
782 |
|
783 lemma of_int_push_bit: |
|
784 \<open>of_int (push_bit n k) = push_bit n (of_int k)\<close> |
|
785 by (simp add: push_bit_eq_mult semiring_bit_shifts_class.push_bit_eq_mult) |
|
786 |
|
787 lemma take_bit_of_int: |
|
788 \<open>take_bit n (of_int k) = of_int (take_bit n k)\<close> |
|
789 by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff) |
|
790 |
|
791 lemma of_int_take_bit: |
|
792 \<open>of_int (take_bit n k) = take_bit n (of_int k)\<close> |
|
793 by (rule bit_eqI) (simp add: bit_take_bit_iff Parity.bit_take_bit_iff bit_of_int_iff) |
|
794 |
|
795 lemma of_int_not_eq: |
|
796 \<open>of_int (NOT k) = NOT (of_int k)\<close> |
|
797 by (rule bit_eqI) (simp add: bit_not_iff Bit_Operations.bit_not_iff bit_of_int_iff) |
|
798 |
|
799 lemma of_int_and_eq: |
|
800 \<open>of_int (k AND l) = of_int k AND of_int l\<close> |
|
801 by (rule bit_eqI) (simp add: bit_of_int_iff bit_and_iff Bit_Operations.bit_and_iff) |
|
802 |
|
803 lemma of_int_or_eq: |
|
804 \<open>of_int (k OR l) = of_int k OR of_int l\<close> |
|
805 by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff) |
|
806 |
|
807 lemma of_int_xor_eq: |
|
808 \<open>of_int (k XOR l) = of_int k XOR of_int l\<close> |
|
809 by (rule bit_eqI) (simp add: bit_of_int_iff bit_xor_iff Bit_Operations.bit_xor_iff) |
|
810 |
|
811 lemma of_int_mask_eq: |
|
812 \<open>of_int (mask n) = mask n\<close> |
|
813 by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_int_or_eq) |
|
814 |
|
815 end |
|
816 |
740 |
817 |
741 subsection \<open>Bit concatenation\<close> |
818 subsection \<open>Bit concatenation\<close> |
742 |
819 |
743 definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close> |
820 definition concat_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int\<close> |
744 where \<open>concat_bit n k l = (k AND mask n) OR push_bit n l\<close> |
821 where \<open>concat_bit n k l = take_bit n k OR push_bit n l\<close> |
745 |
822 |
746 lemma bit_concat_bit_iff: |
823 lemma bit_concat_bit_iff: |
747 \<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close> |
824 \<open>bit (concat_bit m k l) n \<longleftrightarrow> n < m \<and> bit k n \<or> m \<le> n \<and> bit l (n - m)\<close> |
748 by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_mask_iff bit_push_bit_iff ac_simps) |
825 by (simp add: concat_bit_def bit_or_iff bit_and_iff bit_take_bit_iff bit_push_bit_iff ac_simps) |
749 |
826 |
750 lemma concat_bit_eq: |
827 lemma concat_bit_eq: |
751 \<open>concat_bit n k l = take_bit n k + push_bit n l\<close> |
828 \<open>concat_bit n k l = take_bit n k + push_bit n l\<close> |
752 by (simp add: concat_bit_def take_bit_eq_mask |
829 by (simp add: concat_bit_def take_bit_eq_mask |
753 bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add) |
830 bit_and_iff bit_mask_iff bit_push_bit_iff disjunctive_add) |
782 |
859 |
783 lemma concat_bit_assoc_sym: |
860 lemma concat_bit_assoc_sym: |
784 \<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\<close> |
861 \<open>concat_bit m (concat_bit n k l) r = concat_bit (min m n) k (concat_bit (m - n) l r)\<close> |
785 by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def) |
862 by (rule bit_eqI) (auto simp add: bit_concat_bit_iff ac_simps min_def) |
786 |
863 |
|
864 lemma concat_bit_eq_iff: |
|
865 \<open>concat_bit n k l = concat_bit n r s |
|
866 \<longleftrightarrow> take_bit n k = take_bit n r \<and> l = s\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) |
|
867 proof |
|
868 assume ?Q |
|
869 then show ?P |
|
870 by (simp add: concat_bit_def) |
|
871 next |
|
872 assume ?P |
|
873 then have *: \<open>bit (concat_bit n k l) m = bit (concat_bit n r s) m\<close> for m |
|
874 by (simp add: bit_eq_iff) |
|
875 have \<open>take_bit n k = take_bit n r\<close> |
|
876 proof (rule bit_eqI) |
|
877 fix m |
|
878 from * [of m] |
|
879 show \<open>bit (take_bit n k) m \<longleftrightarrow> bit (take_bit n r) m\<close> |
|
880 by (auto simp add: bit_take_bit_iff bit_concat_bit_iff) |
|
881 qed |
|
882 moreover have \<open>push_bit n l = push_bit n s\<close> |
|
883 proof (rule bit_eqI) |
|
884 fix m |
|
885 from * [of m] |
|
886 show \<open>bit (push_bit n l) m \<longleftrightarrow> bit (push_bit n s) m\<close> |
|
887 by (auto simp add: bit_push_bit_iff bit_concat_bit_iff) |
|
888 qed |
|
889 then have \<open>l = s\<close> |
|
890 by (simp add: push_bit_eq_mult) |
|
891 ultimately show ?Q |
|
892 by (simp add: concat_bit_def) |
|
893 qed |
|
894 |
|
895 lemma take_bit_concat_bit_eq: |
|
896 \<open>take_bit m (concat_bit n k l) = concat_bit (min m n) k (take_bit (m - n) l)\<close> |
|
897 by (rule bit_eqI) |
|
898 (auto simp add: bit_take_bit_iff bit_concat_bit_iff min_def) |
|
899 |
787 |
900 |
788 subsection \<open>Taking bit with sign propagation\<close> |
901 subsection \<open>Taking bit with sign propagation\<close> |
789 |
902 |
790 definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
903 definition signed_take_bit :: \<open>nat \<Rightarrow> int \<Rightarrow> int\<close> |
791 where \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close> |
904 where \<open>signed_take_bit n k = concat_bit n k (- of_bool (bit k n))\<close> |
|
905 |
|
906 lemma signed_take_bit_unfold: |
|
907 \<open>signed_take_bit n k = take_bit n k OR (of_bool (bit k n) * NOT (mask n))\<close> |
|
908 by (simp add: signed_take_bit_def concat_bit_def push_bit_minus_one_eq_not_mask) |
792 |
909 |
793 lemma signed_take_bit_eq: |
910 lemma signed_take_bit_eq: |
794 \<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close> |
911 \<open>signed_take_bit n k = take_bit n k\<close> if \<open>\<not> bit k n\<close> |
795 using that by (simp add: signed_take_bit_def) |
912 using that by (simp add: signed_take_bit_def) |
796 |
913 |
1042 where \<open>mask n = (2 :: nat) ^ n - 1\<close> |
1159 where \<open>mask n = (2 :: nat) ^ n - 1\<close> |
1043 |
1160 |
1044 instance proof |
1161 instance proof |
1045 fix m n q :: nat |
1162 fix m n q :: nat |
1046 show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close> |
1163 show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close> |
1047 by (auto simp add: and_nat_def bit_and_iff less_le bit_eq_iff) |
1164 by (auto simp add: bit_nat_iff and_nat_def bit_and_iff less_le bit_eq_iff) |
1048 show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close> |
1165 show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close> |
1049 by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff) |
1166 by (auto simp add: bit_nat_iff or_nat_def bit_or_iff less_le bit_eq_iff) |
1050 show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close> |
1167 show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close> |
1051 by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff) |
1168 by (auto simp add: bit_nat_iff xor_nat_def bit_xor_iff less_le bit_eq_iff) |
1052 qed (simp add: mask_nat_def) |
1169 qed (simp add: mask_nat_def) |
1053 |
1170 |
1054 end |
1171 end |
1055 |
1172 |
1056 lemma and_nat_rec: |
1173 lemma and_nat_rec: |
1086 using one_xor_eq [of n] by simp |
1203 using one_xor_eq [of n] by simp |
1087 |
1204 |
1088 lemma xor_Suc_0_eq: |
1205 lemma xor_Suc_0_eq: |
1089 \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close> |
1206 \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close> |
1090 using xor_one_eq [of n] by simp |
1207 using xor_one_eq [of n] by simp |
|
1208 |
|
1209 context semiring_bit_operations |
|
1210 begin |
|
1211 |
|
1212 lemma of_nat_and_eq: |
|
1213 \<open>of_nat (m AND n) = of_nat m AND of_nat n\<close> |
|
1214 by (rule bit_eqI) (simp add: bit_of_nat_iff bit_and_iff Bit_Operations.bit_and_iff) |
|
1215 |
|
1216 lemma of_nat_or_eq: |
|
1217 \<open>of_nat (m OR n) = of_nat m OR of_nat n\<close> |
|
1218 by (rule bit_eqI) (simp add: bit_of_nat_iff bit_or_iff Bit_Operations.bit_or_iff) |
|
1219 |
|
1220 lemma of_nat_xor_eq: |
|
1221 \<open>of_nat (m XOR n) = of_nat m XOR of_nat n\<close> |
|
1222 by (rule bit_eqI) (simp add: bit_of_nat_iff bit_xor_iff Bit_Operations.bit_xor_iff) |
|
1223 |
|
1224 end |
|
1225 |
|
1226 context ring_bit_operations |
|
1227 begin |
|
1228 |
|
1229 lemma of_nat_mask_eq: |
|
1230 \<open>of_nat (mask n) = mask n\<close> |
|
1231 by (induction n) (simp_all add: mask_Suc_double Bit_Operations.mask_Suc_double of_nat_or_eq) |
|
1232 |
|
1233 end |
1091 |
1234 |
1092 |
1235 |
1093 subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close> |
1236 subsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close> |
1094 |
1237 |
1095 unbundle integer.lifting natural.lifting |
1238 unbundle integer.lifting natural.lifting |
1222 \<^item> Truncation centered towards \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]} |
1365 \<^item> Truncation centered towards \<^term>\<open>0::int\<close>: @{thm signed_take_bit_def [no_vars]} |
1223 |
1366 |
1224 \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} |
1367 \<^item> (Bounded) conversion from and to a list of bits: @{thm horner_sum_bit_eq_take_bit [where ?'a = int, no_vars]} |
1225 \<close> |
1368 \<close> |
1226 |
1369 |
|
1370 context semiring_bit_operations |
|
1371 begin |
|
1372 |
|
1373 lemma push_bit_and [simp]: |
|
1374 \<open>push_bit n (a AND b) = push_bit n a AND push_bit n b\<close> |
|
1375 by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_and_iff) |
|
1376 |
|
1377 lemma push_bit_or [simp]: |
|
1378 \<open>push_bit n (a OR b) = push_bit n a OR push_bit n b\<close> |
|
1379 by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_or_iff) |
|
1380 |
|
1381 lemma push_bit_xor [simp]: |
|
1382 \<open>push_bit n (a XOR b) = push_bit n a XOR push_bit n b\<close> |
|
1383 by (rule bit_eqI) (auto simp add: bit_push_bit_iff bit_xor_iff) |
|
1384 |
|
1385 lemma drop_bit_and [simp]: |
|
1386 \<open>drop_bit n (a AND b) = drop_bit n a AND drop_bit n b\<close> |
|
1387 by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_and_iff) |
|
1388 |
|
1389 lemma drop_bit_or [simp]: |
|
1390 \<open>drop_bit n (a OR b) = drop_bit n a OR drop_bit n b\<close> |
|
1391 by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_or_iff) |
|
1392 |
|
1393 lemma drop_bit_xor [simp]: |
|
1394 \<open>drop_bit n (a XOR b) = drop_bit n a XOR drop_bit n b\<close> |
|
1395 by (rule bit_eqI) (auto simp add: bit_drop_bit_eq bit_xor_iff) |
|
1396 |
1227 end |
1397 end |
|
1398 |
|
1399 end |