# HG changeset patch
# User haftmann
# Date 1522908902 0
# Node ID 9c31678d21392e0c9a553095fb4899a587db9865
# Parent  ac66cbe795e516051d54b0da4bf0d1e51c1229f2
even more on bit operations

diff -r ac66cbe795e5 -r 9c31678d2139 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Apr 04 20:52:36 2018 +0200
+++ b/src/HOL/Parity.thy	Thu Apr 05 06:15:02 2018 +0000
@@ -796,10 +796,14 @@
   "take_bit n 0 = 0"
   by (simp add: take_bit_eq_mod)
 
-lemma take_bit_plus:
+lemma take_bit_add:
   "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)
@@ -808,6 +812,10 @@
   "push_bit n a = 0 \<longleftrightarrow> a = 0"
   by (simp add: push_bit_eq_mult)
 
+lemma push_bit_add:
+  "push_bit n (a + b) = push_bit n a + push_bit n b"
+  by (simp add: push_bit_eq_mult algebra_simps)
+
 lemma drop_bit_0 [simp]:
   "drop_bit 0 = id"
   by (simp add: fun_eq_iff drop_bit_eq_div)
diff -r ac66cbe795e5 -r 9c31678d2139 src/HOL/ex/Word_Type.thy
--- a/src/HOL/ex/Word_Type.thy	Wed Apr 04 20:52:36 2018 +0200
+++ b/src/HOL/ex/Word_Type.thy	Thu Apr 05 06:15:02 2018 +0000
@@ -72,12 +72,12 @@
     assume ?Q
     have "take_bit (Suc m) (k + 2 ^ m) =
       take_bit (Suc m) (take_bit (Suc m) k + take_bit (Suc m) (2 ^ m))"
-      by (simp only: take_bit_plus)
+      by (simp only: take_bit_add)
     also have "\<dots> =
       take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))"
       by (simp only: \<open>?Q\<close> m [symmetric])
     also have "\<dots> = take_bit (Suc m) (l + 2 ^ m)"
-      by (simp only: take_bit_plus)
+      by (simp only: take_bit_add)
     finally show ?P
       by (simp only: signed_take_bit_eq_take_bit m) simp
   next
@@ -114,7 +114,7 @@
 
 lift_definition plus_word :: "'a word \<Rightarrow> 'a word \<Rightarrow> 'a word"
   is plus
-  by (subst take_bit_plus [symmetric]) (simp add: take_bit_plus)
+  by (subst take_bit_add [symmetric]) (simp add: take_bit_add)
 
 lift_definition uminus_word :: "'a word \<Rightarrow> 'a word"
   is uminus