--- a/src/HOL/Word/Word.thy Sun Jul 05 11:06:09 2020 +0200
+++ b/src/HOL/Word/Word.thy Mon Jul 06 10:47:30 2020 +0000
@@ -919,25 +919,15 @@
end
-instantiation word :: (len) bit_operations
+instantiation word :: (len) semiring_bit_syntax
begin
definition word_test_bit_def: "test_bit a = bin_nth (uint a)"
-definition word_set_bit_def: "set_bit a n x = word_of_int (bin_sc n x (uint a))"
-
-definition word_lsb_def: "lsb a \<longleftrightarrow> bin_last (uint a)"
-
-definition "msb a \<longleftrightarrow> bin_sign (sbintrunc (LENGTH('a) - 1) (uint a)) = - 1"
-
definition shiftl_def: "w << n = (shiftl1 ^^ n) w"
definition shiftr_def: "w >> n = (shiftr1 ^^ n) w"
-instance ..
-
-end
-
lemma test_bit_word_eq:
\<open>test_bit w = bit w\<close> for w :: \<open>'a::len word\<close>
apply (simp add: word_test_bit_def fun_eq_iff)
@@ -945,36 +935,19 @@
apply (simp add: bit_take_bit_iff)
done
-lemma set_bit_unfold:
- \<open>set_bit w n b = (if b then Bit_Operations.set_bit n w else unset_bit n w)\<close>
- for w :: \<open>'a::len word\<close>
- 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)
- apply simp_all
- done
-
-lemma bit_set_bit_word_iff:
- \<open>bit (set_bit w m b) n \<longleftrightarrow> (if m = n then n < LENGTH('a) \<and> b else bit w n)\<close>
- for w :: \<open>'a::len word\<close>
- 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)
-
-lemma lsb_word_eq:
- \<open>lsb = (odd :: 'a word \<Rightarrow> bool)\<close> for w :: \<open>'a::len word\<close>
- apply (simp add: word_lsb_def fun_eq_iff)
- apply transfer
- apply simp
- done
-
-lemma msb_word_eq:
- \<open>msb w \<longleftrightarrow> bit w (LENGTH('a) - 1)\<close> for w :: \<open>'a::len word\<close>
- apply (simp add: msb_word_def bin_sign_lem)
- apply transfer
- apply (simp add: bit_take_bit_iff)
- done
-
lemma shiftl_word_eq:
\<open>w << n = push_bit n w\<close> for w :: \<open>'a::len word\<close>
by (induction n) (simp_all add: shiftl_def shiftl1_eq_mult_2 push_bit_double)
+lemma shiftr_word_eq:
+ \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close>
+ by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half)
+
+instance by standard
+ (simp_all add: fun_eq_iff test_bit_word_eq shiftl_word_eq shiftr_word_eq)
+
+end
+
lemma bit_shiftl_word_iff:
\<open>bit (w << m) n \<longleftrightarrow> m \<le> n \<and> n < LENGTH('a) \<and> bit w (n - m)\<close>
for w :: \<open>'a::len word\<close>
@@ -984,10 +957,6 @@
\<open>push_bit n w = w << n\<close> for w :: \<open>'a::len word\<close>
by (simp add: shiftl_word_eq)
-lemma shiftr_word_eq:
- \<open>w >> n = drop_bit n w\<close> for w :: \<open>'a::len word\<close>
- by (induction n) (simp_all add: shiftr_def shiftr1_eq_div_2 drop_bit_Suc drop_bit_half)
-
lemma bit_shiftr_word_iff:
\<open>bit (w >> m) n \<longleftrightarrow> bit w (m + n)\<close>
for w :: \<open>'a::len word\<close>
@@ -1005,10 +974,6 @@
\<open>push_bit n 1 = (2 :: 'a::len word) ^ n\<close>
by (fact push_bit_of_1)
-lemma word_msb_def:
- "msb a \<longleftrightarrow> bin_sign (sint a) = - 1"
- by (simp add: msb_word_def sint_uint)
-
lemma [code]:
shows word_not_def: "NOT (a::'a::len word) = word_of_int (NOT (uint a))"
and word_and_def: "(a::'a word) AND b = word_of_int (uint a AND uint b)"
@@ -1017,30 +982,20 @@
by (transfer, simp add: take_bit_not_take_bit)+
definition setBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"
- where "setBit w n = set_bit w n True"
-
-lemma setBit_eq_set_bit:
- \<open>setBit w n = Bit_Operations.set_bit n w\<close>
- for w :: \<open>'a::len word\<close>
- by (simp add: setBit_def set_bit_unfold)
+ where \<open>setBit w n = Bit_Operations.set_bit n w\<close>
lemma bit_setBit_iff:
\<open>bit (setBit w m) n \<longleftrightarrow> (m = n \<and> n < LENGTH('a) \<or> bit w n)\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: setBit_eq_set_bit bit_set_bit_iff exp_eq_zero_iff not_le ac_simps)
+ by (simp add: setBit_def bit_set_bit_iff exp_eq_zero_iff not_le ac_simps)
definition clearBit :: "'a::len word \<Rightarrow> nat \<Rightarrow> 'a word"
- where "clearBit w n = set_bit w n False"
-
-lemma clearBit_eq_unset_bit:
- \<open>clearBit w n = unset_bit n w\<close>
- for w :: \<open>'a::len word\<close>
- by (simp add: clearBit_def set_bit_unfold)
+ where \<open>clearBit w n = unset_bit n w\<close>
lemma bit_clearBit_iff:
\<open>bit (clearBit w m) n \<longleftrightarrow> m \<noteq> n \<and> bit w n\<close>
for w :: \<open>'a::len word\<close>
- by (simp add: clearBit_eq_unset_bit bit_unset_bit_iff ac_simps)
+ by (simp add: clearBit_def bit_unset_bit_iff ac_simps)
definition even_word :: \<open>'a::len word \<Rightarrow> bool\<close>
where [code_abbrev]: \<open>even_word = even\<close>
@@ -1777,6 +1732,30 @@
lemmas word_log_defs = word_and_def word_or_def word_xor_def word_not_def
+lemma bit_last_iff:
+ \<open>bit w (LENGTH('a) - Suc 0) \<longleftrightarrow> sint w < 0\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+ for w :: \<open>'a::len word\<close>
+proof -
+ have \<open>?P \<longleftrightarrow> bit (uint w) (LENGTH('a) - Suc 0)\<close>
+ by (simp add: bit_uint_iff)
+ also have \<open>\<dots> \<longleftrightarrow> ?Q\<close>
+ by (simp add: sint_uint bin_sign_def flip: bin_sign_lem)
+ finally show ?thesis .
+qed
+
+lemma drop_bit_eq_zero_iff_not_bit_last:
+ \<open>drop_bit (LENGTH('a) - Suc 0) w = 0 \<longleftrightarrow> \<not> bit w (LENGTH('a) - Suc 0)\<close>
+ for w :: "'a::len word"
+ apply (cases \<open>LENGTH('a)\<close>)
+ apply simp_all
+ apply (simp add: bit_iff_odd_drop_bit)
+ apply transfer
+ apply (simp add: take_bit_drop_bit)
+ apply (auto simp add: drop_bit_eq_div take_bit_eq_mod min_def)
+ apply (auto elim!: evenE)
+ apply (metis div_exp_eq mod_div_trivial mult.commute nonzero_mult_div_cancel_left power_Suc0_right power_add zero_neq_numeral)
+ done
+
subsection \<open>Word Arithmetic\<close>
@@ -2919,6 +2898,9 @@
for x :: "'a::len word"
by transfer (auto simp add: bin_nth_ops)
+lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
+lemmas msb1 = msb0 [where i = 0]
+
lemma test_bit_numeral [simp]:
"(numeral w :: 'a::len word) !! n \<longleftrightarrow>
n < LENGTH('a) \<and> bin_nth (numeral w) n"
@@ -3061,63 +3043,6 @@
unfolding to_bl_def word_log_defs bl_and_bin
by (simp add: word_ubin.eq_norm)
-lemma word_lsb_alt: "lsb w = test_bit w 0"
- for w :: "'a::len word"
- by (auto simp: word_test_bit_def word_lsb_def)
-
-lemma word_lsb_1_0 [simp]: "lsb (1::'a::len word) \<and> \<not> lsb (0::'b::len word)"
- unfolding word_lsb_def uint_eq_0 uint_1 by simp
-
-lemma word_lsb_last: "lsb w = last (to_bl w)"
- for w :: "'a::len word"
- apply (unfold word_lsb_def uint_bl bin_to_bl_def)
- apply (rule_tac bin="uint w" in bin_exhaust)
- apply (cases "size w")
- apply auto
- apply (auto simp add: bin_to_bl_aux_alt)
- done
-
-lemma word_lsb_int: "lsb w \<longleftrightarrow> uint w mod 2 = 1"
- by (auto simp: word_lsb_def bin_last_def)
-
-lemma word_msb_sint: "msb w \<longleftrightarrow> sint w < 0"
- by (simp only: word_msb_def sign_Min_lt_0)
-
-lemma msb_word_of_int: "msb (word_of_int x::'a::len word) = bin_nth x (LENGTH('a) - 1)"
- by (simp add: word_msb_def word_sbin.eq_norm bin_sign_lem)
-
-lemma word_msb_numeral [simp]:
- "msb (numeral w::'a::len word) = bin_nth (numeral w) (LENGTH('a) - 1)"
- unfolding word_numeral_alt by (rule msb_word_of_int)
-
-lemma word_msb_neg_numeral [simp]:
- "msb (- numeral w::'a::len word) = bin_nth (- numeral w) (LENGTH('a) - 1)"
- unfolding word_neg_numeral_alt by (rule msb_word_of_int)
-
-lemma word_msb_0 [simp]: "\<not> msb (0::'a::len word)"
- by (simp add: word_msb_def)
-
-lemma word_msb_1 [simp]: "msb (1::'a::len word) \<longleftrightarrow> LENGTH('a) = 1"
- unfolding word_1_wi msb_word_of_int eq_iff [where 'a=nat]
- by (simp add: Suc_le_eq)
-
-lemma word_msb_nth: "msb w = bin_nth (uint w) (LENGTH('a) - 1)"
- for w :: "'a::len word"
- by (simp add: word_msb_def sint_uint bin_sign_lem)
-
-lemma word_msb_alt: "msb w = hd (to_bl w)"
- for w :: "'a::len word"
- apply (unfold word_msb_nth uint_bl)
- apply (subst hd_conv_nth)
- apply (rule length_greater_0_conv [THEN iffD1])
- apply simp
- apply (simp add : nth_bin_to_bl word_size)
- done
-
-lemma word_set_nth [simp]: "set_bit w n (test_bit w n) = w"
- for w :: "'a::len word"
- by (auto simp: word_test_bit_def word_set_bit_def)
-
lemma bin_nth_uint': "bin_nth (uint w) n \<longleftrightarrow> rev (bin_to_bl (size w) (uint w)) ! n \<and> n < size w"
apply (unfold word_size)
apply (safe elim!: bin_nth_uint_imp)
@@ -3163,19 +3088,6 @@
if \<open>n < LENGTH('a)\<close> for w :: \<open>'a::len word\<close>
using that by (simp add: to_bl_unfold rev_nth)
-lemma test_bit_set: "(set_bit w n x) !! n \<longleftrightarrow> n < size w \<and> x"
- for w :: "'a::len word"
- by (auto simp: word_size word_test_bit_def word_set_bit_def word_ubin.eq_norm nth_bintr)
-
-lemma test_bit_set_gen:
- "test_bit (set_bit w n x) m = (if m = n then n < size w \<and> x else test_bit w m)"
- for w :: "'a::len word"
- apply (unfold word_size word_test_bit_def word_set_bit_def)
- apply (clarsimp simp add: word_ubin.eq_norm nth_bintr bin_nth_sc_gen)
- apply (auto elim!: test_bit_size [unfolded word_size]
- simp add: word_test_bit_def [symmetric])
- done
-
lemma of_bl_rep_False: "of_bl (replicate n False @ bs) = of_bl bs"
by (auto simp: of_bl_def bl_to_bin_rep_F)
@@ -3202,26 +3114,8 @@
for w :: \<open>'a::len word\<close>
by (simp add: slice_def word_size bit_slice1_iff)
-lemma msb_nth: "msb w = w !! (LENGTH('a) - 1)"
- for w :: "'a::len word"
- by (simp add: word_msb_nth word_test_bit_def)
-
-lemmas msb0 = len_gt_0 [THEN diff_Suc_less, THEN word_ops_nth_size [unfolded word_size]]
-lemmas msb1 = msb0 [where i = 0]
-lemmas word_ops_msb = msb1 [unfolded msb_nth [symmetric, unfolded One_nat_def]]
lemmas lsb0 = len_gt_0 [THEN word_ops_nth_size [unfolded word_size]]
-lemmas word_ops_lsb = lsb0 [unfolded word_lsb_alt]
-
-lemma word_set_set_same [simp]: "set_bit (set_bit w n x) n y = set_bit w n y"
- for w :: "'a::len word"
- by (rule word_eqI) (simp add : test_bit_set_gen word_size)
-
-lemma word_set_set_diff:
- fixes w :: "'a::len word"
- assumes "m \<noteq> n"
- shows "set_bit (set_bit w m x) n y = set_bit (set_bit w n y) m x"
- by (rule word_eqI) (auto simp: test_bit_set_gen word_size assms)
lemma nth_sint:
fixes w :: "'a::len word"
@@ -3230,40 +3124,18 @@
unfolding sint_uint l_def
by (auto simp: nth_sbintr word_test_bit_def [symmetric])
-lemma word_lsb_numeral [simp]:
- "lsb (numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (numeral bin)"
- unfolding word_lsb_alt test_bit_numeral by simp
-
-lemma word_lsb_neg_numeral [simp]:
- "lsb (- numeral bin :: 'a::len word) \<longleftrightarrow> bin_last (- numeral bin)"
- by (simp add: word_lsb_alt)
-
-lemma set_bit_word_of_int: "set_bit (word_of_int x) n b = word_of_int (bin_sc n b x)"
- unfolding word_set_bit_def
- by (rule word_eqI)(simp add: word_size bin_nth_sc_gen word_ubin.eq_norm nth_bintr)
-
-lemma word_set_numeral [simp]:
- "set_bit (numeral bin::'a::len word) n b =
- word_of_int (bin_sc n b (numeral bin))"
- unfolding word_numeral_alt by (rule set_bit_word_of_int)
-
-lemma word_set_neg_numeral [simp]:
- "set_bit (- numeral bin::'a::len word) n b =
- word_of_int (bin_sc n b (- numeral bin))"
- unfolding word_neg_numeral_alt by (rule set_bit_word_of_int)
-
-lemma word_set_bit_0 [simp]: "set_bit 0 n b = word_of_int (bin_sc n b 0)"
- unfolding word_0_wi by (rule set_bit_word_of_int)
-
-lemma word_set_bit_1 [simp]: "set_bit 1 n b = word_of_int (bin_sc n b 1)"
- unfolding word_1_wi by (rule set_bit_word_of_int)
-
lemma setBit_no [simp]: "setBit (numeral bin) n = word_of_int (bin_sc n True (numeral bin))"
- by (simp add: setBit_def)
-
+ apply (simp add: setBit_def bin_sc_eq set_bit_def)
+ apply transfer
+ apply simp
+ done
+
lemma clearBit_no [simp]:
"clearBit (numeral bin) n = word_of_int (bin_sc n False (numeral bin))"
- by (simp add: clearBit_def)
+ apply (simp add: clearBit_def bin_sc_eq unset_bit_def)
+ apply transfer
+ apply simp
+ done
lemma to_bl_n1 [simp]: "to_bl (-1::'a::len word) = replicate (LENGTH('a)) True"
apply (rule word_bl.Abs_inverse')
@@ -3273,24 +3145,6 @@
apply (auto simp add: word_bl.Abs_inverse test_bit_bl word_size)
done
-lemma word_msb_n1 [simp]: "msb (-1::'a::len word)"
- unfolding word_msb_alt to_bl_n1 by simp
-
-lemma word_set_nth_iff: "set_bit w n b = w \<longleftrightarrow> w !! n = b \<or> n \<ge> size w"
- for w :: "'a::len word"
- apply (rule iffI)
- apply (rule disjCI)
- apply (drule word_eqD)
- apply (erule sym [THEN trans])
- apply (simp add: test_bit_set)
- apply (erule disjE)
- apply clarsimp
- apply (rule word_eqI)
- apply (clarsimp simp add : test_bit_set_gen)
- apply (drule test_bit_size)
- apply force
- done
-
lemma test_bit_2p: "(word_of_int (2 ^ n)::'a::len word) !! m \<longleftrightarrow> m = n \<and> m < LENGTH('a)"
by (auto simp: word_test_bit_def word_ubin.eq_norm nth_bintr nth_2p_bin)
@@ -3328,25 +3182,6 @@
apply (auto simp add: word_ao_nth nth_w2p word_size)
done
-lemma word_clr_le: "w \<ge> set_bit w n False"
- for w :: "'a::len word"
- apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
- apply (rule order_trans)
- apply (rule bintr_bin_clr_le)
- apply simp
- done
-
-lemma word_set_ge: "w \<le> set_bit w n True"
- for w :: "'a::len word"
- apply (unfold word_set_bit_def word_le_def word_ubin.eq_norm)
- apply (rule order_trans [OF _ bintr_bin_set_ge])
- apply simp
- done
-
-lemma set_bit_beyond:
- "size x \<le> n \<Longrightarrow> set_bit x n b = x" for x :: "'a :: len word"
- by (auto intro: word_eqI simp add: test_bit_set_gen word_size)
-
lemma rbl_word_or: "rev (to_bl (x OR y)) = map2 (\<or>) (rev (to_bl x)) (rev (to_bl y))"
by (simp add: zip_rev bl_word_or rev_map)
@@ -3815,14 +3650,6 @@
for x :: "'a::len word"
using shiftr_bl_of [where 'a='a, of "to_bl x"] by simp
-lemma msb_shift: "msb w \<longleftrightarrow> w >> (LENGTH('a) - 1) \<noteq> 0"
- for w :: "'a::len word"
- apply (unfold shiftr_bl word_msb_alt)
- apply (simp add: word_size Suc_le_eq take_Suc)
- apply (cases "hd (to_bl w)")
- apply (auto simp: word_1_bl of_bl_rep_False [where n=1 and bs="[]", simplified])
- done
-
lemma zip_replicate: "n \<ge> length ys \<Longrightarrow> zip (replicate n x) ys = map (\<lambda>y. (x, y)) ys"
apply (induct ys arbitrary: n)
apply simp_all
@@ -4248,33 +4075,40 @@
criterion for overflow of addition of signed integers\<close>
lemma sofl_test:
- "(sint x + sint y = sint (x + y)) =
- ((((x + y) XOR x) AND ((x + y) XOR y)) >> (size x - 1) = 0)"
- for x y :: "'a::len word"
- apply (unfold word_size)
- apply (cases "LENGTH('a)", simp)
- apply (subst msb_shift [THEN sym_notr])
- apply (simp add: word_ops_msb)
- apply (simp add: word_msb_sint)
- apply safe
- apply simp_all
- apply (unfold sint_word_ariths)
- apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
- apply safe
- apply (insert sint_range' [where x=x])
- apply (insert sint_range' [where x=y])
+ \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
+ (x + y XOR x) AND (x + y XOR y) >> (size x - 1) = 0\<close>
+ for x y :: \<open>'a::len word\<close>
+proof -
+ obtain n where n: \<open>LENGTH('a) = Suc n\<close>
+ by (cases \<open>LENGTH('a)\<close>) simp_all
+ have \<open>sint x + sint y = sint (x + y) \<longleftrightarrow>
+ (sint (x + y) < 0 \<longleftrightarrow> sint x < 0) \<or>
+ (sint (x + y) < 0 \<longleftrightarrow> sint y < 0)\<close>
+ apply safe
+ apply simp_all
+ apply (unfold sint_word_ariths)
+ apply (unfold word_sbin.set_iff_norm [symmetric] sints_num)
+ apply safe
+ apply (insert sint_range' [where x=x])
+ apply (insert sint_range' [where x=y])
+ defer
+ apply (simp (no_asm), arith)
+ apply (simp (no_asm), arith)
+ defer
defer
apply (simp (no_asm), arith)
apply (simp (no_asm), arith)
- defer
- defer
- apply (simp (no_asm), arith)
- apply (simp (no_asm), arith)
- apply (rule notI [THEN notnotD],
- drule leI not_le_imp_less,
- drule sbintrunc_inc sbintrunc_dec,
- simp)+
- done
+ apply (simp_all add: n not_less)
+ apply (rule notI [THEN notnotD],
+ drule leI not_le_imp_less,
+ drule sbintrunc_inc sbintrunc_dec,
+ simp)+
+ done
+ then show ?thesis
+ apply (simp add: word_size shiftr_word_eq drop_bit_eq_zero_iff_not_bit_last bit_and_iff bit_xor_iff)
+ apply (simp add: bit_last_iff)
+ done
+qed
lemma shiftr_zero_size: "size x \<le> n \<Longrightarrow> x >> n = 0"
for x :: "'a :: len word"