augmented and tuned facts on even/odd and division
authorhaftmann
Mon Oct 20 07:45:58 2014 +0200 (2014-10-20)
changeset 587107216a10d69ba
parent 58709 efdc6c533bd3
child 58711 3f7886cd75b9
child 58714 ca0b7d7cc9a3
augmented and tuned facts on even/odd and division
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Commutative_Ring_Complete.thy
src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
src/HOL/Divides.thy
src/HOL/Enum.thy
src/HOL/Library/Nat_Bijection.thy
src/HOL/Library/Stream.thy
src/HOL/Parity.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Oct 19 18:05:26 2014 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Mon Oct 20 07:45:58 2014 +0200
     1.3 @@ -140,19 +140,17 @@
     1.4      mkPX (sqr A) (x + x) (sqr B) \<oplus> mkPX (Pc (1 + 1) \<otimes> A \<otimes> mkPinj 1 B) x (Pc 0)"
     1.5  
     1.6  text {* Fast Exponentation *}
     1.7 +
     1.8  fun pow :: "nat \<Rightarrow> 'a::{comm_ring_1} pol \<Rightarrow> 'a pol"
     1.9  where
    1.10 -  "pow 0 P = Pc 1"
    1.11 -| "pow n P =
    1.12 -    (if even n then pow (n div 2) (sqr P)
    1.13 -     else P \<otimes> pow (n div 2) (sqr P))"
    1.14 -
    1.15 -lemma pow_if:
    1.16 -  "pow n P =
    1.17 +  pow_if [simp del]: "pow n P =
    1.18     (if n = 0 then Pc 1 else if even n then pow (n div 2) (sqr P)
    1.19      else P \<otimes> pow (n div 2) (sqr P))"
    1.20 -  by (cases n) simp_all
    1.21  
    1.22 +lemma pow_simps [simp]:    
    1.23 +  "pow 0 P = Pc 1"
    1.24 +  "pow (Suc n) P = (if odd n then pow (Suc n div 2) (sqr P) else P \<otimes> pow (Suc n div 2) (sqr P))"
    1.25 +  by (simp_all add: pow_if)
    1.26  
    1.27  text {* Normalization of polynomial expressions *}
    1.28  
    1.29 @@ -244,7 +242,8 @@
    1.30      (simp_all add: add_ci mkPinj_ci mkPX_ci mul_ci algebra_simps power_add)
    1.31  
    1.32  text {* Power *}
    1.33 -lemma even_pow:"even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
    1.34 +lemma even_pow:
    1.35 +  "even n \<Longrightarrow> pow n P = pow (n div 2) (sqr P)"
    1.36    by (induct n) simp_all
    1.37  
    1.38  lemma pow_ci: "Ipol ls (pow n P) = Ipol ls P ^ n"
    1.39 @@ -260,12 +259,12 @@
    1.40      proof cases
    1.41        assume "even l"
    1.42        then have "Suc l div 2 = l div 2"
    1.43 -        by (simp add: eval_nat_numeral even_nat_plus_one_div_two)
    1.44 +        by simp
    1.45        moreover
    1.46        from Suc have "l < k" by simp
    1.47        with 1 have "\<And>P. Ipol ls (pow l P) = Ipol ls P ^ l" by simp
    1.48        moreover
    1.49 -      note Suc `even l` even_nat_plus_one_div_two
    1.50 +      note Suc `even l`
    1.51        ultimately show ?thesis by (auto simp add: mul_ci even_pow)
    1.52      next
    1.53        assume "odd l"
    1.54 @@ -278,8 +277,8 @@
    1.55          next
    1.56            case (Suc w)
    1.57            with `odd l` have "even w" by simp
    1.58 -          have two_times: "2 * (w div 2) = w"
    1.59 -            by (simp only: numerals even_nat_div_two_times_two [OF `even w`])
    1.60 +          then have two_times: "2 * (w div 2) = w"
    1.61 +            by (simp add: even_two_times_div_two)
    1.62            have "Ipol ls P * Ipol ls P = Ipol ls P ^ Suc (Suc 0)"
    1.63              by simp
    1.64            then have "Ipol ls P * Ipol ls P = (Ipol ls P)\<^sup>2"
    1.65 @@ -288,7 +287,9 @@
    1.66              by (auto simp add: power_mult [symmetric, of _ 2 _] two_times mul_ci sqr_ci
    1.67                       simp del: power_Suc)
    1.68          qed
    1.69 -      } with 1 Suc `odd l` show ?thesis by simp
    1.70 +      }
    1.71 +      with 1 `odd l` Suc show ?thesis
    1.72 +        by (simp del: odd_Suc_div_two)
    1.73      qed
    1.74    qed
    1.75  qed
     2.1 --- a/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Sun Oct 19 18:05:26 2014 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring_Complete.thy	Mon Oct 20 07:45:58 2014 +0200
     2.3 @@ -551,7 +551,7 @@
     2.4      then have K2: "k div 2 < k" by (cases k) auto
     2.5      from less have "isnorm (sqr P)" by (simp add: sqr_cn)
     2.6      with less False K2 show ?thesis
     2.7 -      by (simp add: allE[of _ "(k div 2)" _] allE[of _ "(sqr P)" _], cases k, auto simp add: mul_cn)
     2.8 +      by (cases k) (auto simp del: odd_Suc_div_two simp add: mul_cn)
     2.9    qed
    2.10  qed
    2.11  
     3.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Sun Oct 19 18:05:26 2014 +0200
     3.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy	Mon Oct 20 07:45:58 2014 +0200
     3.3 @@ -789,20 +789,18 @@
     3.4        by (simp only: power_add power_one_right) simp
     3.5      also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))"
     3.6        by (simp only: th)
     3.7 -    finally have ?case
     3.8 -    using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp
     3.9 +    finally have ?case unfolding numeral_2_eq_2 [symmetric]
    3.10 +    using odd_two_times_div_two_Suc [OF odd] by simp
    3.11    }
    3.12    moreover
    3.13    {
    3.14      assume even: "even (Suc n)"
    3.15 -    have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2"
    3.16 -      by arith
    3.17      from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d"
    3.18        by (simp add: Let_def)
    3.19 -    also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
    3.20 -      using "2.hyps" by (simp only: power_add) simp
    3.21 -    finally have ?case using even_nat_div_two_times_two[OF even]
    3.22 -      by (simp only: th)
    3.23 +    also have "\<dots> = (Ipoly bs p) ^ (2 * (Suc n div 2))"
    3.24 +      using "2.hyps" by (simp only: mult_2 power_add) simp
    3.25 +    finally have ?case using even_two_times_div_two [OF even]
    3.26 +      by simp
    3.27    }
    3.28    ultimately show ?case by blast
    3.29  qed
    3.30 @@ -823,8 +821,8 @@
    3.31      by simp
    3.32    from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n"
    3.33      by simp
    3.34 -  from dn on show ?case
    3.35 -    by (simp add: Let_def)
    3.36 +  from dn on show ?case by (simp, unfold Let_def) auto
    3.37 +    
    3.38  qed
    3.39  
    3.40  lemma polypow_norm:
     4.1 --- a/src/HOL/Divides.thy	Sun Oct 19 18:05:26 2014 +0200
     4.2 +++ b/src/HOL/Divides.thy	Mon Oct 20 07:45:58 2014 +0200
     4.3 @@ -507,6 +507,7 @@
     4.4  class semiring_div_parity = semiring_div + semiring_numeral +
     4.5    assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
     4.6    assumes one_mod_two_eq_one: "1 mod 2 = 1"
     4.7 +  assumes zero_not_eq_two: "0 \<noteq> 2"
     4.8  begin
     4.9  
    4.10  lemma parity_cases [case_names even odd]:
    4.11 @@ -573,6 +574,9 @@
    4.12  next
    4.13    show "1 mod 2 = 1"
    4.14      by (rule mod_less) simp_all
    4.15 +next
    4.16 +  show "0 \<noteq> 2"
    4.17 +    by simp
    4.18  qed
    4.19  
    4.20  lemma divmod_digit_1:
     5.1 --- a/src/HOL/Enum.thy	Sun Oct 19 18:05:26 2014 +0200
     5.2 +++ b/src/HOL/Enum.thy	Mon Oct 20 07:45:58 2014 +0200
     5.3 @@ -705,10 +705,6 @@
     5.4    "2 = a\<^sub>1"
     5.5    by (simp add: numeral.simps plus_finite_2_def)
     5.6    
     5.7 -instance finite_2 :: semiring_div_parity
     5.8 -by intro_classes (simp_all add: mod_finite_2_def split: finite_2.splits)
     5.9 -
    5.10 -
    5.11  hide_const (open) a\<^sub>1 a\<^sub>2
    5.12  
    5.13  datatype (plugins only: code "quickcheck" extraction) finite_3 =
     6.1 --- a/src/HOL/Library/Nat_Bijection.thy	Sun Oct 19 18:05:26 2014 +0200
     6.2 +++ b/src/HOL/Library/Nat_Bijection.thy	Mon Oct 20 07:45:58 2014 +0200
     6.3 @@ -122,9 +122,7 @@
     6.4  by (induct x) simp_all
     6.5  
     6.6  lemma sum_decode_inverse [simp]: "sum_encode (sum_decode n) = n"
     6.7 -unfolding sum_decode_def sum_encode_def numeral_2_eq_2
     6.8 -by (simp add: even_nat_div_two_times_two odd_nat_div_two_times_two_plus_one
     6.9 -         del: mult_Suc)
    6.10 +  by (simp add: even_two_times_div_two odd_two_times_div_two_Suc sum_decode_def sum_encode_def)
    6.11  
    6.12  lemma inj_sum_encode: "inj_on sum_encode A"
    6.13  by (rule inj_on_inverseI, rule sum_encode_inverse)
    6.14 @@ -270,18 +268,15 @@
    6.15    "Suc -` insert (Suc n) A = insert n (Suc -` A)"
    6.16  by auto
    6.17  
    6.18 -lemma even_nat_Suc_div_2: "even x \<Longrightarrow> Suc x div 2 = x div 2"
    6.19 -by (simp only: numeral_2_eq_2 even_nat_plus_one_div_two)
    6.20 -
    6.21  lemma div2_even_ext_nat:
    6.22 -  "\<lbrakk>x div 2 = y div 2; even x = even y\<rbrakk> \<Longrightarrow> (x::nat) = y"
    6.23 +  "x div 2 = y div 2 \<Longrightarrow> even x \<longleftrightarrow> even y \<Longrightarrow> (x::nat) = y"
    6.24  apply (rule mod_div_equality [of x 2, THEN subst])
    6.25  apply (rule mod_div_equality [of y 2, THEN subst])
    6.26 -apply (case_tac "even x")
    6.27 -apply (simp add: numeral_2_eq_2 even_nat_equiv_def)
    6.28 -apply (simp add: numeral_2_eq_2 odd_nat_equiv_def)
    6.29 +apply (cases "even x")
    6.30 +apply (simp_all add: even_iff_mod_2_eq_zero)
    6.31  done
    6.32  
    6.33 +
    6.34  subsubsection {* From sets to naturals *}
    6.35  
    6.36  definition
    6.37 @@ -303,7 +298,7 @@
    6.38  apply (cases "finite A")
    6.39  apply (erule finite_induct, simp)
    6.40  apply (case_tac x)
    6.41 -apply (simp add: even_nat_Suc_div_2 even_set_encode_iff vimage_Suc_insert_0)
    6.42 +apply (simp add: even_set_encode_iff vimage_Suc_insert_0)
    6.43  apply (simp add: finite_vimageI add.commute vimage_Suc_insert_Suc)
    6.44  apply (simp add: set_encode_def finite_vimage_Suc_iff)
    6.45  done
    6.46 @@ -333,7 +328,7 @@
    6.47  lemma set_decode_plus_power_2:
    6.48    "n \<notin> set_decode z \<Longrightarrow> set_decode (2 ^ n + z) = insert n (set_decode z)"
    6.49   apply (induct n arbitrary: z, simp_all)
    6.50 -  apply (rule set_eqI, induct_tac x, simp, simp add: even_nat_Suc_div_2)
    6.51 +  apply (rule set_eqI, induct_tac x, simp, simp)
    6.52   apply (rule set_eqI, induct_tac x, simp, simp add: add.commute)
    6.53  done
    6.54  
     7.1 --- a/src/HOL/Library/Stream.thy	Sun Oct 19 18:05:26 2014 +0200
     7.2 +++ b/src/HOL/Library/Stream.thy	Mon Oct 20 07:45:58 2014 +0200
     7.3 @@ -491,9 +491,8 @@
     7.4  
     7.5  lemma sinterleave_snth[simp]:
     7.6    "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
     7.7 -   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
     7.8 -  by (induct n arbitrary: s1 s2)
     7.9 -    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
    7.10 +  "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
    7.11 +  by (induct n arbitrary: s1 s2) simp_all
    7.12  
    7.13  lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
    7.14  proof (intro equalityI subsetI)
     8.1 --- a/src/HOL/Parity.thy	Sun Oct 19 18:05:26 2014 +0200
     8.2 +++ b/src/HOL/Parity.thy	Mon Oct 20 07:45:58 2014 +0200
     8.3 @@ -279,13 +279,45 @@
     8.4  
     8.5  end
     8.6  
     8.7 +
     8.8 +subsubsection {* Parity and division *}
     8.9 +
    8.10  context semiring_div_parity
    8.11  begin
    8.12  
    8.13 +lemma one_div_two_eq_zero [simp]: -- \<open>FIXME move\<close>
    8.14 +  "1 div 2 = 0"
    8.15 +proof (cases "2 = 0")
    8.16 +  case True then show ?thesis by simp
    8.17 +next
    8.18 +  case False
    8.19 +  from mod_div_equality have "1 div 2 * 2 + 1 mod 2 = 1" .
    8.20 +  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
    8.21 +  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq)
    8.22 +  then have "1 div 2 = 0 \<or> 2 = 0" by (rule divisors_zero)
    8.23 +  with False show ?thesis by auto
    8.24 +qed
    8.25 +
    8.26  lemma even_iff_mod_2_eq_zero [presburger]:
    8.27    "even a \<longleftrightarrow> a mod 2 = 0"
    8.28    by (simp add: even_def dvd_eq_mod_eq_0)
    8.29  
    8.30 +lemma even_succ_div_two [simp]:
    8.31 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
    8.32 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
    8.33 +
    8.34 +lemma odd_succ_div_two [simp]:
    8.35 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
    8.36 +  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
    8.37 +
    8.38 +lemma even_two_times_div_two:
    8.39 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
    8.40 +  by (rule dvd_mult_div_cancel) (simp add: even_def)
    8.41 +
    8.42 +lemma odd_two_times_div_two_succ:
    8.43 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
    8.44 +  using mod_div_equality2 [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
    8.45 +  
    8.46  end
    8.47  
    8.48  
    8.49 @@ -312,8 +344,37 @@
    8.50    "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
    8.51    by (simp add: even_int_iff [symmetric])
    8.52  
    8.53 +lemma even_num_iff:
    8.54 +  "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
    8.55 +  by simp
    8.56  
    8.57 -subsubsection {* Parity and powers *}
    8.58 +lemma even_Suc_div_two [simp]:
    8.59 +  "even n \<Longrightarrow> Suc n div 2 = n div 2"
    8.60 +  using even_succ_div_two [of n] by simp
    8.61 +  
    8.62 +lemma odd_Suc_div_two [simp]:
    8.63 +  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
    8.64 +  using odd_succ_div_two [of n] by simp
    8.65 +
    8.66 +lemma odd_two_times_div_two_Suc:
    8.67 +  "odd n \<Longrightarrow> Suc (2 * (n div 2)) = n"
    8.68 +  using odd_two_times_div_two_succ [of n] by simp
    8.69 +  
    8.70 +text {* Nice facts about division by @{term 4} *}  
    8.71 +
    8.72 +lemma even_even_mod_4_iff:
    8.73 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    8.74 +  by presburger
    8.75 +
    8.76 +lemma odd_mod_4_div_2:
    8.77 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    8.78 +  by presburger
    8.79 +
    8.80 +lemma even_mod_4_div_2:
    8.81 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    8.82 +  by presburger
    8.83 +  
    8.84 +text {* Parity and powers *}
    8.85  
    8.86  context comm_ring_1
    8.87  begin
    8.88 @@ -370,7 +431,7 @@
    8.89    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
    8.90    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
    8.91  
    8.92 -lemma zero_le_power_iff [presburger]:
    8.93 +lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. zero_le_power_eq\<close>
    8.94    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
    8.95  proof (cases "even n")
    8.96    case True
    8.97 @@ -385,7 +446,7 @@
    8.98      by (auto simp add: zero_le_mult_iff zero_le_even_power)
    8.99  qed
   8.100  
   8.101 -lemma zero_le_power_eq [presburger]: -- \<open>FIXME weaker version of @{text zero_le_power_iff}\<close>
   8.102 +lemma zero_le_power_eq [presburger]:
   8.103    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
   8.104    using zero_le_power_iff [of a n] by auto
   8.105  
   8.106 @@ -395,7 +456,7 @@
   8.107    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
   8.108      unfolding power_eq_0_iff' [of a n, symmetric] by blast
   8.109    show ?thesis
   8.110 -  unfolding less_le zero_le_power_iff by auto
   8.111 +  unfolding less_le zero_le_power_eq by auto
   8.112  qed
   8.113  
   8.114  lemma power_less_zero_eq [presburger]:
   8.115 @@ -511,64 +572,5 @@
   8.116    "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
   8.117    by presburger
   8.118  
   8.119 -
   8.120 -subsubsection {* Miscellaneous *}
   8.121 -
   8.122 -lemma even_nat_plus_one_div_two:
   8.123 -  "even (x::nat) ==> (Suc x) div Suc (Suc 0) = x div Suc (Suc 0)"
   8.124 -  by presburger
   8.125 -
   8.126 -lemma odd_nat_plus_one_div_two:
   8.127 -  "odd (x::nat) ==> (Suc x) div Suc (Suc 0) = Suc (x div Suc (Suc 0))"
   8.128 -  by presburger
   8.129 -
   8.130 -lemma even_nat_mod_two_eq_zero:
   8.131 -  "even (x::nat) ==> x mod Suc (Suc 0) = 0"
   8.132 -  by presburger
   8.133 -
   8.134 -lemma odd_nat_mod_two_eq_one:
   8.135 -  "odd (x::nat) ==> x mod Suc (Suc 0) = Suc 0"
   8.136 -  by presburger
   8.137 -
   8.138 -lemma even_nat_equiv_def:
   8.139 -  "even (x::nat) = (x mod Suc (Suc 0) = 0)"
   8.140 -  by presburger
   8.141 -
   8.142 -lemma odd_nat_equiv_def:
   8.143 -  "odd (x::nat) = (x mod Suc (Suc 0) = Suc 0)"
   8.144 -  by presburger
   8.145 -
   8.146 -lemma even_nat_div_two_times_two:
   8.147 -  "even (x::nat) ==> Suc (Suc 0) * (x div Suc (Suc 0)) = x"
   8.148 -  by presburger
   8.149 -
   8.150 -lemma odd_nat_div_two_times_two_plus_one:
   8.151 -  "odd (x::nat) ==> Suc (Suc (Suc 0) * (x div Suc (Suc 0))) = x"
   8.152 -  by presburger
   8.153 -
   8.154 -lemma lemma_even_div2 [simp]:
   8.155 -  "even (n::nat) ==> (n + 1) div 2 = n div 2"
   8.156 -  by presburger
   8.157 -
   8.158 -lemma lemma_odd_div2 [simp]:
   8.159 -  "odd n ==> (n + 1) div 2 = Suc (n div 2)"
   8.160 -  by presburger
   8.161 -
   8.162 -lemma even_num_iff:
   8.163 -  "0 < n ==> even n = (odd (n - 1 :: nat))"
   8.164 -  by presburger
   8.165 -
   8.166 -lemma even_even_mod_4_iff:
   8.167 -  "even (n::nat) = even (n mod 4)"
   8.168 -  by presburger
   8.169 -
   8.170 -lemma lemma_odd_mod_4_div_2:
   8.171 -  "n mod 4 = (3::nat) ==> odd((n - 1) div 2)"
   8.172 -  by presburger
   8.173 -
   8.174 -lemma lemma_even_mod_4_div_2:
   8.175 -  "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
   8.176 -  by presburger
   8.177 -
   8.178  end
   8.179  
     9.1 --- a/src/HOL/Transcendental.thy	Sun Oct 19 18:05:26 2014 +0200
     9.2 +++ b/src/HOL/Transcendental.thy	Mon Oct 20 07:45:58 2014 +0200
     9.3 @@ -200,14 +200,10 @@
     9.4      have "?SUM (2 * (m div 2)) = ?SUM m"
     9.5      proof (cases "even m")
     9.6        case True
     9.7 -      show ?thesis
     9.8 -        unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
     9.9 +      then show ?thesis by (auto simp add: even_two_times_div_two)
    9.10      next
    9.11        case False
    9.12 -      hence "even (Suc m)" by auto
    9.13 -      from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]]
    9.14 -        odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
    9.15 -      have eq: "Suc (2 * (m div 2)) = m" by auto
    9.16 +      then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
    9.17        hence "even (2 * (m div 2))" using `odd m` by auto
    9.18        have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
    9.19        also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
    9.20 @@ -321,9 +317,7 @@
    9.21        have "norm (?Sa n - l) < r"
    9.22        proof (cases "even n")
    9.23          case True
    9.24 -        from even_nat_div_two_times_two[OF this]
    9.25 -        have n_eq: "2 * (n div 2) = n"
    9.26 -          unfolding numeral_2_eq_2[symmetric] by auto
    9.27 +        then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two)
    9.28          with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
    9.29            by auto
    9.30          from f[OF this] show ?thesis
    9.31 @@ -331,9 +325,8 @@
    9.32        next
    9.33          case False
    9.34          hence "even (n - 1)" by simp
    9.35 -        from even_nat_div_two_times_two[OF this]
    9.36 -        have n_eq: "2 * ((n - 1) div 2) = n - 1"
    9.37 -          unfolding numeral_2_eq_2[symmetric] by auto
    9.38 +        then have n_eq: "2 * ((n - 1) div 2) = n - 1"
    9.39 +          by (simp add: even_two_times_div_two)
    9.40          hence range_eq: "n - 1 + 1 = n"
    9.41            using odd_pos[OF False] by auto
    9.42