# HG changeset patch
# User haftmann
# Date 1581285787 0
# Node ID 745e518d3d0b2cb5e83c72fd09842c1fc92dce90
# Parent  f2da99316b869bf932bfa026296c4b0bbbb6a104
easy abstraction over pointwise bit operations

diff -r f2da99316b86 -r 745e518d3d0b src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sun Feb 09 21:58:42 2020 +0000
+++ b/src/HOL/Parity.thy	Sun Feb 09 22:03:07 2020 +0000
@@ -42,9 +42,6 @@
   "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   by (cases a rule: parity_cases) simp_all
 
-lemma mod2_eq_if: "a mod 2 = (if 2 dvd a then 0 else 1)"
-  by (simp add: even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one)
-
 lemma evenE [elim?]:
   assumes "even a"
   obtains b where "a = 2 * b"
@@ -69,6 +66,14 @@
   "of_bool (odd a) = a mod 2"
   by (simp add: mod_2_eq_odd)
 
+lemma even_mod_2_iff [simp]:
+  \<open>even (a mod 2) \<longleftrightarrow> even a\<close>
+  by (simp add: mod_2_eq_odd)
+
+lemma mod2_eq_if:
+  "a mod 2 = (if even a then 0 else 1)"
+  by (simp add: mod_2_eq_odd)
+
 lemma even_zero [simp]:
   "even 0"
   by (fact dvd_0_right)
@@ -854,19 +859,6 @@
   \<open>a = b \<longleftrightarrow> (\<forall>n. bit a n \<longleftrightarrow> bit b n)\<close>
   by (auto intro: bit_eqI)
 
-lemma bit_eq_rec:
-  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
-  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 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:
   \<open>bit (2 ^ m) n \<longleftrightarrow> 2 ^ m \<noteq> 0 \<and> m = n\<close>
   by (auto simp add: bit_def exp_div_exp_eq)
@@ -892,6 +884,24 @@
   ultimately show ?thesis by (simp add: ac_simps)
 qed
 
+lemma bit_double_iff:
+  \<open>bit (2 * a) n \<longleftrightarrow> bit a (n - 1) \<and> n \<noteq> 0 \<and> 2 ^ n \<noteq> 0\<close>
+  using even_mult_exp_div_exp_iff [of a 1 n]
+  by (cases n, auto simp add: bit_def ac_simps)
+
+lemma bit_eq_rec:
+  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
+  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 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_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)
diff -r f2da99316b86 -r 745e518d3d0b src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Sun Feb 09 21:58:42 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Sun Feb 09 22:03:07 2020 +0000
@@ -12,9 +12,9 @@
 subsection \<open>Bit operations in suitable algebraic structures\<close>
 
 class semiring_bit_operations = semiring_bit_shifts +
-  fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "AND" 64)
-    and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "OR"  59)
-    and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr "XOR" 59)
+  fixes "and" :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>AND\<close> 64)
+    and or :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>OR\<close>  59)
+    and xor :: \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close>  (infixr \<open>XOR\<close> 59)
   assumes bit_and_iff: \<open>\<And>n. bit (a AND b) n \<longleftrightarrow> bit a n \<and> bit b n\<close>
     and bit_or_iff: \<open>\<And>n. bit (a OR b) n \<longleftrightarrow> bit a n \<or> bit b n\<close>
     and bit_xor_iff: \<open>\<And>n. bit (a XOR b) n \<longleftrightarrow> bit a n \<noteq> bit b n\<close>
@@ -28,61 +28,10 @@
   are specified as definitional class operations.
 \<close>
 
-definition map_bit :: \<open>nat \<Rightarrow> (bool \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>map_bit n f a = take_bit n a + push_bit n (of_bool (f (bit a n)) + 2 * drop_bit (Suc n) a)\<close>
-
-definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>set_bit n = map_bit n top\<close>
-
-definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>unset_bit n = map_bit n bot\<close>
-
-definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
-  where \<open>flip_bit n = map_bit n Not\<close>
-
-text \<open>
-  Having 
-  \<^const>\<open>set_bit\<close>, \<^const>\<open>unset_bit\<close> and \<^const>\<open>flip_bit\<close> as separate
-  operations allows to implement them using bit masks later.
-\<close>
-
 lemma stable_imp_drop_eq:
   \<open>drop_bit n a = a\<close> if \<open>a div 2 = a\<close>
   by (induction n) (simp_all add: that)
 
-lemma map_bit_0 [simp]:
-  \<open>map_bit 0 f a = of_bool (f (odd a)) + 2 * (a div 2)\<close>
-  by (simp add: map_bit_def)
-
-lemma map_bit_Suc [simp]:
-  \<open>map_bit (Suc n) f a = a mod 2 + 2 * map_bit n f (a div 2)\<close>
-  by (auto simp add: map_bit_def algebra_simps mod2_eq_if push_bit_add mult_2
-    elim: evenE oddE)
-
-lemma set_bit_0 [simp]:
-  \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
-  by (simp add: set_bit_def)
-
-lemma set_bit_Suc [simp]:
-  \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
-  by (simp add: set_bit_def)
-
-lemma unset_bit_0 [simp]:
-  \<open>unset_bit 0 a = 2 * (a div 2)\<close>
-  by (simp add: unset_bit_def)
-
-lemma unset_bit_Suc [simp]:
-  \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
-  by (simp add: unset_bit_def)
-
-lemma flip_bit_0 [simp]:
-  \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
-  by (simp add: flip_bit_def)
-
-lemma flip_bit_Suc [simp]:
-  \<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)
 
@@ -193,9 +142,8 @@
 
 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)
+  apply (simp add: bit_eq_iff bit_and_iff)
+  apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff)
   done
 
 sublocale bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
@@ -203,14 +151,12 @@
 proof -
   interpret bit: boolean_algebra \<open>(AND)\<close> \<open>(OR)\<close> NOT 0 \<open>- 1\<close>
     apply standard
-         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)
+         apply (simp_all add: bit_eq_iff bit_and_iff bit_or_iff bit_not_iff)
+      apply (auto simp add: exp_eq_0_imp_not_bit bit_exp_iff)
     done
   show \<open>boolean_algebra (AND) (OR) NOT 0 (- 1)\<close>
     by standard
-  show \<open>boolean_algebra.xor (AND) (OR) NOT = (XOR)\<close> 
+  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_all add: bit_exp_iff, simp_all add: bit_def)
         apply (metis local.bit_exp_iff local.bits_div_by_0)
@@ -233,6 +179,130 @@
   apply (use local.exp_eq_0_imp_not_bit in blast)
   done
 
+definition set_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>set_bit n a = a OR 2 ^ n\<close>
+
+definition unset_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>unset_bit n a = a AND NOT (2 ^ n)\<close>
+
+definition flip_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+  where \<open>flip_bit n a = a XOR 2 ^ n\<close>
+
+lemma bit_set_bit_iff:
+  \<open>bit (set_bit m a) n \<longleftrightarrow> bit a n \<or> (m = n \<and> 2 ^ n \<noteq> 0)\<close>
+  by (auto simp add: set_bit_def bit_or_iff bit_exp_iff)
+
+lemma even_set_bit_iff:
+  \<open>even (set_bit m a) \<longleftrightarrow> even a \<and> m \<noteq> 0\<close>
+  using bit_set_bit_iff [of m a 0] by auto
+
+lemma bit_unset_bit_iff:
+  \<open>bit (unset_bit m a) n \<longleftrightarrow> bit a n \<and> m \<noteq> n\<close>
+  by (auto simp add: unset_bit_def bit_and_iff bit_not_iff bit_exp_iff exp_eq_0_imp_not_bit)
+
+lemma even_unset_bit_iff:
+  \<open>even (unset_bit m a) \<longleftrightarrow> even a \<or> m = 0\<close>
+  using bit_unset_bit_iff [of m a 0] by auto
+
+lemma bit_flip_bit_iff:
+  \<open>bit (flip_bit m a) n \<longleftrightarrow> (m = n \<longleftrightarrow> \<not> bit a n) \<and> 2 ^ n \<noteq> 0\<close>
+  by (auto simp add: flip_bit_def bit_xor_iff bit_exp_iff exp_eq_0_imp_not_bit)
+
+lemma even_flip_bit_iff:
+  \<open>even (flip_bit m a) \<longleftrightarrow> \<not> (even a \<longleftrightarrow> m = 0)\<close>
+  using bit_flip_bit_iff [of m a 0] by auto
+
+lemma set_bit_0 [simp]:
+  \<open>set_bit 0 a = 1 + 2 * (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  then show \<open>bit (set_bit 0 a) m = bit (1 + 2 * (a div 2)) m\<close>
+    by (simp add: bit_set_bit_iff bit_double_iff even_bit_succ_iff)
+      (cases m, simp_all)
+qed
+
+lemma set_bit_Suc [simp]:
+  \<open>set_bit (Suc n) a = a mod 2 + 2 * set_bit n (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  show \<open>bit (set_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * set_bit n (a div 2)) m\<close>
+  proof (cases m)
+    case 0
+    then show ?thesis
+      by (simp add: even_set_bit_iff)
+  next
+    case (Suc m)
+    with * have \<open>2 ^ m \<noteq> 0\<close>
+      using mult_2 by auto
+    show ?thesis
+      by (cases a rule: parity_cases)
+        (simp_all add: bit_set_bit_iff bit_double_iff even_bit_succ_iff *,
+        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+  qed
+qed
+
+lemma unset_bit_0 [simp]:
+  \<open>unset_bit 0 a = 2 * (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  then show \<open>bit (unset_bit 0 a) m = bit (2 * (a div 2)) m\<close>
+    by (simp add: bit_unset_bit_iff bit_double_iff)
+      (cases m, simp_all)
+qed
+
+lemma unset_bit_Suc [simp]:
+  \<open>unset_bit (Suc n) a = a mod 2 + 2 * unset_bit n (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  then show \<open>bit (unset_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * unset_bit n (a div 2)) m\<close>
+  proof (cases m)
+    case 0
+    then show ?thesis
+      by (simp add: even_unset_bit_iff)
+  next
+    case (Suc m)
+    show ?thesis
+      by (cases a rule: parity_cases)
+        (simp_all add: bit_unset_bit_iff bit_double_iff even_bit_succ_iff *,
+         simp_all add: Suc)
+  qed
+qed
+
+lemma flip_bit_0 [simp]:
+  \<open>flip_bit 0 a = of_bool (even a) + 2 * (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  then show \<open>bit (flip_bit 0 a) m = bit (of_bool (even a) + 2 * (a div 2)) m\<close>
+    by (simp add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff)
+      (cases m, simp_all)
+qed
+
+lemma flip_bit_Suc [simp]:
+  \<open>flip_bit (Suc n) a = a mod 2 + 2 * flip_bit n (a div 2)\<close>
+proof (rule bit_eqI)
+  fix m
+  assume *: \<open>2 ^ m \<noteq> 0\<close>
+  show \<open>bit (flip_bit (Suc n) a) m \<longleftrightarrow> bit (a mod 2 + 2 * flip_bit n (a div 2)) m\<close>
+  proof (cases m)
+    case 0
+    then show ?thesis
+      by (simp add: even_flip_bit_iff)
+  next
+    case (Suc m)
+    with * have \<open>2 ^ m \<noteq> 0\<close>
+      using mult_2 by auto
+    show ?thesis
+      by (cases a rule: parity_cases)
+        (simp_all add: bit_flip_bit_iff bit_double_iff even_bit_succ_iff,
+        simp_all add: Suc \<open>2 ^ m \<noteq> 0\<close>)
+  qed
+qed
+
 end