# HG changeset patch
# User bulwahn
# Date 1292398441 -3600
# Node ID 74e41b2d48eaa325b4eeb33a4d21fee659258e43
# Parent  573f557ed716accf87c47828a89772762d7c70e4
adding an Isar version of the MacLaurin theorem from some students' work in 2005

diff -r 573f557ed716 -r 74e41b2d48ea src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Dec 14 00:16:30 2010 +0100
+++ b/src/HOL/MacLaurin.thy	Wed Dec 15 08:34:01 2010 +0100
@@ -1,6 +1,7 @@
 (*  Author      : Jacques D. Fleuriot
     Copyright   : 2001 University of Edinburgh
     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+    Conversion of Mac Laurin to Isar by Lukas Bulwahn and Bernhard Häupler, 2005
 *)
 
 header{*MacLaurin Series*}
@@ -18,11 +19,9 @@
     "0 < h ==>
      \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
                (B * ((h^n) / real(fact n)))"
-apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
+by (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
                  real(fact n) / (h^n)"
-       in exI)
-apply (simp) 
-done
+       in exI, simp)
 
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
 by arith
@@ -32,46 +31,141 @@
   by (subst fact_reduce_nat, auto)
 
 lemma Maclaurin_lemma2:
-  assumes diff: "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-  assumes n: "n = Suc k"
-  assumes difg: "difg =
-        (\<lambda>m t. diff m t -
-               ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) +
-                B * (t ^ (n - m) / real (fact (n - m)))))"
-  shows
-      "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
-unfolding difg
- apply clarify
- apply (rule DERIV_diff)
-  apply (simp add: diff)
- apply (simp only: n)
- apply (rule DERIV_add)
-  apply (rule_tac [2] DERIV_cmult)
-  apply (rule_tac [2] lemma_DERIV_subst)
-   apply (rule_tac [2] DERIV_quotient)
-     apply (rule_tac [3] DERIV_const)
-    apply (rule_tac [2] DERIV_pow)
-   prefer 3 
+  assumes DERIV : "\<forall>m t. m < n \<and> 0\<le>t \<and> t\<le>h \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+  and INIT : "n = Suc k"
+  and DIFG_DEF: "difg = (\<lambda>m t. diff m t - ((\<Sum>p = 0..<n - m. diff (m + p) 0 / real (fact p) * t ^ p) + 
+  B * (t ^ (n - m) / real (fact (n - m)))))"
+  shows "\<forall>m t. m < n & 0 \<le> t & t \<le> h --> DERIV (difg m) t :> difg (Suc m) t"
+proof (rule allI)+
+  fix m
+  fix t
+  show "m < n \<and> 0 \<le> t \<and> t \<le> h \<longrightarrow> DERIV (difg m) t :> difg (Suc m) t"
+  proof
+    assume INIT2: "m < n & 0 \<le> t & t \<le> h"
+    hence INTERV: "0 \<le> t & t \<le> h" ..
+    from INIT2 and INIT have mtok: "m < Suc k" by arith
+    have "DERIV (\<lambda>t. diff m t -
+    ((\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * t ^ p) +
+    B * (t ^ (Suc k - m) / real (fact (Suc k - m)))))
+    t :> diff (Suc m) t -
+    ((\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
+    B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))))"
+    proof -
+      from DERIV and INIT2 have "DERIV (diff m) t :> diff (Suc m) t" by simp
+      moreover
+      have " DERIV (\<lambda>x. (\<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) +
+	B * (x ^ (Suc k - m) / real (fact (Suc k - m))))
+	t :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p) +
+	B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
+      proof -
+	have "DERIV (\<lambda>x. \<Sum>p = 0..<Suc k - m. diff (m + p) 0 / real (fact p) * x ^ p) t
+	  :> (\<Sum>p = 0..<Suc k - Suc m. diff (Suc m + p) 0 / real (fact p) * t ^ p)"
+	proof -
+	  have "\<exists> d. k = m + d"
+	  proof -
+	    from INIT2 have "m < n" ..
+	    hence "\<exists> d. n = m + d + Suc 0" by arith
+	    with INIT show ?thesis by (simp del: setsum_op_ivl_Suc)
+	  qed
+	  from this obtain d where kmd: "k = m + d" ..
+	  have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) +
+            diff m 0)
+	    t :> (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"
+	    
+	  proof - 
+	    have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma))) + diff m 0) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0"
+	    proof -
+	      from DERIV and INTERV have "DERIV (\<lambda>x. (\<Sum>ma = 0..<d. diff (Suc (m + ma)) 0 * x ^ Suc ma / real (fact (Suc ma)))) t :>  (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r))"
+	      proof -
+		have "\<forall>r. 0 \<le> r \<and> r < 0 + d \<longrightarrow>
+		  DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
+		  :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
+		proof (rule allI)
+		  fix r
+		  show " 0 \<le> r \<and> r < 0 + d \<longrightarrow>
+		    DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r / real (fact (Suc r))) t
+		    :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)"
+		  proof 
+		    assume "0 \<le> r & r < 0 + d"
+		    have "DERIV (\<lambda>x. diff (Suc (m + r)) 0 *
+                      (x ^ Suc r * inverse (real (fact (Suc r)))))
+		      t :> diff (Suc (m + r)) 0 * (t ^ r * inverse (real (fact r)))"
+		    proof -
+                      have "(1 + real r) * real (fact r) \<noteq> 0" by auto
+		      from this have "real (fact r) + real r * real (fact r) \<noteq> 0"
+                        by (metis add_nonneg_eq_0_iff mult_nonneg_nonneg real_of_nat_fact_not_zero real_of_nat_ge_zero)
+                      from this have "DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t :> real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
+			0 * t ^ Suc r"
+                        apply - by ( rule DERIV_intros | rule refl)+ auto
+		      moreover
+		      have "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (fact (Suc r))) +
+			0 * t ^ Suc r =
+			t ^ r * inverse (real (fact r))"
+		      proof -
+			
+			have " real (Suc r) * t ^ (Suc r - Suc 0) *
+			  inverse (real (Suc r) * real (fact r)) +
+			  0 * t ^ Suc r =
+			  t ^ r * inverse (real (fact r))" by (simp add: mult_ac)
+			hence "real (Suc r) * t ^ (Suc r - Suc 0) * inverse (real (Suc r * fact r)) +
+			  0 * t ^ Suc r =
+			  t ^ r * inverse (real (fact r))" by (subst real_of_nat_mult)
+			thus ?thesis by (subst fact_Suc)
+		      qed
+		      ultimately have " DERIV (\<lambda>x. x ^ Suc r * inverse (real (fact (Suc r)))) t
+			:> t ^ r * inverse (real (fact r))" by (rule lemma_DERIV_subst)
+		      thus ?thesis by (rule DERIV_cmult)
+		    qed
+		    thus "DERIV (\<lambda>x. diff (Suc (m + r)) 0 * x ^ Suc r /
+                      real (fact (Suc r)))
+		      t :> diff (Suc (m + r)) 0 * t ^ r / real (fact r)" by (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
+		  qed
+		qed
+		thus ?thesis by (rule DERIV_sumr)
+	      qed
+	      moreover
+	      from DERIV_const have "DERIV (\<lambda>x. diff m 0) t :> 0" .
+	      ultimately show ?thesis by (rule DERIV_add)
+	    qed
+	    moreover
+	    have " (\<Sum>r = 0..<d. diff (Suc (m + r)) 0 * t ^ r / real (fact r)) + 0 =  (\<Sum>p = 0..<d. diff (Suc (m + p)) 0 * t ^ p / real (fact p))"  by simp
+	    ultimately show ?thesis by (rule lemma_DERIV_subst)
+	  qed
+	  with kmd and sumr_offset4 [of 1] show ?thesis by (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
+	qed
+	moreover
+	have " DERIV (\<lambda>x. B * (x ^ (Suc k - m) / real (fact (Suc k - m)))) t
+	  :> B * (t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m)))"
+	proof -
+	  have " DERIV (\<lambda>x. x ^ (Suc k - m) / real (fact (Suc k - m))) t
+	    :> t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))"
+	  proof -
+	    have "DERIV (\<lambda>x. x ^ (Suc k - m)) t :> real (Suc k - m) * t ^ (Suc k - m - Suc 0)" by (rule DERIV_pow)
+	    moreover
+	    have "DERIV (\<lambda>x. real (fact (Suc k - m))) t :> 0" by (rule DERIV_const)
+	    moreover
+	    have "(\<lambda>x. real (fact (Suc k - m))) t \<noteq> 0" by simp
+	    ultimately have " DERIV (\<lambda>y. y ^ (Suc k - m) / real (fact (Suc k - m))) t
+	      :>  ( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
+	      real (fact (Suc k - m)) ^ Suc (Suc 0)"
+              apply -
+              apply (rule DERIV_cong) by (rule DERIV_intros | rule refl)+ auto
+	    moreover
+	    from mtok and INIT have "( real (Suc k - m) * t ^ (Suc k - m - Suc 0) * real (fact (Suc k - m)) + - (0 * t ^ (Suc k - m))) /
+	      real (fact (Suc k - m)) ^ Suc (Suc 0) =  t ^ (Suc k - Suc m) / real (fact (Suc k - Suc m))" by (simp add: fact_diff_Suc)
+	    ultimately show ?thesis by (rule lemma_DERIV_subst)
+	  qed
+	  moreover
+	  thus ?thesis by (rule DERIV_cmult)
+	qed
+	ultimately show ?thesis by (rule DERIV_add)
+      qed
+      ultimately show ?thesis by (rule DERIV_diff) 
+    qed
+    from INIT and this and DIFG_DEF show "DERIV (difg m) t :> difg (Suc m) t" by clarify
+  qed
+qed
 
-apply (simp add: fact_diff_Suc)
-  prefer 2 apply simp
- apply (frule less_iff_Suc_add [THEN iffD1], clarify)
- apply (simp del: setsum_op_ivl_Suc)
- apply (insert sumr_offset4 [of "Suc 0"])
- apply (simp del: setsum_op_ivl_Suc fact_Suc power_Suc)
- apply (rule lemma_DERIV_subst)
-  apply (rule DERIV_add)
-   apply (rule_tac [2] DERIV_const)
-  apply (rule DERIV_sumr, clarify)
-  prefer 2 apply simp
- apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
- apply (rule DERIV_cmult)
- apply (rule lemma_DERIV_subst)
-  apply (best intro!: DERIV_intros)
- apply (subst fact_Suc)
- apply (subst real_of_nat_mult)
- apply (simp add: mult_ac)
-done
 
 lemma Maclaurin:
   assumes h: "0 < h"
@@ -83,7 +177,7 @@
     "\<exists>t. 0 < t & t < h &
               f h =
               setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
-              (diff n t / real (fact n)) * h ^ n"
+              (diff n t / real (fact n)) * h ^ n"  
 proof -
   from n obtain m where m: "n = Suc m"
     by (cases n, simp add: n)
@@ -195,17 +289,23 @@
 
 
 lemma Maclaurin2:
-   "[| 0 < h; diff 0 = f;
-       \<forall>m t.
-          m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t |]
-    ==> \<exists>t. 0 < t &
-              t \<le> h &
-              f h =
-              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
-              diff n t / real (fact n) * h ^ n"
-apply (case_tac "n", auto)
-apply (drule Maclaurin, auto)
-done
+  assumes INIT1: "0 < h " and INIT2: "diff 0 = f"
+  and DERIV: "\<forall>m t.
+  m < n & 0 \<le> t & t \<le> h --> DERIV (diff m) t :> diff (Suc m) t"
+  shows "\<exists>t. 0 < t \<and> t \<le> h \<and> f h =
+  (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
+  diff n t / real (fact n) * h ^ n"
+proof (cases "n")
+  case 0 with INIT1 INIT2 show ?thesis by fastsimp
+next
+  case Suc 
+  hence "n > 0" by simp
+  from INIT1 this INIT2 DERIV have "\<exists>t>0. t < h \<and>
+    f h =
+    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n t / real (fact n) * h ^ n" 
+    by (rule Maclaurin)
+  thus ?thesis by fastsimp
+qed
 
 lemma Maclaurin2_objl:
      "0 < h & diff 0 = f &
@@ -219,31 +319,62 @@
 by (blast intro: Maclaurin2)
 
 lemma Maclaurin_minus:
-   "[| h < 0; n > 0; diff 0 = f;
-       \<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t |]
-    ==> \<exists>t. h < t &
-              t < 0 &
-              f h =
-              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
-              diff n t / real (fact n) * h ^ n"
-apply (cut_tac f = "%x. f (-x)"
-        and diff = "%n x. (-1 ^ n) * diff n (-x)"
-        and h = "-h" and n = n in Maclaurin_objl)
-apply (simp)
-apply safe
-apply (subst minus_mult_right)
-apply (rule DERIV_cmult)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_chain2 [where g=uminus])
-apply (rule_tac [2] DERIV_minus, rule_tac [2] DERIV_ident)
-prefer 2 apply force
-apply force
-apply (rule_tac x = "-t" in exI, auto)
-apply (subgoal_tac "(\<Sum>m = 0..<n. -1 ^ m * diff m 0 * (-h)^m / real(fact m)) =
-                    (\<Sum>m = 0..<n. diff m 0 * h ^ m / real(fact m))")
-apply (rule_tac [2] setsum_cong[OF refl])
-apply (auto simp add: divide_inverse power_mult_distrib [symmetric])
-done
+  assumes INTERV : "h < 0" and
+  INIT : "0 < n" "diff 0 = f" and
+             ABL : "\<forall>m t. m < n & h \<le> t & t \<le> 0 --> DERIV (diff m) t :> diff (Suc m) t"
+  shows "\<exists>t. h < t & t < 0 &
+         f h = (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
+         diff n t / real (fact n) * h ^ n"
+proof -
+  from INTERV have "0 < -h" by simp
+  moreover
+  from INIT have "0 < n" by simp
+  moreover
+  from INIT have "(% x. ( - 1) ^ 0 * diff 0 (- x)) = (% x. f (- x))" by simp
+  moreover
+  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> - h \<longrightarrow>
+    DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
+  proof (rule allI impI)+
+    fix m t
+    assume tINTERV:" m < n \<and> 0 \<le> t \<and> t \<le> - h"
+    with ABL show "DERIV (\<lambda>x. (- 1) ^ m * diff m (- x)) t :> (- 1) ^ Suc m * diff (Suc m) (- t)"
+    proof -
+      
+      from ABL and tINTERV have "DERIV (\<lambda>x. diff m (- x)) t :> - diff (Suc m) (- t)" (is ?tABL)
+      proof -
+	from ABL and tINTERV have "DERIV (diff m) (- t) :> diff (Suc m) (- t)" by force
+	moreover
+	from DERIV_ident[of t] have "DERIV uminus t :> (- 1)" by (rule DERIV_minus) 
+	ultimately have "DERIV (\<lambda>x. diff m (- x)) t :> diff (Suc m) (- t) * - 1" by (rule DERIV_chain2)
+	thus ?thesis by simp
+      qed
+      thus ?thesis
+      proof -
+	assume ?tABL hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> -1 ^ m * - diff (Suc m) (- t)" by (rule DERIV_cmult)
+	hence "DERIV (\<lambda>x. -1 ^ m * diff m (- x)) t :> - (-1 ^ m * diff (Suc m) (- t))" by (subst minus_mult_right)
+	thus ?thesis by simp 
+      qed
+    qed
+  qed
+  ultimately have t_exists: "\<exists>t>0. t < - h \<and>
+    f (- (- h)) =
+    (\<Sum>m = 0..<n.
+    (- 1) ^ m * diff m (- 0) / real (fact m) * (- h) ^ m) +
+    (- 1) ^ n * diff n (- t) / real (fact n) * (- h) ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
+  from this obtain t where t_def: "?P t" ..
+  moreover
+  have "-1 ^ n * diff n (- t) * (- h) ^ n / real (fact n) = diff n (- t) * h ^ n / real (fact n)"
+    by (auto simp add: power_mult_distrib[symmetric])
+  moreover
+  have "(SUM m = 0..<n. -1 ^ m * diff m 0 * (- h) ^ m / real (fact m)) = (SUM m = 0..<n. diff m 0 * h ^ m / real (fact m))"
+    by (auto intro: setsum_cong simp add: power_mult_distrib[symmetric])
+  ultimately have " h < - t \<and>
+    - t < 0 \<and>
+    f h =
+    (\<Sum>m = 0..<n. diff m 0 / real (fact m) * h ^ m) + diff n (- t) / real (fact n) * h ^ n"
+    by auto
+  thus ?thesis ..
+qed
 
 lemma Maclaurin_minus_objl:
      "(h < 0 & n > 0 & diff 0 = f &
@@ -269,42 +400,109 @@
 by (induct "n", auto)
 
 lemma Maclaurin_bi_le:
-   "[| diff 0 = f;
-       \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
-    ==> \<exists>t. abs t \<le> abs x &
+   assumes INIT : "diff 0 = f"
+   and DERIV : "\<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
+   shows "\<exists>t. abs t \<le> abs x &
               f x =
               (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
               diff n t / real (fact n) * x ^ n"
-apply (case_tac "n = 0", force)
-apply (case_tac "x = 0")
- apply (rule_tac x = 0 in exI)
- apply (force simp add: Maclaurin_bi_le_lemma)
-apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
- txt{*Case 1, where @{term "x < 0"}*}
- apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
-  apply (simp add: abs_if)
- apply (rule_tac x = t in exI)
- apply (simp add: abs_if)
-txt{*Case 2, where @{term "0 < x"}*}
-apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_objl, safe)
- apply (simp add: abs_if)
-apply (rule_tac x = t in exI)
-apply (simp add: abs_if)
-done
+proof (cases "n = 0")
+  case True from INIT True show ?thesis by force
+next
+  case False
+  from this have n_not_zero:"n \<noteq> 0" .
+  from False INIT DERIV show ?thesis
+  proof (cases "x = 0")
+    case True show ?thesis
+    proof -
+      from n_not_zero True INIT DERIV have "\<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
+	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n" by(force simp add: Maclaurin_bi_le_lemma) 
+      thus ?thesis ..
+    qed
+  next
+    case False 
+    note linorder_less_linear [of "x" "0"] 
+    thus ?thesis
+    proof (elim disjE)
+      assume "x = 0" with False show ?thesis ..
+      next
+      assume x_less_zero: "x < 0" moreover
+      from n_not_zero have "0 < n" by simp moreover
+      have "diff 0 = diff 0" by simp moreover
+      have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+      proof (rule allI, rule allI, rule impI)
+	fix m t
+	assume "m < n & x \<le> t & t \<le> 0"
+	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by (fastsimp simp add: abs_if)
+      qed
+      ultimately have t_exists:"\<exists>t>x. t < 0 \<and>
+        diff 0 x =
+        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
+      from this obtain t where t_def: "?P t" ..
+      from t_def x_less_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
+	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
+	by (simp add: abs_if order_less_le)
+      thus ?thesis by (rule exI)
+    next
+    assume x_greater_zero: "x > 0" moreover
+    from n_not_zero have "0 < n" by simp moreover
+    have "diff 0 = diff 0" by simp moreover
+    have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+      proof (rule allI, rule allI, rule impI)
+	fix m t
+	assume "m < n & 0 \<le> t & t \<le> x"
+	with DERIV show " DERIV (diff m) t :> diff (Suc m) t" by fastsimp
+      qed
+      ultimately have t_exists:"\<exists>t>0. t < x \<and>
+        diff 0 x =
+        (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
+      from this obtain t where t_def: "?P t" ..
+      from t_def x_greater_zero INIT  have "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
+	f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n"
+	by fastsimp
+      thus ?thesis ..
+    qed
+  qed
+qed
+
 
 lemma Maclaurin_all_lt:
-     "[| diff 0 = f;
-         \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
-        x ~= 0; n > 0
-      |] ==> \<exists>t. 0 < abs t & abs t < abs x &
+  assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
+  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
+  shows "\<exists>t. 0 < abs t & abs t < abs x &
                f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
-                     (diff n t / real (fact n)) * x ^ n"
-apply (rule_tac x = x and y = 0 in linorder_cases)
-prefer 2 apply blast
-apply (drule_tac [2] diff=diff in Maclaurin)
-apply (drule_tac diff=diff in Maclaurin_minus, simp_all, safe)
-apply (rule_tac [!] x = t in exI, auto)
-done
+                     (diff n t / real (fact n)) * x ^ n" 
+proof -
+  have "(x = 0) \<Longrightarrow> ?thesis"
+  proof -
+    assume "x = 0"
+    with INIT3 show "(x = 0) \<Longrightarrow> ?thesis"..
+  qed
+  moreover have "(x < 0) \<Longrightarrow> ?thesis"
+  proof -
+    assume x_less_zero: "x < 0"
+    from DERIV have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp 
+    with x_less_zero INIT2 INIT1 have "\<exists>t>x. t < 0 \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_minus)
+    from this obtain t where "?P t" ..
+    with x_less_zero have "0 < \<bar>t\<bar> \<and>
+      \<bar>t\<bar> < \<bar>x\<bar> \<and>
+      f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by simp
+    thus ?thesis ..
+  qed
+  moreover have "(x > 0) \<Longrightarrow> ?thesis"
+  proof -
+    assume x_greater_zero: "x > 0"
+    from DERIV have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t" by simp
+    with x_greater_zero INIT2 INIT1 have "\<exists>t>0. t < x \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin)
+    from this obtain t where "?P t" ..
+    with x_greater_zero have "0 < \<bar>t\<bar> \<and>
+      \<bar>t\<bar> < \<bar>x\<bar> \<and>
+      f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by fastsimp
+    thus ?thesis ..
+  qed
+  ultimately show ?thesis by (fastsimp) 
+qed
+
 
 lemma Maclaurin_all_lt_objl:
      "diff 0 = f &
@@ -322,20 +520,42 @@
           diff 0 0"
 by (induct n, auto)
 
-lemma Maclaurin_all_le: "[| diff 0 = f;
-        \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
-      |] ==> \<exists>t. abs t \<le> abs x &
+
+lemma Maclaurin_all_le:
+  assumes INIT: "diff 0 = f"
+  and DERIV: "\<forall>m x. DERIV (diff m) x :> diff (Suc m) x"
+  shows "\<exists>t. abs t \<le> abs x &
               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                     (diff n t / real (fact n)) * x ^ n"
-apply(cases "n=0")
-apply (force)
-apply (case_tac "x = 0")
-apply (frule_tac diff = diff and n = n in Maclaurin_zero, assumption)
-apply (drule not0_implies_Suc)
-apply (rule_tac x = 0 in exI, force)
-apply (frule_tac diff = diff and n = n in Maclaurin_all_lt, auto)
-apply (rule_tac x = t in exI, auto)
-done
+proof -
+  note linorder_le_less_linear [of n 0]
+  thus ?thesis
+  proof
+    assume "n\<le> 0" with INIT show ?thesis by force
+  next
+    assume n_greater_zero: "n > 0" show ?thesis
+    proof (cases "x = 0")
+      case True
+      from n_greater_zero have "n \<noteq> 0" by auto
+      from True this  have f_0:"(\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) = diff 0 0" by (rule Maclaurin_zero)
+      from n_greater_zero have "n \<noteq> 0" by (rule gr_implies_not0)
+      hence "\<exists> m. n = Suc m" by (rule not0_implies_Suc)
+      with f_0 True INIT have " \<bar>0\<bar> \<le> \<bar>x\<bar> \<and>
+       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n 0 / real (fact n) * x ^ n"
+	by force
+      thus ?thesis ..
+    next
+      case False
+      from INIT n_greater_zero this DERIV have "\<exists>t. 0 < \<bar>t\<bar> \<and>
+	\<bar>t\<bar> < \<bar>x\<bar> \<and> f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" (is "\<exists> t. ?P t") by (rule Maclaurin_all_lt)
+      from this obtain t where "?P t" ..
+      hence "\<bar>t\<bar> \<le> \<bar>x\<bar> \<and>
+       f x = (\<Sum>m = 0..<n. diff m 0 / real (fact m) * x ^ m) + diff n t / real (fact n) * x ^ n" by (simp add: order_less_le)
+      thus ?thesis ..
+    qed
+  qed
+qed
+
 
 lemma Maclaurin_all_le_objl: "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)