# HG changeset patch
# User huffman
# Date 1230071507 28800
# Node ID e72d07a878f8ceabfb781e16dc5082c4643e7733
# Parent  89b0803404d7d24514a6605683c4ca1bb6ea5815
clean up some proofs; remove unused lemmas

diff -r 89b0803404d7 -r e72d07a878f8 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Dec 23 00:56:03 2008 +0100
+++ b/src/HOL/Transcendental.thy	Tue Dec 23 14:31:47 2008 -0800
@@ -26,8 +26,8 @@
   fixes y :: "'a::{recpower,comm_semiring_0}" shows
      "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ (Suc n - p)) =  
       y * (\<Sum>p=0..<Suc n. (x ^ p) * y ^ (n - p))"
-by (auto simp add: setsum_right_distrib lemma_realpow_diff mult_ac
-  simp del: setsum_op_ivl_Suc cong: strong_setsum_cong)
+by (simp add: setsum_right_distrib lemma_realpow_diff mult_ac
+         del: setsum_op_ivl_Suc cong: strong_setsum_cong)
 
 lemma lemma_realpow_diff_sumr2:
   fixes y :: "'a::{recpower,comm_ring}" shows
@@ -124,33 +124,22 @@
 lemma diffs_minus: "diffs (%n. - c n) = (%n. - diffs c n)"
 by (simp add: diffs_def)
 
-text{*Show that we can shift the terms down one*}
-lemma lemma_diffs:
-     "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) =  
-      (\<Sum>n=0..<n. of_nat n * c(n) * (x ^ (n - Suc 0))) +  
-      (of_nat n * c(n) * x ^ (n - Suc 0))"
-apply (induct "n")
-apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
+lemma sums_Suc_imp:
+  assumes f: "f 0 = 0"
+  shows "(\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s"
+unfolding sums_def
+apply (rule LIMSEQ_imp_Suc)
+apply (subst setsum_shift_lb_Suc0_0_upt [where f=f, OF f, symmetric])
+apply (simp only: setsum_shift_bounds_Suc_ivl)
 done
 
-lemma lemma_diffs2:
-     "(\<Sum>n=0..<n. of_nat n * c(n) * (x ^ (n - Suc 0))) =  
-      (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) -  
-      (of_nat n * c(n) * x ^ (n - Suc 0))"
-by (auto simp add: lemma_diffs)
-
-
 lemma diffs_equiv:
      "summable (%n. (diffs c)(n) * (x ^ n)) ==>  
       (%n. of_nat n * c(n) * (x ^ (n - Suc 0))) sums  
          (\<Sum>n. (diffs c)(n) * (x ^ n))"
-apply (subgoal_tac " (%n. of_nat n * c (n) * (x ^ (n - Suc 0))) ----> 0")
-apply (rule_tac [2] LIMSEQ_imp_Suc)
-apply (drule summable_sums) 
-apply (auto simp add: sums_def)
-apply (drule_tac X="(\<lambda>n. \<Sum>n = 0..<n. diffs c n * x ^ n)" in LIMSEQ_diff)
-apply (auto simp add: lemma_diffs2 [symmetric] diffs_def [symmetric])
-apply (simp add: diffs_def summable_LIMSEQ_zero)
+unfolding diffs_def
+apply (drule summable_sums)
+apply (rule sums_Suc_imp, simp_all)
 done
 
 lemma lemma_termdiff1:
@@ -160,12 +149,6 @@
 by (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac
   cong: strong_setsum_cong)
 
-lemma less_add_one: "m < n ==> (\<exists>d. n = m + d + Suc 0)"
-by (simp add: less_iff_Suc_add)
-
-lemma sumdiff: "a + b - (c + d) = a - c + b - (d::real)"
-by arith
-
 lemma sumr_diff_mult_const2:
   "setsum f {0..<n} - of_nat n * (r::'a::ring_1) = (\<Sum>i = 0..<n. f i - r)"
 by (simp add: setsum_subtractf)
@@ -252,15 +235,15 @@
   assumes k: "0 < (k::real)"
   assumes le: "\<And>h. \<lbrakk>h \<noteq> 0; norm h < k\<rbrakk> \<Longrightarrow> norm (f h) \<le> K * norm h"
   shows "f -- 0 --> 0"
-proof (simp add: LIM_def, safe)
+unfolding LIM_def diff_0_right
+proof (safe)
+  let ?h = "of_real (k / 2)::'a"
+  have "?h \<noteq> 0" and "norm ?h < k" using k by simp_all
+  hence "norm (f ?h) \<le> K * norm ?h" by (rule le)
+  hence "0 \<le> K * norm ?h" by (rule order_trans [OF norm_ge_zero])
+  hence zero_le_K: "0 \<le> K" using k by (simp add: zero_le_mult_iff)
+
   fix r::real assume r: "0 < r"
-  have zero_le_K: "0 \<le> K"
-    apply (cut_tac k)
-    apply (cut_tac h="of_real (k/2)" in le, simp)
-    apply (simp del: of_real_divide)
-    apply (drule order_trans [OF norm_ge_zero])
-    apply (simp add: zero_le_mult_iff)
-    done
   show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> 0 \<and> norm x < s \<longrightarrow> norm (f x) < r)"
   proof (cases)
     assume "K = 0"
@@ -392,11 +375,12 @@
   assumes 3: "summable (\<lambda>n. (diffs (diffs c)) n * K ^ n)"
   assumes 4: "norm x < norm K"
   shows "DERIV (\<lambda>x. \<Sum>n. c n * x ^ n) x :> (\<Sum>n. (diffs c) n * x ^ n)"
-proof (simp add: deriv_def, rule LIM_zero_cancel)
+unfolding deriv_def
+proof (rule LIM_zero_cancel)
   show "(\<lambda>h. (suminf (\<lambda>n. c n * (x + h) ^ n) - suminf (\<lambda>n. c n * x ^ n)) / h
             - suminf (\<lambda>n. diffs c n * x ^ n)) -- 0 --> 0"
   proof (rule LIM_equal2)
-    show "0 < norm K - norm x" by (simp add: less_diff_eq 4)
+    show "0 < norm K - norm x" using 4 by (simp add: less_diff_eq)
   next
     fix h :: 'a
     assume "h \<noteq> 0"
@@ -421,8 +405,7 @@
       apply (rule summable_divide)
       apply (rule summable_diff [OF B A])
       apply (rule sums_summable [OF diffs_equiv [OF C]])
-      apply (rule_tac f="suminf" in arg_cong)
-      apply (rule ext)
+      apply (rule arg_cong [where f="suminf"], rule ext)
       apply (simp add: ring_simps)
       done
   next