simplified theory structure;
authorwenzelm
Sun Jul 31 18:05:20 2016 +0200 (2016-07-31)
changeset 635701826a90b9cbc
parent 63569 7e0b0db5e9ac
child 63571 aee0d92995b6
simplified theory structure;
src/HOL/Complex_Main.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/MacLaurin.thy
src/HOL/Taylor.thy
     1.1 --- a/src/HOL/Complex_Main.thy	Sun Jul 31 17:25:38 2016 +0200
     1.2 +++ b/src/HOL/Complex_Main.thy	Sun Jul 31 18:05:20 2016 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4    Real
     1.5    Complex
     1.6    Transcendental
     1.7 -  Taylor
     1.8 +  MacLaurin
     1.9    Deriv
    1.10  begin
    1.11  
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 31 17:25:38 2016 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Jul 31 18:05:20 2016 +0200
     2.3 @@ -4075,7 +4075,7 @@
     2.4        case False
     2.5        have "lx \<le> real_of_float c" "real_of_float c \<le> ux" "lx \<le> xs!x" "xs!x \<le> ux"
     2.6          using Suc bnd_c \<open>bounded_by xs vs\<close>[THEN bounded_byE, OF \<open>x < length vs\<close>] bnd_x by auto
     2.7 -      from Taylor.taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
     2.8 +      from taylor[OF zero_less_Suc, of F, OF F0 DERIV[unfolded Suc] this False]
     2.9        obtain t::real where t_bnd: "if xs ! x < c then xs ! x < t \<and> t < c else c < t \<and> t < xs ! x"
    2.10          and fl_eq: "interpret_floatarith f (xs[x := xs ! x]) =
    2.11             (\<Sum>m = 0..<Suc n'. F m c / (fact m) * (xs ! x - c) ^ m) +
     3.1 --- a/src/HOL/MacLaurin.thy	Sun Jul 31 17:25:38 2016 +0200
     3.2 +++ b/src/HOL/MacLaurin.thy	Sun Jul 31 18:05:20 2016 +0200
     3.3 @@ -4,7 +4,7 @@
     3.4      Author:     Lukas Bulwahn and Bernhard Häupler, 2005
     3.5  *)
     3.6  
     3.7 -section \<open>MacLaurin Series\<close>
     3.8 +section \<open>MacLaurin and Taylor Series\<close>
     3.9  
    3.10  theory MacLaurin
    3.11  imports Transcendental
    3.12 @@ -556,4 +556,118 @@
    3.13      done
    3.14  qed
    3.15  
    3.16 +
    3.17 +section \<open>Taylor series\<close>
    3.18 +
    3.19 +text \<open>
    3.20 +  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
    3.21 +  to prove Taylor's theorem.
    3.22 +\<close>
    3.23 +
    3.24 +lemma taylor_up:
    3.25 +  assumes INIT: "n > 0" "diff 0 = f"
    3.26 +    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
    3.27 +    and INTERV: "a \<le> c" "c < b"
    3.28 +  shows "\<exists>t::real. c < t \<and> t < b \<and>
    3.29 +    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
    3.30 +proof -
    3.31 +  from INTERV have "0 < b - c" by arith
    3.32 +  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
    3.33 +    by auto
    3.34 +  moreover
    3.35 +  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)"
    3.36 +  proof (intro strip)
    3.37 +    fix m t
    3.38 +    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
    3.39 +    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
    3.40 +      by auto
    3.41 +    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
    3.42 +      by (rule DERIV_add)
    3.43 +    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
    3.44 +      by (rule DERIV_chain2)
    3.45 +    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    3.46 +      by simp
    3.47 +  qed
    3.48 +  ultimately obtain x where
    3.49 +    "0 < x \<and> x < b - c \<and>
    3.50 +      f (b - c + c) =
    3.51 +        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
    3.52 +     by (rule Maclaurin [THEN exE])
    3.53 +   then have "c < x + c \<and> x + c < b \<and> f b =
    3.54 +     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
    3.55 +    by fastforce
    3.56 +  then show ?thesis by fastforce
    3.57 +qed
    3.58 +
    3.59 +lemma taylor_down:
    3.60 +  fixes a :: real and n :: nat
    3.61 +  assumes INIT: "n > 0" "diff 0 = f"
    3.62 +    and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
    3.63 +    and INTERV: "a < c" "c \<le> b"
    3.64 +  shows "\<exists>t. a < t \<and> t < c \<and>
    3.65 +    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
    3.66 +proof -
    3.67 +  from INTERV have "a-c < 0" by arith
    3.68 +  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
    3.69 +    by auto
    3.70 +  moreover
    3.71 +  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)"
    3.72 +  proof (rule allI impI)+
    3.73 +    fix m t
    3.74 +    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
    3.75 +    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
    3.76 +      by auto
    3.77 +    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
    3.78 +      by (rule DERIV_add)
    3.79 +    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
    3.80 +      by (rule DERIV_chain2)
    3.81 +    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    3.82 +      by simp
    3.83 +  qed
    3.84 +  ultimately obtain x where
    3.85 +    "a - c < x \<and> x < 0 \<and>
    3.86 +      f (a - c + c) =
    3.87 +        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
    3.88 +    by (rule Maclaurin_minus [THEN exE])
    3.89 +  then have "a < x + c \<and> x + c < c \<and>
    3.90 +    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
    3.91 +    by fastforce
    3.92 +  then show ?thesis by fastforce
    3.93 +qed
    3.94 +
    3.95 +theorem taylor:
    3.96 +  fixes a :: real and n :: nat
    3.97 +  assumes INIT: "n > 0" "diff 0 = f"
    3.98 +    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    3.99 +    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
   3.100 +  shows "\<exists>t.
   3.101 +    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
   3.102 +    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
   3.103 +proof (cases "x < c")
   3.104 +  case True
   3.105 +  note INIT
   3.106 +  moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   3.107 +    using DERIV and INTERV by fastforce
   3.108 +  moreover note True
   3.109 +  moreover from INTERV have "c \<le> b"
   3.110 +    by simp
   3.111 +  ultimately have "\<exists>t>x. t < c \<and> f x =
   3.112 +    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
   3.113 +    by (rule taylor_down)
   3.114 +  with True show ?thesis by simp
   3.115 +next
   3.116 +  case False
   3.117 +  note INIT
   3.118 +  moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   3.119 +    using DERIV and INTERV by fastforce
   3.120 +  moreover from INTERV have "a \<le> c"
   3.121 +    by arith
   3.122 +  moreover from False and INTERV have "c < x"
   3.123 +    by arith
   3.124 +  ultimately have "\<exists>t>c. t < x \<and> f x =
   3.125 +    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
   3.126 +    by (rule taylor_up)
   3.127 +  with False show ?thesis by simp
   3.128 +qed
   3.129 +
   3.130  end
     4.1 --- a/src/HOL/Taylor.thy	Sun Jul 31 17:25:38 2016 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,122 +0,0 @@
     4.4 -(*  Title:      HOL/Taylor.thy
     4.5 -    Author:     Lukas Bulwahn, Bernhard Haeupler, Technische Universitaet Muenchen
     4.6 -*)
     4.7 -
     4.8 -section \<open>Taylor series\<close>
     4.9 -
    4.10 -theory Taylor
    4.11 -imports MacLaurin
    4.12 -begin
    4.13 -
    4.14 -text \<open>
    4.15 -  We use MacLaurin and the translation of the expansion point \<open>c\<close> to \<open>0\<close>
    4.16 -  to prove Taylor's theorem.
    4.17 -\<close>
    4.18 -
    4.19 -lemma taylor_up:
    4.20 -  assumes INIT: "n > 0" "diff 0 = f"
    4.21 -    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> (diff (Suc m) t)"
    4.22 -    and INTERV: "a \<le> c" "c < b"
    4.23 -  shows "\<exists>t::real. c < t \<and> t < b \<and>
    4.24 -    f b = (\<Sum>m<n. (diff m c / fact m) * (b - c)^m) + (diff n t / fact n) * (b - c)^n"
    4.25 -proof -
    4.26 -  from INTERV have "0 < b - c" by arith
    4.27 -  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
    4.28 -    by auto
    4.29 -  moreover
    4.30 -  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)"
    4.31 -  proof (intro strip)
    4.32 -    fix m t
    4.33 -    assume "m < n \<and> 0 \<le> t \<and> t \<le> b - c"
    4.34 -    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
    4.35 -      by auto
    4.36 -    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
    4.37 -      by (rule DERIV_add)
    4.38 -    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
    4.39 -      by (rule DERIV_chain2)
    4.40 -    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    4.41 -      by simp
    4.42 -  qed
    4.43 -  ultimately obtain x where
    4.44 -    "0 < x \<and> x < b - c \<and>
    4.45 -      f (b - c + c) =
    4.46 -        (\<Sum>m<n. diff m (0 + c) / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
    4.47 -     by (rule Maclaurin [THEN exE])
    4.48 -   then have "c < x + c \<and> x + c < b \<and> f b =
    4.49 -     (\<Sum>m<n. diff m c / fact m * (b - c) ^ m) + diff n (x + c) / fact n * (b - c) ^ n"
    4.50 -    by fastforce
    4.51 -  then show ?thesis by fastforce
    4.52 -qed
    4.53 -
    4.54 -lemma taylor_down:
    4.55 -  fixes a :: real and n :: nat
    4.56 -  assumes INIT: "n > 0" "diff 0 = f"
    4.57 -    and DERIV: "(\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t)"
    4.58 -    and INTERV: "a < c" "c \<le> b"
    4.59 -  shows "\<exists>t. a < t \<and> t < c \<and>
    4.60 -    f a = (\<Sum>m<n. (diff m c / fact m) * (a - c)^m) + (diff n t / fact n) * (a - c)^n"
    4.61 -proof -
    4.62 -  from INTERV have "a-c < 0" by arith
    4.63 -  moreover from INIT have "n > 0" "(\<lambda>m x. diff m (x + c)) 0 = (\<lambda>x. f (x + c))"
    4.64 -    by auto
    4.65 -  moreover
    4.66 -  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)"
    4.67 -  proof (rule allI impI)+
    4.68 -    fix m t
    4.69 -    assume "m < n \<and> a - c \<le> t \<and> t \<le> 0"
    4.70 -    with DERIV and INTERV have "DERIV (diff m) (t + c) :> diff (Suc m) (t + c)"
    4.71 -      by auto
    4.72 -    moreover from DERIV_ident and DERIV_const have "DERIV (\<lambda>x. x + c) t :> 1 + 0"
    4.73 -      by (rule DERIV_add)
    4.74 -    ultimately have "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c) * (1 + 0)"
    4.75 -      by (rule DERIV_chain2)
    4.76 -    then show "DERIV (\<lambda>x. diff m (x + c)) t :> diff (Suc m) (t + c)"
    4.77 -      by simp
    4.78 -  qed
    4.79 -  ultimately obtain x where
    4.80 -    "a - c < x \<and> x < 0 \<and>
    4.81 -      f (a - c + c) =
    4.82 -        (\<Sum>m<n. diff m (0 + c) / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
    4.83 -    by (rule Maclaurin_minus [THEN exE])
    4.84 -  then have "a < x + c \<and> x + c < c \<and>
    4.85 -    f a = (\<Sum>m<n. diff m c / fact m * (a - c) ^ m) + diff n (x + c) / fact n * (a - c) ^ n"
    4.86 -    by fastforce
    4.87 -  then show ?thesis by fastforce
    4.88 -qed
    4.89 -
    4.90 -theorem taylor:
    4.91 -  fixes a :: real and n :: nat
    4.92 -  assumes INIT: "n > 0" "diff 0 = f"
    4.93 -    and DERIV: "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
    4.94 -    and INTERV: "a \<le> c " "c \<le> b" "a \<le> x" "x \<le> b" "x \<noteq> c"
    4.95 -  shows "\<exists>t.
    4.96 -    (if x < c then x < t \<and> t < c else c < t \<and> t < x) \<and>
    4.97 -    f x = (\<Sum>m<n. (diff m c / fact m) * (x - c)^m) + (diff n t / fact n) * (x - c)^n"
    4.98 -proof (cases "x < c")
    4.99 -  case True
   4.100 -  note INIT
   4.101 -  moreover have "\<forall>m t. m < n \<and> x \<le> t \<and> t \<le> b \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   4.102 -    using DERIV and INTERV by fastforce
   4.103 -  moreover note True
   4.104 -  moreover from INTERV have "c \<le> b"
   4.105 -    by simp
   4.106 -  ultimately have "\<exists>t>x. t < c \<and> f x =
   4.107 -    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
   4.108 -    by (rule taylor_down)
   4.109 -  with True show ?thesis by simp
   4.110 -next
   4.111 -  case False
   4.112 -  note INIT
   4.113 -  moreover have "\<forall>m t. m < n \<and> a \<le> t \<and> t \<le> x \<longrightarrow> DERIV (diff m) t :> diff (Suc m) t"
   4.114 -    using DERIV and INTERV by fastforce
   4.115 -  moreover from INTERV have "a \<le> c"
   4.116 -    by arith
   4.117 -  moreover from False and INTERV have "c < x"
   4.118 -    by arith
   4.119 -  ultimately have "\<exists>t>c. t < x \<and> f x =
   4.120 -    (\<Sum>m<n. diff m c / (fact m) * (x - c) ^ m) + diff n t / (fact n) * (x - c) ^ n"
   4.121 -    by (rule taylor_up)
   4.122 -  with False show ?thesis by simp
   4.123 -qed
   4.124 -
   4.125 -end