--- a/src/HOL/ex/Bit_Operations.thy Thu Jun 04 15:30:22 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy Thu Jun 04 19:38:50 2020 +0000
@@ -57,11 +57,11 @@
"a AND 0 = 0"
by (simp add: bit_eq_iff bit_and_iff)
-lemma one_and_eq [simp]:
+lemma one_and_eq:
"1 AND a = a mod 2"
by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff)
-lemma and_one_eq [simp]:
+lemma and_one_eq:
"a AND 1 = a mod 2"
using one_and_eq [of a] by (simp add: ac_simps)
--- a/src/HOL/ex/Word.thy Thu Jun 04 15:30:22 2020 +0000
+++ b/src/HOL/ex/Word.thy Thu Jun 04 19:38:50 2020 +0000
@@ -721,14 +721,14 @@
lemma even_word_iff [code]:
\<open>even_word a \<longleftrightarrow> a AND 1 = 0\<close>
- by (simp add: even_word_def even_iff_mod_2_eq_zero)
+ by (simp add: even_word_def and_one_eq even_iff_mod_2_eq_zero)
definition bit_word :: \<open>'a::len word \<Rightarrow> nat \<Rightarrow> bool\<close>
where [code_abbrev]: \<open>bit_word = bit\<close>
lemma bit_word_iff [code]:
\<open>bit_word a n \<longleftrightarrow> drop_bit n a AND 1 = 1\<close>
- by (simp add: bit_word_def bit_iff_odd_drop_bit odd_iff_mod_2_eq_one)
+ by (simp add: bit_word_def bit_iff_odd_drop_bit and_one_eq odd_iff_mod_2_eq_one)
lifting_update word.lifting
lifting_forget word.lifting