# HG changeset patch # User haftmann # Date 1580762524 0 # Node ID bd9d27ccb3a32179ce6fa7bcf70235c2e5fe9a50 # Parent 89d05db6dd1f8f22a107c840a9321294d5c6b421 more theorems diff -r 89d05db6dd1f -r bd9d27ccb3a3 src/HOL/Parity.thy --- a/src/HOL/Parity.thy Tue Feb 04 16:19:15 2020 +0000 +++ b/src/HOL/Parity.thy Mon Feb 03 20:42:04 2020 +0000 @@ -791,46 +791,62 @@ using \a div 2 = a\ by (simp add: hyp) qed +lemma exp_eq_0_imp_not_bit: + \\ bit a n\ if \2 ^ n = 0\ + using that by (simp add: bit_def) + lemma bit_eqI: - \a = b\ if \\n. bit a n \ bit b n\ -using that proof (induction a arbitrary: b rule: bits_induct) - case (stable a) - from stable(2) [of 0] have **: \even b \ even a\ - by simp - have \b div 2 = b\ - proof (rule bit_iff_idd_imp_stable) - fix n - from stable have *: \bit b n \ bit a n\ - by simp - also have \bit a n \ odd a\ - using stable by (simp add: stable_imp_bit_iff_odd) - finally show \bit b n \ odd b\ - by (simp add: **) + \a = b\ if \\n. 2 ^ n \ 0 \ bit a n \ bit b n\ +proof - + have \bit a n \ bit b n\ for n + proof (cases \2 ^ n = 0\) + case True + then show ?thesis + by (simp add: exp_eq_0_imp_not_bit) + next + case False + then show ?thesis + by (rule that) qed - from ** have \a mod 2 = b mod 2\ - by (simp add: mod2_eq_if) - then have \a mod 2 + (a + b) = b mod 2 + (a + b)\ - by simp - then have \a + a mod 2 + b = b + b mod 2 + a\ - by (simp add: ac_simps) - with \a div 2 = a\ \b div 2 = b\ show ?case - by (simp add: bits_stable_imp_add_self) -next - case (rec a p) - from rec.prems [of 0] have [simp]: \p = odd b\ - by simp - from rec.hyps have \bit a n \ bit (b div 2) n\ for n - using rec.prems [of \Suc n\] by simp - then have \a = b div 2\ - by (rule rec.IH) - then have \2 * a = 2 * (b div 2)\ - by simp - then have \b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\ - by simp - also have \\ = b\ - by (fact mod_mult_div_eq) - finally show ?case - by (auto simp add: mod2_eq_if) + then show ?thesis proof (induction a arbitrary: b rule: bits_induct) + case (stable a) + from stable(2) [of 0] have **: \even b \ even a\ + by simp + have \b div 2 = b\ + proof (rule bit_iff_idd_imp_stable) + fix n + from stable have *: \bit b n \ bit a n\ + by simp + also have \bit a n \ odd a\ + using stable by (simp add: stable_imp_bit_iff_odd) + finally show \bit b n \ odd b\ + by (simp add: **) + qed + from ** have \a mod 2 = b mod 2\ + by (simp add: mod2_eq_if) + then have \a mod 2 + (a + b) = b mod 2 + (a + b)\ + by simp + then have \a + a mod 2 + b = b + b mod 2 + a\ + by (simp add: ac_simps) + with \a div 2 = a\ \b div 2 = b\ show ?case + by (simp add: bits_stable_imp_add_self) + next + case (rec a p) + from rec.prems [of 0] have [simp]: \p = odd b\ + by simp + from rec.hyps have \bit a n \ bit (b div 2) n\ for n + using rec.prems [of \Suc n\] by simp + then have \a = b div 2\ + by (rule rec.IH) + then have \2 * a = 2 * (b div 2)\ + by simp + then have \b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\ + by simp + also have \\ = b\ + by (fact mod_mult_div_eq) + finally show ?case + by (auto simp add: mod2_eq_if) + qed qed lemma bit_eq_iff: @@ -839,16 +855,15 @@ lemma bit_eq_rec: \a = b \ (even a \ even b) \ a div 2 = b div 2\ - apply (simp add: bit_eq_iff) - apply auto + apply (auto simp add: bit_eq_iff) using bit_0 apply blast using bit_0 apply blast using bit_Suc apply blast using bit_Suc apply blast - apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq) - apply (metis bit_eq_iff local.even_iff_mod_2_eq_zero local.mod_div_mult_eq) - apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq) - apply (metis bit_eq_iff local.mod2_eq_if local.mod_div_mult_eq) + apply (metis bit_eq_iff even_iff_mod_2_eq_zero mod_div_mult_eq) + apply (metis bit_eq_iff even_iff_mod_2_eq_zero mod_div_mult_eq) + apply (metis bit_eq_iff mod2_eq_if mod_div_mult_eq) + apply (metis bit_eq_iff mod2_eq_if mod_div_mult_eq) done lemma bit_exp_iff: @@ -863,6 +878,23 @@ \bit 2 n \ 2 \ 0 \ n = 1\ using bit_exp_iff [of 1 n] by auto +lemma even_bit_succ_iff: + \bit (1 + a) n \ bit a n \ n = 0\ if \even a\ + using that by (cases \n = 0\) (simp_all add: bit_def) + +lemma odd_bit_iff_bit_pred: + \bit a n \ bit (a - 1) n \ n = 0\ if \odd a\ +proof - + from \odd a\ obtain b where \a = 2 * b + 1\ .. + moreover have \bit (2 * b) n \ n = 0 \ bit (1 + 2 * b) n\ + using even_bit_succ_iff by simp + ultimately show ?thesis by (simp add: ac_simps) +qed + +lemma bit_mask_iff: + \bit (2 ^ m - 1) n \ 2 ^ n \ 0 \ n < m\ + by (simp add: bit_def even_mask_div_iff not_le) + end lemma nat_bit_induct [case_names zero even odd]: diff -r 89d05db6dd1f -r bd9d27ccb3a3 src/HOL/ex/Bit_Operations.thy --- a/src/HOL/ex/Bit_Operations.thy Tue Feb 04 16:19:15 2020 +0000 +++ b/src/HOL/ex/Bit_Operations.thy Mon Feb 03 20:42:04 2020 +0000 @@ -9,15 +9,6 @@ Main begin -context semiring_bits -begin - -lemma bit_mask_iff: - \bit (2 ^ m - 1) n \ 2 ^ n \ 0 \ n < m\ - by (simp add: bit_def even_mask_div_iff not_le) - -end - context semiring_bit_shifts begin @@ -101,6 +92,15 @@ \flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\ by (simp add: flip_bit_def) +sublocale "and": semilattice \(AND)\ + by standard (auto simp add: bit_eq_iff bit_and_iff) + +sublocale or: semilattice_neutr \(OR)\ 0 + by standard (auto simp add: bit_eq_iff bit_or_iff) + +sublocale xor: comm_monoid \(XOR)\ 0 + by standard (auto simp add: bit_eq_iff bit_xor_iff) + lemma zero_and_eq [simp]: "0 AND a = 0" by (simp add: bit_eq_iff bit_and_iff) @@ -109,21 +109,29 @@ "a AND 0 = 0" by (simp add: bit_eq_iff bit_and_iff) -lemma zero_or_eq [simp]: - "0 OR a = a" - by (simp add: bit_eq_iff bit_or_iff) +lemma one_and_eq [simp]: + "1 AND a = of_bool (odd a)" + by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) -lemma or_zero_eq [simp]: - "a OR 0 = a" - by (simp add: bit_eq_iff bit_or_iff) +lemma and_one_eq [simp]: + "a AND 1 = of_bool (odd a)" + using one_and_eq [of a] by (simp add: ac_simps) + +lemma one_or_eq [simp]: + "1 OR a = a + of_bool (even a)" + by (simp add: bit_eq_iff bit_or_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff) -lemma zero_xor_eq [simp]: - "0 XOR a = a" - by (simp add: bit_eq_iff bit_xor_iff) +lemma or_one_eq [simp]: + "a OR 1 = a + of_bool (even a)" + using one_or_eq [of a] by (simp add: ac_simps) -lemma xor_zero_eq [simp]: - "a XOR 0 = a" - by (simp add: bit_eq_iff bit_xor_iff) +lemma one_xor_eq [simp]: + "1 XOR a = a + of_bool (even a) - of_bool (odd a)" + by (simp add: bit_eq_iff bit_xor_iff add.commute [of _ 1] even_bit_succ_iff) (auto simp add: bit_1_iff odd_bit_iff_bit_pred elim: oddE) + +lemma xor_one_int_eq [simp]: + "a XOR 1 = a + of_bool (even a) - of_bool (odd a)" + using one_xor_eq [of a] by (simp add: ac_simps) lemma take_bit_and [simp]: \take_bit n (a AND b) = take_bit n a AND take_bit n b\ @@ -168,6 +176,10 @@ \bit (- a) n \ 2 ^ n \ 0 \ \ bit (a - 1) n\ by (simp add: minus_eq_not_minus_1 bit_not_iff) +lemma even_not_iff [simp]: + "even (NOT a) \ odd a" + using bit_not_iff [of a 0] by auto + lemma bit_not_exp_iff: \bit (NOT (2 ^ m)) n \ 2 ^ n \ 0 \ n \ m\ by (auto simp add: bit_not_iff bit_exp_iff) @@ -184,24 +196,34 @@ \bit (- 2) n \ 2 ^ n \ 0 \ n > 0\ by (simp add: bit_minus_iff bit_1_iff) +lemma not_one [simp]: + "NOT 1 = - 2" + by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff) + +sublocale "and": semilattice_neutr \(AND)\ \- 1\ + apply standard + apply (auto simp add: bit_eq_iff bit_and_iff) + apply (simp add: bit_exp_iff) + apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) + done + sublocale bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ rewrites \bit.xor = (XOR)\ proof - interpret bit: boolean_algebra \(AND)\ \(OR)\ NOT 0 \- 1\ apply standard - apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff) - apply (simp_all add: bit_exp_iff) - apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) + apply simp_all + apply (auto simp add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff) + apply (simp add: bit_exp_iff) apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) done show \boolean_algebra (AND) (OR) NOT 0 (- 1)\ by standard show \boolean_algebra.xor (AND) (OR) NOT = (XOR)\ apply (auto simp add: fun_eq_iff bit.xor_def bit_eq_iff bit_and_iff bit_or_iff bit_not_iff bit_xor_iff) - apply (simp add: bit_exp_iff, simp add: bit_def) - apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) - apply (metis local.bit_def local.bit_exp_iff local.bits_div_by_0) - apply (simp_all add: bit_exp_iff, simp_all add: bit_def) + apply (simp_all add: bit_exp_iff, simp_all add: bit_def) + apply (metis local.bit_exp_iff local.bits_div_by_0) + apply (metis local.bit_exp_iff local.bits_div_by_0) done qed @@ -213,6 +235,13 @@ \take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\ by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff) +lemma take_bit_not_iff: + "take_bit n (NOT a) = take_bit n (NOT b) \ take_bit n a = take_bit n b" + apply (simp add: bit_eq_iff bit_not_iff bit_take_bit_iff) + apply (simp add: bit_exp_iff) + apply (use local.exp_eq_0_imp_not_bit in blast) + done + end @@ -718,7 +747,7 @@ end -lemma not_div_2: +lemma not_int_div_2: "NOT k div 2 = NOT (k div 2)" for k :: int by (simp add: complement_div_2 not_int_def) @@ -726,46 +755,4 @@ "k \ 0 \ k \ - 1 \ NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int by (auto simp add: not_int_def elim: oddE) -lemma not_one_int [simp]: - "NOT 1 = (- 2 :: int)" - by (simp add: bit_eq_iff bit_not_iff) (simp add: bit_1_iff) - -lemma even_not_int_iff [simp]: - "even (NOT k) \ odd k" for k :: int - using bit_not_iff [of k 0] by auto - -lemma one_and_int_eq [simp]: - "1 AND k = of_bool (odd k)" for k :: int - by (simp add: bit_eq_iff bit_and_iff) (auto simp add: bit_1_iff) - -lemma and_one_int_eq [simp]: - "k AND 1 = of_bool (odd k)" for k :: int - using one_and_int_eq [of 1] by (simp add: ac_simps) - -lemma one_or_int_eq [simp]: - "1 OR k = k + of_bool (even k)" for k :: int - using or_int.rec [of 1] by (auto elim: oddE) - -lemma or_one_int_eq [simp]: - "k OR 1 = k + of_bool (even k)" for k :: int - using one_or_int_eq [of k] by (simp add: ac_simps) - -lemma one_xor_int_eq [simp]: - "1 XOR k = k + of_bool (even k) - of_bool (odd k)" for k :: int - using xor_int.rec [of 1] by (auto elim: oddE) - -lemma xor_one_int_eq [simp]: - "k XOR 1 = k + of_bool (even k) - of_bool (odd k)" for k :: int - using one_xor_int_eq [of k] by (simp add: ac_simps) - -lemma take_bit_complement_iff: - "take_bit n (complement k) = take_bit n (complement l) \ take_bit n k = take_bit n l" - for k l :: int - by (simp add: take_bit_eq_mod mod_eq_dvd_iff dvd_diff_commute) - -lemma take_bit_not_iff_int: - "take_bit n (NOT k) = take_bit n (NOT l) \ take_bit n k = take_bit n l" - for k l :: int - by (auto simp add: bit_eq_iff bit_take_bit_iff bit_not_iff_int) - end diff -r 89d05db6dd1f -r bd9d27ccb3a3 src/HOL/ex/Word.thy --- a/src/HOL/ex/Word.thy Tue Feb 04 16:19:15 2020 +0000 +++ b/src/HOL/ex/Word.thy Mon Feb 03 20:42:04 2020 +0000 @@ -674,7 +674,7 @@ lift_definition not_word :: "'a word \ 'a word" is not - by (simp add: take_bit_not_iff_int) + by (simp add: take_bit_not_iff) lift_definition and_word :: "'a word \ 'a word \ 'a word" is \and\