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