# HG changeset patch
# User haftmann
# Date 1581245192 0
# Node ID e83fe2c31088ecf978ecd45f1ee5de9062aa36ee
# Parent  7ae4dcf332ae9a52a47b45ad773385b3145acda3
rule concerning bit (push_bit ...)

diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Sun Feb 09 10:21:01 2020 +0000
+++ b/src/HOL/Code_Numeral.thy	Sun Feb 09 10:46:32 2020 +0000
@@ -300,7 +300,7 @@
   (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
-    even_mask_div_iff)+
+    even_mask_div_iff even_mult_exp_div_exp_iff)+
 
 end
 
@@ -997,7 +997,7 @@
   (fact bit_eq_rec bits_induct push_bit_eq_mult drop_bit_eq_div
     bits_div_0 bits_div_by_1 bits_mod_div_trivial even_succ_div_2
     exp_div_exp_eq div_exp_eq mod_exp_eq mult_exp_mod_exp_eq div_exp_mod_exp_eq
-    even_mask_div_iff)+
+    even_mask_div_iff even_mult_exp_div_exp_iff)+
 
 end
 
diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Feb 09 10:21:01 2020 +0000
+++ b/src/HOL/Parity.thy	Sun Feb 09 10:46:32 2020 +0000
@@ -674,6 +674,7 @@
     and mod_exp_eq: \<open>a mod 2 ^ m mod 2 ^ n = a mod 2 ^ min m n\<close>
     and mult_exp_mod_exp_eq: \<open>m \<le> n \<Longrightarrow> (a * 2 ^ m) mod (2 ^ n) = (a mod 2 ^ (n - m)) * 2 ^ m\<close>
     and div_exp_mod_exp_eq: \<open>a div 2 ^ n mod 2 ^ m = a mod (2 ^ (n + m)) div 2 ^ n\<close>
+    and even_mult_exp_div_exp_iff: \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> m > n \<or> 2 ^ n = 0 \<or> (m \<le> n \<and> even (a div 2 ^ (n - m)))\<close>
 begin
 
 lemma bits_div_by_0 [simp]:
@@ -958,6 +959,11 @@
   show \<open>even ((2 ^ m - (1::nat)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::nat) \<or> m \<le> n\<close>
     for m n :: nat
     using even_mask_div_iff' [where ?'a = nat, of m n] by simp
+  show \<open>even (q * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::nat) ^ n = 0 \<or> m \<le> n \<and> even (q div 2 ^ (n - m))\<close>
+    for m n q r :: nat
+    apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
+    apply (metis (full_types) dvd_mult dvd_mult_imp_div dvd_power_iff_le not_less not_less_eq order_refl power_Suc)
+    done
 qed (auto simp add: div_mult2_eq mod_mult2_eq power_add power_diff)
 
 lemma int_bit_induct [case_names zero minus even odd]:
@@ -1074,6 +1080,11 @@
   show \<open>even ((2 ^ m - (1::int)) div 2 ^ n) \<longleftrightarrow> 2 ^ n = (0::int) \<or> m \<le> n\<close>
     for m n :: nat
     using even_mask_div_iff' [where ?'a = int, of m n] by simp
+  show \<open>even (k * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::int) ^ n = 0 \<or> m \<le> n \<and> even (k div 2 ^ (n - m))\<close>
+    for m n :: nat and k l :: int
+    apply (auto simp add: not_less power_add ac_simps dest!: le_Suc_ex)
+    apply (metis Suc_leI dvd_mult dvd_mult_imp_div dvd_power_le dvd_refl power.simps(2))
+    done
 qed (auto simp add: zdiv_zmult2_eq zmod_zmult2_eq power_add power_diff not_le)
 
 class semiring_bit_shifts = semiring_bits +
@@ -1250,6 +1261,14 @@
     by simp
 qed
 
+lemma even_push_bit_iff [simp]:
+  \<open>even (push_bit n a) \<longleftrightarrow> n \<noteq> 0 \<or> even a\<close>
+  by (simp add: push_bit_eq_mult) auto
+
+lemma bit_push_bit_iff:
+  \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> (n < m \<or> bit a (n - m))\<close>
+  by (auto simp add: bit_def push_bit_eq_mult even_mult_exp_div_exp_iff)
+
 lemma bit_drop_bit_eq:
   \<open>bit (drop_bit n a) = bit a \<circ> (+) n\<close>
   by (simp add: bit_def fun_eq_iff ac_simps flip: drop_bit_eq_div)
@@ -1298,35 +1317,11 @@
 
 lemma bit_push_bit_iff_nat:
   \<open>bit (push_bit m q) n \<longleftrightarrow> m \<le> n \<and> bit q (n - m)\<close> for q :: nat
-proof (cases \<open>m \<le> n\<close>)
-  case True
-  then obtain r where \<open>n = m + r\<close>
-    using le_Suc_ex by blast
-  with True show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
-next
-  case False
-  then obtain r where \<open>m = Suc (n + r)\<close>
-    using less_imp_Suc_add not_le by blast
-  with False show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
-qed
+  by (auto simp add: bit_push_bit_iff)
 
 lemma bit_push_bit_iff_int:
   \<open>bit (push_bit m k) n \<longleftrightarrow> m \<le> n \<and> bit k (n - m)\<close> for k :: int
-proof (cases \<open>m \<le> n\<close>)
-  case True
-  then obtain r where \<open>n = m + r\<close>
-    using le_Suc_ex by blast
-  with True show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add mult.commute [of \<open>2 ^ m\<close>])
-next
-  case False
-  then obtain r where \<open>m = Suc (n + r)\<close>
-    using less_imp_Suc_add not_le by blast
-  with False show ?thesis
-    by (simp add: push_bit_eq_mult bit_def power_add mult.left_commute [of _ \<open>2 ^ n\<close>])
-qed
+  by (auto simp add: bit_push_bit_iff)
 
 class unique_euclidean_semiring_with_bit_shifts =
   unique_euclidean_semiring_with_nat + semiring_bit_shifts
@@ -1421,13 +1416,7 @@
 
 lemma bit_push_bit_iff_of_nat_iff:
   \<open>bit (push_bit m (of_nat r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
-proof -
-  from bit_push_bit_iff_nat
-  have \<open>bit (of_nat (push_bit m r)) n \<longleftrightarrow> m \<le> n \<and> bit (of_nat r) (n - m)\<close>
-    by simp
-  then show ?thesis
-    by (simp add: of_nat_push_bit)
-qed
+  by (auto simp add: bit_push_bit_iff)
 
 end
 
@@ -1463,12 +1452,12 @@
   \<open>drop_bit n (- 1 :: int) = - 1\<close>
   by (simp add: drop_bit_eq_div minus_1_div_exp_eq_int)
 
-lemma take_bit_uminus:
+lemma take_bit_minus:
   "take_bit n (- (take_bit n k)) = take_bit n (- k)"
     for k :: int
   by (simp add: take_bit_eq_mod mod_minus_eq)
 
-lemma take_bit_minus:
+lemma take_bit_diff:
   "take_bit n (take_bit n k - take_bit n l) = take_bit n (k - l)"
     for k l :: int
   by (simp add: take_bit_eq_mod mod_diff_eq)
@@ -1478,4 +1467,9 @@
     for k :: int
   by (simp add: take_bit_eq_mod)
 
+lemma drop_bit_push_bit_int:
+  \<open>drop_bit m (push_bit n k) = drop_bit (m - n) (push_bit (n - m) k)\<close> for k :: int
+  by (cases \<open>m \<le> n\<close>) (auto simp add: mult.left_commute [of _ \<open>2 ^ n\<close>] mult.commute [of _ \<open>2 ^ n\<close>] mult.assoc
+     mult.commute [of k] drop_bit_eq_div push_bit_eq_mult not_le power_add dest!: le_Suc_ex less_imp_Suc_add)
+
 end
diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Sun Feb 09 10:21:01 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Sun Feb 09 10:46:32 2020 +0000
@@ -9,15 +9,6 @@
     Main
 begin
 
-context semiring_bit_shifts
-begin
-
-(*lemma bit_push_bit_iff:
-  \<open>bit (push_bit m a) n \<longleftrightarrow> n \<ge> m \<and> 2 ^ n \<noteq> 0 \<and> bit a (n - m)\<close>*)
-
-end
-
-
 subsection \<open>Bit operations in suitable algebraic structures\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
diff -r 7ae4dcf332ae -r e83fe2c31088 src/HOL/ex/Word.thy
--- a/src/HOL/ex/Word.thy	Sun Feb 09 10:21:01 2020 +0000
+++ b/src/HOL/ex/Word.thy	Sun Feb 09 10:46:32 2020 +0000
@@ -105,11 +105,11 @@
 
 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   is uminus
-  by (subst take_bit_uminus [symmetric]) (simp add: take_bit_uminus)
+  by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
 
 lift_definition minus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is minus
-  by (subst take_bit_minus [symmetric]) (simp add: take_bit_minus)
+  by (subst take_bit_diff [symmetric]) (simp add: take_bit_diff)
 
 lift_definition times_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is times
@@ -617,6 +617,17 @@
   show \<open>even ((2 ^ m - 1) div (2::'a word) ^ n) \<longleftrightarrow> 2 ^ n = (0::'a word) \<or> m \<le> n\<close>
     for m n :: nat
     by transfer (auto simp add: take_bit_of_mask even_mask_div_iff)
+  show \<open>even (a * 2 ^ m div 2 ^ n) \<longleftrightarrow> n < m \<or> (2::'a word) ^ n = 0 \<or> m \<le> n \<and> even (a div 2 ^ (n - m))\<close>
+    for a :: \<open>'a word\<close> and m n :: nat
+  proof transfer
+    show \<open>even (take_bit LENGTH('a) (k * 2 ^ m) div take_bit LENGTH('a) (2 ^ n)) \<longleftrightarrow>
+      n < m
+      \<or> take_bit LENGTH('a) ((2::int) ^ n) = take_bit LENGTH('a) 0
+      \<or> (m \<le> n \<and> even (take_bit LENGTH('a) k div take_bit LENGTH('a) (2 ^ (n - m))))\<close>
+    for m n :: nat and k l :: int
+      by (auto simp flip: take_bit_eq_mod drop_bit_eq_div push_bit_eq_mult
+        simp add: div_push_bit_of_1_eq_drop_bit drop_bit_take_bit drop_bit_push_bit_int [of n m])
+  qed
 qed
 
 context