tuned proof
authorhaftmann
Tue Feb 11 19:03:56 2020 +0100 (2 weeks ago)
changeset 714414e66867fd63f
parent 71440 8b0b8b9ea653
child 71442 d45495e897f4
tuned proof
src/HOL/Parity.thy
     1.1 --- a/src/HOL/Parity.thy	Wed Feb 12 21:18:04 2020 +0100
     1.2 +++ b/src/HOL/Parity.thy	Tue Feb 11 19:03:56 2020 +0100
     1.3 @@ -890,17 +890,32 @@
     1.4    by (cases n, auto simp add: bit_def ac_simps)
     1.5  
     1.6  lemma bit_eq_rec:
     1.7 -  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close>
     1.8 -  apply (auto simp add: bit_eq_iff)
     1.9 -  using bit_0 apply blast
    1.10 -  using bit_0 apply blast
    1.11 -  using bit_Suc apply blast
    1.12 -  using bit_Suc apply blast
    1.13 -     apply (metis bit_eq_iff even_iff_mod_2_eq_zero mod_div_mult_eq)
    1.14 -    apply (metis bit_eq_iff even_iff_mod_2_eq_zero mod_div_mult_eq)
    1.15 -   apply (metis bit_eq_iff mod2_eq_if mod_div_mult_eq)
    1.16 -  apply (metis bit_eq_iff mod2_eq_if mod_div_mult_eq)
    1.17 -  done
    1.18 +  \<open>a = b \<longleftrightarrow> (even a \<longleftrightarrow> even b) \<and> a div 2 = b div 2\<close> (is \<open>?P = ?Q\<close>)
    1.19 +proof
    1.20 +  assume ?P
    1.21 +  then show ?Q
    1.22 +    by simp
    1.23 +next
    1.24 +  assume ?Q
    1.25 +  then have \<open>even a \<longleftrightarrow> even b\<close> and \<open>a div 2 = b div 2\<close>
    1.26 +    by simp_all
    1.27 +  show ?P
    1.28 +  proof (rule bit_eqI)
    1.29 +    fix n
    1.30 +    show \<open>bit a n \<longleftrightarrow> bit b n\<close>
    1.31 +    proof (cases n)
    1.32 +      case 0
    1.33 +      with \<open>even a \<longleftrightarrow> even b\<close> show ?thesis
    1.34 +        by simp
    1.35 +    next
    1.36 +      case (Suc n)
    1.37 +      moreover from \<open>a div 2 = b div 2\<close> have \<open>bit (a div 2) n = bit (b div 2) n\<close>
    1.38 +        by simp
    1.39 +      ultimately show ?thesis
    1.40 +        by simp
    1.41 +    qed
    1.42 +  qed
    1.43 +qed
    1.44  
    1.45  lemma bit_mask_iff:
    1.46    \<open>bit (2 ^ m - 1) n \<longleftrightarrow> 2 ^ n \<noteq> 0 \<and> n < m\<close>