diff -r f10bffaa2bae -r b612edee9b0c src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy Mon Mar 09 19:35:07 2020 +0100 +++ b/src/HOL/ex/Bit_Operations.thy Sun Mar 08 17:07:49 2020 +0000 @@ -28,10 +28,6 @@ are specified as definitional class operations. \ -lemma stable_imp_drop_eq: - \drop_bit n a = a\ if \a div 2 = a\ - by (induction n) (simp_all add: that) - sublocale "and": semilattice \(AND)\ by standard (auto simp add: bit_eq_iff bit_and_iff) @@ -219,7 +215,7 @@ assume *: \2 ^ m \ 0\ then show \bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\ by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff) - (cases m, simp_all) + (cases m, simp_all add: bit_Suc) qed lemma set_bit_Suc [simp]: @@ -239,7 +235,7 @@ show ?thesis by (cases a rule: parity_cases) (simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *, - simp_all add: Suc \2 ^ m \ 0\) + simp_all add: Suc \2 ^ m \ 0\ bit_Suc) qed qed @@ -250,7 +246,7 @@ assume *: \2 ^ m \ 0\ then show \bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\ by (simp add: bit_unset_bit_iff bit_double_iff) - (cases m, simp_all) + (cases m, simp_all add: bit_Suc) qed lemma unset_bit_Suc [simp]: @@ -268,7 +264,7 @@ show ?thesis by (cases a rule: parity_cases) (simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *, - simp_all add: Suc) + simp_all add: Suc bit_Suc) qed qed @@ -279,7 +275,7 @@ assume *: \2 ^ m \ 0\ then show \bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\ by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff) - (cases m, simp_all) + (cases m, simp_all add: bit_Suc) qed lemma flip_bit_Suc [simp]: @@ -299,7 +295,7 @@ show ?thesis by (cases a rule: parity_cases) (simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff, - simp_all add: Suc \2 ^ m \ 0\) + simp_all add: Suc \2 ^ m \ 0\ bit_Suc) qed qed @@ -348,7 +344,7 @@ next case (Suc n) then show ?case - by (simp add: rec [of m n]) + by (simp add: rec [of m n] bit_Suc) qed sublocale abel_semigroup F @@ -461,7 +457,7 @@ next case (Suc n) then show ?case - by (simp add: rec [of k l]) + by (simp add: rec [of k l] bit_Suc) qed sublocale abel_semigroup F @@ -514,7 +510,7 @@ lemma bit_not_iff_int: \bit (NOT k) n \ \ bit k n\ for k :: int - by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int) + by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc) instance proof fix k l :: int and n :: nat