--- a/src/HOL/Parity.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Parity.thy Thu Jun 18 09:07:54 2020 +0000
@@ -1296,10 +1296,6 @@
"drop_bit n (of_bool b) = of_bool (n = 0 \<and> b)"
by (cases n) simp_all
-lemma take_bit_eq_0_imp_dvd:
- "take_bit n a = 0 \<Longrightarrow> 2 ^ n dvd a"
- by (simp add: take_bit_eq_mod mod_0_imp_dvd)
-
lemma even_take_bit_eq [simp]:
\<open>even (take_bit n a) \<longleftrightarrow> n = 0 \<or> even a\<close>
by (simp add: take_bit_rec [of n a])
@@ -1388,6 +1384,30 @@
by (simp add: bit_take_bit_iff bit_mask_iff stable_imp_bit_iff_odd)
qed
+lemma exp_dvdE:
+ assumes \<open>2 ^ n dvd a\<close>
+ obtains b where \<open>a = push_bit n b\<close>
+proof -
+ from assms obtain b where \<open>a = 2 ^ n * b\<close> ..
+ then have \<open>a = push_bit n b\<close>
+ by (simp add: push_bit_eq_mult ac_simps)
+ with that show thesis .
+qed
+
+lemma take_bit_eq_0_iff:
+ \<open>take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume ?P
+ then show ?Q
+ by (simp add: take_bit_eq_mod mod_0_imp_dvd)
+next
+ assume ?Q
+ then obtain b where \<open>a = push_bit n b\<close>
+ by (rule exp_dvdE)
+ then show ?P
+ by (simp add: take_bit_push_bit)
+qed
+
end
instantiation nat :: semiring_bit_shifts
@@ -1466,10 +1486,6 @@
"take_bit n (take_bit n a + take_bit n b) = take_bit n (a + b)"
by (simp add: take_bit_eq_mod mod_simps)
-lemma take_bit_eq_0_iff:
- "take_bit n a = 0 \<longleftrightarrow> 2 ^ n dvd a"
- by (simp add: take_bit_eq_mod mod_eq_0_iff_dvd)
-
lemma take_bit_of_1_eq_0_iff [simp]:
"take_bit n 1 = 0 \<longleftrightarrow> n = 0"
by (simp add: take_bit_eq_mod)
--- a/src/HOL/Word/Word.thy Thu Jun 18 09:07:30 2020 +0000
+++ b/src/HOL/Word/Word.thy Thu Jun 18 09:07:54 2020 +0000
@@ -385,7 +385,7 @@
begin
lemma [transfer_rule]:
- "(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)"
+ \<open>(pcr_word ===> (\<longleftrightarrow>)) even ((dvd) 2 :: 'a::len word \<Rightarrow> bool)\<close>
proof -
have even_word_unfold: "even k \<longleftrightarrow> (\<exists>l. take_bit LENGTH('a) k = take_bit LENGTH('a) (2 * l))" (is "?P \<longleftrightarrow> ?Q")
for k :: int
@@ -449,6 +449,24 @@
\<open>2 ^ n = (0 :: 'a::len word) \<longleftrightarrow> n \<ge> LENGTH('a)\<close>
by transfer simp
+lemma double_eq_zero_iff:
+ \<open>2 * a = 0 \<longleftrightarrow> a = 0 \<or> a = 2 ^ (LENGTH('a) - Suc 0)\<close>
+ for a :: \<open>'a::len word\<close>
+proof -
+ define n where \<open>n = LENGTH('a) - Suc 0\<close>
+ then have *: \<open>LENGTH('a) = Suc n\<close>
+ by simp
+ have \<open>a = 0\<close> if \<open>2 * a = 0\<close> and \<open>a \<noteq> 2 ^ (LENGTH('a) - Suc 0)\<close>
+ using that by transfer
+ (auto simp add: take_bit_eq_0_iff take_bit_eq_mod *)
+ moreover have \<open>2 ^ LENGTH('a) = (0 :: 'a word)\<close>
+ by transfer simp
+ then have \<open>2 * 2 ^ (LENGTH('a) - Suc 0) = (0 :: 'a word)\<close>
+ by (simp add: *)
+ ultimately show ?thesis
+ by auto
+qed
+
subsection \<open>Ordering\<close>
@@ -779,6 +797,11 @@
end
+lemma bit_word_eqI:
+ \<open>a = b\<close> if \<open>\<And>n. n \<le> LENGTH('a) \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
+ for a b :: \<open>'a::len word\<close>
+ by (rule bit_eqI, rule that) (simp add: exp_eq_zero_iff)
+
definition shiftl1 :: "'a::len word \<Rightarrow> 'a word"
where "shiftl1 w = word_of_int (uint w BIT False)"
@@ -1453,6 +1476,16 @@
by (simp add: ucast_def test_bit_bin word_ubin.eq_norm nth_bintr word_size)
(fast elim!: bin_nth_uint_imp)
+context
+ includes lifting_syntax
+begin
+
+lemma transfer_rule_mask_word [transfer_rule]:
+ \<open>((=) ===> pcr_word) Bit_Operations.mask Bit_Operations.mask\<close>
+ by (simp only: mask_eq_exp_minus_1 [abs_def]) transfer_prover
+
+end
+
lemma ucast_mask_eq:
\<open>ucast (Bit_Operations.mask n :: 'b word) = Bit_Operations.mask (min LENGTH('b::len) n)\<close>
by (simp add: bit_eq_iff) (auto simp add: bit_mask_iff bit_ucast_iff exp_eq_zero_iff)