src/HOL/Hyperreal/Integration.thy
author paulson
Fri Jul 30 18:37:58 2004 +0200 (2004-07-30)
changeset 15093 49ede01e9ee6
parent 13958 c1c67582c9b5
child 15094 a7d1a3fdc30d
permissions -rw-r--r--
conversion of Integration and NSPrimes to Isar scripts
     1 (*  Title       : Integration.thy
     2     Author      : Jacques D. Fleuriot
     3     Copyright   : 2000  University of Edinburgh
     4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     5 *)
     6 
     7 header{*Theory of Integration*}
     8 
     9 theory Integration = MacLaurin:
    10 
    11 text{*We follow John Harrison in formalizing the Gauge integral.*}
    12 
    13 constdefs
    14 
    15   --{*Partitions and tagged partitions etc.*}
    16 
    17   partition :: "[(real*real),nat => real] => bool"
    18   "partition == %(a,b) D. ((D 0 = a) &
    19                          (\<exists>N. ((\<forall>n. n < N --> D(n) < D(Suc n)) &
    20                             (\<forall>n. N \<le> n --> (D(n) = b)))))"
    21 
    22   psize :: "(nat => real) => nat"
    23   "psize D == @N. (\<forall>n. n < N --> D(n) < D(Suc n)) &
    24                   (\<forall>n. N \<le> n --> (D(n) = D(N)))"
    25 
    26   tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
    27   "tpart == %(a,b) (D,p). partition(a,b) D &
    28                           (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))"
    29 
    30   --{*Gauges and gauge-fine divisions*}
    31 
    32   gauge :: "[real => bool, real => real] => bool"
    33   "gauge E g == \<forall>x. E x --> 0 < g(x)"
    34 
    35   fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
    36   "fine == % g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
    37 
    38   --{*Riemann sum*}
    39 
    40   rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
    41   "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
    42 
    43   --{*Gauge integrability (definite)*}
    44 
    45    Integral :: "[(real*real),real=>real,real] => bool"
    46    "Integral == %(a,b) f k. \<forall>e. 0 < e -->
    47                                (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
    48                                (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
    49                                          \<bar>rsum(D,p) f - k\<bar> < e))"
    50 
    51 
    52 lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
    53 by (auto simp add: psize_def)
    54 
    55 lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1"
    56 apply (simp add: psize_def)
    57 apply (rule some_equality, auto)
    58 apply (drule_tac x = 1 in spec, auto)
    59 done
    60 
    61 lemma partition_single [simp]:
    62      "a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)"
    63 by (auto simp add: partition_def order_le_less)
    64 
    65 lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)"
    66 by (simp add: partition_def)
    67 
    68 lemma partition:
    69        "(partition(a,b) D) =
    70         ((D 0 = a) &
    71          (\<forall>n. n < (psize D) --> D n < D(Suc n)) &
    72          (\<forall>n. (psize D) \<le> n --> (D n = b)))"
    73 apply (simp add: partition_def, auto)
    74 apply (subgoal_tac [!] "psize D = N", auto)
    75 apply (simp_all (no_asm) add: psize_def)
    76 apply (rule_tac [!] some_equality, blast)
    77   prefer 2 apply blast
    78 apply (rule_tac [!] ccontr)
    79 apply (simp_all add: linorder_neq_iff, safe)
    80 apply (drule_tac x = Na in spec)
    81 apply (rotate_tac 3)
    82 apply (drule_tac x = "Suc Na" in spec, simp)
    83 apply (rotate_tac 2)
    84 apply (drule_tac x = N in spec, simp)
    85 apply (drule_tac x = Na in spec)
    86 apply (drule_tac x = "Suc Na" and P = "%n. Na \<le> n \<longrightarrow> D n = D Na" in spec, auto)
    87 done
    88 
    89 lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)"
    90 by (simp add: partition)
    91 
    92 lemma partition_rhs2: "[|partition(a,b) D; psize D \<le> n |] ==> (D n = b)"
    93 by (simp add: partition)
    94 
    95 lemma lemma_partition_lt_gen [rule_format]:
    96  "partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) --> D(m) < D(m + Suc d)"
    97 apply (induct_tac "d", auto simp add: partition)
    98 apply (blast dest: Suc_le_lessD  intro: less_le_trans order_less_trans)
    99 done
   100 
   101 lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d"
   102 by (auto simp add: less_iff_Suc_add)
   103 
   104 lemma partition_lt_gen:
   105      "[|partition(a,b) D; m < n; n \<le> (psize D)|] ==> D(m) < D(n)"
   106 by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen)
   107 
   108 lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)"
   109 apply (induct "n")
   110 apply (auto simp add: partition)
   111 done
   112 
   113 lemma partition_le: "partition(a,b) D ==> a \<le> b"
   114 apply (frule partition [THEN iffD1], safe)
   115 apply (rotate_tac 2)
   116 apply (drule_tac x = "psize D" in spec, safe)
   117 apply (rule ccontr)
   118 apply (case_tac "psize D = 0", safe)
   119 apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
   120 done
   121 
   122 lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
   123 by (auto intro: partition_lt_gen)
   124 
   125 lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))"
   126 apply (frule partition [THEN iffD1], safe)
   127 apply (rotate_tac 2)
   128 apply (drule_tac x = "psize D" in spec)
   129 apply (rule ccontr)
   130 apply (drule_tac n = "psize D - 1" in partition_lt)
   131 prefer 3 apply (blast, auto)
   132 done
   133 
   134 lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)"
   135 apply (frule partition [THEN iffD1], safe)
   136 apply (induct_tac "r")
   137 apply (cut_tac [2] y = "Suc n" and x = "psize D" in linorder_le_less_linear, safe)
   138  apply (blast intro: order_trans partition_le)
   139 apply (drule_tac x = n in spec)
   140 apply (best intro: order_less_trans order_trans order_less_imp_le)
   141 done
   142 
   143 lemma partition_lb_lt: "[| partition(a,b) D; psize D ~= 0 |] ==> a < D(Suc n)"
   144 apply (rule_tac t = a in partition_lhs [THEN subst], assumption)
   145 apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear)
   146 apply (frule partition [THEN iffD1], safe)
   147  apply (blast intro: partition_lt less_le_trans)
   148 apply (rotate_tac 3)
   149 apply (drule_tac x = "Suc n" in spec)
   150 apply (erule impE)
   151 apply (erule less_imp_le)
   152 apply (frule partition_rhs)
   153 apply (drule partition_gt, assumption)
   154 apply (simp (no_asm_simp))
   155 done
   156 
   157 lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b"
   158 apply (frule partition [THEN iffD1])
   159 apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast)
   160 apply (subgoal_tac "\<forall>x. D ((psize D) - x) \<le> b")
   161 apply (rotate_tac 4)
   162 apply (drule_tac x = "psize D - r" in spec)
   163 apply (subgoal_tac "psize D - (psize D - r) = r")
   164 apply simp
   165 apply arith
   166 apply safe
   167 apply (induct_tac "x")
   168 apply (simp (no_asm), blast)
   169 apply (case_tac "psize D - Suc n = 0")
   170 apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl)
   171 apply (simp (no_asm_simp) add: partition_le)
   172 apply (rule order_trans)
   173  prefer 2 apply assumption
   174 apply (subgoal_tac "psize D - n = Suc (psize D - Suc n)")
   175  prefer 2 apply arith
   176 apply (drule_tac x = "psize D - Suc n" in spec)
   177 apply (erule_tac V = "\<forall>n. psize D \<le> n --> D n = b" in thin_rl, simp)
   178 done
   179 
   180 lemma partition_ub_lt: "[| partition(a,b) D; n < psize D |] ==> D(n) < b"
   181 by (blast intro: partition_rhs [THEN subst] partition_gt)
   182 
   183 lemma lemma_partition_append1:
   184      "[| partition (a, b) D1; partition (b, c) D2 |]
   185        ==> (\<forall>n.
   186              n < psize D1 + psize D2 -->
   187              (if n < psize D1 then D1 n else D2 (n - psize D1))
   188              < (if Suc n < psize D1 then D1 (Suc n)
   189                 else D2 (Suc n - psize D1))) &
   190          (\<forall>n.
   191              psize D1 + psize D2 \<le> n -->
   192              (if n < psize D1 then D1 n else D2 (n - psize D1)) =
   193              (if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2)
   194               else D2 (psize D1 + psize D2 - psize D1)))"
   195 apply safe
   196 apply (auto intro: partition_lt_gen)
   197 apply (subgoal_tac "psize D1 = Suc n")
   198 apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt)
   199 apply (auto intro!: partition_rhs2 simp add: partition_rhs
   200             split: nat_diff_split)
   201 done
   202 
   203 lemma lemma_psize1:
   204      "[| partition (a, b) D1; partition (b, c) D2; N < psize D1 |]
   205       ==> D1(N) < D2 (psize D2)"
   206 apply (rule_tac y = "D1 (psize D1) " in order_less_le_trans)
   207 apply (erule partition_gt, assumption)
   208 apply (auto simp add: partition_rhs partition_le)
   209 done
   210 
   211 lemma lemma_partition_append2:
   212      "[| partition (a, b) D1; partition (b, c) D2 |]
   213       ==> psize (%n. if n < psize D1 then D1 n else D2 (n - psize D1)) =
   214           psize D1 + psize D2"
   215 apply (rule_tac D2 = "%n. if n < psize D1 then D1 n else D2 (n - psize D1) "
   216        in psize_def [THEN meta_eq_to_obj_eq, THEN ssubst])
   217 apply (rule some1_equality)
   218 prefer 2 apply (blast intro!: lemma_partition_append1)
   219 apply (rule ex1I, rule lemma_partition_append1, auto)
   220 apply (rule ccontr)
   221 apply (simp add: linorder_neq_iff, safe)
   222 apply (rotate_tac 3)
   223 apply (drule_tac x = "psize D1 + psize D2" in spec, auto)
   224 apply (case_tac "N < psize D1")
   225 apply (auto dest: lemma_psize1)
   226 apply (subgoal_tac "N - psize D1 < psize D2")
   227  prefer 2 apply arith
   228 apply (drule_tac a = b and b = c in partition_gt, auto)
   229 apply (drule_tac x = "psize D1 + psize D2" in spec)
   230 apply (auto simp add: partition_rhs2)
   231 done
   232 
   233 lemma tpart_eq_lhs_rhs:
   234 "[|psize D = 0; tpart(a,b) (D,p)|] ==> a = b"
   235 apply (simp add: tpart_def)
   236 apply (auto simp add: partition_eq)
   237 done
   238 
   239 lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D"
   240 by (simp add: tpart_def)
   241 
   242 lemma partition_append:
   243      "[| tpart(a,b) (D1,p1); fine(g) (D1,p1);
   244          tpart(b,c) (D2,p2); fine(g) (D2,p2) |]
   245        ==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)"
   246 apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n - psize D1)"
   247        in exI)
   248 apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n - psize D1)"
   249        in exI)
   250 apply (case_tac "psize D1 = 0")
   251 apply (auto dest: tpart_eq_lhs_rhs)
   252  prefer 2
   253 apply (simp add: fine_def
   254                  lemma_partition_append2 [OF tpart_partition tpart_partition])
   255   --{*But must not expand @{term fine} in other subgoals*}
   256 apply auto
   257 apply (subgoal_tac "psize D1 = Suc n")
   258  prefer 2 apply arith
   259 apply (drule tpart_partition [THEN partition_rhs])
   260 apply (drule tpart_partition [THEN partition_lhs])
   261 apply (auto split: nat_diff_split)
   262 apply (auto simp add: tpart_def)
   263 defer 1
   264  apply (subgoal_tac "psize D1 = Suc n")
   265   prefer 2 apply arith
   266  apply (drule partition_rhs)
   267  apply (drule partition_lhs, auto)
   268 apply (simp split: nat_diff_split)
   269 apply (subst partition)
   270 apply (subst lemma_partition_append2)
   271 apply (rule_tac [3] conjI)
   272 apply (drule_tac [4] lemma_partition_append1)
   273 apply (auto simp add: partition_lhs partition_rhs)
   274 done
   275 
   276 text{*We can always find a division which is fine wrt any gauge*}
   277 
   278 lemma partition_exists:
   279      "[| a \<le> b; gauge(%x. a \<le> x & x \<le> b) g |]
   280       ==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)"
   281 apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b --> 
   282                    (\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))" 
   283        in lemma_BOLZANO2)
   284 apply safe
   285 apply (blast intro: real_le_trans)+
   286 apply (auto intro: partition_append)
   287 apply (case_tac "a \<le> x & x \<le> b")
   288 apply (rule_tac [2] x = 1 in exI, auto)
   289 apply (rule_tac x = "g x" in exI)
   290 apply (auto simp add: gauge_def)
   291 apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI)
   292 apply (rule_tac x = "%n. if n = 0 then x else ba" in exI)
   293 apply (auto simp add: tpart_def fine_def)
   294 done
   295 
   296 text{*Lemmas about combining gauges*}
   297 
   298 lemma gauge_min:
   299      "[| gauge(E) g1; gauge(E) g2 |]
   300       ==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))"
   301 by (simp add: gauge_def)
   302 
   303 lemma fine_min:
   304       "fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p)
   305        ==> fine(g1) (D,p) & fine(g2) (D,p)"
   306 by (auto simp add: fine_def split: split_if_asm)
   307 
   308 
   309 text{*The integral is unique if it exists*}
   310 
   311 lemma Integral_unique:
   312     "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
   313 apply (simp add: Integral_def)
   314 apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
   315 apply auto
   316 apply (drule gauge_min, assumption)
   317 apply (drule_tac g = "%x. if g x < ga x then g x else ga x" 
   318        in partition_exists, assumption, auto)
   319 apply (drule fine_min)
   320 apply (drule spec)+
   321 apply auto
   322 apply (subgoal_tac "abs ((rsum (D,p) f - k2) - (rsum (D,p) f - k1)) < \<bar>k1 - k2\<bar> ")
   323 apply arith
   324 apply (drule add_strict_mono, assumption)
   325 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
   326                 mult_less_cancel_right, arith)
   327 done
   328 
   329 lemma Integral_zero [simp]: "Integral(a,a) f 0"
   330 apply (auto simp add: Integral_def)
   331 apply (rule_tac x = "%x. 1" in exI)
   332 apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def)
   333 done
   334 
   335 lemma sumr_partition_eq_diff_bounds [simp]:
   336      "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
   337 by (induct_tac "m", auto)
   338 
   339 lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
   340 apply (drule real_le_imp_less_or_eq, auto)
   341 apply (auto simp add: rsum_def Integral_def)
   342 apply (rule_tac x = "%x. b - a" in exI)
   343 apply (auto simp add: gauge_def abs_interval_iff tpart_def partition)
   344 done
   345 
   346 lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
   347 apply (drule real_le_imp_less_or_eq, auto)
   348 apply (auto simp add: rsum_def Integral_def)
   349 apply (rule_tac x = "%x. b - a" in exI)
   350 apply (auto simp add: sumr_mult [symmetric] gauge_def abs_interval_iff 
   351                right_diff_distrib [symmetric] partition tpart_def)
   352 done
   353 
   354 lemma Integral_mult:
   355      "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
   356 apply (drule real_le_imp_less_or_eq)
   357 apply (auto dest: Integral_unique [OF real_le_refl Integral_zero])
   358 apply (auto simp add: rsum_def Integral_def sumr_mult [symmetric] real_mult_assoc)
   359 apply (rule_tac a2 = c in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
   360  prefer 2 apply force
   361 apply (drule_tac x = "e/abs c" in spec, auto)
   362 apply (simp add: zero_less_mult_iff divide_inverse)
   363 apply (rule exI, auto)
   364 apply (drule spec)+
   365 apply auto
   366 apply (rule_tac z1 = "inverse (abs c) " in real_mult_less_iff1 [THEN iffD1])
   367 apply (auto simp add: divide_inverse [symmetric] right_diff_distrib [symmetric])
   368 done
   369 
   370 text{*Fundamental theorem of calculus (Part I)*}
   371 
   372 text{*"Straddle Lemma" : Swartz & Thompson: AMM 95(7) 1988 *}
   373 
   374 lemma choiceP: "\<forall>x. P(x) --> (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) --> Q x (f x))"
   375 by meson
   376 
   377 lemma choiceP2: "\<forall>x. P(x) --> (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
   378       \<exists>f fa. (\<forall>x. P(x) --> R(f x) & Q x (f x) (fa x))"
   379 by meson
   380 
   381 (*UNUSED
   382 lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==>
   383       \<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))"
   384 *)
   385 
   386 
   387 (* new simplifications e.g. (y < x/n) = (y * n < x) are a real nuisance
   388    they break the original proofs and make new proofs longer!                 *)
   389 lemma strad1:
   390        "\<lbrakk>\<forall>xa::real. xa \<noteq> x \<and> \<bar>xa + - x\<bar> < s \<longrightarrow>
   391              \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e;
   392         0 < e; a \<le> x; x \<le> b; 0 < s\<rbrakk>
   393        \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> * 2 \<le> e * \<bar>z - x\<bar>"
   394 apply auto
   395 apply (case_tac "0 < \<bar>z - x\<bar> ")
   396  prefer 2 apply (simp add: zero_less_abs_iff)
   397 apply (drule_tac x = z in spec)
   398 apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
   399        in real_mult_le_cancel_iff2 [THEN iffD1])
   400  apply simp
   401 apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
   402           mult_assoc [symmetric])
   403 apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) 
   404                     = (f z - f x) / (z - x) - f' x")
   405  apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
   406 apply (subst mult_commute)
   407 apply (simp add: left_distrib diff_minus)
   408 apply (simp add: mult_assoc divide_inverse)
   409 apply (simp add: left_distrib)
   410 done
   411 
   412 lemma lemma_straddle:
   413      "[| \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x); 0 < e |]
   414       ==> \<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
   415                 (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
   416                   --> abs((f(v) - f(u)) - (f'(x) * (v - u))) \<le> e * (v - u))"
   417 apply (simp add: gauge_def)
   418 apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> 
   419         (\<exists>d. 0 < d & (\<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> abs ((f (v) - f (u)) - (f' (x) * (v - u))) \<le> e * (v - u)))")
   420 apply (drule choiceP, auto)
   421 apply (drule spec, auto)
   422 apply (auto simp add: DERIV_iff2 LIM_def)
   423 apply (drule_tac x = "e/2" in spec, auto)
   424 apply (frule strad1, assumption+)
   425 apply (rule_tac x = s in exI, auto)
   426 apply (rule_tac x = u and y = v in linorder_cases, auto)
   427 apply (rule_tac j = "abs ((f (v) - f (x)) - (f' (x) * (v - x))) + abs ((f (x) - f (u)) - (f' (x) * (x - u)))"
   428        in real_le_trans)
   429 apply (rule abs_triangle_ineq [THEN [2] real_le_trans])
   430 apply (simp add: right_diff_distrib, arith)
   431 apply (rule_tac t = "e* (v - u) " in real_sum_of_halves [THEN subst])
   432 apply (rule add_mono)
   433 apply (rule_tac j = " (e / 2) * \<bar>v - x\<bar> " in real_le_trans)
   434  prefer 2 apply simp apply arith
   435 apply (erule_tac [!]
   436        V= "\<forall>xa. xa ~= x & \<bar>xa + - x\<bar> < s --> \<bar>(f xa - f x) / (xa - x) + - f' x\<bar> * 2 < e"
   437         in thin_rl)
   438 apply (drule_tac x = v in spec, auto, arith)
   439 apply (drule_tac x = u in spec, auto, arith)
   440 apply (subgoal_tac "\<bar>f u - f x - f' x * (u - x)\<bar> = \<bar>f x - f u - f' x * (x - u)\<bar>")
   441 apply (rule order_trans)
   442 apply (auto simp add: abs_le_interval_iff)
   443 apply (simp add: right_diff_distrib, arith)
   444 done
   445 
   446 lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
   447       ==> Integral(a,b) f' (f(b) - f(a))"
   448 apply (drule real_le_imp_less_or_eq, auto)
   449 apply (auto simp add: Integral_def)
   450 apply (rule ccontr)
   451 apply (subgoal_tac "\<forall>e. 0 < e --> (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g & (\<forall>D p. tpart (a, b) (D, p) & fine g (D, p) --> \<bar>rsum (D, p) f' - (f b - f a)\<bar> \<le> e))")
   452 apply (rotate_tac 3)
   453 apply (drule_tac x = "e/2" in spec, auto)
   454 apply (drule spec, auto)
   455 apply ((drule spec)+, auto)
   456 apply (drule_tac e = "ea/ (b - a) " in lemma_straddle)
   457 apply (auto simp add: zero_less_divide_iff)
   458 apply (rule exI)
   459 apply (auto simp add: tpart_def rsum_def)
   460 apply (subgoal_tac "sumr 0 (psize D) (%n. f (D (Suc n)) - f (D n)) = f b - f a")
   461  prefer 2
   462  apply (cut_tac D = "%n. f (D n) " and m = "psize D"
   463         in sumr_partition_eq_diff_bounds)
   464  apply (simp add: partition_lhs partition_rhs)
   465 apply (drule sym, simp)
   466 apply (simp (no_asm) add: sumr_diff)
   467 apply (rule sumr_rabs [THEN real_le_trans])
   468 apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n))) ")
   469 apply (simp add: abs_minus_commute)
   470 apply (rule_tac t = ea in ssubst, assumption)
   471 apply (rule sumr_le2)
   472 apply (rule_tac [2] sumr_mult [THEN subst])
   473 apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
   474           fine_def)
   475 done
   476 
   477 
   478 lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
   479 by simp
   480 
   481 lemma Integral_add:
   482      "[| a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2;
   483          \<forall>x. a \<le> x & x \<le> c --> DERIV f x :> f' x |]
   484      ==> Integral(a,c) f' (k1 + k2)"
   485 apply (rule FTC1 [THEN Integral_subst], auto)
   486 apply (frule FTC1, auto)
   487 apply (frule_tac a = b in FTC1, auto)
   488 apply (drule_tac x = x in spec, auto)
   489 apply (drule_tac ?k2.0 = "f b - f a" in Integral_unique)
   490 apply (drule_tac [3] ?k2.0 = "f c - f b" in Integral_unique, auto)
   491 done
   492 
   493 lemma partition_psize_Least:
   494      "partition(a,b) D ==> psize D = (LEAST n. D(n) = b)"
   495 apply (auto intro!: Least_equality [symmetric] partition_rhs)
   496 apply (rule ccontr)
   497 apply (drule partition_ub_lt)
   498 apply (auto simp add: linorder_not_less [symmetric])
   499 done
   500 
   501 lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))"
   502 apply safe
   503 apply (drule_tac r = n in partition_ub, auto)
   504 done
   505 
   506 lemma lemma_partition_eq:
   507      "partition (a, c) D ==> D = (%n. if D n < c then D n else c)"
   508 apply (rule ext, auto)
   509 apply (auto dest!: lemma_partition_bounded)
   510 apply (drule_tac x = n in spec, auto)
   511 done
   512 
   513 lemma lemma_partition_eq2:
   514      "partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)"
   515 apply (rule ext, auto)
   516 apply (auto dest!: lemma_partition_bounded)
   517 apply (drule_tac x = n in spec, auto)
   518 done
   519 
   520 lemma partition_lt_Suc:
   521      "[| partition(a,b) D; n < psize D |] ==> D n < D (Suc n)"
   522 by (auto simp add: partition)
   523 
   524 lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)"
   525 apply (rule ext)
   526 apply (auto simp add: tpart_def)
   527 apply (drule linorder_not_less [THEN iffD1])
   528 apply (drule_tac r = "Suc n" in partition_ub)
   529 apply (drule_tac x = n in spec, auto)
   530 done
   531 
   532 subsection{*Lemmas for Additivity Theorem of Gauge Integral*}
   533 
   534 lemma lemma_additivity1:
   535      "[| a \<le> D n; D n < b; partition(a,b) D |] ==> n < psize D"
   536 by (auto simp add: partition linorder_not_less [symmetric])
   537 
   538 lemma lemma_additivity2: "[| a \<le> D n; partition(a,D n) D |] ==> psize D \<le> n"
   539 apply (rule ccontr, drule not_leE)
   540 apply (frule partition [THEN iffD1], safe)
   541 apply (frule_tac r = "Suc n" in partition_ub)
   542 apply (auto dest!: spec)
   543 done
   544 
   545 lemma partition_eq_bound:
   546      "[| partition(a,b) D; psize D < m |] ==> D(m) = D(psize D)"
   547 by (auto simp add: partition)
   548 
   549 lemma partition_ub2: "[| partition(a,b) D; psize D < m |] ==> D(r) \<le> D(m)"
   550 by (simp add: partition partition_ub)
   551 
   552 lemma tag_point_eq_partition_point:
   553     "[| tpart(a,b) (D,p); psize D \<le> m |] ==> p(m) = D(m)"
   554 apply (simp add: tpart_def, auto)
   555 apply (drule_tac x = m in spec)
   556 apply (auto simp add: partition_rhs2)
   557 done
   558 
   559 lemma partition_lt_cancel: "[| partition(a,b) D; D m < D n |] ==> m < n"
   560 apply (cut_tac m = n and n = "psize D" in less_linear, auto)
   561 apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   562 apply (cut_tac m = m and n = "psize D" in less_linear)
   563 apply (auto dest: partition_gt)
   564 apply (drule_tac n = m in partition_lt_gen, auto)
   565 apply (frule partition_eq_bound)
   566 apply (drule_tac [2] partition_gt, auto)
   567 apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   568 apply (auto dest: partition_eq_bound)
   569 apply (rule ccontr, drule leI, drule le_imp_less_or_eq)
   570 apply (frule partition_eq_bound, assumption)
   571 apply (drule_tac m = m in partition_eq_bound, auto)
   572 done
   573 
   574 lemma lemma_additivity4_psize_eq:
   575      "[| a \<le> D n; D n < b; partition (a, b) D |]
   576       ==> psize (%x. if D x < D n then D(x) else D n) = n"
   577 apply (unfold psize_def)
   578 apply (frule lemma_additivity1)
   579 apply (assumption, assumption)
   580 apply (rule some_equality)
   581 apply (auto intro: partition_lt_Suc)
   582 apply (drule_tac n = n in partition_lt_gen)
   583 apply (assumption, arith, arith)
   584 apply (cut_tac m = na and n = "psize D" in less_linear)
   585 apply (auto dest: partition_lt_cancel)
   586 apply (rule_tac x=N and y=n in linorder_cases)
   587 apply (drule_tac x = n and P="%m. N \<le> m --> ?f m = ?g m" in spec, auto)
   588 apply (drule_tac n = n in partition_lt_gen, auto, arith)
   589 apply (drule_tac x = n in spec)
   590 apply (simp split: split_if_asm)
   591 done
   592 
   593 lemma lemma_psize_left_less_psize:
   594      "partition (a, b) D
   595       ==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D"
   596 apply (frule_tac r = n in partition_ub)
   597 apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
   598 apply (auto simp add: lemma_partition_eq [symmetric])
   599 apply (frule_tac r = n in partition_lb)
   600 apply (drule lemma_additivity4_psize_eq)
   601 apply (rule_tac [3] ccontr, auto)
   602 apply (frule_tac not_leE [THEN [2] partition_eq_bound])
   603 apply (auto simp add: partition_rhs)
   604 done
   605 
   606 lemma lemma_psize_left_less_psize2:
   607      "[| partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) |]
   608       ==> na < psize D"
   609 apply (erule_tac lemma_psize_left_less_psize [THEN [2] less_le_trans], assumption)
   610 done
   611 
   612 
   613 lemma lemma_additivity3:
   614      "[| partition(a,b) D; D na < D n; D n < D (Suc na);
   615          n < psize D |]
   616       ==> False"
   617 apply (cut_tac m = n and n = "Suc na" in less_linear, auto)
   618 apply (drule_tac [2] n = n in partition_lt_gen, auto)
   619 apply (cut_tac m = "psize D" and n = na in less_linear)
   620 apply (auto simp add: partition_rhs2 less_Suc_eq)
   621 apply (drule_tac n = na in partition_lt_gen, auto)
   622 done
   623 
   624 lemma psize_const [simp]: "psize (%x. k) = 0"
   625 by (simp add: psize_def, auto)
   626 
   627 lemma lemma_additivity3a:
   628      "[| partition(a,b) D; D na < D n; D n < D (Suc na);
   629          na < psize D |]
   630       ==> False"
   631 apply (frule_tac m = n in partition_lt_cancel)
   632 apply (auto intro: lemma_additivity3)
   633 done
   634 
   635 lemma better_lemma_psize_right_eq1:
   636      "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D - n"
   637 apply (simp add: psize_def [of "(%x. D (x + n))"]);
   638 apply (rule_tac a = "psize D - n" in someI2, auto)
   639   apply (simp add: partition less_diff_conv)
   640  apply (simp add: le_diff_conv)
   641  apply (case_tac "psize D \<le> n")
   642   apply (simp add: partition_rhs2)
   643  apply (simp add: partition linorder_not_le)
   644 apply (rule ccontr, drule not_leE)
   645 apply (drule_tac x = "psize D - n" in spec, auto)
   646 apply (frule partition_rhs, safe)
   647 apply (frule partition_lt_cancel, assumption)
   648 apply (drule partition [THEN iffD1], safe)
   649 apply (subgoal_tac "~ D (psize D - n + n) < D (Suc (psize D - n + n))")
   650  apply blast
   651 apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)"
   652        in spec)
   653 apply (simp (no_asm_simp))
   654 done
   655 
   656 lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n"
   657 apply (rule ccontr, drule not_leE)
   658 apply (frule partition_lt_Suc, assumption)
   659 apply (frule_tac r = "Suc n" in partition_ub, auto)
   660 done
   661 
   662 lemma better_lemma_psize_right_eq1a:
   663      "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D - n"
   664 apply (simp add: psize_def [of "(%x. D (x + n))"]);
   665 apply (rule_tac a = "psize D - n" in someI2, auto)
   666   apply (simp add: partition less_diff_conv)
   667  apply (simp add: le_diff_conv)
   668 apply (case_tac "psize D \<le> n")
   669   apply (force intro: partition_rhs2)
   670  apply (simp add: partition linorder_not_le)
   671 apply (rule ccontr, drule not_leE)
   672 apply (frule psize_le_n)
   673 apply (drule_tac x = "psize D - n" in spec, simp)
   674 apply (drule partition [THEN iffD1], safe)
   675 apply (drule_tac x = "Suc n" and P="%na. psize D \<le> na \<longrightarrow> D na = D n" in spec, auto)
   676 done
   677 
   678 lemma better_lemma_psize_right_eq:
   679      "partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D - n"
   680 apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
   681 apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1)
   682 done
   683 
   684 lemma lemma_psize_right_eq1:
   685      "[| partition(a,b) D; D n < b |] ==> psize (%x. D (x + n)) \<le> psize D"
   686 apply (simp add: psize_def [of "(%x. D (x + n))"]);
   687 apply (rule_tac a = "psize D - n" in someI2, auto)
   688   apply (simp add: partition less_diff_conv)
   689  apply (subgoal_tac "n \<le> psize D")
   690   apply (simp add: partition le_diff_conv)
   691  apply (rule ccontr, drule not_leE)
   692  apply (drule_tac less_imp_le [THEN [2] partition_rhs2], auto)
   693 apply (rule ccontr, drule not_leE)
   694 apply (drule_tac x = "psize D" in spec)
   695 apply (simp add: partition)
   696 done
   697 
   698 (* should be combined with previous theorem; also proof has redundancy *)
   699 lemma lemma_psize_right_eq1a:
   700      "partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D"
   701 apply (simp add: psize_def [of "(%x. D (x + n))"]);
   702 apply (rule_tac a = "psize D - n" in someI2, auto)
   703   apply (simp add: partition less_diff_conv)
   704  apply (case_tac "psize D \<le> n")
   705   apply (force intro: partition_rhs2 simp add: le_diff_conv)
   706  apply (simp add: partition le_diff_conv)
   707 apply (rule ccontr, drule not_leE)
   708 apply (drule_tac x = "psize D" in spec)
   709 apply (simp add: partition)
   710 done
   711 
   712 lemma lemma_psize_right_eq:
   713      "[| partition(a,b) D |] ==> psize (%x. D (x + n)) \<le> psize D"
   714 apply (frule_tac r1 = n in partition_ub [THEN real_le_imp_less_or_eq])
   715 apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1)
   716 done
   717 
   718 lemma tpart_left1:
   719      "[| a \<le> D n; tpart (a, b) (D, p) |]
   720       ==> tpart(a, D n) (%x. if D x < D n then D(x) else D n,
   721           %x. if D x < D n then p(x) else D n)"
   722 apply (frule_tac r = n in tpart_partition [THEN partition_ub])
   723 apply (drule_tac x = "D n" in real_le_imp_less_or_eq)
   724 apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric])
   725 apply (frule_tac tpart_partition [THEN [3] lemma_additivity1])
   726 apply (auto simp add: tpart_def)
   727 apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN real_le_imp_less_or_eq], auto)
   728   prefer 3
   729   apply (drule linorder_not_less [THEN iffD1])
   730   apply (drule_tac x=na in spec, arith)
   731  prefer 2 apply (blast dest: lemma_additivity3)
   732 apply (frule lemma_additivity4_psize_eq)
   733 apply (assumption+)
   734 apply (rule partition [THEN iffD2])
   735 apply (frule partition [THEN iffD1])
   736 apply (auto intro: partition_lt_gen)
   737 apply (drule_tac n = n in partition_lt_gen)
   738 apply (assumption, arith, blast)
   739 apply (drule partition_lt_cancel, auto)
   740 done
   741 
   742 lemma fine_left1:
   743      "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g;
   744          fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
   745                  else if x = D n then min (g (D n)) (ga (D n))
   746                       else min (ga x) ((x - D n)/ 2)) (D, p) |]
   747       ==> fine g
   748            (%x. if D x < D n then D(x) else D n,
   749             %x. if D x < D n then p(x) else D n)"
   750 apply (auto simp add: fine_def tpart_def gauge_def)
   751 apply (frule_tac [!] na=na in lemma_psize_left_less_psize2)
   752 apply (drule_tac [!] x = na in spec, auto)
   753 apply (drule_tac [!] x = na in spec, auto)
   754 apply (auto dest: lemma_additivity3a simp add: split_if_asm)
   755 done
   756 
   757 lemma tpart_right1:
   758      "[| a \<le> D n; tpart (a, b) (D, p) |]
   759       ==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))"
   760 apply (simp add: tpart_def partition_def, safe)
   761 apply (rule_tac x = "N - n" in exI, auto)
   762 apply (rotate_tac 2)
   763 apply (drule_tac x = "na + n" in spec)
   764 apply (rotate_tac [2] 3)
   765 apply (drule_tac [2] x = "na + n" in spec, arith+)
   766 done
   767 
   768 lemma fine_right1:
   769      "[| a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga;
   770          fine (%x. if x < D n then min (g x) ((D n - x)/ 2)
   771                  else if x = D n then min (g (D n)) (ga (D n))
   772                       else min (ga x) ((x - D n)/ 2)) (D, p) |]
   773       ==> fine ga (%x. D(x + n),%x. p(x + n))"
   774 apply (auto simp add: fine_def gauge_def)
   775 apply (drule_tac x = "na + n" in spec)
   776 apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto, arith)
   777 apply (simp add: tpart_def, safe)
   778 apply (subgoal_tac "D n \<le> p (na + n) ")
   779 apply (drule_tac y = "p (na + n) " in real_le_imp_less_or_eq)
   780 apply safe
   781 apply (simp split: split_if_asm, simp)
   782 apply (drule less_le_trans, assumption)
   783 apply (rotate_tac 5)
   784 apply (drule_tac x = "na + n" in spec, safe)
   785 apply (rule_tac y="D (na + n)" in order_trans)
   786 apply (case_tac "na = 0", auto)
   787 apply (erule partition_lt_gen [THEN order_less_imp_le], arith+)
   788 done
   789 
   790 lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
   791 by (simp add: rsum_def sumr_add left_distrib)
   792 
   793 (* Bartle/Sherbert: Theorem 10.1.5 p. 278 *)
   794 lemma Integral_add_fun:
   795     "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
   796      ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
   797 apply (simp add: Integral_def, auto)
   798 apply ((drule_tac x = "e/2" in spec)+)
   799 apply auto
   800 apply (drule gauge_min, assumption)
   801 apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x) " in exI)
   802 apply auto
   803 apply (drule fine_min)
   804 apply ((drule spec)+, auto)
   805 apply (drule_tac a = "\<bar>rsum (D, p) f - k1\<bar> * 2" and c = "\<bar>rsum (D, p) g - k2\<bar> * 2" in add_strict_mono, assumption)
   806 apply (auto simp only: rsum_add left_distrib [symmetric]
   807                 mult_2_right [symmetric] real_mult_less_iff1, arith)
   808 done
   809 
   810 lemma partition_lt_gen2:
   811      "[| partition(a,b) D; r < psize D |] ==> 0 < D (Suc r) - D r"
   812 by (auto simp add: partition)
   813 
   814 lemma lemma_Integral_le:
   815      "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
   816          tpart(a,b) (D,p)
   817       |] ==> \<forall>n. n \<le> psize D --> f (p n) \<le> g (p n)"
   818 apply (simp add: tpart_def)
   819 apply (auto, frule partition [THEN iffD1], auto)
   820 apply (drule_tac x = "p n" in spec, auto)
   821 apply (case_tac "n = 0", simp)
   822 apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto)
   823 apply (drule le_imp_less_or_eq, auto)
   824 apply (drule_tac [2] x = "psize D" in spec, auto)
   825 apply (drule_tac r = "Suc n" in partition_ub)
   826 apply (drule_tac x = n in spec, auto)
   827 done
   828 
   829 lemma lemma_Integral_rsum_le:
   830      "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
   831          tpart(a,b) (D,p)
   832       |] ==> rsum(D,p) f \<le> rsum(D,p) g"
   833 apply (simp add: rsum_def)
   834 apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2]
   835                dest!: lemma_Integral_le)
   836 done
   837 
   838 lemma Integral_le:
   839     "[| a \<le> b;
   840         \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x);
   841         Integral(a,b) f k1; Integral(a,b) g k2
   842      |] ==> k1 \<le> k2"
   843 apply (simp add: Integral_def)
   844 apply (rotate_tac 2)
   845 apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
   846 apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
   847 apply auto
   848 apply (drule gauge_min, assumption)
   849 apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x" 
   850        in partition_exists, assumption, auto)
   851 apply (drule fine_min)
   852 apply (drule_tac x = D in spec, drule_tac x = D in spec)
   853 apply (drule_tac x = p in spec, drule_tac x = p in spec, auto)
   854 apply (frule lemma_Integral_rsum_le, assumption)
   855 apply (subgoal_tac "\<bar>(rsum (D,p) f - k1) - (rsum (D,p) g - k2)\<bar> < \<bar>k1 - k2\<bar> ")
   856 apply arith
   857 apply (drule add_strict_mono, assumption)
   858 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   859                        real_mult_less_iff1, arith)
   860 done
   861 
   862 lemma Integral_imp_Cauchy:
   863      "(\<exists>k. Integral(a,b) f k) ==>
   864       (\<forall>e. 0 < e -->
   865                (\<exists>g. gauge (%x. a \<le> x & x \<le> b) g &
   866                        (\<forall>D1 D2 p1 p2.
   867                             tpart(a,b) (D1, p1) & fine g (D1,p1) &
   868                             tpart(a,b) (D2, p2) & fine g (D2,p2) -->
   869                             \<bar>rsum(D1,p1) f - rsum(D2,p2) f\<bar> < e)))"
   870 apply (simp add: Integral_def, auto)
   871 apply (drule_tac x = "e/2" in spec, auto)
   872 apply (rule exI, auto)
   873 apply (frule_tac x = D1 in spec)
   874 apply (frule_tac x = D2 in spec)
   875 apply ((drule spec)+, auto)
   876 apply (erule_tac V = "0 < e" in thin_rl)
   877 apply (drule add_strict_mono, assumption)
   878 apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
   879                        real_mult_less_iff1, arith)
   880 done
   881 
   882 lemma Cauchy_iff2:
   883      "Cauchy X =
   884       (\<forall>j. (\<exists>M. \<forall>m n. M \<le> m & M \<le> n -->
   885                \<bar>X m + - X n\<bar> < inverse(real (Suc j))))"
   886 apply (simp add: Cauchy_def, auto)
   887 apply (drule reals_Archimedean, safe)
   888 apply (drule_tac x = n in spec, auto)
   889 apply (rule_tac x = M in exI, auto)
   890 apply (drule_tac x = m in spec)
   891 apply (drule_tac x = na in spec, auto)
   892 done
   893 
   894 lemma partition_exists2:
   895      "[| a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) |]
   896       ==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)"
   897 apply safe
   898 apply (rule partition_exists, auto)
   899 done
   900 
   901 lemma monotonic_anti_derivative:
   902      "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
   903          \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
   904       ==> f b - f a \<le> g b - g a"
   905 apply (rule Integral_le, assumption)
   906 apply (rule_tac [2] FTC1)
   907 apply (rule_tac [4] FTC1, auto)
   908 done
   909 
   910 end