# HG changeset patch
# User wenzelm
# Date 1469981120 -7200
# Node ID 1826a90b9cbc2e5729895a318dfaf40e0f160d69
# Parent  7e0b0db5e9acf42301235e55803a76cd34acef80
simplified theory structure;

diff -r 7e0b0db5e9ac -r 1826a90b9cbc src/HOL/Complex_Main.thy
--- a/src/HOL/Complex_Main.thy	Sun Jul 31 17:25:38 2016 +0200
+++ b/src/HOL/Complex_Main.thy	Sun Jul 31 18:05:20 2016 +0200
@@ -6,7 +6,7 @@
   Real
   Complex
   Transcendental
-  Taylor
+  MacLaurin
   Deriv
 begin
 
diff -r 7e0b0db5e9ac -r 1826a90b9cbc src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 31 17:25:38 2016 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 31 18:05:20 2016 +0200
@@ -4075,7 +4075,7 @@
       case False
       have "lx \<le> real_of_float c" "real_of_float c \<le> ux" "lx \<le> xs!x" "xs!x \<le> ux"
         using Suc bnd_c \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto
-      from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
+      from taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
       obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
         and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
            (\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +
diff -r 7e0b0db5e9ac -r 1826a90b9cbc src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sun Jul 31 17:25:38 2016 +0200
+++ b/src/HOL/MacLaurin.thy	Sun Jul 31 18:05:20 2016 +0200
@@ -4,7 +4,7 @@
     Author:     Lukas Bulwahn and Bernhard Häupler, 2005
 *)
 
-section \<open>MacLaurin Series\<close>
+section \<open>MacLaurin and Taylor Series\<close>
 
 theory MacLaurin
 imports Transcendental
@@ -556,4 +556,118 @@
     done
 qed
 
+
+section \<open>Taylor series\<close>
+
+text \<open>
+  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
+  to prove Taylor's theorem.
+\<close>
+
+lemma taylor_up:
+  assumes INIT: "n > 0" "diff 0 = f"
+    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
+    and INTERV: "a \<le> c" "c < b"
+  shows "\<exists>t::real. c < t \<and> t < b \<and>
+    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
+proof -
+  from INTERV have "0 < b - c" by arith
+  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
+    by auto
+  moreover
+  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> b - c \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+  proof (intro strip)
+    fix m t
+    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
+    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
+      by auto
+    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
+      by (rule DERIV_add)
+    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
+      by (rule DERIV_chain2)
+    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+      by simp
+  qed
+  ultimately obtain x where
+    "0 < x \<and> x < b - c \<and>
+      f (b - c + c) =
+        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
+     by (rule Maclaurin [THEN exE])
+   then have "c < x + c \<and> x + c < b \<and> f b =
+     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
+    by fastforce
+  then show ?thesis by fastforce
+qed
+
+lemma taylor_down:
+  fixes a :: real and n :: nat
+  assumes INIT: "n > 0" "diff 0 = f"
+    and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
+    and INTERV: "a < c" "c \<le> b"
+  shows "\<exists>t. a < t \<and> t < c \<and>
+    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
+proof -
+  from INTERV have "a-c < 0" by arith
+  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
+    by auto
+  moreover
+  have "\<forall>m t. m < n \<and> a - c \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+  proof (rule allI impI)+
+    fix m t
+    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
+    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
+      by auto
+    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
+      by (rule DERIV_add)
+    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
+      by (rule DERIV_chain2)
+    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
+      by simp
+  qed
+  ultimately obtain x where
+    "a - c < x \<and> x < 0 \<and>
+      f (a - c + c) =
+        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
+    by (rule Maclaurin_minus [THEN exE])
+  then have "a < x + c \<and> x + c < c \<and>
+    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
+    by fastforce
+  then show ?thesis by fastforce
+qed
+
+theorem taylor:
+  fixes a :: real and n :: nat
+  assumes INIT: "n > 0" "diff 0 = f"
+    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
+  shows "\<exists>t.
+    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
+    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
+proof (cases "x < c")
+  case True
+  note INIT
+  moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    using DERIV and INTERV by fastforce
+  moreover note True
+  moreover from INTERV have "c \<le> b"
+    by simp
+  ultimately have "\<exists>t>x. t < c \<and> f x =
+    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
+    by (rule taylor_down)
+  with True show ?thesis by simp
+next
+  case False
+  note INIT
+  moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
+    using DERIV and INTERV by fastforce
+  moreover from INTERV have "a \<le> c"
+    by arith
+  moreover from False and INTERV have "c < x"
+    by arith
+  ultimately have "\<exists>t>c. t < x \<and> f x =
+    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
+    by (rule taylor_up)
+  with False show ?thesis by simp
+qed
+
 end
diff -r 7e0b0db5e9ac -r 1826a90b9cbc src/HOL/Taylor.thy
--- a/src/HOL/Taylor.thy	Sun Jul 31 17:25:38 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,122 +0,0 @@
-(*  Title:      HOL/Taylor.thy
-    Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
-*)
-
-section \<open>Taylor series\<close>
-
-theory Taylor
-imports MacLaurin
-begin
-
-text \<open>
-  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
-  to prove Taylor's theorem.
-\<close>
-
-lemma taylor_up:
-  assumes INIT: "n > 0" "diff 0 = f"
-    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
-    and INTERV: "a \<le> c" "c < b"
-  shows "\<exists>t::real. c < t \<and> t < b \<and>
-    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
-proof -
-  from INTERV have "0 < b - c" by arith
-  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
-    by auto
-  moreover
-  have "\<forall>m t. m < n \<and> 0 \<le> t \<and> t \<le> b - c \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
-  proof (intro strip)
-    fix m t
-    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
-    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
-      by auto
-    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
-      by (rule DERIV_add)
-    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
-      by (rule DERIV_chain2)
-    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
-      by simp
-  qed
-  ultimately obtain x where
-    "0 < x \<and> x < b - c \<and>
-      f (b - c + c) =
-        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
-     by (rule Maclaurin [THEN exE])
-   then have "c < x + c \<and> x + c < b \<and> f b =
-     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
-    by fastforce
-  then show ?thesis by fastforce
-qed
-
-lemma taylor_down:
-  fixes a :: real and n :: nat
-  assumes INIT: "n > 0" "diff 0 = f"
-    and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
-    and INTERV: "a < c" "c \<le> b"
-  shows "\<exists>t. a < t \<and> t < c \<and>
-    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
-proof -
-  from INTERV have "a-c < 0" by arith
-  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
-    by auto
-  moreover
-  have "\<forall>m t. m < n \<and> a - c \<le> t \<and> t \<le> 0 \<longrightarrow> DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
-  proof (rule allI impI)+
-    fix m t
-    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
-    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
-      by auto
-    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
-      by (rule DERIV_add)
-    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
-      by (rule DERIV_chain2)
-    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
-      by simp
-  qed
-  ultimately obtain x where
-    "a - c < x \<and> x < 0 \<and>
-      f (a - c + c) =
-        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
-    by (rule Maclaurin_minus [THEN exE])
-  then have "a < x + c \<and> x + c < c \<and>
-    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
-    by fastforce
-  then show ?thesis by fastforce
-qed
-
-theorem taylor:
-  fixes a :: real and n :: nat
-  assumes INIT: "n > 0" "diff 0 = f"
-    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
-  shows "\<exists>t.
-    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
-    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
-proof (cases "x < c")
-  case True
-  note INIT
-  moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-    using DERIV and INTERV by fastforce
-  moreover note True
-  moreover from INTERV have "c \<le> b"
-    by simp
-  ultimately have "\<exists>t>x. t < c \<and> f x =
-    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
-    by (rule taylor_down)
-  with True show ?thesis by simp
-next
-  case False
-  note INIT
-  moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
-    using DERIV and INTERV by fastforce
-  moreover from INTERV have "a \<le> c"
-    by arith
-  moreover from False and INTERV have "c < x"
-    by arith
-  ultimately have "\<exists>t>c. t < x \<and> f x =
-    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
-    by (rule taylor_up)
-  with False show ?thesis by simp
-qed
-
-end