src/HOL/Transcendental.thy
changeset 68594 5b05ede597b8
parent 68527 2f4e2aab190a
child 68601 7828f3b85156
--- a/src/HOL/Transcendental.thy	Thu Jul 05 18:27:24 2018 +0100
+++ b/src/HOL/Transcendental.thy	Thu Jul 05 23:37:00 2018 +0100
@@ -626,38 +626,41 @@
   fixes h :: "'a::field"
   assumes h: "h \<noteq> 0"
   shows "((z + h) ^ n - z ^ n) / h - of_nat n * z ^ (n - Suc 0) =
-    h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
+         h * (\<Sum>p< n - Suc 0. \<Sum>q< n - Suc 0 - p. (z + h) ^ q * z ^ (n - 2 - q))"
     (is "?lhs = ?rhs")
-  apply (subgoal_tac "h * ?lhs = h * ?rhs")
-   apply (simp add: h)
-  apply (simp add: right_diff_distrib diff_divide_distrib h)
-  apply (simp add: mult.assoc [symmetric])
-  apply (cases n)
-  apply simp
-  apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
-      del: power_Suc sum_lessThan_Suc of_nat_Suc)
-  apply (subst lemma_realpow_rev_sumr)
-  apply (subst sumr_diff_mult_const2)
-  apply simp
-  apply (simp only: lemma_termdiff1 sum_distrib_left)
-  apply (rule sum.cong [OF refl])
-  apply (simp add: less_iff_Suc_add)
-  apply clarify
-  apply (simp add: sum_distrib_left diff_power_eq_sum ac_simps
-      del: sum_lessThan_Suc power_Suc)
-  apply (subst mult.assoc [symmetric], subst power_add [symmetric])
-  apply (simp add: ac_simps)
-  done
+proof (cases n)
+  case (Suc n)
+  have 0: "\<And>x k. (\<Sum>n<Suc k. h * (z ^ x * (z ^ (k - n) * (h + z) ^ n))) =
+                 (\<Sum>j<Suc k.  h * ((h + z) ^ j * z ^ (x + k - j)))"
+    apply (rule sum.cong [OF refl])
+    by (simp add: power_add [symmetric] mult.commute)
+  have *: "(\<Sum>i<n. z ^ i * ((z + h) ^ (n - i) - z ^ (n - i))) =
+           (\<Sum>i<n. \<Sum>j<n - i. h * ((z + h) ^ j * z ^ (n - Suc j)))"
+    apply (rule sum.cong [OF refl])
+    apply (clarsimp simp add: less_iff_Suc_add sum_distrib_left diff_power_eq_sum ac_simps 0
+        simp del: sum_lessThan_Suc power_Suc)
+    done
+  have "h * ?lhs = h * ?rhs"
+    apply (simp add: right_diff_distrib diff_divide_distrib h mult.assoc [symmetric])
+    using Suc
+    apply (simp add: diff_power_eq_sum h right_diff_distrib [symmetric] mult.assoc
+        del: power_Suc sum_lessThan_Suc of_nat_Suc)
+    apply (subst lemma_realpow_rev_sumr)
+    apply (subst sumr_diff_mult_const2)
+    apply (simp add: lemma_termdiff1 sum_distrib_left *)
+    done
+  then show ?thesis
+    by (simp add: h)
+qed auto
+
 
 lemma real_sum_nat_ivl_bounded2:
   fixes K :: "'a::linordered_semidom"
   assumes f: "\<And>p::nat. p < n \<Longrightarrow> f p \<le> K"
     and K: "0 \<le> K"
   shows "sum f {..<n-k} \<le> of_nat n * K"
-  apply (rule order_trans [OF sum_mono])
-   apply (rule f)
-   apply simp
-  apply (simp add: mult_right_mono K)
+  apply (rule order_trans [OF sum_mono [OF f]])
+  apply (auto simp add: mult_right_mono K)
   done
 
 lemma lemma_termdiff3:
@@ -775,9 +778,8 @@
     also have "(\<lambda>n. of_nat n * diffs (\<lambda>n. norm (c n)) n * r ^ (n - Suc 0)) =
       (\<lambda>n. diffs (\<lambda>m. of_nat (m - Suc 0) * norm (c m) * inverse r) n * (r ^ n))"
       apply (rule ext)
-      apply (simp add: diffs_def)
       apply (case_tac n)
-       apply (simp_all add: r_neq_0)
+      apply (simp_all add: diffs_def r_neq_0)
       done
     finally have "summable
       (\<lambda>n. of_nat n * (of_nat (n - Suc 0) * norm (c n) * inverse r) * r ^ (n - Suc 0))"
@@ -874,12 +876,13 @@
     apply (auto simp: norm_divide norm_mult norm_power field_simps)
     done
   have "summable (\<lambda>n. (of_nat n * c n) * x ^ n)"
-    apply (rule summable_comparison_test' [of "\<lambda>n. norm(c n * (of_real r) ^ n)" N])
-     apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
-    using N r norm_of_real [of "r + K", where 'a = 'a]
-      apply (auto simp add: norm_divide norm_mult norm_power field_simps)
-    apply (fastforce simp: less_eq_real_def)
-    done
+  proof (rule summable_comparison_test')
+    show "summable (\<lambda>n. norm (c n * of_real r ^ n))"
+      apply (rule powser_insidea [OF sm [of "of_real ((r+K)/2)"]])
+      using N r norm_of_real [of "r + K", where 'a = 'a] by auto
+    show "\<And>n. N \<le> n \<Longrightarrow> norm (of_nat n * c n * x ^ n) \<le> norm (c n * of_real r ^ n)"
+      using N r by (fastforce simp add: norm_mult norm_power less_eq_real_def)
+  qed
   then have "summable (\<lambda>n. (of_nat (Suc n) * c(Suc n)) * x ^ Suc n)"
     using summable_iff_shift [of "\<lambda>n. of_nat n * c n * x ^ n" 1]
     by simp
@@ -894,10 +897,7 @@
   fixes x :: "'a::{real_normed_field,banach}"
   assumes "\<And>x. summable (\<lambda>n. c n * x^n)"
   shows "summable (\<lambda>n. diffs c n * x^n)"
-  apply (rule termdiff_converges [where K = "1 + norm x"])
-  using assms
-   apply auto
-  done
+  by (rule termdiff_converges [where K = "1 + norm x"]) (use assms in auto)
 
 lemma termdiffs_strong:
   fixes K x :: "'a::{real_normed_field,banach}"
@@ -921,9 +921,9 @@
     by (blast intro: sm termdiff_converges powser_inside)
   ultimately show ?thesis
     apply (rule termdiffs [where K = "of_real (norm x + norm K) / 2"])
+    using K
       apply (auto simp: field_simps)
-    using K
-    apply (simp_all add: of_real_add [symmetric] del: of_real_add)
+    apply (simp flip: of_real_add)
     done
 qed