# HG changeset patch
# User haftmann
# Date 1592471274 0
# Node ID 4320875eb8a12c77337f384e8e919a297674a95b
# Parent  3e162c63371a79271344fa5b27e029a6be7acd5c
more lemmas

diff -r 3e162c63371a -r 4320875eb8a1 src/HOL/Parity.thy
--- 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)
diff -r 3e162c63371a -r 4320875eb8a1 src/HOL/Word/Word.thy
--- 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)