author haftmann Mon, 03 Feb 2020 20:42:04 +0000 changeset 71418 bd9d27ccb3a3 parent 71417 89d05db6dd1f child 71419 1d8e914e04d6
more theorems
 src/HOL/Parity.thy file | annotate | diff | comparison | revisions src/HOL/ex/Bit_Operations.thy file | annotate | diff | comparison | revisions src/HOL/ex/Word.thy file | annotate | diff | comparison | revisions
```--- 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>
+  \<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
+  next
+    case False
+    then show ?thesis
+      by (rule that)
qed
-  from ** have \<open>a mod 2 = b mod 2\<close>
-  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>
-  with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
-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>
+    qed
+    from ** have \<open>a mod 2 = b mod 2\<close>
+    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>
+    with \<open>a div 2 = a\<close> \<open>b div 2 = b\<close> show ?case
+  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 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
+
+  \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
+
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
-
-  \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>
-
-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>

+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"
@@ -109,21 +109,29 @@
"a AND 0 = 0"

-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)"

-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)"

-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>

+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>

+lemma not_one [simp]:
+  "NOT 1 = - 2"
+
+sublocale "and": semilattice_neutr \<open>(AND)\<close> \<open>- 1\<close>
+  apply standard
+  apply (auto simp add: bit_eq_iff bit_and_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 (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 (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 (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 (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 (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

@@ -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)"
-
-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
-
-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