src/HOL/Transcendental.thy
changeset 58710 7216a10d69ba
parent 58709 efdc6c533bd3
child 58729 e8ecc79aee43
     1.1 --- a/src/HOL/Transcendental.thy	Sun Oct 19 18:05:26 2014 +0200
     1.2 +++ b/src/HOL/Transcendental.thy	Mon Oct 20 07:45:58 2014 +0200
     1.3 @@ -200,14 +200,10 @@
     1.4      have "?SUM (2 * (m div 2)) = ?SUM m"
     1.5      proof (cases "even m")
     1.6        case True
     1.7 -      show ?thesis
     1.8 -        unfolding even_nat_div_two_times_two[OF True, unfolded numeral_2_eq_2[symmetric]] ..
     1.9 +      then show ?thesis by (auto simp add: even_two_times_div_two)
    1.10      next
    1.11        case False
    1.12 -      hence "even (Suc m)" by auto
    1.13 -      from even_nat_div_two_times_two[OF this, unfolded numeral_2_eq_2[symmetric]]
    1.14 -        odd_nat_plus_one_div_two[OF False, unfolded numeral_2_eq_2[symmetric]]
    1.15 -      have eq: "Suc (2 * (m div 2)) = m" by auto
    1.16 +      then have eq: "Suc (2 * (m div 2)) = m" by (simp add: odd_two_times_div_two_Suc)
    1.17        hence "even (2 * (m div 2))" using `odd m` by auto
    1.18        have "?SUM m = ?SUM (Suc (2 * (m div 2)))" unfolding eq ..
    1.19        also have "\<dots> = ?SUM (2 * (m div 2))" using `even (2 * (m div 2))` by auto
    1.20 @@ -321,9 +317,7 @@
    1.21        have "norm (?Sa n - l) < r"
    1.22        proof (cases "even n")
    1.23          case True
    1.24 -        from even_nat_div_two_times_two[OF this]
    1.25 -        have n_eq: "2 * (n div 2) = n"
    1.26 -          unfolding numeral_2_eq_2[symmetric] by auto
    1.27 +        then have n_eq: "2 * (n div 2) = n" by (simp add: even_two_times_div_two)
    1.28          with `n \<ge> 2 * f_no` have "n div 2 \<ge> f_no"
    1.29            by auto
    1.30          from f[OF this] show ?thesis
    1.31 @@ -331,9 +325,8 @@
    1.32        next
    1.33          case False
    1.34          hence "even (n - 1)" by simp
    1.35 -        from even_nat_div_two_times_two[OF this]
    1.36 -        have n_eq: "2 * ((n - 1) div 2) = n - 1"
    1.37 -          unfolding numeral_2_eq_2[symmetric] by auto
    1.38 +        then have n_eq: "2 * ((n - 1) div 2) = n - 1"
    1.39 +          by (simp add: even_two_times_div_two)
    1.40          hence range_eq: "n - 1 + 1 = n"
    1.41            using odd_pos[OF False] by auto
    1.42