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