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
```