--- 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)
--- 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