--- 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 \<open>a div 2 = a\<close> by (simp add: hyp)
qed
+lemma exp_eq_0_imp_not_bit:
+ \<open>\<not> bit a n\<close> if \<open>2 ^ n = 0\<close>
+ using that by (simp add: bit_def)
+
lemma bit_eqI:
- \<open>a = b\<close> if \<open>\<And>n. bit a n \<longleftrightarrow> bit b n\<close>
-using that proof (induction a arbitrary: b rule: bits_induct)
- case (stable a)
- from stable(2) [of 0] have **: \<open>even b \<longleftrightarrow> even a\<close>
- by simp
- have \<open>b div 2 = b\<close>
- proof (rule bit_iff_idd_imp_stable)
- fix n
- from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close>
- by simp
- also have \<open>bit a n \<longleftrightarrow> odd a\<close>
- using stable by (simp add: stable_imp_bit_iff_odd)
- finally show \<open>bit b n \<longleftrightarrow> odd b\<close>
- by (simp add: **)
+ \<open>a = b\<close> if \<open>\<And>n. 2 ^ n \<noteq> 0 \<Longrightarrow> bit a n \<longleftrightarrow> bit b n\<close>
+proof -
+ have \<open>bit a n \<longleftrightarrow> bit b n\<close> for n
+ proof (cases \<open>2 ^ n = 0\<close>)
+ 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 \<open>a mod 2 = b mod 2\<close>
- by (simp add: mod2_eq_if)
- then have \<open>a mod 2 + (a + b) = b mod 2 + (a + b)\<close>
- by simp
- then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
- by (simp add: ac_simps)
- with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
- by (simp add: bits_stable_imp_add_self)
-next
- case (rec a p)
- from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
- by simp
- from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
- using rec.prems [of \<open>Suc n\<close>] by simp
- then have \<open>a = b div 2\<close>
- by (rule rec.IH)
- then have \<open>2 * a = 2 * (b div 2)\<close>
- by simp
- then have \<open>b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\<close>
- by simp
- also have \<open>\<dots> = b\<close>
- 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 **: \<open>even b \<longleftrightarrow> even a\<close>
+ by simp
+ have \<open>b div 2 = b\<close>
+ proof (rule bit_iff_idd_imp_stable)
+ fix n
+ from stable have *: \<open>bit b n \<longleftrightarrow> bit a n\<close>
+ by simp
+ also have \<open>bit a n \<longleftrightarrow> odd a\<close>
+ using stable by (simp add: stable_imp_bit_iff_odd)
+ finally show \<open>bit b n \<longleftrightarrow> odd b\<close>
+ by (simp add: **)
+ qed
+ from ** have \<open>a mod 2 = b mod 2\<close>
+ by (simp add: mod2_eq_if)
+ then have \<open>a mod 2 + (a + b) = b mod 2 + (a + b)\<close>
+ by simp
+ then have \<open>a + a mod 2 + b = b + b mod 2 + a\<close>
+ by (simp add: ac_simps)
+ with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
+ by (simp add: bits_stable_imp_add_self)
+ next
+ case (rec a p)
+ from rec.prems [of 0] have [simp]: \<open>p = odd b\<close>
+ by simp
+ from rec.hyps have \<open>bit a n \<longleftrightarrow> bit (b div 2) n\<close> for n
+ using rec.prems [of \<open>Suc n\<close>] by simp
+ then have \<open>a = b div 2\<close>
+ by (rule rec.IH)
+ then have \<open>2 * a = 2 * (b div 2)\<close>
+ by simp
+ then have \<open>b mod 2 + 2 * a = b mod 2 + 2 * (b div 2)\<close>
+ by simp
+ also have \<open>\<dots> = b\<close>
+ 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:
\<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
- 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 @@
\<open>bit 2 n \<longleftrightarrow> 2 \<noteq> 0 \<and> n = 1\<close>
using bit_exp_iff [of 1 n] by auto
+lemma even_bit_succ_iff:
+ \<open>bit (1 + a) n \<longleftrightarrow> bit a n \<or> n = 0\<close> if \<open>even a\<close>
+ using that by (cases \<open>n = 0\<close>) (simp_all add: bit_def)
+
+lemma odd_bit_iff_bit_pred:
+ \<open>bit a n \<longleftrightarrow> bit (a - 1) n \<or> n = 0\<close> if \<open>odd a\<close>
+proof -
+ from \<open>odd a\<close> obtain b where \<open>a = 2 * b + 1\<close> ..
+ moreover have \<open>bit (2 * b) n \<or> n = 0 \<longleftrightarrow> bit (1 + 2 * b) n\<close>
+ using even_bit_succ_iff by simp
+ ultimately show ?thesis by (simp add: ac_simps)
+qed
+
+lemma bit_mask_iff:
+ \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
+ by (simp add: bit_def even_mask_div_iff not_le)
+
end
lemma nat_bit_induct [case_names zero even odd]:
--- 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:
- \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
- by (simp add: bit_def even_mask_div_iff not_le)
-
-end
-
context semiring_bit_shifts
begin
@@ -101,6 +92,15 @@
\<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
by (simp add: flip_bit_def)
+sublocale "and": semilattice \<open>(AND)\<close>
+ by standard (auto simp add: bit_eq_iff bit_and_iff)
+
+sublocale or: semilattice_neutr \<open>(OR)\<close> 0
+ by standard (auto simp add: bit_eq_iff bit_or_iff)
+
+sublocale xor: comm_monoid \<open>(XOR)\<close> 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]:
\<open>take_bit n (a AND b) = take_bit n a AND take_bit n b\<close>
@@ -168,6 +176,10 @@
\<open>bit (- a) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> \<not> bit (a - 1) n\<close>
by (simp add: minus_eq_not_minus_1 bit_not_iff)
+lemma even_not_iff [simp]:
+ "even (NOT a) \<longleftrightarrow> odd a"
+ using bit_not_iff [of a 0] by auto
+
lemma bit_not_exp_iff:
\<open>bit (NOT (2 ^ m)) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n \<noteq> m\<close>
by (auto simp add: bit_not_iff bit_exp_iff)
@@ -184,24 +196,34 @@
\<open>bit (- 2) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n > 0\<close>
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 \<open>(AND)\<close> \<open>- 1\<close>
+ 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 \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
rewrites \<open>bit.xor = (XOR)\<close>
proof -
interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
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 \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
by standard
show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close>
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 @@
\<open>take_bit n (NOT (take_bit n a)) = take_bit n (NOT a)\<close>
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) \<longleftrightarrow> 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 \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> 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) \<longleftrightarrow> 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) \<longleftrightarrow> 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) \<longleftrightarrow> 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
--- 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 \<Rightarrow> '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 \<Rightarrow> 'a word \<Rightarrow> 'a word"
is \<open>and\<close>