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