# HG changeset patch
# User haftmann
# Date 1580933820 0
# Node ID 572ab9e64e182bd49bdf1444d4c3c848bd915fd0
# Parent  1d8e914e04d67b933648c666dac00354618dcbcd
simplified logical constructions

diff -r 1d8e914e04d6 -r 572ab9e64e18 src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/Library/More_List.thy	Wed Feb 05 20:17:00 2020 +0000
@@ -378,5 +378,18 @@
     by simp
 qed
 
+lemma nth_default_map2:
+  \<open>nth_default d (map2 f xs ys) n = f (nth_default d1 xs n) (nth_default d2 ys n)\<close>
+    if \<open>length xs = length ys\<close> and \<open>f d1 d2 = d\<close> for bs cs
+using that proof (induction xs ys arbitrary: n rule: list_induct2)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons x xs y ys)
+  then show ?case
+    by (cases n) simp_all
+qed
+
 end
 
diff -r 1d8e914e04d6 -r 572ab9e64e18 src/HOL/ex/Bit_Lists.thy
--- a/src/HOL/ex/Bit_Lists.thy	Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/ex/Bit_Lists.thy	Wed Feb 05 20:17:00 2020 +0000
@@ -5,9 +5,19 @@
 
 theory Bit_Lists
   imports
-    Word
+    Word "HOL-Library.More_List"
 begin
 
+lemma hd_zip:
+  \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+  using that by (cases xs; cases ys) simp_all
+
+lemma last_zip:
+  \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+    and \<open>length xs = length ys\<close>
+  using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all
+
+
 subsection \<open>Fragments of algebraic bit representations\<close>
 
 context comm_semiring_1
@@ -36,7 +46,7 @@
     simp_all add: algebra_simps)
 
 lemma unsigned_of_bits_take [simp]:
-  "unsigned_of_bits (take n bs) = Parity.take_bit n (unsigned_of_bits bs)"
+  "unsigned_of_bits (take n bs) = take_bit n (unsigned_of_bits bs)"
 proof (induction bs arbitrary: n)
   case Nil
   then show ?case
@@ -59,6 +69,18 @@
     by (cases n) simp_all
 qed
 
+lemma bit_unsigned_of_bits_iff:
+  \<open>bit (unsigned_of_bits bs) n \<longleftrightarrow> nth_default False bs n\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  then show ?case
+    by (cases n) simp_all
+qed
+
 primrec n_bits_of :: "nat \<Rightarrow> 'a \<Rightarrow> bool list"
   where
     "n_bits_of 0 a = []"
@@ -125,6 +147,10 @@
 
 end
 
+lemma bit_of_bits_nat_iff:
+  \<open>bit (of_bits bs :: nat) n \<longleftrightarrow> nth_default False bs n\<close>
+  by (simp add: bit_unsigned_of_bits_iff)
+
 lemma bits_of_Suc_0 [simp]:
   "bits_of (Suc 0) = [True]"
   by simp
@@ -211,6 +237,18 @@
     by (simp_all add: *)
 qed
 
+lemma bit_of_bits_int_iff:
+  \<open>bit (of_bits bs :: int) n \<longleftrightarrow> nth_default (bs \<noteq> [] \<and> last bs) bs n\<close>
+proof (induction bs arbitrary: n)
+  case Nil
+  then show ?case
+    by simp
+next
+  case (Cons b bs)
+  then show ?case
+    by (cases n; cases b; cases bs) simp_all
+qed
+
 lemma of_bits_append [simp]:
   "of_bits (bs @ cs) = of_bits bs + push_bit (length bs) (of_bits cs :: int)"
     if "bs \<noteq> []" "\<not> last bs"
@@ -291,24 +329,14 @@
 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
-using that proof (induction bs cs rule: list_induct2)
-  case Nil
-  then show ?case
-    by simp
-next
-  case (Cons b bs c cs)
-  then show ?case
-    by (cases "of_bits bs = (0::nat) \<or> of_bits cs = (0::nat)")
-      (auto simp add: ac_simps end_of_bits rec [of "Suc 0"])
-qed
-
+  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
@@ -321,32 +349,22 @@
 begin
  
 lemma of_bits:
-  "of_bits bs \<^bold>\<times> of_bits cs = (of_bits (map2 (\<^bold>*) bs cs) :: int)"
-    if "length bs = length cs" and "\<not> False \<^bold>* False" for bs cs
-using \<open>length bs = length cs\<close> proof (induction bs cs rule: list_induct2)
-  case Nil
-  then show ?case
-    using \<open>\<not> False \<^bold>* False\<close> by (auto simp add: False_False_imp_True_True split: bool.splits)
+  \<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 (Cons b bs c cs)
-  show ?case
-  proof (cases "bs = []")
-    case True
-    with Cons show ?thesis
-      using \<open>\<not> False \<^bold>* False\<close> by (cases b; cases c)
-        (auto simp add: ac_simps split: bool.splits)
-  next
-    case False
-    with Cons.hyps have "cs \<noteq> []"
-      by auto
-    with \<open>bs \<noteq> []\<close> have "map2 (\<^bold>*) bs cs \<noteq> []"
-      by (simp add: zip_eq_Nil_iff)
-    from \<open>bs \<noteq> []\<close> \<open>cs \<noteq> []\<close> \<open>map2 (\<^bold>*) bs cs \<noteq> []\<close> Cons show ?thesis
-      by (cases b; cases c)
-        (auto simp add: \<open>\<not> False \<^bold>* False\<close> ac_simps
-          rec [of "of_bits bs * 2"] rec [of "of_bits cs * 2"]
-          rec [of "1 + of_bits bs * 2"])
-  qed
+  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
 qed
 
 end
diff -r 1d8e914e04d6 -r 572ab9e64e18 src/HOL/ex/Bit_Operations.thy
--- a/src/HOL/ex/Bit_Operations.thy	Wed Feb 05 20:16:59 2020 +0000
+++ b/src/HOL/ex/Bit_Operations.thy	Wed Feb 05 20:17:00 2020 +0000
@@ -248,176 +248,92 @@
 subsubsection \<open>Instance \<^typ>\<open>nat\<close>\<close>
 
 locale zip_nat = single: abel_semigroup f
-    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70) +
-  assumes end_of_bits: "\<not> False \<^bold>* False"
+    for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl \<open>\<^bold>*\<close> 70) +
+  assumes end_of_bits: \<open>\<not> False \<^bold>* False\<close>
 begin
 
-lemma False_P_imp:
-  "False \<^bold>* True \<and> P" if "False \<^bold>* P"
-  using that end_of_bits by (cases P) simp_all
-
-function F :: "nat \<Rightarrow> nat \<Rightarrow> nat"  (infixl "\<^bold>\<times>" 70)
-  where "m \<^bold>\<times> n = (if m = 0 \<and> n = 0 then 0
-    else of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2)"
+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
 
-lemma zero_left_eq:
-  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
-  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma zero_right_eq:
-  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
-  by (induction m rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma simps [simp]:
-  "0 \<^bold>\<times> 0 = 0"
-  "0 \<^bold>\<times> n = of_bool (False \<^bold>* True) * n"
-  "m \<^bold>\<times> 0 = of_bool (True \<^bold>* False) * m"
-  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> m \<^bold>\<times> n = of_bool (odd m \<^bold>* odd n) + (m div 2) \<^bold>\<times> (n div 2) * 2"
-  by (simp_all only: zero_left_eq zero_right_eq) simp
+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"
-  by (cases "m = 0 \<and> n = 0") (auto simp add: end_of_bits)
+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
 
-declare F.simps [simp del]
+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])
+qed
 
 sublocale abel_semigroup F
-proof
-  show "m \<^bold>\<times> n \<^bold>\<times> q = m \<^bold>\<times> (n \<^bold>\<times> q)" for m n q :: nat
-  proof (induction m arbitrary: n q rule: nat_bit_induct)
-    case zero
-    show ?case
-      by simp
-  next
-    case (even m)
-    with rec [of "2 * m"] rec [of _ q] show ?case
-      by (cases "even n") (auto simp add: ac_simps dest: False_P_imp)
-  next
-    case (odd m)
-    with rec [of "Suc (2 * m)"] rec [of _ q] show ?case
-      by (cases "even n"; cases "even q")
-        (auto dest: False_P_imp simp add: ac_simps)
-  qed
-  show "m \<^bold>\<times> n = n \<^bold>\<times> m" for m n :: nat
-  proof (induction m arbitrary: n rule: nat_bit_induct)
-    case zero
-    show ?case
-      by (simp add: ac_simps)
-  next
-    case (even m)
-    with rec [of "2 * m" n] rec [of n "2 * m"] show ?case
-      by (simp add: ac_simps)
-  next
-    case (odd m)
-    with rec [of "Suc (2 * m)" n] rec [of n "Suc (2 * m)"] show ?case
-      by (simp add: ac_simps)
-  qed
-qed
-
-lemma self [simp]:
-  "n \<^bold>\<times> n = of_bool (True \<^bold>* True) * n"
-  by (induction n rule: nat_bit_induct) (simp_all add: end_of_bits)
-
-lemma even_iff [simp]:
-  "even (m \<^bold>\<times> n) \<longleftrightarrow> \<not> (odd m \<^bold>* odd n)"
-proof (induction m arbitrary: n rule: nat_bit_induct)
-  case zero
-  show ?case
-    by (cases "even n") (simp_all add: end_of_bits)
-next
-  case (even m)
-  then show ?case
-    by (simp add: rec [of "2 * m"])
-next
-  case (odd m)
-  then show ?case
-    by (simp add: rec [of "Suc (2 * m)"])
-qed
+  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 "(\<and>)"
+global_interpretation and_nat: zip_nat \<open>(\<and>)\<close>
   defines and_nat = and_nat.F
   by standard auto
 
-global_interpretation and_nat: semilattice "(AND) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+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 "n AND n = n" for n :: nat
-    by (simp add: and_nat.self)
+  show \<open>n AND n = n\<close> for n :: nat
+    by (simp add: bit_eq_iff and_nat.bit_eq_iff)
 qed
 
-declare and_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation or_nat: zip_nat "(\<or>)"
+global_interpretation or_nat: zip_nat \<open>(\<or>)\<close>
   defines or_nat = or_nat.F
   by standard auto
 
-global_interpretation or_nat: semilattice "(OR) :: nat \<Rightarrow> nat \<Rightarrow> nat"
+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 "n OR n = n" for n :: nat
-    by (simp add: or_nat.self)
+  show \<open>n OR n = n\<close> for n :: nat
+    by (simp add: bit_eq_iff or_nat.bit_eq_iff)
 qed
 
-declare or_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
-global_interpretation xor_nat: zip_nat "(\<noteq>)"
+global_interpretation xor_nat: zip_nat \<open>(\<noteq>)\<close>
   defines xor_nat = xor_nat.F
   by standard auto
 
-declare xor_nat.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
 instance proof
   fix m n q :: nat
   show \<open>bit (m AND n) q \<longleftrightarrow> bit m q \<and> bit n q\<close>
-  proof (rule sym, induction q arbitrary: m n)
-    case 0
-    then show ?case
-      by (simp add: and_nat.even_iff)
-  next
-    case (Suc q)
-    with and_nat.rec [of m n] show ?case
-      by simp
-  qed
+    by (fact and_nat.bit_eq_iff)
   show \<open>bit (m OR n) q \<longleftrightarrow> bit m q \<or> bit n q\<close>
-  proof (rule sym, induction q arbitrary: m n)
-    case 0
-    then show ?case
-      by (simp add: or_nat.even_iff)
-  next
-    case (Suc q)
-    with or_nat.rec [of m n] show ?case
-      by simp
-  qed
+    by (fact or_nat.bit_eq_iff)
   show \<open>bit (m XOR n) q \<longleftrightarrow> bit m q \<noteq> bit n q\<close>
-  proof (rule sym, induction q arbitrary: m n)
-    case 0
-    then show ?case
-      by (simp add: xor_nat.even_iff)
-  next
-    case (Suc q)
-    with xor_nat.rec [of m n] show ?case
-      by simp
-  qed
+    by (fact xor_nat.bit_eq_iff)
 qed
 
 end
 
-global_interpretation or_nat: semilattice_neutr "(OR)" "0 :: nat"
-  by standard simp
-
-global_interpretation xor_nat: comm_monoid "(XOR)" "0 :: nat"
-  by standard simp
-
 lemma Suc_0_and_eq [simp]:
   \<open>Suc 0 AND n = of_bool (odd n)\<close>
   using one_and_eq [of n] by simp
@@ -445,314 +361,112 @@
 
 subsubsection \<open>Instance \<^typ>\<open>int\<close>\<close>
 
-abbreviation (input) complement :: "int \<Rightarrow> int"
-  where "complement k \<equiv> - k - 1"
-
-lemma complement_half:
-  "complement (k * 2) div 2 = complement k"
-  by simp
-
-lemma complement_div_2:
-  "complement (k div 2) = complement k div 2"
-  by linarith
-
 locale zip_int = single: abel_semigroup f
-  for f :: "bool \<Rightarrow> bool \<Rightarrow> bool"  (infixl "\<^bold>*" 70)
+  for f :: \<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>  (infixl \<open>\<^bold>*\<close> 70)
 begin
- 
-lemma False_False_imp_True_True:
-  "True \<^bold>* True" if "False \<^bold>* False"
-proof (rule ccontr)
-  assume "\<not> True \<^bold>* True"
-  with that show False
-    using single.assoc [of False True True]
-    by (cases "False \<^bold>* True") simp_all
-qed
 
-function F :: "int \<Rightarrow> int \<Rightarrow> int"  (infixl "\<^bold>\<times>" 70)
-  where "k \<^bold>\<times> l = (if k \<in> {0, - 1} \<and> l \<in> {0, - 1}
+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) + (k div 2) \<^bold>\<times> (l div 2) * 2)"
+    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
 
-lemma zero_left_eq:
-  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction l rule: int_bit_induct)
-   (simp_all split: bool.split) 
-
-lemma minus_left_eq:
-  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction l rule: int_bit_induct)
-   (simp_all split: bool.split) 
-
-lemma zero_right_eq:
-  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct)
-    (simp_all add: ac_simps split: bool.split)
-
-lemma minus_right_eq:
-  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct)
-    (simp_all add: ac_simps split: bool.split)
-
-lemma simps [simp]:
-  "0 \<^bold>\<times> 0 = - of_bool (False \<^bold>* False)"
-  "- 1 \<^bold>\<times> 0 = - of_bool (True \<^bold>* False)"
-  "0 \<^bold>\<times> - 1 = - of_bool (False \<^bold>* True)"
-  "- 1 \<^bold>\<times> - 1 = - of_bool (True \<^bold>* True)"
-  "0 \<^bold>\<times> l = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  "- 1 \<^bold>\<times> l = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> l
-     | (True, False) \<Rightarrow> complement l
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<^bold>\<times> 0 = (case (False \<^bold>* False, False \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<^bold>\<times> - 1 = (case (True \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, False) \<Rightarrow> complement k
-     | (True, True) \<Rightarrow> - 1)"
-  "k \<noteq> 0 \<Longrightarrow> k \<noteq> - 1 \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> l \<noteq> - 1
-    \<Longrightarrow> k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
-  by simp_all[4] (simp_all only: zero_left_eq minus_left_eq zero_right_eq minus_right_eq, simp)
-
 declare F.simps [simp del]
 
 lemma rec:
-  "k \<^bold>\<times> l = of_bool (odd k \<^bold>* odd l) + (k div 2) \<^bold>\<times> (l div 2) * 2"
-  by (cases "k \<in> {0, - 1} \<and> l \<in> {0, - 1}") (auto simp add: ac_simps F.simps [of k l] split: bool.split)
+  \<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])
+qed
 
 sublocale abel_semigroup F
-proof
-  show "k \<^bold>\<times> l \<^bold>\<times> r = k \<^bold>\<times> (l \<^bold>\<times> r)" for k l r :: int
-  proof (induction k arbitrary: l r rule: int_bit_induct)
-    case zero
-    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "False \<^bold>* False" "\<not> False \<^bold>* True"
-    proof (induction l arbitrary: r rule: int_bit_induct)
-      case zero
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case minus
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (even l)
-      with that rec [of _ r] show ?case
-        by (cases "even r")
-          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (odd l)
-      moreover have "- l - 1 = - 1 - l"
-        by simp
-      ultimately show ?case
-        using that rec [of _ r]
-        by (cases "even r")
-          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    qed
-    then show ?case
-      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-  next
-    case minus
-    have "complement l \<^bold>\<times> r = complement (l \<^bold>\<times> r)" if "\<not> True \<^bold>* True" "False \<^bold>* True"
-    proof (induction l arbitrary: r rule: int_bit_induct)
-      case zero
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case minus
-      from that show ?case
-        by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (even l)
-      with that rec [of _ r] show ?case
-        by (cases "even r")
-          (auto simp add: complement_half ac_simps False_False_imp_True_True split: bool.splits)
-    next
-      case (odd l)
-      moreover have "- l - 1 = - 1 - l"
-        by simp
-      ultimately show ?case
-        using that rec [of _ r]
-        by (cases "even r")
-          (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-    qed
-    then show ?case
-      by (auto simp add: ac_simps False_False_imp_True_True split: bool.splits)
-  next
-    case (even k)
-    with rec [of "k * 2"] rec [of _ r] show ?case
-      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
-  next
-    case (odd k)
-    with rec [of "1 + k * 2"] rec [of _ r] show ?case
-      by (cases "even r"; cases "even l") (auto simp add: ac_simps False_False_imp_True_True)
-  qed
-  show "k \<^bold>\<times> l = l \<^bold>\<times> k" for k l :: int
-  proof (induction k arbitrary: l rule: int_bit_induct)
-    case zero
-    show ?case
-      by simp
-  next
-    case minus
-    show ?case
-      by simp
-  next
-    case (even k)
-    with rec [of "k * 2" l] rec [of l "k * 2"] show ?case
-      by (simp add: ac_simps)
-  next
-    case (odd k)
-    with rec [of "k * 2 + 1" l] rec [of l "k * 2 + 1"] show ?case
-      by (simp add: ac_simps)
-  qed
-qed
-
-lemma self [simp]:
-  "k \<^bold>\<times> k = (case (False \<^bold>* False, True \<^bold>* True)
-    of (False, False) \<Rightarrow> 0
-     | (False, True) \<Rightarrow> k
-     | (True, True) \<Rightarrow> - 1)"
-  by (induction k rule: int_bit_induct) (auto simp add: False_False_imp_True_True split: bool.split)
-
-lemma even_iff [simp]:
-  "even (k \<^bold>\<times> l) \<longleftrightarrow> \<not> (odd k \<^bold>* odd l)"
-proof (induction k arbitrary: l rule: int_bit_induct)
-  case zero
-  show ?case
-    by (cases "even l") (simp_all split: bool.splits)
-next
-  case minus
-  show ?case
-    by (cases "even l") (simp_all split: bool.splits)
-next
-  case (even k)
-  then show ?case
-    by (simp add: rec [of "k * 2"])
-next
-  case (odd k)
-  then show ?case
-    by (simp add: rec [of "1 + k * 2"])
-qed
+  by standard (simp_all add: Parity.bit_eq_iff bit_eq_iff ac_simps)
 
 end
 
 instantiation int :: ring_bit_operations
 begin
 
-definition not_int :: "int \<Rightarrow> int"
-  where "not_int = complement"
-
 global_interpretation and_int: zip_int "(\<and>)"
   defines and_int = and_int.F
   by standard
 
-declare and_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
 global_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: and_int.self)
+    by (simp add: bit_eq_iff and_int.bit_eq_iff)
 qed
 
 global_interpretation or_int: zip_int "(\<or>)"
   defines or_int = or_int.F
   by standard
 
-declare or_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
-
 global_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: or_int.self)
+    by (simp add: bit_eq_iff or_int.bit_eq_iff)
 qed
 
 global_interpretation xor_int: zip_int "(\<noteq>)"
   defines xor_int = xor_int.F
   by standard
 
-declare xor_int.simps [simp] \<comment> \<open>inconsistent declaration handling by
-  \<open>global_interpretation\<close> in \<open>instantiation\<close>\<close>
+definition not_int :: \<open>int \<Rightarrow> int\<close>
+  where \<open>not_int k = - k - 1\<close>
+
+lemma not_int_rec:
+  "NOT k = of_bool (even k) + 2 * NOT (k div 2)" for k :: int
+  by (auto simp add: not_int_def elim: oddE)
+
+lemma even_not_iff_int:
+  \<open>even (NOT k) \<longleftrightarrow> odd k\<close> for k :: int
+  by (simp add: not_int_def)
+
+lemma not_int_div_2:
+  \<open>NOT k div 2 = NOT (k div 2)\<close> for k :: int
+  by (simp add: not_int_def)
 
 lemma bit_not_iff_int:
   \<open>bit (NOT k) n \<longleftrightarrow> \<not> bit k n\<close>
     for k :: int
-    by (induction n arbitrary: k)
-      (simp_all add: not_int_def flip: complement_div_2)
+  by (induction n arbitrary: k) (simp_all add: not_int_div_2 even_not_iff_int)
 
 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>
-  proof (rule sym, induction n arbitrary: k l)
-    case 0
-    then show ?case
-      by (simp add: and_int.even_iff)
-  next
-    case (Suc n)
-    with and_int.rec [of k l] show ?case
-      by simp
-  qed
+    by (fact and_int.bit_eq_iff)
   show \<open>bit (k OR l) n \<longleftrightarrow> bit k n \<or> bit l n\<close>
-  proof (rule sym, induction n arbitrary: k l)
-    case 0
-    then show ?case
-      by (simp add: or_int.even_iff)
-  next
-    case (Suc n)
-    with or_int.rec [of k l] show ?case
-      by simp
-  qed
+    by (fact or_int.bit_eq_iff)
   show \<open>bit (k XOR l) n \<longleftrightarrow> bit k n \<noteq> bit l n\<close>
-  proof (rule sym, induction n arbitrary: k l)
-    case 0
-    then show ?case
-      by (simp add: xor_int.even_iff)
-  next
-    case (Suc n)
-    with xor_int.rec [of k l] show ?case
-      by simp
-  qed
-qed (simp_all add: minus_1_div_exp_eq_int bit_not_iff_int)
+    by (fact xor_int.bit_eq_iff)
+qed (simp_all add: bit_not_iff_int)
 
 end
 
-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)
-
-lemma not_int_rec [simp]:
-  "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)
-
 end