src/HOL/Integration.thy
author haftmann
Fri Nov 27 08:41:10 2009 +0100 (2009-11-27)
changeset 33963 977b94b64905
parent 33640 0d82107dc07a
permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
wenzelm@32960
     1
(*  Author:     Jacques D. Fleuriot, University of Edinburgh
paulson@15093
     2
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
paulson@13958
     3
*)
paulson@13958
     4
paulson@15093
     5
header{*Theory of Integration*}
paulson@13958
     6
nipkow@15131
     7
theory Integration
huffman@29469
     8
imports Deriv ATP_Linkup
nipkow@15131
     9
begin
paulson@15093
    10
paulson@15093
    11
text{*We follow John Harrison in formalizing the Gauge integral.*}
paulson@13958
    12
huffman@31259
    13
subsection {* Gauges *}
paulson@15093
    14
wenzelm@21404
    15
definition
huffman@31253
    16
  gauge :: "[real set, real => real] => bool" where
huffman@31253
    17
  [code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))"
paulson@13958
    18
huffman@31259
    19
huffman@31259
    20
subsection {* Gauge-fine divisions *}
huffman@31259
    21
huffman@31259
    22
inductive
huffman@31259
    23
  fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
huffman@31259
    24
for
huffman@31259
    25
  \<delta> :: "real \<Rightarrow> real"
huffman@31259
    26
where
huffman@31259
    27
  fine_Nil:
huffman@31259
    28
    "fine \<delta> (a, a) []"
huffman@31259
    29
| fine_Cons:
huffman@31259
    30
    "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
huffman@31259
    31
      \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
huffman@31259
    32
huffman@31259
    33
lemmas fine_induct [induct set: fine] =
huffman@31259
    34
  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv, standard]
huffman@31259
    35
huffman@31259
    36
lemma fine_single:
huffman@31259
    37
  "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
huffman@31259
    38
by (rule fine_Cons [OF fine_Nil])
huffman@31259
    39
huffman@31259
    40
lemma fine_append:
huffman@31259
    41
  "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
huffman@31259
    42
by (induct set: fine, simp, simp add: fine_Cons)
huffman@31259
    43
huffman@31259
    44
lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
huffman@31259
    45
by (induct set: fine, simp_all)
huffman@31259
    46
huffman@31259
    47
lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
huffman@31259
    48
apply (induct set: fine, simp)
huffman@31259
    49
apply (drule fine_imp_le, simp)
huffman@31259
    50
done
huffman@31259
    51
huffman@31259
    52
lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
huffman@31259
    53
by (induct set: fine, simp_all)
huffman@31259
    54
huffman@31259
    55
lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []"
huffman@31259
    56
apply (cases "D = []")
huffman@31259
    57
apply (drule (1) empty_fine_imp_eq, simp)
huffman@31259
    58
apply (drule (1) nonempty_fine_imp_less, simp)
huffman@31259
    59
done
huffman@31259
    60
huffman@31259
    61
lemma mem_fine:
huffman@31259
    62
  "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
huffman@31259
    63
by (induct set: fine, simp, force)
paulson@13958
    64
huffman@31259
    65
lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
huffman@31259
    66
apply (induct arbitrary: z u v set: fine, auto)
huffman@31259
    67
apply (simp add: fine_imp_le)
huffman@31259
    68
apply (erule order_trans [OF less_imp_le], simp)
huffman@31259
    69
done
huffman@31259
    70
huffman@31259
    71
lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
huffman@31259
    72
by (induct arbitrary: z u v set: fine) auto
huffman@31259
    73
huffman@31259
    74
lemma BOLZANO:
huffman@31259
    75
  fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
huffman@31259
    76
  assumes 1: "a \<le> b"
huffman@31259
    77
  assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
huffman@31259
    78
  assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
huffman@31259
    79
  shows "P a b"
huffman@31259
    80
apply (subgoal_tac "split P (a,b)", simp)
huffman@31259
    81
apply (rule lemma_BOLZANO [OF _ _ 1])
huffman@31259
    82
apply (clarify, erule (3) 2)
huffman@31259
    83
apply (clarify, rule 3)
huffman@31259
    84
done
huffman@31259
    85
huffman@31259
    86
text{*We can always find a division that is fine wrt any gauge*}
huffman@31259
    87
huffman@31259
    88
lemma fine_exists:
huffman@31259
    89
  assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
huffman@31259
    90
proof -
huffman@31259
    91
  {
huffman@31259
    92
    fix u v :: real assume "u \<le> v"
huffman@31259
    93
    have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
huffman@31259
    94
      apply (induct u v rule: BOLZANO, rule `u \<le> v`)
huffman@31259
    95
       apply (simp, fast intro: fine_append)
huffman@31259
    96
      apply (case_tac "a \<le> x \<and> x \<le> b")
huffman@31259
    97
       apply (rule_tac x="\<delta> x" in exI)
huffman@31259
    98
       apply (rule conjI)
huffman@31259
    99
        apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
huffman@31259
   100
       apply (clarify, rename_tac u v)
huffman@31259
   101
       apply (case_tac "u = v")
huffman@31259
   102
        apply (fast intro: fine_Nil)
huffman@31259
   103
       apply (subgoal_tac "u < v", fast intro: fine_single, simp)
huffman@31259
   104
      apply (rule_tac x="1" in exI, clarsimp)
huffman@31259
   105
      done
huffman@31259
   106
  }
huffman@31259
   107
  with `a \<le> b` show ?thesis by auto
huffman@31259
   108
qed
huffman@31259
   109
hoelzl@31364
   110
lemma fine_covers_all:
hoelzl@31364
   111
  assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
hoelzl@31364
   112
  shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
hoelzl@31364
   113
  using assms
hoelzl@31364
   114
proof (induct set: fine)
hoelzl@31364
   115
  case (2 b c D a t)
hoelzl@31364
   116
  thus ?case
hoelzl@31364
   117
  proof (cases "b < x")
hoelzl@31364
   118
    case True
hoelzl@31364
   119
    with 2 obtain N where *: "N < length D"
hoelzl@31364
   120
      and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
hoelzl@31364
   121
    hence "Suc N < length ((a,t,b)#D) \<and>
hoelzl@31364
   122
           (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
hoelzl@31364
   123
    thus ?thesis by auto
hoelzl@31364
   124
  next
hoelzl@31364
   125
    case False with 2
hoelzl@31364
   126
    have "0 < length ((a,t,b)#D) \<and>
hoelzl@31364
   127
           (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
hoelzl@31364
   128
    thus ?thesis by auto
hoelzl@31364
   129
  qed
hoelzl@31364
   130
qed auto
hoelzl@31364
   131
hoelzl@31364
   132
lemma fine_append_split:
hoelzl@31364
   133
  assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
hoelzl@31364
   134
  shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
hoelzl@31364
   135
  and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
hoelzl@31364
   136
proof -
hoelzl@31364
   137
  from assms
hoelzl@31364
   138
  have "?fine1 \<and> ?fine2"
hoelzl@31364
   139
  proof (induct arbitrary: D1 D2)
hoelzl@31364
   140
    case (2 b c D a' x D1 D2)
hoelzl@31364
   141
    note induct = this
hoelzl@31364
   142
hoelzl@31364
   143
    thus ?case
hoelzl@31364
   144
    proof (cases D1)
hoelzl@31364
   145
      case Nil
hoelzl@31364
   146
      hence "fst (hd D2) = a'" using 2 by auto
hoelzl@31364
   147
      with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
hoelzl@31364
   148
      show ?thesis by (auto intro: fine_Nil)
hoelzl@31364
   149
    next
hoelzl@31364
   150
      case (Cons d1 D1')
hoelzl@31364
   151
      with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
hoelzl@31364
   152
      have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
wenzelm@32960
   153
        "d1 = (a', x, b)" by auto
hoelzl@31364
   154
      with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
hoelzl@31364
   155
      show ?thesis by auto
hoelzl@31364
   156
    qed
hoelzl@31364
   157
  qed auto
hoelzl@31364
   158
  thus ?fine1 and ?fine2 by auto
hoelzl@31364
   159
qed
hoelzl@31364
   160
hoelzl@31364
   161
lemma fine_\<delta>_expand:
hoelzl@31364
   162
  assumes "fine \<delta> (a,b) D"
hoelzl@31364
   163
  and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x"
hoelzl@31364
   164
  shows "fine \<delta>' (a,b) D"
hoelzl@31364
   165
using assms proof induct
hoelzl@31364
   166
  case 1 show ?case by (rule fine_Nil)
hoelzl@31364
   167
next
hoelzl@31364
   168
  case (2 b c D a x)
hoelzl@31364
   169
  show ?case
hoelzl@31364
   170
  proof (rule fine_Cons)
hoelzl@31364
   171
    show "fine \<delta>' (b,c) D" using 2 by auto
hoelzl@31364
   172
    from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
hoelzl@31364
   173
    show "b - a < \<delta>' x"
hoelzl@31364
   174
      using 2(7)[OF `a \<le> x`] by auto
hoelzl@31364
   175
  qed (auto simp add: 2)
hoelzl@31364
   176
qed
hoelzl@31364
   177
hoelzl@31364
   178
lemma fine_single_boundaries:
hoelzl@31364
   179
  assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
hoelzl@31364
   180
  shows "a = d \<and> b = e"
hoelzl@31364
   181
using assms proof induct
hoelzl@31364
   182
  case (2 b c  D a x)
hoelzl@31364
   183
  hence "D = []" and "a = d" and "b = e" by auto
hoelzl@31364
   184
  moreover
hoelzl@31364
   185
  from `fine \<delta> (b,c) D` `D = []` have "b = c"
hoelzl@31364
   186
    by (rule empty_fine_imp_eq)
hoelzl@31364
   187
  ultimately show ?case by simp
hoelzl@31364
   188
qed auto
hoelzl@31364
   189
huffman@31259
   190
huffman@31259
   191
subsection {* Riemann sum *}
paulson@13958
   192
wenzelm@21404
   193
definition
huffman@31259
   194
  rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
huffman@31259
   195
  "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
huffman@31259
   196
huffman@31259
   197
lemma rsum_Nil [simp]: "rsum [] f = 0"
huffman@31259
   198
unfolding rsum_def by simp
huffman@31259
   199
huffman@31259
   200
lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
huffman@31259
   201
unfolding rsum_def by simp
huffman@31259
   202
huffman@31259
   203
lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
huffman@31259
   204
by (induct D, auto)
paulson@13958
   205
huffman@31259
   206
lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
huffman@31259
   207
by (induct D, auto simp add: algebra_simps)
huffman@31259
   208
huffman@31259
   209
lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
huffman@31259
   210
by (induct D, auto simp add: algebra_simps)
huffman@31259
   211
huffman@31259
   212
lemma rsum_add: "rsum D (\<lambda>x. f x + g x) =  rsum D f + rsum D g"
huffman@31259
   213
by (induct D, auto simp add: algebra_simps)
huffman@31259
   214
hoelzl@31364
   215
lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
hoelzl@31364
   216
unfolding rsum_def map_append listsum_append ..
hoelzl@31364
   217
huffman@31259
   218
huffman@31259
   219
subsection {* Gauge integrability (definite) *}
paulson@13958
   220
wenzelm@21404
   221
definition
wenzelm@21404
   222
  Integral :: "[(real*real),real=>real,real] => bool" where
haftmann@28562
   223
  [code del]: "Integral = (%(a,b) f k. \<forall>e > 0.
huffman@31259
   224
                               (\<exists>\<delta>. gauge {a .. b} \<delta> &
huffman@31259
   225
                               (\<forall>D. fine \<delta> (a,b) D -->
huffman@31259
   226
                                         \<bar>rsum D f - k\<bar> < e)))"
paulson@15093
   227
huffman@31252
   228
lemma Integral_def2:
huffman@31259
   229
  "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
huffman@31259
   230
                               (\<forall>D. fine \<delta> (a,b) D -->
huffman@31259
   231
                                         \<bar>rsum D f - k\<bar> \<le> e)))"
huffman@31252
   232
unfolding Integral_def
huffman@31252
   233
apply (safe intro!: ext)
huffman@31252
   234
apply (fast intro: less_imp_le)
huffman@31252
   235
apply (drule_tac x="e/2" in spec)
huffman@31252
   236
apply force
huffman@31252
   237
done
huffman@31252
   238
paulson@15093
   239
text{*Lemmas about combining gauges*}
paulson@15093
   240
paulson@15093
   241
lemma gauge_min:
paulson@15093
   242
     "[| gauge(E) g1; gauge(E) g2 |]
huffman@31259
   243
      ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
paulson@15093
   244
by (simp add: gauge_def)
paulson@15093
   245
paulson@15093
   246
lemma fine_min:
huffman@31259
   247
      "fine (%x. min (g1(x)) (g2(x))) (a,b) D
huffman@31259
   248
       ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
huffman@31259
   249
apply (erule fine.induct)
huffman@31259
   250
apply (simp add: fine_Nil)
huffman@31259
   251
apply (simp add: fine_Cons)
huffman@31259
   252
done
paulson@15093
   253
paulson@15093
   254
text{*The integral is unique if it exists*}
paulson@15093
   255
paulson@15093
   256
lemma Integral_unique:
paulson@15093
   257
    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) f k2 |] ==> k1 = k2"
paulson@15093
   258
apply (simp add: Integral_def)
paulson@15093
   259
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)+
paulson@15093
   260
apply auto
paulson@15093
   261
apply (drule gauge_min, assumption)
huffman@31259
   262
apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)"
huffman@31259
   263
       in fine_exists, assumption, auto)
paulson@15093
   264
apply (drule fine_min)
paulson@15093
   265
apply (drule spec)+
paulson@15093
   266
apply auto
huffman@31259
   267
apply (subgoal_tac "\<bar>(rsum D f - k2) - (rsum D f - k1)\<bar> < \<bar>k1 - k2\<bar>")
paulson@15093
   268
apply arith
paulson@15093
   269
apply (drule add_strict_mono, assumption)
paulson@15093
   270
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric] 
huffman@17318
   271
                mult_less_cancel_right)
paulson@15093
   272
done
paulson@15093
   273
paulson@15093
   274
lemma Integral_zero [simp]: "Integral(a,a) f 0"
paulson@15093
   275
apply (auto simp add: Integral_def)
paulson@15093
   276
apply (rule_tac x = "%x. 1" in exI)
huffman@31259
   277
apply (auto dest: fine_eq simp add: gauge_def rsum_def)
paulson@15093
   278
done
paulson@15093
   279
huffman@31259
   280
lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
huffman@31259
   281
unfolding rsum_def
huffman@31259
   282
by (induct set: fine, auto simp add: algebra_simps)
paulson@15093
   283
paulson@15093
   284
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
huffman@31259
   285
apply (cases "a = b", simp)
huffman@31259
   286
apply (simp add: Integral_def, clarify)
paulson@15093
   287
apply (rule_tac x = "%x. b - a" in exI)
huffman@31259
   288
apply (rule conjI, simp add: gauge_def)
huffman@31259
   289
apply (clarify)
huffman@31259
   290
apply (subst fine_rsum_const, assumption, simp)
paulson@15093
   291
done
paulson@15093
   292
paulson@15093
   293
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c)  (c*(b - a))"
huffman@31259
   294
apply (cases "a = b", simp)
huffman@31259
   295
apply (simp add: Integral_def, clarify)
paulson@15093
   296
apply (rule_tac x = "%x. b - a" in exI)
huffman@31259
   297
apply (rule conjI, simp add: gauge_def)
huffman@31259
   298
apply (clarify)
huffman@31259
   299
apply (subst fine_rsum_const, assumption, simp)
paulson@15093
   300
done
paulson@15093
   301
paulson@15093
   302
lemma Integral_mult:
paulson@15093
   303
     "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
paulson@15221
   304
apply (auto simp add: order_le_less 
paulson@15221
   305
            dest: Integral_unique [OF order_refl Integral_zero])
huffman@31257
   306
apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
huffman@31257
   307
apply (case_tac "c = 0", force)
huffman@31257
   308
apply (drule_tac x = "e/abs c" in spec)
huffman@31257
   309
apply (simp add: divide_pos_pos)
huffman@31257
   310
apply clarify
huffman@31259
   311
apply (rule_tac x="\<delta>" in exI, clarify)
huffman@31259
   312
apply (drule_tac x="D" in spec, clarify)
huffman@31257
   313
apply (simp add: pos_less_divide_eq abs_mult [symmetric]
huffman@31257
   314
                 algebra_simps rsum_right_distrib)
paulson@15093
   315
done
paulson@15093
   316
hoelzl@31364
   317
lemma Integral_add:
hoelzl@31364
   318
  assumes "Integral (a, b) f x1"
hoelzl@31364
   319
  assumes "Integral (b, c) f x2"
hoelzl@31364
   320
  assumes "a \<le> b" and "b \<le> c"
hoelzl@31364
   321
  shows "Integral (a, c) f (x1 + x2)"
hoelzl@31364
   322
proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI)
hoelzl@31364
   323
  fix \<epsilon> :: real assume "0 < \<epsilon>"
hoelzl@31364
   324
  hence "0 < \<epsilon> / 2" by auto
hoelzl@31364
   325
hoelzl@31364
   326
  assume "a < b \<and> b < c"
hoelzl@31364
   327
  hence "a < b" and "b < c" by auto
hoelzl@31364
   328
hoelzl@31364
   329
  from `Integral (a, b) f x1`[simplified Integral_def split_conv,
hoelzl@31364
   330
                              rule_format, OF `0 < \<epsilon>/2`]
hoelzl@31364
   331
  obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
hoelzl@31364
   332
    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)" by auto
hoelzl@31364
   333
hoelzl@31364
   334
  from `Integral (b, c) f x2`[simplified Integral_def split_conv,
hoelzl@31364
   335
                              rule_format, OF `0 < \<epsilon>/2`]
hoelzl@31364
   336
  obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
hoelzl@31364
   337
    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)" by auto
hoelzl@31364
   338
hoelzl@31364
   339
  def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
hoelzl@31364
   340
           else if x = b then min (\<delta>1 b) (\<delta>2 b)
hoelzl@31364
   341
                         else min (\<delta>2 x) (x - b)"
hoelzl@31364
   342
hoelzl@31364
   343
  have "gauge {a..c} \<delta>"
hoelzl@31364
   344
    using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
hoelzl@31364
   345
  moreover {
hoelzl@31364
   346
    fix D :: "(real \<times> real \<times> real) list"
hoelzl@31364
   347
    assume fine: "fine \<delta> (a,c) D"
hoelzl@31364
   348
    from fine_covers_all[OF this `a < b` `b \<le> c`]
hoelzl@31364
   349
    obtain N where "N < length D"
hoelzl@31364
   350
      and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
hoelzl@31364
   351
      by auto
hoelzl@31364
   352
    obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
hoelzl@31364
   353
    with * have "d < b" and "b \<le> e" by auto
hoelzl@31364
   354
    have in_D: "(d, t, e) \<in> set D"
hoelzl@31364
   355
      using D_eq[symmetric] using `N < length D` by auto
hoelzl@31364
   356
hoelzl@31364
   357
    from mem_fine[OF fine in_D]
hoelzl@31364
   358
    have "d < e" and "d \<le> t" and "t \<le> e" by auto
hoelzl@31364
   359
hoelzl@31364
   360
    have "t = b"
hoelzl@31364
   361
    proof (rule ccontr)
hoelzl@31364
   362
      assume "t \<noteq> b"
hoelzl@31364
   363
      with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
hoelzl@31364
   364
      show False by (cases "t < b") auto
hoelzl@31364
   365
    qed
hoelzl@31364
   366
hoelzl@31364
   367
    let ?D1 = "take N D"
hoelzl@31364
   368
    let ?D2 = "drop N D"
hoelzl@31364
   369
    def D1 \<equiv> "take N D @ [(d, t, b)]"
hoelzl@31364
   370
    def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
hoelzl@31364
   371
hoelzl@31364
   372
    have "D \<noteq> []" using `N < length D` by auto
hoelzl@31364
   373
    from hd_drop_conv_nth[OF this `N < length D`]
hoelzl@31364
   374
    have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
hoelzl@31364
   375
    with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
hoelzl@31364
   376
    have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
hoelzl@31364
   377
      using `N < length D` fine by auto
hoelzl@31364
   378
hoelzl@31364
   379
    have "fine \<delta>1 (a,b) D1" unfolding D1_def
hoelzl@31364
   380
    proof (rule fine_append)
hoelzl@31364
   381
      show "fine \<delta>1 (a, d) ?D1"
hoelzl@31364
   382
      proof (rule fine1[THEN fine_\<delta>_expand])
wenzelm@32960
   383
        fix x assume "a \<le> x" "x \<le> d"
wenzelm@32960
   384
        hence "x \<le> b" using `d < b` `x \<le> d` by auto
wenzelm@32960
   385
        thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
hoelzl@31364
   386
      qed
hoelzl@31364
   387
hoelzl@31364
   388
      have "b - d < \<delta>1 t"
wenzelm@32960
   389
        using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
hoelzl@31364
   390
      from `d < b` `d \<le> t` `t = b` this
hoelzl@31364
   391
      show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
hoelzl@31364
   392
    qed
hoelzl@31364
   393
    note rsum1 = I1[OF this]
hoelzl@31364
   394
hoelzl@31364
   395
    have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
hoelzl@31364
   396
      using nth_drop'[OF `N < length D`] by simp
hoelzl@31364
   397
hoelzl@31364
   398
    have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
hoelzl@31364
   399
    proof (cases "drop (Suc N) D = []")
hoelzl@31364
   400
      case True
hoelzl@31364
   401
      note * = fine2[simplified drop_split True D_eq append_Nil2]
hoelzl@31364
   402
      have "e = c" using fine_single_boundaries[OF * refl] by auto
hoelzl@31364
   403
      thus ?thesis unfolding True using fine_Nil by auto
hoelzl@31364
   404
    next
hoelzl@31364
   405
      case False
hoelzl@31364
   406
      note * = fine_append_split[OF fine2 False drop_split]
hoelzl@31364
   407
      from fine_single_boundaries[OF *(1)]
hoelzl@31364
   408
      have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
hoelzl@31364
   409
      with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
hoelzl@31364
   410
      thus ?thesis
hoelzl@31364
   411
      proof (rule fine_\<delta>_expand)
wenzelm@32960
   412
        fix x assume "e \<le> x" and "x \<le> c"
wenzelm@32960
   413
        thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
hoelzl@31364
   414
      qed
hoelzl@31364
   415
    qed
hoelzl@31364
   416
hoelzl@31364
   417
    have "fine \<delta>2 (b, c) D2"
hoelzl@31364
   418
    proof (cases "e = b")
hoelzl@31364
   419
      case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
hoelzl@31364
   420
    next
hoelzl@31364
   421
      case False
hoelzl@31364
   422
      have "e - b < \<delta>2 b"
wenzelm@32960
   423
        using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
hoelzl@31364
   424
      with False `t = b` `b \<le> e`
hoelzl@31364
   425
      show ?thesis using D2_def
wenzelm@32960
   426
        by (auto intro!: fine_append[OF _ fine2] fine_single
wenzelm@32960
   427
               simp del: append_Cons)
hoelzl@31364
   428
    qed
hoelzl@31364
   429
    note rsum2 = I2[OF this]
hoelzl@31364
   430
hoelzl@31364
   431
    have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
hoelzl@31364
   432
      using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
hoelzl@31364
   433
    also have "\<dots> = rsum D1 f + rsum D2 f"
hoelzl@31366
   434
      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
hoelzl@31364
   435
    finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
hoelzl@31364
   436
      using add_strict_mono[OF rsum1 rsum2] by simp
hoelzl@31364
   437
  }
hoelzl@31364
   438
  ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
hoelzl@31364
   439
    (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
hoelzl@31364
   440
    by blast
hoelzl@31364
   441
next
hoelzl@31364
   442
  case False
hoelzl@31364
   443
  hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
hoelzl@31364
   444
  thus ?thesis
hoelzl@31364
   445
  proof (rule disjE)
hoelzl@31364
   446
    assume "a = b" hence "x1 = 0"
hoelzl@31364
   447
      using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto
hoelzl@31364
   448
    thus ?thesis using `a = b` `Integral (b, c) f x2` by auto
hoelzl@31364
   449
  next
hoelzl@31364
   450
    assume "b = c" hence "x2 = 0"
hoelzl@31364
   451
      using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto
hoelzl@31364
   452
    thus ?thesis using `b = c` `Integral (a, b) f x1` by auto
hoelzl@31364
   453
  qed
hoelzl@31364
   454
qed
huffman@31259
   455
paulson@15093
   456
text{*Fundamental theorem of calculus (Part I)*}
paulson@15093
   457
nipkow@15105
   458
text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
paulson@15093
   459
paulson@15093
   460
lemma strad1:
huffman@31252
   461
       "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
huffman@31252
   462
             \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
huffman@31252
   463
        0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
huffman@31252
   464
       \<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>"
huffman@31252
   465
apply clarify
huffman@31253
   466
apply (case_tac "z = x", simp)
paulson@15093
   467
apply (drule_tac x = z in spec)
paulson@15093
   468
apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
paulson@15093
   469
       in real_mult_le_cancel_iff2 [THEN iffD1])
paulson@15093
   470
 apply simp
paulson@15093
   471
apply (simp del: abs_inverse abs_mult add: abs_mult [symmetric]
paulson@15093
   472
          mult_assoc [symmetric])
paulson@15093
   473
apply (subgoal_tac "inverse (z - x) * (f z - f x - f' x * (z - x)) 
paulson@15093
   474
                    = (f z - f x) / (z - x) - f' x")
paulson@15093
   475
 apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
paulson@15093
   476
apply (subst mult_commute)
paulson@15093
   477
apply (simp add: left_distrib diff_minus)
paulson@15093
   478
apply (simp add: mult_assoc divide_inverse)
paulson@15093
   479
apply (simp add: left_distrib)
paulson@15093
   480
done
paulson@15093
   481
paulson@15093
   482
lemma lemma_straddle:
huffman@31252
   483
  assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
huffman@31253
   484
  shows "\<exists>g. gauge {a..b} g &
paulson@15093
   485
                (\<forall>x u v. a \<le> u & u \<le> x & x \<le> v & v \<le> b & (v - u) < g(x)
paulson@15094
   486
                  --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
huffman@31252
   487
proof -
huffman@31253
   488
  have "\<forall>x\<in>{a..b}.
nipkow@15360
   489
        (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
huffman@31252
   490
                       \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
huffman@31253
   491
  proof (clarsimp)
huffman@31252
   492
    fix x :: real assume "a \<le> x" and "x \<le> b"
huffman@31252
   493
    with f' have "DERIV f x :> f'(x)" by simp
huffman@31252
   494
    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"
huffman@31338
   495
      by (simp add: DERIV_iff2 LIM_eq)
huffman@31252
   496
    with `0 < e` obtain s
huffman@31252
   497
    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"
huffman@31252
   498
      by (drule_tac x="e/2" in spec, auto)
huffman@31252
   499
    then have strad [rule_format]:
huffman@31252
   500
        "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
huffman@31252
   501
      using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
huffman@31252
   502
    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)"
huffman@31252
   503
    proof (safe intro!: exI)
huffman@31252
   504
      show "0 < s" by fact
huffman@31252
   505
    next
huffman@31252
   506
      fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
huffman@31252
   507
      have "\<bar>f v - f u - f' x * (v - u)\<bar> =
huffman@31252
   508
            \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
huffman@31252
   509
        by (simp add: right_diff_distrib)
huffman@31252
   510
      also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
huffman@31252
   511
        by (rule abs_triangle_ineq)
huffman@31252
   512
      also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
huffman@31252
   513
        by (simp add: right_diff_distrib)
huffman@31252
   514
      also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
huffman@31252
   515
        using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
huffman@31252
   516
      also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
huffman@31252
   517
        using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
huffman@31252
   518
      also have "\<dots> = e * (v - u)"
huffman@31252
   519
        by simp
huffman@31252
   520
      finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
huffman@31252
   521
    qed
huffman@31252
   522
  qed
huffman@31252
   523
  thus ?thesis
huffman@31253
   524
    by (simp add: gauge_def) (drule bchoice, auto)
huffman@31252
   525
qed
paulson@15093
   526
huffman@31259
   527
lemma fine_listsum_eq_diff:
huffman@31259
   528
  fixes f :: "real \<Rightarrow> real"
huffman@31259
   529
  shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
huffman@31259
   530
by (induct set: fine) simp_all
huffman@31259
   531
paulson@15093
   532
lemma FTC1: "[|a \<le> b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
paulson@15219
   533
             ==> Integral(a,b) f' (f(b) - f(a))"
huffman@31252
   534
 apply (drule order_le_imp_less_or_eq, auto)
huffman@31252
   535
 apply (auto simp add: Integral_def2)
huffman@31252
   536
 apply (drule_tac e = "e / (b - a)" in lemma_straddle)
huffman@31252
   537
  apply (simp add: divide_pos_pos)
huffman@31252
   538
 apply clarify
huffman@31252
   539
 apply (rule_tac x="g" in exI, clarify)
huffman@31259
   540
 apply (clarsimp simp add: rsum_def)
huffman@31259
   541
 apply (frule fine_listsum_eq_diff [where f=f])
huffman@31252
   542
 apply (erule subst)
huffman@31259
   543
 apply (subst listsum_subtractf [symmetric])
huffman@31259
   544
 apply (rule listsum_abs [THEN order_trans])
hoelzl@33640
   545
 apply (subst map_map [unfolded o_def])
huffman@31259
   546
 apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))")
huffman@31252
   547
  apply (erule ssubst)
huffman@31252
   548
  apply (simp add: abs_minus_commute)
huffman@31259
   549
  apply (rule listsum_mono)
huffman@31259
   550
  apply (clarify, rename_tac u x v)
huffman@31259
   551
  apply ((drule spec)+, erule mp)
huffman@31259
   552
  apply (simp add: mem_fine mem_fine2 mem_fine3)
huffman@31259
   553
 apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"])
huffman@31259
   554
 apply (simp only: split_def)
huffman@31259
   555
 apply (subst listsum_const_mult)
huffman@31259
   556
 apply simp
paulson@15093
   557
done
paulson@13958
   558
paulson@15093
   559
lemma Integral_subst: "[| Integral(a,b) f k1; k2=k1 |] ==> Integral(a,b) f k2"
paulson@15093
   560
by simp
paulson@15093
   561
huffman@31259
   562
subsection {* Additivity Theorem of Gauge Integral *}
paulson@15093
   563
paulson@15094
   564
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
paulson@15093
   565
lemma Integral_add_fun:
paulson@15093
   566
    "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]
paulson@15093
   567
     ==> Integral(a,b) (%x. f x + g x) (k1 + k2)"
huffman@31259
   568
unfolding Integral_def
huffman@31259
   569
apply clarify
huffman@31259
   570
apply (drule_tac x = "e/2" in spec)+
huffman@31259
   571
apply clarsimp
huffman@31259
   572
apply (rule_tac x = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in exI)
huffman@31259
   573
apply (rule conjI, erule (1) gauge_min)
huffman@31259
   574
apply clarify
paulson@15093
   575
apply (drule fine_min)
huffman@31259
   576
apply (drule_tac x=D in spec, simp)+
huffman@31259
   577
apply (drule_tac a = "\<bar>rsum D f - k1\<bar> * 2" and c = "\<bar>rsum D g - k2\<bar> * 2" in add_strict_mono, assumption)
paulson@15093
   578
apply (auto simp only: rsum_add left_distrib [symmetric]
webertj@20217
   579
                mult_2_right [symmetric] real_mult_less_iff1)
paulson@15093
   580
done
paulson@15093
   581
paulson@15093
   582
lemma lemma_Integral_rsum_le:
paulson@15093
   583
     "[| \<forall>x. a \<le> x & x \<le> b --> f x \<le> g x;
huffman@31259
   584
         fine \<delta> (a,b) D
huffman@31259
   585
      |] ==> rsum D f \<le> rsum D g"
huffman@31259
   586
unfolding rsum_def
huffman@31259
   587
apply (rule listsum_mono)
huffman@31259
   588
apply clarify
huffman@31259
   589
apply (rule mult_right_mono)
huffman@31259
   590
apply (drule spec, erule mp)
huffman@31259
   591
apply (frule (1) mem_fine)
huffman@31259
   592
apply (frule (1) mem_fine2)
huffman@31259
   593
apply simp
huffman@31259
   594
apply (frule (1) mem_fine)
huffman@31259
   595
apply simp
paulson@15093
   596
done
paulson@15093
   597
paulson@15093
   598
lemma Integral_le:
paulson@15093
   599
    "[| a \<le> b;
paulson@15093
   600
        \<forall>x. a \<le> x & x \<le> b --> f(x) \<le> g(x);
paulson@15093
   601
        Integral(a,b) f k1; Integral(a,b) g k2
paulson@15093
   602
     |] ==> k1 \<le> k2"
paulson@15093
   603
apply (simp add: Integral_def)
paulson@15093
   604
apply (rotate_tac 2)
paulson@15093
   605
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec)
paulson@15221
   606
apply (drule_tac x = "\<bar>k1 - k2\<bar> /2" in spec, auto)
paulson@15093
   607
apply (drule gauge_min, assumption)
huffman@31259
   608
apply (drule_tac \<delta> = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in fine_exists, assumption, clarify)
paulson@15093
   609
apply (drule fine_min)
huffman@31259
   610
apply (drule_tac x = D in spec, drule_tac x = D in spec, clarsimp)
paulson@15093
   611
apply (frule lemma_Integral_rsum_le, assumption)
huffman@31259
   612
apply (subgoal_tac "\<bar>(rsum D f - k1) - (rsum D g - k2)\<bar> < \<bar>k1 - k2\<bar>")
paulson@15093
   613
apply arith
paulson@15093
   614
apply (drule add_strict_mono, assumption)
paulson@15093
   615
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
webertj@20217
   616
                       real_mult_less_iff1)
paulson@15093
   617
done
paulson@15093
   618
paulson@15093
   619
lemma Integral_imp_Cauchy:
paulson@15093
   620
     "(\<exists>k. Integral(a,b) f k) ==>
huffman@31259
   621
      (\<forall>e > 0. \<exists>\<delta>. gauge {a..b} \<delta> &
huffman@31259
   622
                       (\<forall>D1 D2.
huffman@31259
   623
                            fine \<delta> (a,b) D1 &
huffman@31259
   624
                            fine \<delta> (a,b) D2 -->
huffman@31259
   625
                            \<bar>rsum D1 f - rsum D2 f\<bar> < e))"
paulson@15093
   626
apply (simp add: Integral_def, auto)
paulson@15093
   627
apply (drule_tac x = "e/2" in spec, auto)
paulson@15093
   628
apply (rule exI, auto)
paulson@15093
   629
apply (frule_tac x = D1 in spec)
huffman@31259
   630
apply (drule_tac x = D2 in spec)
huffman@31259
   631
apply simp
huffman@31259
   632
apply (thin_tac "0 < e")
paulson@15093
   633
apply (drule add_strict_mono, assumption)
paulson@15093
   634
apply (auto simp only: left_distrib [symmetric] mult_2_right [symmetric]
webertj@20217
   635
                       real_mult_less_iff1)
paulson@15093
   636
done
paulson@15093
   637
paulson@15093
   638
lemma Cauchy_iff2:
paulson@15093
   639
     "Cauchy X =
huffman@20563
   640
      (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse(real (Suc j))))"
huffman@31336
   641
apply (simp add: Cauchy_iff, auto)
paulson@15093
   642
apply (drule reals_Archimedean, safe)
paulson@15093
   643
apply (drule_tac x = n in spec, auto)
paulson@15093
   644
apply (rule_tac x = M in exI, auto)
nipkow@15360
   645
apply (drule_tac x = m in spec, simp)
paulson@15093
   646
apply (drule_tac x = na in spec, auto)
paulson@15093
   647
done
paulson@15093
   648
paulson@15093
   649
lemma monotonic_anti_derivative:
huffman@20792
   650
  fixes f g :: "real => real" shows
paulson@15093
   651
     "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
paulson@15093
   652
         \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
paulson@15093
   653
      ==> f b - f a \<le> g b - g a"
paulson@15093
   654
apply (rule Integral_le, assumption)
paulson@15219
   655
apply (auto intro: FTC1) 
paulson@15093
   656
done
paulson@15093
   657
paulson@15093
   658
end