# 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 \<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]:
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:
-  \<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
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 \<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>