# HG changeset patch # User haftmann # Date 1701550189 0 # Node ID 7476818dfd5d7c9525f81546356b7a00a9a4bc7c # Parent b90bf6636260e760b78349cf2bb496be6fa1067d generalized diff -r b90bf6636260 -r 7476818dfd5d src/HOL/Bit_Operations.thy --- a/src/HOL/Bit_Operations.thy Sat Dec 02 20:49:48 2023 +0000 +++ b/src/HOL/Bit_Operations.thy Sat Dec 02 20:49:49 2023 +0000 @@ -5,7 +5,7 @@ theory Bit_Operations imports Presburger Groups_List -begin +begin subsection \Abstract bit structures\ @@ -83,10 +83,6 @@ \0 mod a = 0\ using div_mult_mod_eq [of 0 a] by simp -lemma bits_one_mod_two_eq_one [simp]: - \1 mod 2 = 1\ - by (simp add: mod2_eq_if) - lemma bit_0: \bit a 0 \ odd a\ by (simp add: bit_iff_odd) @@ -3764,6 +3760,8 @@ context semiring_bit_operations begin +lemmas bits_one_mod_two_eq_one [no_atp] = one_mod_two_eq_one + lemmas set_bit_def [no_atp] = set_bit_eq_or lemmas unset_bit_def [no_atp] = unset_bit_eq_and_not diff -r b90bf6636260 -r 7476818dfd5d src/HOL/Parity.thy --- a/src/HOL/Parity.thy Sat Dec 02 20:49:48 2023 +0000 +++ b/src/HOL/Parity.thy Sat Dec 02 20:49:49 2023 +0000 @@ -41,25 +41,6 @@ context semiring_parity begin -lemma parity_cases [case_names even odd]: - assumes "even a \ a mod 2 = 0 \ P" - assumes "odd a \ a mod 2 = 1 \ P" - shows P - using assms by (cases "even a") - (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric]) - -lemma odd_of_bool_self [simp]: - \odd (of_bool p) \ p\ - by (cases p) simp_all - -lemma not_mod_2_eq_0_eq_1 [simp]: - "a mod 2 \ 0 \ a mod 2 = 1" - by (cases a rule: parity_cases) simp_all - -lemma not_mod_2_eq_1_eq_0 [simp]: - "a mod 2 \ 1 \ a mod 2 = 0" - by (cases a rule: parity_cases) simp_all - lemma evenE [elim?]: assumes "even a" obtains b where "a = 2 * b" @@ -77,11 +58,23 @@ qed lemma mod_2_eq_odd: - "a mod 2 = of_bool (odd a)" - by (auto elim: oddE simp add: even_iff_mod_2_eq_zero) + \a mod 2 = of_bool (odd a)\ + by (simp_all flip: odd_iff_mod_2_eq_one even_iff_mod_2_eq_zero) lemma of_bool_odd_eq_mod_2: - "of_bool (odd a) = a mod 2" + \of_bool (odd a) = a mod 2\ + by (simp add: mod_2_eq_odd) + +lemma odd_of_bool_self [simp]: + \odd (of_bool p) \ p\ + by (cases p) simp_all + +lemma not_mod_2_eq_0_eq_1 [simp]: + \a mod 2 \ 0 \ a mod 2 = 1\ + by (simp add: mod_2_eq_odd) + +lemma not_mod_2_eq_1_eq_0 [simp]: + \a mod 2 \ 1 \ a mod 2 = 0\ by (simp add: mod_2_eq_odd) lemma even_mod_2_iff [simp]: @@ -92,8 +85,22 @@ "a mod 2 = (if even a then 0 else 1)" by (simp add: mod_2_eq_odd) +lemma zero_mod_two_eq_zero [simp]: + \0 mod 2 = 0\ + by (simp add: mod_2_eq_odd) + +lemma one_mod_two_eq_one [simp]: + \1 mod 2 = 1\ + by (simp add: mod_2_eq_odd) + +lemma parity_cases [case_names even odd]: + assumes \even a \ a mod 2 = 0 \ P\ + assumes \odd a \ a mod 2 = 1 \ P\ + shows P + using assms by (auto simp add: mod_2_eq_odd) + lemma even_zero [simp]: - "even 0" + \even 0\ by (fact dvd_0_right) lemma odd_even_add: @@ -622,15 +629,6 @@ by simp qed -lemma one_mod_two_eq_one [simp]: - "1 mod 2 = 1" -proof - - from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1" - by (simp only:) simp - then show ?thesis - by simp -qed - lemma one_mod_2_pow_eq [simp]: "1 mod (2 ^ n) = of_bool (n > 0)" proof -