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