# 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 \ 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 \ n = 0" by (simp add: take_bit_eq_mod) @@ -808,6 +812,10 @@ "push_bit n a = 0 \ 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 "\ = take_bit (Suc m) (take_bit (Suc m) l + take_bit (Suc m) (2 ^ m))" by (simp only: \?Q\ m [symmetric]) also have "\ = 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 \ 'a word \ '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 \ 'a word" is uminus