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