# HG changeset patch
# User haftmann
# Date 1581444236 -3600
# Node ID 4e66867fd63fc23c4bfd5d247134297b291061e2
# Parent  8b0b8b9ea653364a05070eb6ae943947b030b6b5
tuned proof

diff -r 8b0b8b9ea653 -r 4e66867fd63f src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Wed Feb 12 21:18:04 2020 +0100
+++ b/src/HOL/Parity.thy	Tue Feb 11 19:03:56 2020 +0100
@@ -890,17 +890,32 @@
   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
+  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
+proof
+  assume ?P
+  then show ?Q
+    by simp
+next
+  assume ?Q
+  then have \<open>even a \<longleftrightarrow> even b\<close> and \<open>a div 2 = b div 2\<close>
+    by simp_all
+  show ?P
+  proof (rule bit_eqI)
+    fix n
+    show \<open>bit a n \<longleftrightarrow> bit b n\<close>
+    proof (cases n)
+      case 0
+      with \<open>even a \<longleftrightarrow> even b\<close> show ?thesis
+        by simp
+    next
+      case (Suc n)
+      moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close>
+        by simp
+      ultimately show ?thesis
+        by simp
+    qed
+  qed
+qed
 
 lemma bit_mask_iff:
   \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>