917 by transfer (auto simp add: bit_xor_iff) |
917 by transfer (auto simp add: bit_xor_iff) |
918 qed |
918 qed |
919 |
919 |
920 end |
920 end |
921 |
921 |
922 instantiation word :: (len) bit_operations |
922 instantiation word :: (len) semiring_bit_syntax |
923 begin |
923 begin |
924 |
924 |
925 definition word_test_bit_def: "test_bit a = bin_nth (uint a)" |
925 definition word_test_bit_def: "test_bit a = bin_nth (uint a)" |
926 |
926 |
927 definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))" |
|
928 |
|
929 definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)" |
|
930 |
|
931 definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1" |
|
932 |
|
933 definition shiftl_def: "w << n = (shiftl1 ^^ n) w" |
927 definition shiftl_def: "w << n = (shiftl1 ^^ n) w" |
934 |
928 |
935 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w" |
929 definition shiftr_def: "w >> n = (shiftr1 ^^ n) w" |
936 |
|
937 instance .. |
|
938 |
|
939 end |
|
940 |
930 |
941 lemma test_bit_word_eq: |
931 lemma test_bit_word_eq: |
942 \<open>test_bit w = bit w\<close> for w :: \<open>'a::len word\<close> |
932 \<open>test_bit w = bit w\<close> for w :: \<open>'a::len word\<close> |
943 apply (simp add: word_test_bit_def fun_eq_iff) |
933 apply (simp add: word_test_bit_def fun_eq_iff) |
944 apply transfer |
934 apply transfer |
945 apply (simp add: bit_take_bit_iff) |
935 apply (simp add: bit_take_bit_iff) |
946 done |
936 done |
947 |
937 |
948 lemma set_bit_unfold: |
|
949 \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close> |
|
950 for w :: \<open>'a::len word\<close> |
|
951 apply (auto simp add: word_set_bit_def bin_clr_conv_NAND bin_set_conv_OR unset_bit_def set_bit_def shiftl_int_def push_bit_of_1; transfer) |
|
952 apply simp_all |
|
953 done |
|
954 |
|
955 lemma bit_set_bit_word_iff: |
|
956 \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close> |
|
957 for w :: \<open>'a::len word\<close> |
|
958 by (auto simp add: set_bit_unfold bit_unset_bit_iff bit_set_bit_iff exp_eq_zero_iff not_le bit_imp_le_length) |
|
959 |
|
960 lemma lsb_word_eq: |
|
961 \<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close> |
|
962 apply (simp add: word_lsb_def fun_eq_iff) |
|
963 apply transfer |
|
964 apply simp |
|
965 done |
|
966 |
|
967 lemma msb_word_eq: |
|
968 \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close> |
|
969 apply (simp add: msb_word_def bin_sign_lem) |
|
970 apply transfer |
|
971 apply (simp add: bit_take_bit_iff) |
|
972 done |
|
973 |
|
974 lemma shiftl_word_eq: |
938 lemma shiftl_word_eq: |
975 \<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close> |
939 \<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close> |
976 by (induction n) (simp_all add: shiftl_def shiftl1_eq_mult_2 push_bit_double) |
940 by (induction n) (simp_all add: shiftl_def shiftl1_eq_mult_2 push_bit_double) |
|
941 |
|
942 lemma shiftr_word_eq: |
|
943 \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close> |
|
944 by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half) |
|
945 |
|
946 instance by standard |
|
947 (simp_all add: fun_eq_iff test_bit_word_eq shiftl_word_eq shiftr_word_eq) |
|
948 |
|
949 end |
977 |
950 |
978 lemma bit_shiftl_word_iff: |
951 lemma bit_shiftl_word_iff: |
979 \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close> |
952 \<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close> |
980 for w :: \<open>'a::len word\<close> |
953 for w :: \<open>'a::len word\<close> |
981 by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) |
954 by (simp add: shiftl_word_eq bit_push_bit_iff exp_eq_zero_iff not_le) |
982 |
955 |
983 lemma [code]: |
956 lemma [code]: |
984 \<open>push_bit n w = w << n\<close> for w :: \<open>'a::len word\<close> |
957 \<open>push_bit n w = w << n\<close> for w :: \<open>'a::len word\<close> |
985 by (simp add: shiftl_word_eq) |
958 by (simp add: shiftl_word_eq) |
986 |
959 |
987 lemma shiftr_word_eq: |
|
988 \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close> |
|
989 by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half) |
|
990 |
|
991 lemma bit_shiftr_word_iff: |
960 lemma bit_shiftr_word_iff: |
992 \<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close> |
961 \<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close> |
993 for w :: \<open>'a::len word\<close> |
962 for w :: \<open>'a::len word\<close> |
994 by (simp add: shiftr_word_eq bit_drop_bit_eq) |
963 by (simp add: shiftr_word_eq bit_drop_bit_eq) |
995 |
964 |
1002 by (fact take_bit_eq_mask) |
971 by (fact take_bit_eq_mask) |
1003 |
972 |
1004 lemma [code_abbrev]: |
973 lemma [code_abbrev]: |
1005 \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> |
974 \<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close> |
1006 by (fact push_bit_of_1) |
975 by (fact push_bit_of_1) |
1007 |
|
1008 lemma word_msb_def: |
|
1009 "msb a \<longleftrightarrow> bin_sign (sint a) = - 1" |
|
1010 by (simp add: msb_word_def sint_uint) |
|
1011 |
976 |
1012 lemma [code]: |
977 lemma [code]: |
1013 shows word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" |
978 shows word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))" |
1014 and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" |
979 and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)" |
1015 and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" |
980 and word_or_def: "(a::'a word) OR b = word_of_int (uint a OR uint b)" |
1016 and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" |
981 and word_xor_def: "(a::'a word) XOR b = word_of_int (uint a XOR uint b)" |
1017 by (transfer, simp add: take_bit_not_take_bit)+ |
982 by (transfer, simp add: take_bit_not_take_bit)+ |
1018 |
983 |
1019 definition setBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" |
984 definition setBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" |
1020 where "setBit w n = set_bit w n True" |
985 where \<open>setBit w n = Bit_Operations.set_bit n w\<close> |
1021 |
|
1022 lemma setBit_eq_set_bit: |
|
1023 \<open>setBit w n = Bit_Operations.set_bit n w\<close> |
|
1024 for w :: \<open>'a::len word\<close> |
|
1025 by (simp add: setBit_def set_bit_unfold) |
|
1026 |
986 |
1027 lemma bit_setBit_iff: |
987 lemma bit_setBit_iff: |
1028 \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close> |
988 \<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close> |
1029 for w :: \<open>'a::len word\<close> |
989 for w :: \<open>'a::len word\<close> |
1030 by (simp add: setBit_eq_set_bit bit_set_bit_iff exp_eq_zero_iff not_le ac_simps) |
990 by (simp add: setBit_def bit_set_bit_iff exp_eq_zero_iff not_le ac_simps) |
1031 |
991 |
1032 definition clearBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" |
992 definition clearBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word" |
1033 where "clearBit w n = set_bit w n False" |
993 where \<open>clearBit w n = unset_bit n w\<close> |
1034 |
|
1035 lemma clearBit_eq_unset_bit: |
|
1036 \<open>clearBit w n = unset_bit n w\<close> |
|
1037 for w :: \<open>'a::len word\<close> |
|
1038 by (simp add: clearBit_def set_bit_unfold) |
|
1039 |
994 |
1040 lemma bit_clearBit_iff: |
995 lemma bit_clearBit_iff: |
1041 \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close> |
996 \<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close> |
1042 for w :: \<open>'a::len word\<close> |
997 for w :: \<open>'a::len word\<close> |
1043 by (simp add: clearBit_eq_unset_bit bit_unset_bit_iff ac_simps) |
998 by (simp add: clearBit_def bit_unset_bit_iff ac_simps) |
1044 |
999 |
1045 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> |
1000 definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close> |
1046 where [code_abbrev]: \<open>even_word = even\<close> |
1001 where [code_abbrev]: \<open>even_word = even\<close> |
1047 |
1002 |
1048 lemma even_word_iff [code]: |
1003 lemma even_word_iff [code]: |
1775 lemmas slice_def' = slice_def [unfolded word_size] |
1730 lemmas slice_def' = slice_def [unfolded word_size] |
1776 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] |
1731 lemmas test_bit_def' = word_test_bit_def [THEN fun_cong] |
1777 |
1732 |
1778 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def |
1733 lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def |
1779 |
1734 |
|
1735 lemma bit_last_iff: |
|
1736 \<open>bit w (LENGTH('a) - Suc 0) \<longleftrightarrow> sint w < 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>) |
|
1737 for w :: \<open>'a::len word\<close> |
|
1738 proof - |
|
1739 have \<open>?P \<longleftrightarrow> bit (uint w) (LENGTH('a) - Suc 0)\<close> |
|
1740 by (simp add: bit_uint_iff) |
|
1741 also have \<open>\<dots> \<longleftrightarrow> ?Q\<close> |
|
1742 by (simp add: sint_uint bin_sign_def flip: bin_sign_lem) |
|
1743 finally show ?thesis . |
|
1744 qed |
|
1745 |
|
1746 lemma drop_bit_eq_zero_iff_not_bit_last: |
|
1747 \<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close> |
|
1748 for w :: "'a::len word" |
|
1749 apply (cases \<open>LENGTH('a)\<close>) |
|
1750 apply simp_all |
|
1751 apply (simp add: bit_iff_odd_drop_bit) |
|
1752 apply transfer |
|
1753 apply (simp add: take_bit_drop_bit) |
|
1754 apply (auto simp add: drop_bit_eq_div take_bit_eq_mod min_def) |
|
1755 apply (auto elim!: evenE) |
|
1756 apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral) |
|
1757 done |
|
1758 |
1780 |
1759 |
1781 subsection \<open>Word Arithmetic\<close> |
1760 subsection \<open>Word Arithmetic\<close> |
1782 |
1761 |
1783 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" |
1762 lemma word_less_alt: "a < b \<longleftrightarrow> uint a < uint b" |
1784 by (fact word_less_def) |
1763 by (fact word_less_def) |
3059 |
3041 |
3060 lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)" |
3042 lemma bl_word_and: "to_bl (v AND w) = map2 (\<and>) (to_bl v) (to_bl w)" |
3061 unfolding to_bl_def word_log_defs bl_and_bin |
3043 unfolding to_bl_def word_log_defs bl_and_bin |
3062 by (simp add: word_ubin.eq_norm) |
3044 by (simp add: word_ubin.eq_norm) |
3063 |
3045 |
3064 lemma word_lsb_alt: "lsb w = test_bit w 0" |
|
3065 for w :: "'a::len word" |
|
3066 by (auto simp: word_test_bit_def word_lsb_def) |
|
3067 |
|
3068 lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)" |
|
3069 unfolding word_lsb_def uint_eq_0 uint_1 by simp |
|
3070 |
|
3071 lemma word_lsb_last: "lsb w = last (to_bl w)" |
|
3072 for w :: "'a::len word" |
|
3073 apply (unfold word_lsb_def uint_bl bin_to_bl_def) |
|
3074 apply (rule_tac bin="uint w" in bin_exhaust) |
|
3075 apply (cases "size w") |
|
3076 apply auto |
|
3077 apply (auto simp add: bin_to_bl_aux_alt) |
|
3078 done |
|
3079 |
|
3080 lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1" |
|
3081 by (auto simp: word_lsb_def bin_last_def) |
|
3082 |
|
3083 lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0" |
|
3084 by (simp only: word_msb_def sign_Min_lt_0) |
|
3085 |
|
3086 lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)" |
|
3087 by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem) |
|
3088 |
|
3089 lemma word_msb_numeral [simp]: |
|
3090 "msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)" |
|
3091 unfolding word_numeral_alt by (rule msb_word_of_int) |
|
3092 |
|
3093 lemma word_msb_neg_numeral [simp]: |
|
3094 "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)" |
|
3095 unfolding word_neg_numeral_alt by (rule msb_word_of_int) |
|
3096 |
|
3097 lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)" |
|
3098 by (simp add: word_msb_def) |
|
3099 |
|
3100 lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1" |
|
3101 unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat] |
|
3102 by (simp add: Suc_le_eq) |
|
3103 |
|
3104 lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)" |
|
3105 for w :: "'a::len word" |
|
3106 by (simp add: word_msb_def sint_uint bin_sign_lem) |
|
3107 |
|
3108 lemma word_msb_alt: "msb w = hd (to_bl w)" |
|
3109 for w :: "'a::len word" |
|
3110 apply (unfold word_msb_nth uint_bl) |
|
3111 apply (subst hd_conv_nth) |
|
3112 apply (rule length_greater_0_conv [THEN iffD1]) |
|
3113 apply simp |
|
3114 apply (simp add : nth_bin_to_bl word_size) |
|
3115 done |
|
3116 |
|
3117 lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w" |
|
3118 for w :: "'a::len word" |
|
3119 by (auto simp: word_test_bit_def word_set_bit_def) |
|
3120 |
|
3121 lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w" |
3046 lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w" |
3122 apply (unfold word_size) |
3047 apply (unfold word_size) |
3123 apply (safe elim!: bin_nth_uint_imp) |
3048 apply (safe elim!: bin_nth_uint_imp) |
3124 apply (frule bin_nth_uint_imp) |
3049 apply (frule bin_nth_uint_imp) |
3125 apply (fast dest!: bin_nth_bl)+ |
3050 apply (fast dest!: bin_nth_bl)+ |
3161 lemma nth_to_bl: |
3086 lemma nth_to_bl: |
3162 \<open>to_bl w ! n \<longleftrightarrow> bit w (LENGTH('a) - Suc n)\<close> |
3087 \<open>to_bl w ! n \<longleftrightarrow> bit w (LENGTH('a) - Suc n)\<close> |
3163 if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
3088 if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close> |
3164 using that by (simp add: to_bl_unfold rev_nth) |
3089 using that by (simp add: to_bl_unfold rev_nth) |
3165 |
3090 |
3166 lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x" |
|
3167 for w :: "'a::len word" |
|
3168 by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr) |
|
3169 |
|
3170 lemma test_bit_set_gen: |
|
3171 "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)" |
|
3172 for w :: "'a::len word" |
|
3173 apply (unfold word_size word_test_bit_def word_set_bit_def) |
|
3174 apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen) |
|
3175 apply (auto elim!: test_bit_size [unfolded word_size] |
|
3176 simp add: word_test_bit_def [symmetric]) |
|
3177 done |
|
3178 |
|
3179 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" |
3091 lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs" |
3180 by (auto simp: of_bl_def bl_to_bin_rep_F) |
3092 by (auto simp: of_bl_def bl_to_bin_rep_F) |
3181 |
3093 |
3182 lemma bit_word_reverse_iff: |
3094 lemma bit_word_reverse_iff: |
3183 \<open>bit (word_reverse w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w (LENGTH('a) - Suc n)\<close> |
3095 \<open>bit (word_reverse w) n \<longleftrightarrow> n < LENGTH('a) \<and> bit w (LENGTH('a) - Suc n)\<close> |
3200 lemma bit_slice_iff: |
3112 lemma bit_slice_iff: |
3201 \<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close> |
3113 \<open>bit (slice m w :: 'b::len word) n \<longleftrightarrow> n < min LENGTH('b) (LENGTH('a) - m) \<and> bit w (n + LENGTH('a) - (LENGTH('a) - m))\<close> |
3202 for w :: \<open>'a::len word\<close> |
3114 for w :: \<open>'a::len word\<close> |
3203 by (simp add: slice_def word_size bit_slice1_iff) |
3115 by (simp add: slice_def word_size bit_slice1_iff) |
3204 |
3116 |
3205 lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)" |
|
3206 for w :: "'a::len word" |
|
3207 by (simp add: word_msb_nth word_test_bit_def) |
|
3208 |
|
3209 lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]] |
|
3210 lemmas msb1 = msb0 [where i = 0] |
|
3211 lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]] |
|
3212 |
3117 |
3213 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]] |
3118 lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]] |
3214 lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt] |
|
3215 |
|
3216 lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y" |
|
3217 for w :: "'a::len word" |
|
3218 by (rule word_eqI) (simp add : test_bit_set_gen word_size) |
|
3219 |
|
3220 lemma word_set_set_diff: |
|
3221 fixes w :: "'a::len word" |
|
3222 assumes "m \<noteq> n" |
|
3223 shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x" |
|
3224 by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms) |
|
3225 |
3119 |
3226 lemma nth_sint: |
3120 lemma nth_sint: |
3227 fixes w :: "'a::len word" |
3121 fixes w :: "'a::len word" |
3228 defines "l \<equiv> LENGTH('a)" |
3122 defines "l \<equiv> LENGTH('a)" |
3229 shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" |
3123 shows "bin_nth (sint w) n = (if n < l - 1 then w !! n else w !! (l - 1))" |
3230 unfolding sint_uint l_def |
3124 unfolding sint_uint l_def |
3231 by (auto simp: nth_sbintr word_test_bit_def [symmetric]) |
3125 by (auto simp: nth_sbintr word_test_bit_def [symmetric]) |
3232 |
3126 |
3233 lemma word_lsb_numeral [simp]: |
|
3234 "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)" |
|
3235 unfolding word_lsb_alt test_bit_numeral by simp |
|
3236 |
|
3237 lemma word_lsb_neg_numeral [simp]: |
|
3238 "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)" |
|
3239 by (simp add: word_lsb_alt) |
|
3240 |
|
3241 lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)" |
|
3242 unfolding word_set_bit_def |
|
3243 by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr) |
|
3244 |
|
3245 lemma word_set_numeral [simp]: |
|
3246 "set_bit (numeral bin::'a::len word) n b = |
|
3247 word_of_int (bin_sc n b (numeral bin))" |
|
3248 unfolding word_numeral_alt by (rule set_bit_word_of_int) |
|
3249 |
|
3250 lemma word_set_neg_numeral [simp]: |
|
3251 "set_bit (- numeral bin::'a::len word) n b = |
|
3252 word_of_int (bin_sc n b (- numeral bin))" |
|
3253 unfolding word_neg_numeral_alt by (rule set_bit_word_of_int) |
|
3254 |
|
3255 lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)" |
|
3256 unfolding word_0_wi by (rule set_bit_word_of_int) |
|
3257 |
|
3258 lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)" |
|
3259 unfolding word_1_wi by (rule set_bit_word_of_int) |
|
3260 |
|
3261 lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))" |
3127 lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))" |
3262 by (simp add: setBit_def) |
3128 apply (simp add: setBit_def bin_sc_eq set_bit_def) |
3263 |
3129 apply transfer |
|
3130 apply simp |
|
3131 done |
|
3132 |
3264 lemma clearBit_no [simp]: |
3133 lemma clearBit_no [simp]: |
3265 "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))" |
3134 "clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))" |
3266 by (simp add: clearBit_def) |
3135 apply (simp add: clearBit_def bin_sc_eq unset_bit_def) |
|
3136 apply transfer |
|
3137 apply simp |
|
3138 done |
3267 |
3139 |
3268 lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True" |
3140 lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True" |
3269 apply (rule word_bl.Abs_inverse') |
3141 apply (rule word_bl.Abs_inverse') |
3270 apply simp |
3142 apply simp |
3271 apply (rule word_eqI) |
3143 apply (rule word_eqI) |
3272 apply (clarsimp simp add: word_size) |
3144 apply (clarsimp simp add: word_size) |
3273 apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) |
3145 apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size) |
3274 done |
|
3275 |
|
3276 lemma word_msb_n1 [simp]: "msb (-1::'a::len word)" |
|
3277 unfolding word_msb_alt to_bl_n1 by simp |
|
3278 |
|
3279 lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w" |
|
3280 for w :: "'a::len word" |
|
3281 apply (rule iffI) |
|
3282 apply (rule disjCI) |
|
3283 apply (drule word_eqD) |
|
3284 apply (erule sym [THEN trans]) |
|
3285 apply (simp add: test_bit_set) |
|
3286 apply (erule disjE) |
|
3287 apply clarsimp |
|
3288 apply (rule word_eqI) |
|
3289 apply (clarsimp simp add : test_bit_set_gen) |
|
3290 apply (drule test_bit_size) |
|
3291 apply force |
|
3292 done |
3146 done |
3293 |
3147 |
3294 lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)" |
3148 lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)" |
3295 by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin) |
3149 by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin) |
3296 |
3150 |
3325 apply (rule xtrans(3)) |
3179 apply (rule xtrans(3)) |
3326 apply (rule_tac [2] y = "x" in le_word_or2) |
3180 apply (rule_tac [2] y = "x" in le_word_or2) |
3327 apply (rule word_eqI) |
3181 apply (rule word_eqI) |
3328 apply (auto simp add: word_ao_nth nth_w2p word_size) |
3182 apply (auto simp add: word_ao_nth nth_w2p word_size) |
3329 done |
3183 done |
3330 |
|
3331 lemma word_clr_le: "w \<ge> set_bit w n False" |
|
3332 for w :: "'a::len word" |
|
3333 apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm) |
|
3334 apply (rule order_trans) |
|
3335 apply (rule bintr_bin_clr_le) |
|
3336 apply simp |
|
3337 done |
|
3338 |
|
3339 lemma word_set_ge: "w \<le> set_bit w n True" |
|
3340 for w :: "'a::len word" |
|
3341 apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm) |
|
3342 apply (rule order_trans [OF _ bintr_bin_set_ge]) |
|
3343 apply simp |
|
3344 done |
|
3345 |
|
3346 lemma set_bit_beyond: |
|
3347 "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word" |
|
3348 by (auto intro: word_eqI simp add: test_bit_set_gen word_size) |
|
3349 |
3184 |
3350 lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))" |
3185 lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))" |
3351 by (simp add: zip_rev bl_word_or rev_map) |
3186 by (simp add: zip_rev bl_word_or rev_map) |
3352 |
3187 |
3353 lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))" |
3188 lemma rbl_word_and: "rev (to_bl (x AND y)) = map2 (\<and>) (rev (to_bl x)) (rev (to_bl y))" |
4246 |
4073 |
4247 \<comment> \<open>problem posed by TPHOLs referee: |
4074 \<comment> \<open>problem posed by TPHOLs referee: |
4248 criterion for overflow of addition of signed integers\<close> |
4075 criterion for overflow of addition of signed integers\<close> |
4249 |
4076 |
4250 lemma sofl_test: |
4077 lemma sofl_test: |
4251 "(sint x + sint y = sint (x + y)) = |
4078 \<open>sint x + sint y = sint (x + y) \<longleftrightarrow> |
4252 ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)" |
4079 (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close> |
4253 for x y :: "'a::len word" |
4080 for x y :: \<open>'a::len word\<close> |
4254 apply (unfold word_size) |
4081 proof - |
4255 apply (cases "LENGTH('a)", simp) |
4082 obtain n where n: \<open>LENGTH('a) = Suc n\<close> |
4256 apply (subst msb_shift [THEN sym_notr]) |
4083 by (cases \<open>LENGTH('a)\<close>) simp_all |
4257 apply (simp add: word_ops_msb) |
4084 have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow> |
4258 apply (simp add: word_msb_sint) |
4085 (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or> |
4259 apply safe |
4086 (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close> |
4260 apply simp_all |
4087 apply safe |
4261 apply (unfold sint_word_ariths) |
4088 apply simp_all |
4262 apply (unfold word_sbin.set_iff_norm [symmetric] sints_num) |
4089 apply (unfold sint_word_ariths) |
4263 apply safe |
4090 apply (unfold word_sbin.set_iff_norm [symmetric] sints_num) |
4264 apply (insert sint_range' [where x=x]) |
4091 apply safe |
4265 apply (insert sint_range' [where x=y]) |
4092 apply (insert sint_range' [where x=x]) |
|
4093 apply (insert sint_range' [where x=y]) |
|
4094 defer |
|
4095 apply (simp (no_asm), arith) |
|
4096 apply (simp (no_asm), arith) |
|
4097 defer |
4266 defer |
4098 defer |
4267 apply (simp (no_asm), arith) |
4099 apply (simp (no_asm), arith) |
4268 apply (simp (no_asm), arith) |
4100 apply (simp (no_asm), arith) |
4269 defer |
4101 apply (simp_all add: n not_less) |
4270 defer |
4102 apply (rule notI [THEN notnotD], |
4271 apply (simp (no_asm), arith) |
4103 drule leI not_le_imp_less, |
4272 apply (simp (no_asm), arith) |
4104 drule sbintrunc_inc sbintrunc_dec, |
4273 apply (rule notI [THEN notnotD], |
4105 simp)+ |
4274 drule leI not_le_imp_less, |
4106 done |
4275 drule sbintrunc_inc sbintrunc_dec, |
4107 then show ?thesis |
4276 simp)+ |
4108 apply (simp add: word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff) |
4277 done |
4109 apply (simp add: bit_last_iff) |
|
4110 done |
|
4111 qed |
4278 |
4112 |
4279 lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0" |
4113 lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0" |
4280 for x :: "'a :: len word" |
4114 for x :: "'a :: len word" |
4281 by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size) |
4115 by (rule word_eqI) (auto simp add: nth_shiftr dest: test_bit_size) |
4282 |
4116 |