# HG changeset patch
# User haftmann
# Date 1588004331 0
# Node ID 6fd70ed181996d7b0947384a29227ab74eb728e8
# Parent  14914ae80f705666f2a8b31411f17959bf109b54
simplified construction of binary bit operations

diff -r 14914ae80f70 -r 6fd70ed18199 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Apr 25 13:26:25 2020 +0000
+++ b/src/HOL/Parity.thy	Mon Apr 27 16:18:51 2020 +0000
@@ -1509,6 +1509,21 @@
 
 instance int :: unique_euclidean_semiring_with_bit_shifts ..
 
+lemma bit_nat_iff [simp]:
+  \<open>bit (nat k) n \<longleftrightarrow> k > 0 \<and> bit k n\<close>
+proof (cases \<open>k > 0\<close>)
+  case True
+  moreover define m where \<open>m = nat k\<close>
+  ultimately have \<open>k = int m\<close>
+    by simp
+  then show ?thesis
+    by (auto intro: ccontr)
+next
+  case False
+  then show ?thesis
+    by simp
+qed
+
 lemma not_exp_less_eq_0_int [simp]:
   \<open>\<not> 2 ^ n \<le> (0::int)\<close>
   by (simp add: power_le_zero_eq)
diff -r 14914ae80f70 -r 6fd70ed18199 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Sat Apr 25 13:26:25 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Mon Apr 27 16:18:51 2020 +0000
@@ -324,57 +324,38 @@
 class ring_bit_representation = ring_bit_operations + semiring_bit_representation +
   assumes not_eq: "not = of_bits \<circ> map Not \<circ> bits_of"
 
-context zip_nat
-begin
-
-lemma of_bits:
-  "of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: nat)"
-  if "length bs = length cs" for bs cs
-  by (simp add: Parity.bit_eq_iff bit_unsigned_of_bits_iff bit_eq_iff)
-    (simp add: that end_of_bits nth_default_map2 [of _ _ _ False False])
-end
-
 instance nat :: semiring_bit_representation
-  apply standard
-      apply (simp_all only: and_nat.of_bits or_nat.of_bits xor_nat.of_bits)
-   apply simp_all
-  done
+  by standard (simp_all add: bit_eq_iff bit_unsigned_of_bits_iff nth_default_map2 [of _ _ _ False False]
+    bit_and_iff bit_or_iff bit_xor_iff)
 
-context zip_int
-begin
- 
-lemma of_bits:
-  \<open>of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)\<close>
-  if \<open>length bs = length cs\<close> and \<open>\<not> False \<^bold>* False\<close> for bs cs
-proof (cases \<open>bs = []\<close>)
-  case True
-  moreover have \<open>cs = []\<close>
-    using True that by simp
-  ultimately show ?thesis
-    by (simp add: Parity.bit_eq_iff bit_eq_iff that)
-next
-  case False
-  moreover have \<open>cs \<noteq> []\<close>
-    using False that by auto
-  ultimately show ?thesis
-    apply (simp add: Parity.bit_eq_iff bit_of_bits_int_iff bit_eq_iff zip_eq_Nil_iff last_map last_zip that)
-    apply (simp add: that nth_default_map2 [of _ _ _ \<open>last bs\<close> \<open>last cs\<close>])
-    done
+instance int :: ring_bit_representation
+proof
+  {
+    fix bs cs :: \<open>bool list\<close>
+    assume \<open>length bs = length cs\<close>
+    then have \<open>cs = [] \<longleftrightarrow> bs = []\<close>
+      by auto
+    with \<open>length bs = length cs\<close> have \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<and>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<and> (cs \<noteq> [] \<and> last cs)\<close>
+      and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<or>) bs cs) \<longleftrightarrow> (bs \<noteq> [] \<and> last bs) \<or> (cs \<noteq> [] \<and> last cs)\<close>
+      and \<open>zip bs cs \<noteq> [] \<and> last (map2 (\<noteq>) bs cs) \<longleftrightarrow> ((bs \<noteq> [] \<and> last bs) \<noteq> (cs \<noteq> [] \<and> last cs))\<close>
+      by (auto simp add: last_map last_zip zip_eq_Nil_iff prod_eq_iff)
+    then show \<open>of_bits bs AND of_bits cs = (of_bits (map2 (\<and>) bs cs) :: int)\<close>
+      and \<open>of_bits bs OR of_bits cs = (of_bits (map2 (\<or>) bs cs) :: int)\<close>
+      and \<open>of_bits bs XOR of_bits cs = (of_bits (map2 (\<noteq>) bs cs) :: int)\<close>
+      by (simp_all add: fun_eq_iff bit_eq_iff bit_and_iff bit_or_iff bit_xor_iff bit_not_iff bit_of_bits_int_iff \<open>length bs = length cs\<close> nth_default_map2 [of bs cs _ \<open>bs \<noteq> [] \<and> last bs\<close> \<open>cs \<noteq> [] \<and> last cs\<close>])
+  }
+  show \<open>push_bit n k = of_bits (replicate n False @ bits_of k)\<close>
+    for k :: int and n :: nat
+    by (cases "n = 0") simp_all
+  show \<open>drop_bit n k = of_bits (drop n (bits_of k))\<close>
+    if \<open>n < length (bits_of k)\<close> for k :: int and n :: nat
+    using that by simp
+  show \<open>(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of\<close>
+  proof (rule sym, rule ext)
+    fix k :: int
+    show \<open>(of_bits \<circ> map Not \<circ> bits_of) k = NOT k\<close>
+      by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
+  qed
 qed
 
 end
-
-instance int :: ring_bit_representation
-proof
-  show "(not :: int \<Rightarrow> _) = of_bits \<circ> map Not \<circ> bits_of"
-  proof (rule sym, rule ext)
-    fix k :: int
-    show "(of_bits \<circ> map Not \<circ> bits_of) k = NOT k"
-      by (induction k rule: int_bit_induct) (simp_all add: not_int_def)
-  qed
-  show "push_bit n k = of_bits (replicate n False @ bits_of k)"
-    for k :: int and n :: nat
-    by (cases "n = 0") simp_all
-qed (simp_all add: and_int.of_bits or_int.of_bits xor_int.of_bits)
-
-end
diff -r 14914ae80f70 -r 6fd70ed18199 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Sat Apr 25 13:26:25 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Mon Apr 27 16:18:51 2020 +0000
@@ -310,170 +310,8 @@
 end
 
 
-subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
-
-locale zip_nat = single: abel_semigroup f
-    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl \<open>\<^bold>*\<close> 70) +
-  assumes end_of_bits: \<open>\<not> False \<^bold>* False\<close>
-begin
-
-function F :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>  (infixl \<open>\<^bold>\<times>\<close> 70)
-  where \<open>m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
-    else of_bool (odd m \<^bold>* odd n) + 2 * ((m div 2) \<^bold>\<times> (n div 2)))\<close>
-  by auto
-
-termination
-  by (relation "measure (case_prod (+))") auto
-
-declare F.simps [simp del]
-
-lemma rec:
-  "m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
-proof (cases \<open>m = 0 \<and> n = 0\<close>)
-  case True
-  then have \<open>m \<^bold>\<times> n = 0\<close>
-    using True by (simp add: F.simps [of 0 0])
-  moreover have \<open>(m div 2) \<^bold>\<times> (n div 2) = m \<^bold>\<times> n\<close>
-    using True by simp
-  ultimately show ?thesis
-    using True by (simp add: end_of_bits)
-next
-  case False
-  then show ?thesis
-    by (auto simp add: ac_simps F.simps [of m n])
-qed
-
-lemma bit_eq_iff:
-  \<open>bit (m \<^bold>\<times> n) q \<longleftrightarrow> bit m q \<^bold>* bit n q\<close>
-proof (induction q arbitrary: m n)
-  case 0
-  then show ?case
-    by (simp add: rec [of m n])
-next
-  case (Suc n)
-  then show ?case
-    by (simp add: rec [of m n] bit_Suc)
-qed
-
-sublocale abel_semigroup F
-  by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
-
-end
-
-instantiation nat :: semiring_bit_operations
-begin
-
-global_interpretation and_nat: zip_nat \<open>(\<and>)\<close>
-  defines and_nat = and_nat.F
-  by standard auto
-
-global_interpretation and_nat: semilattice \<open>(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-proof (rule semilattice.intro, fact and_nat.abel_semigroup_axioms, standard)
-  show \<open>n AND n = n\<close> for n :: nat
-    by (simp add: bit_eq_iff and_nat.bit_eq_iff)
-qed
-
-global_interpretation or_nat: zip_nat \<open>(\<or>)\<close>
-  defines or_nat = or_nat.F
-  by standard auto
-
-global_interpretation or_nat: semilattice \<open>(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat\<close>
-proof (rule semilattice.intro, fact or_nat.abel_semigroup_axioms, standard)
-  show \<open>n OR n = n\<close> for n :: nat
-    by (simp add: bit_eq_iff or_nat.bit_eq_iff)
-qed
-
-global_interpretation xor_nat: zip_nat \<open>(\<noteq>)\<close>
-  defines xor_nat = xor_nat.F
-  by standard auto
-
-instance proof
-  fix m n q :: nat
-  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-    by (fact and_nat.bit_eq_iff)
-  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-    by (fact or_nat.bit_eq_iff)
-  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-    by (fact xor_nat.bit_eq_iff)
-qed
-
-end
-
-lemma Suc_0_and_eq [simp]:
-  \<open>Suc 0 AND n = of_bool (odd n)\<close>
-  using one_and_eq [of n] by simp
-
-lemma and_Suc_0_eq [simp]:
-  \<open>n AND Suc 0 = of_bool (odd n)\<close>
-  using and_one_eq [of n] by simp
-
-lemma Suc_0_or_eq [simp]:
-  \<open>Suc 0 OR n = n + of_bool (even n)\<close>
-  using one_or_eq [of n] by simp
-
-lemma or_Suc_0_eq [simp]:
-  \<open>n OR Suc 0 = n + of_bool (even n)\<close>
-  using or_one_eq [of n] by simp
-
-lemma Suc_0_xor_eq [simp]:
-  \<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
-  using one_xor_eq [of n] by simp
-
-lemma xor_Suc_0_eq [simp]:
-  \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
-  using xor_one_eq [of n] by simp
-
-
 subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
 
-locale zip_int = single: abel_semigroup f
-  for f :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>  (infixl \<open>\<^bold>*\<close> 70)
-begin
-
-function F :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>  (infixl \<open>\<^bold>\<times>\<close> 70)
-  where \<open>k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
-    then - of_bool (odd k \<^bold>* odd l)
-    else of_bool (odd k \<^bold>* odd l) + 2 * ((k div 2) \<^bold>\<times> (l div 2)))\<close>
-  by auto
-
-termination
-  by (relation "measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))") auto
-
-declare F.simps [simp del]
-
-lemma rec:
-  \<open>k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + 2 * ((k div 2) \<^bold>\<times> (l div 2))\<close>
-proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
-  case True
-  then have \<open>(k div 2) \<^bold>\<times> (l div 2) = k \<^bold>\<times> l\<close>
-    by auto
-  moreover have \<open>of_bool (odd k \<^bold>* odd l) = - (k \<^bold>\<times> l)\<close>
-    using True by (simp add: F.simps [of k l])
-  ultimately show ?thesis by simp
-next
-  case False
-  then show ?thesis
-    by (auto simp add: ac_simps F.simps [of k l])
-qed
-
-lemma bit_eq_iff:
-  \<open>bit (k \<^bold>\<times> l) n \<longleftrightarrow> bit k n \<^bold>* bit l n\<close>
-proof (induction n arbitrary: k l)
-  case 0
-  then show ?case
-    by (simp add: rec [of k l])
-next
-  case (Suc n)
-  then show ?case
-    by (simp add: rec [of k l] bit_Suc)
-qed
-
-lemma abel_semigroup_axioms:
-  \<open>abel_semigroup F\<close>
-  by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
-
-end
-
 instantiation int :: ring_bit_operations
 begin
 
@@ -492,46 +330,89 @@
   \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
   by (simp add: not_int_def)
 
-lemma bit_not_iff_int:
+lemma bit_not_int_iff:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
   by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int bit_Suc)
 
-global_interpretation and_int: zip_int "(\<and>)"
-  defines and_int = and_int.F
-  by standard
+function and_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>(k::int) AND l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
+    then - of_bool (odd k \<and> odd l)
+    else of_bool (odd k \<and> odd l) + 2 * ((k div 2) AND (l div 2)))\<close>
+  by auto
+
+termination
+  by (relation \<open>measure (\<lambda>(k, l). nat (\<bar>k\<bar> + \<bar>l\<bar>))\<close>) auto
+
+declare and_int.simps [simp del]
 
-interpretation and_int: semilattice "(AND) :: int \<Rightarrow> int \<Rightarrow> int"
-proof (rule semilattice.intro, fact and_int.abel_semigroup_axioms, standard)
-  show "k AND k = k" for k :: int
-    by (simp add: bit_eq_iff and_int.bit_eq_iff)
+lemma and_int_rec:
+  \<open>k AND l = of_bool (odd k \<and> odd l) + 2 * ((k div 2) AND (l div 2))\<close>
+    for k l :: int
+proof (cases \<open>k \<in> {0, - 1} \<and> l \<in> {0, - 1}\<close>)
+  case True
+  then show ?thesis
+    by auto (simp_all add: and_int.simps)
+next
+  case False
+  then show ?thesis
+    by (auto simp add: ac_simps and_int.simps [of k l])
 qed
 
-global_interpretation or_int: zip_int "(\<or>)"
-  defines or_int = or_int.F
-  by standard
-
-interpretation or_int: semilattice "(OR) :: int \<Rightarrow> int \<Rightarrow> int"
-proof (rule semilattice.intro, fact or_int.abel_semigroup_axioms, standard)
-  show "k OR k = k" for k :: int
-    by (simp add: bit_eq_iff or_int.bit_eq_iff)
+lemma bit_and_int_iff:
+  \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close> for k l :: int
+proof (induction n arbitrary: k l)
+  case 0
+  then show ?case
+    by (simp add: and_int_rec [of k l])
+next
+  case (Suc n)
+  then show ?case
+    by (simp add: and_int_rec [of k l] bit_Suc)
 qed
 
-global_interpretation xor_int: zip_int "(\<noteq>)"
-  defines xor_int = xor_int.F
-  by standard
+lemma even_and_iff_int:
+  \<open>even (k AND l) \<longleftrightarrow> even k \<or> even l\<close> for k l :: int
+  using bit_and_int_iff [of k l 0] by auto
+
+definition or_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k OR l = NOT (NOT k AND NOT l)\<close> for k l :: int
+
+lemma or_int_rec:
+  \<open>k OR l = of_bool (odd k \<or> odd l) + 2 * ((k div 2) OR (l div 2))\<close>
+  for k l :: int
+  using and_int_rec [of \<open>NOT k\<close> \<open>NOT l\<close>]
+  by (simp add: or_int_def even_not_iff_int not_int_div_2)
+    (simp add: not_int_def)
+
+lemma bit_or_int_iff:
+  \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close> for k l :: int
+  by (simp add: or_int_def bit_not_int_iff bit_and_int_iff)
+
+definition xor_int :: \<open>int \<Rightarrow> int \<Rightarrow> int\<close>
+  where \<open>k XOR l = k AND NOT l OR NOT k AND l\<close> for k l :: int
+
+lemma xor_int_rec:
+  \<open>k XOR l = of_bool (odd k \<noteq> odd l) + 2 * ((k div 2) XOR (l div 2))\<close>
+  for k l :: int
+  by (simp add: xor_int_def or_int_rec [of \<open>k AND NOT l\<close> \<open>NOT k AND l\<close>] even_and_iff_int even_not_iff_int)
+    (simp add: and_int_rec [of \<open>NOT k\<close> \<open>l\<close>] and_int_rec [of \<open>k\<close> \<open>NOT l\<close>] not_int_div_2)
+
+lemma bit_xor_int_iff:
+  \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close> for k l :: int
+  by (auto simp add: xor_int_def bit_or_int_iff bit_and_int_iff bit_not_int_iff)
 
 instance proof
   fix k l :: int and n :: nat
   show \<open>- k = NOT (k - 1)\<close>
     by (simp add: not_int_def)
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
-    by (fact and_int.bit_eq_iff)
+    by (fact bit_and_int_iff)
   show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-    by (fact or_int.bit_eq_iff)
+    by (fact bit_or_int_iff)
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
-    by (fact xor_int.bit_eq_iff)
-qed (simp_all add: bit_not_iff_int)
+    by (fact bit_xor_int_iff)
+qed (simp_all add: bit_not_int_iff)
 
 end
 
@@ -556,14 +437,14 @@
 next
   case (even k)
   then show ?case
-    using and_int.rec [of \<open>k * 2\<close> l] by (simp add: pos_imp_zdiv_nonneg_iff)
+    using and_int_rec [of \<open>k * 2\<close> l] by (simp add: pos_imp_zdiv_nonneg_iff)
 next
   case (odd k)
   from odd have \<open>0 \<le> k AND l div 2 \<longleftrightarrow> 0 \<le> k \<or> 0 \<le> l div 2\<close>
     by simp
   then have \<open>0 \<le> (1 + k * 2) div 2 AND l div 2 \<longleftrightarrow> 0 \<le> (1 + k * 2) div 2\<or> 0 \<le> l div 2\<close>
     by simp
-  with and_int.rec [of \<open>1 + k * 2\<close> l]
+  with and_int_rec [of \<open>1 + k * 2\<close> l]
   show ?case
     by auto
 qed
@@ -613,6 +494,69 @@
   by (simp add: flip_bit_def)
 
 
+subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
+
+instantiation nat :: semiring_bit_operations
+begin
+
+definition and_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m AND n = nat (int m AND int n)\<close> for m n :: nat
+
+definition or_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m OR n = nat (int m OR int n)\<close> for m n :: nat
+
+definition xor_nat :: \<open>nat \<Rightarrow> nat \<Rightarrow> nat\<close>
+  where \<open>m XOR n = nat (int m XOR int n)\<close> for m n :: nat
+
+instance proof
+  fix m n q :: nat
+  show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
+    by (auto simp add: and_nat_def bit_and_iff less_le bit_eq_iff)
+  show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
+    by (auto simp add: or_nat_def bit_or_iff less_le bit_eq_iff)
+  show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
+    by (auto simp add: xor_nat_def bit_xor_iff less_le bit_eq_iff)
+qed
+
+end
+
+lemma and_nat_rec:
+  \<open>m AND n = of_bool (odd m \<and> odd n) + 2 * ((m div 2) AND (n div 2))\<close> for m n :: nat
+  by (simp add: and_nat_def and_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
+
+lemma or_nat_rec:
+  \<open>m OR n = of_bool (odd m \<or> odd n) + 2 * ((m div 2) OR (n div 2))\<close> for m n :: nat
+  by (simp add: or_nat_def or_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
+
+lemma xor_nat_rec:
+  \<open>m XOR n = of_bool (odd m \<noteq> odd n) + 2 * ((m div 2) XOR (n div 2))\<close> for m n :: nat
+  by (simp add: xor_nat_def xor_int_rec [of \<open>int m\<close> \<open>int n\<close>] zdiv_int nat_add_distrib nat_mult_distrib)
+
+lemma Suc_0_and_eq [simp]:
+  \<open>Suc 0 AND n = of_bool (odd n)\<close>
+  using one_and_eq [of n] by simp
+
+lemma and_Suc_0_eq [simp]:
+  \<open>n AND Suc 0 = of_bool (odd n)\<close>
+  using and_one_eq [of n] by simp
+
+lemma Suc_0_or_eq [simp]:
+  \<open>Suc 0 OR n = n + of_bool (even n)\<close>
+  using one_or_eq [of n] by simp
+
+lemma or_Suc_0_eq [simp]:
+  \<open>n OR Suc 0 = n + of_bool (even n)\<close>
+  using or_one_eq [of n] by simp
+
+lemma Suc_0_xor_eq [simp]:
+  \<open>Suc 0 XOR n = n + of_bool (even n) - of_bool (odd n)\<close>
+  using one_xor_eq [of n] by simp
+
+lemma xor_Suc_0_eq [simp]:
+  \<open>n XOR Suc 0 = n + of_bool (even n) - of_bool (odd n)\<close>
+  using xor_one_eq [of n] by simp
+
+
 subsubsection \<open>Instances for \<^typ>\<open>integer\<close> and \<^typ>\<open>natural\<close>\<close>
 
 unbundle integer.lifting natural.lifting
@@ -653,11 +597,11 @@
   show \<open>bit (NOT k) n \<longleftrightarrow> (2 :: integer) ^ n \<noteq> 0 \<and> \<not> bit k n\<close>
     by transfer (fact bit_not_iff)
   show \<open>bit (k AND l) n \<longleftrightarrow> bit k n \<and> bit l n\<close>
-    by transfer (fact and_int.bit_eq_iff)
+    by transfer (fact bit_and_iff)
   show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-    by transfer (fact or_int.bit_eq_iff)
+    by transfer (fact bit_or_iff)
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
-    by transfer (fact xor_int.bit_eq_iff)
+    by transfer (fact bit_xor_iff)
 qed
 
 end
@@ -677,11 +621,11 @@
 instance proof
   fix m n :: \<open>natural\<close> and q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-    by transfer (fact and_nat.bit_eq_iff)
+    by transfer (fact bit_and_iff)
   show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-    by transfer (fact or_nat.bit_eq_iff)
+    by transfer (fact bit_or_iff)
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-    by transfer (fact xor_nat.bit_eq_iff)
+    by transfer (fact bit_xor_iff)
 qed
 
 end