# HG changeset patch
# User paulson
# Date 1385298382 0
# Node ID 07864001495d8a5a6cbbc33f0f19e274855853b8
# Parent  002b8729f22802d984a6255f267d8ed0ceb6a7c6
cleaned up some messy proofs

diff -r 002b8729f228 -r 07864001495d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Nov 24 00:31:50 2013 +0000
+++ b/src/HOL/Transcendental.thy	Sun Nov 24 13:06:22 2013 +0000
@@ -33,24 +33,31 @@
   shows
     "x ^ (Suc n) - y ^ (Suc n) =
       (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
-  apply (induct n)
-  apply simp
-  apply (simp del: setsum_op_ivl_Suc)
-  apply (subst setsum_op_ivl_Suc)
-  apply (subst lemma_realpow_diff_sumr)
-  apply (simp add: distrib_left del: setsum_op_ivl_Suc)
-  apply (subst mult_left_commute [of "x - y"])
-  apply (erule subst)
-  apply (simp add: algebra_simps)
-  done
+proof (induct n)
+  case 0 show ?case
+    by simp
+next
+  case (Suc n)
+  have "x ^ Suc (Suc n) - y ^ Suc (Suc n) = x * (x * x ^ n) - y * (y * y ^ n)"
+    by simp
+  also have "... = y * (x ^ (Suc n) - y ^ (Suc n)) + (x - y) * (x * x ^ n)"
+    by (simp add: algebra_simps)
+  also have "... = y * ((x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
+    by (simp only: Suc)
+  also have "... = (x - y) * (y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))) + (x - y) * (x * x ^ n)"
+    by (simp only: mult_left_commute)
+  also have "... = (x - y) * (\<Sum>p = 0..<Suc (Suc n). x ^ p * y ^ (Suc n - p))"
+    by (simp add: setsum_op_ivl_Suc [where n = "Suc n"] distrib_left lemma_realpow_diff_sumr
+             del: setsum_op_ivl_Suc)
+  finally show ?case .
+qed
 
 lemma lemma_realpow_rev_sumr:
-  "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
+   "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =
     (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p))"
   apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
-  apply (rule inj_onI, simp)
-  apply auto
-  apply (rule_tac x="n - x" in image_eqI, simp, simp)
+  apply (rule inj_onI, auto)
+  apply (metis atLeastLessThan_iff diff_diff_cancel diff_less_Suc imageI le0 less_Suc_eq_le)
   done
 
 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
@@ -388,12 +395,9 @@
       by auto
     ultimately show ?thesis by auto
   qed
-  from this[THEN conjunct1]
-    this[THEN conjunct2, THEN conjunct1]
-    this[THEN conjunct2, THEN conjunct2, THEN conjunct1]
-    this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct1]
-    this[THEN conjunct2, THEN conjunct2, THEN conjunct2, THEN conjunct2]
-  show ?summable and ?pos and ?neg and ?f and ?g .
+  then
+  show ?summable and ?pos and ?neg and ?f and ?g 
+    by safe
 qed
 
 subsection {* Term-by-Term Differentiability of Power Series *}
@@ -420,9 +424,7 @@
       (\<lambda>n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums
          (\<Sum>n. (diffs c)(n) * (x ^ n))"
   unfolding diffs_def
-  apply (drule summable_sums)
-  apply (rule sums_Suc_imp, simp_all)
-  done
+  by (simp add: summable_sums sums_Suc_imp)
 
 lemma lemma_termdiff1:
   fixes z :: "'a :: {monoid_mult,comm_ring}" shows
@@ -482,10 +484,7 @@
   have "norm (((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0)) =
         norm (\<Sum>p = 0..<n - Suc 0. \<Sum>q = 0..<n - Suc 0 - p.
           (z + h) ^ q * z ^ (n - 2 - q)) * norm h"
-    apply (subst lemma_termdiff2 [OF 1])
-    apply (subst norm_mult)
-    apply (rule mult_commute)
-    done
+    by (metis (lifting, no_types) lemma_termdiff2 [OF 1] mult_commute norm_mult)
   also have "\<dots> \<le> of_nat n * (of_nat (n - Suc 0) * K ^ (n - 2)) * norm h"
   proof (rule mult_right_mono [OF _ norm_ge_zero])
     from norm_ge_zero 2 have K: "0 \<le> K"
@@ -3705,8 +3704,8 @@
   assumes "\<bar>x\<bar> < 1"
   shows "x\<^sup>2 < 1"
 proof -
-  from mult_left_mono[OF less_imp_le[OF `\<bar>x\<bar> < 1`] abs_ge_zero[of x]]
-  have "\<bar>x\<^sup>2\<bar> < 1" using `\<bar>x\<bar> < 1` unfolding numeral_2_eq_2 power_Suc2 by auto
+  have "\<bar>x\<^sup>2\<bar> < 1"
+    by (metis abs_power2 assms pos2 power2_abs power_0 power_strict_decreasing zero_eq_power2 zero_less_abs_iff) 
   thus ?thesis using zero_le_power2 by auto
 qed
 
@@ -3867,7 +3866,7 @@
         moreover
         have "suminf (?c x) - arctan x = suminf (?c (-\<bar>x\<bar>)) - arctan (-\<bar>x\<bar>)"
           by (rule suminf_eq_arctan_bounded[where x="x" and a="-\<bar>x\<bar>" and b="\<bar>x\<bar>"])
-            (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
+             (simp_all only: `\<bar>x\<bar> < r` `-\<bar>x\<bar> < \<bar>x\<bar>` neg_less_iff_less)
         ultimately
         show ?thesis using suminf_arctan_zero by auto
       qed
@@ -4085,28 +4084,28 @@
 
 lemmas sin_arccos_lemma1 = sin_arccos_abs [OF cos_x_y_le_one]
 
-lemma polar_ex1: "0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
-  apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
-  apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
-  apply (simp add: cos_arccos_lemma1)
-  apply (simp add: sin_arccos_lemma1)
-  apply (simp add: power_divide)
-  apply (simp add: real_sqrt_mult [symmetric])
-  apply (simp add: right_diff_distrib)
-  done
-
-lemma polar_ex2: "y < 0 ==> \<exists>r a. x = r * cos a & y = r * sin a"
-  using polar_ex1 [where x=x and y="-y"]
-  apply simp
-  apply clarify
-  apply (metis cos_minus minus_minus minus_mult_right sin_minus)
-  done
-
 lemma polar_Ex: "\<exists>r a. x = r * cos a & y = r * sin a"
-  apply (rule_tac x=0 and y=y in linorder_cases)
-  apply (erule polar_ex1)
-  apply (rule_tac x=x in exI, rule_tac x=0 in exI, simp)
-  apply (erule polar_ex2)
-  done
+proof -
+  have polar_ex1: "\<And>y. 0 < y \<Longrightarrow> \<exists>r a. x = r * cos a & y = r * sin a"
+    apply (rule_tac x = "sqrt (x\<^sup>2 + y\<^sup>2)" in exI)
+    apply (rule_tac x = "arccos (x / sqrt (x\<^sup>2 + y\<^sup>2))" in exI)
+    apply (simp add: cos_arccos_lemma1 sin_arccos_lemma1 power_divide
+                     real_sqrt_mult [symmetric] right_diff_distrib)
+    done
+  show ?thesis
+  proof (cases "0::real" y rule: linorder_cases)
+    case less 
+      then show ?thesis by (rule polar_ex1)
+  next
+    case equal
+      then show ?thesis
+        by (force simp add: intro!: cos_zero sin_zero)
+  next
+    case greater
+      then show ?thesis 
+     using polar_ex1 [where y="-y"]
+    by auto (metis cos_minus minus_minus minus_mult_right sin_minus)
+  qed
+qed
 
 end