src/HOL/ex/Gauge_Integration.thy
author wenzelm
Sun, 20 Nov 2011 21:05:23 +0100
changeset 45605 a89b4bc311a5
parent 37765 26bdfb7b680b
child 46501 fe51817749d1
permissions -rw-r--r--
eliminated obsolete "standard";
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
     1
(*  Author:     Jacques D. Fleuriot, University of Edinburgh
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
     2
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
35328
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
     3
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
     4
    Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy .
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
35328
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
     7
header{*Theory of Integration on real intervals*}
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
     8
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
     9
theory Gauge_Integration
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    10
imports Complex_Main
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    11
begin
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    12
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    13
text {*
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    14
35328
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    15
\textbf{Attention}: This theory defines the Integration on real
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    16
intervals.  This is just a example theory for historical / expository interests.
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    17
A better replacement is found in the Multivariate Analysis library. This defines
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    18
the gauge integral on real vector spaces and in the Real Integral theory
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    19
is a specialization to the integral on arbitrary real intervals.  The
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    20
Multivariate Analysis package also provides a better support for analysis on
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    21
integrals.
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    22
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
    23
*}
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
    24
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
    25
text{*We follow John Harrison in formalizing the Gauge integral.*}
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    26
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    27
subsection {* Gauges *}
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
    28
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20792
diff changeset
    29
definition
31253
d54dc8956d48 use interval sets with gauge predicate
huffman
parents: 31252
diff changeset
    30
  gauge :: "[real set, real => real] => bool" where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 35441
diff changeset
    31
  "gauge E g = (\<forall>x\<in>E. 0 < g(x))"
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    32
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    33
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    34
subsection {* Gauge-fine divisions *}
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    35
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    36
inductive
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    37
  fine :: "[real \<Rightarrow> real, real \<times> real, (real \<times> real \<times> real) list] \<Rightarrow> bool"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    38
for
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    39
  \<delta> :: "real \<Rightarrow> real"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    40
where
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    41
  fine_Nil:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    42
    "fine \<delta> (a, a) []"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    43
| fine_Cons:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    44
    "\<lbrakk>fine \<delta> (b, c) D; a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk>
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    45
      \<Longrightarrow> fine \<delta> (a, c) ((a, x, b) # D)"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    46
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    47
lemmas fine_induct [induct set: fine] =
45605
a89b4bc311a5 eliminated obsolete "standard";
wenzelm
parents: 37765
diff changeset
    48
  fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    49
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    50
lemma fine_single:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    51
  "\<lbrakk>a < b; a \<le> x; x \<le> b; b - a < \<delta> x\<rbrakk> \<Longrightarrow> fine \<delta> (a, b) [(a, x, b)]"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    52
by (rule fine_Cons [OF fine_Nil])
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    53
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    54
lemma fine_append:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    55
  "\<lbrakk>fine \<delta> (a, b) D; fine \<delta> (b, c) D'\<rbrakk> \<Longrightarrow> fine \<delta> (a, c) (D @ D')"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    56
by (induct set: fine, simp, simp add: fine_Cons)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    57
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    58
lemma fine_imp_le: "fine \<delta> (a, b) D \<Longrightarrow> a \<le> b"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    59
by (induct set: fine, simp_all)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    60
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    61
lemma nonempty_fine_imp_less: "\<lbrakk>fine \<delta> (a, b) D; D \<noteq> []\<rbrakk> \<Longrightarrow> a < b"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    62
apply (induct set: fine, simp)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    63
apply (drule fine_imp_le, simp)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    64
done
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    65
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    66
lemma fine_Nil_iff: "fine \<delta> (a, b) [] \<longleftrightarrow> a = b"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    67
by (auto elim: fine.cases intro: fine.intros)
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    68
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    69
lemma fine_same_iff: "fine \<delta> (a, a) D \<longleftrightarrow> D = []"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    70
proof
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    71
  assume "fine \<delta> (a, a) D" thus "D = []"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    72
    by (metis nonempty_fine_imp_less less_irrefl)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    73
next
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    74
  assume "D = []" thus "fine \<delta> (a, a) D"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    75
    by (simp add: fine_Nil)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    76
qed
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    77
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    78
lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
    79
by (simp add: fine_Nil_iff)
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    80
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    81
lemma mem_fine:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    82
  "\<lbrakk>fine \<delta> (a, b) D; (u, x, v) \<in> set D\<rbrakk> \<Longrightarrow> u < v \<and> u \<le> x \<and> x \<le> v"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    83
by (induct set: fine, simp, force)
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
    84
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    85
lemma mem_fine2: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> a \<le> u \<and> v \<le> b"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    86
apply (induct arbitrary: z u v set: fine, auto)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    87
apply (simp add: fine_imp_le)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    88
apply (erule order_trans [OF less_imp_le], simp)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    89
done
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    90
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    91
lemma mem_fine3: "\<lbrakk>fine \<delta> (a, b) D; (u, z, v) \<in> set D\<rbrakk> \<Longrightarrow> v - u < \<delta> z"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    92
by (induct arbitrary: z u v set: fine) auto
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    93
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    94
lemma BOLZANO:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    95
  fixes P :: "real \<Rightarrow> real \<Rightarrow> bool"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    96
  assumes 1: "a \<le> b"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    97
  assumes 2: "\<And>a b c. \<lbrakk>P a b; P b c; a \<le> b; b \<le> c\<rbrakk> \<Longrightarrow> P a c"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    98
  assumes 3: "\<And>x. \<exists>d>0. \<forall>a b. a \<le> x & x \<le> b & (b-a) < d \<longrightarrow> P a b"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
    99
  shows "P a b"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   100
apply (subgoal_tac "split P (a,b)", simp)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   101
apply (rule lemma_BOLZANO [OF _ _ 1])
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   102
apply (clarify, erule (3) 2)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   103
apply (clarify, rule 3)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   104
done
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   105
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   106
text{*We can always find a division that is fine wrt any gauge*}
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   107
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   108
lemma fine_exists:
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   109
  assumes "a \<le> b" and "gauge {a..b} \<delta>" shows "\<exists>D. fine \<delta> (a, b) D"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   110
proof -
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   111
  {
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   112
    fix u v :: real assume "u \<le> v"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   113
    have "a \<le> u \<Longrightarrow> v \<le> b \<Longrightarrow> \<exists>D. fine \<delta> (u, v) D"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   114
      apply (induct u v rule: BOLZANO, rule `u \<le> v`)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   115
       apply (simp, fast intro: fine_append)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   116
      apply (case_tac "a \<le> x \<and> x \<le> b")
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   117
       apply (rule_tac x="\<delta> x" in exI)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   118
       apply (rule conjI)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   119
        apply (simp add: `gauge {a..b} \<delta>` [unfolded gauge_def])
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   120
       apply (clarify, rename_tac u v)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   121
       apply (case_tac "u = v")
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   122
        apply (fast intro: fine_Nil)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   123
       apply (subgoal_tac "u < v", fast intro: fine_single, simp)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   124
      apply (rule_tac x="1" in exI, clarsimp)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   125
      done
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   126
  }
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   127
  with `a \<le> b` show ?thesis by auto
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   128
qed
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   129
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   130
lemma fine_covers_all:
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   131
  assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   132
  shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   133
  using assms
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   134
proof (induct set: fine)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   135
  case (2 b c D a t)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   136
  thus ?case
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   137
  proof (cases "b < x")
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   138
    case True
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   139
    with 2 obtain N where *: "N < length D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   140
      and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   141
    hence "Suc N < length ((a,t,b)#D) \<and>
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   142
           (\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   143
    thus ?thesis by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   144
  next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   145
    case False with 2
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   146
    have "0 < length ((a,t,b)#D) \<and>
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   147
           (\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   148
    thus ?thesis by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   149
  qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   150
qed auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   151
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   152
lemma fine_append_split:
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   153
  assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   154
  shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1")
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   155
  and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2")
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   156
proof -
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   157
  from assms
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   158
  have "?fine1 \<and> ?fine2"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   159
  proof (induct arbitrary: D1 D2)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   160
    case (2 b c D a' x D1 D2)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   161
    note induct = this
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   162
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   163
    thus ?case
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   164
    proof (cases D1)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   165
      case Nil
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   166
      hence "fst (hd D2) = a'" using 2 by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   167
      with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   168
      show ?thesis by (auto intro: fine_Nil)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   169
    next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   170
      case (Cons d1 D1')
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   171
      with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   172
      have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   173
        "d1 = (a', x, b)" by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   174
      with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   175
      show ?thesis by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   176
    qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   177
  qed auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   178
  thus ?fine1 and ?fine2 by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   179
qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   180
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   181
lemma fine_\<delta>_expand:
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   182
  assumes "fine \<delta> (a,b) D"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   183
  and "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<delta> x \<le> \<delta>' x"
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   184
  shows "fine \<delta>' (a,b) D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   185
using assms proof induct
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   186
  case 1 show ?case by (rule fine_Nil)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   187
next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   188
  case (2 b c D a x)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   189
  show ?case
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   190
  proof (rule fine_Cons)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   191
    show "fine \<delta>' (b,c) D" using 2 by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   192
    from fine_imp_le[OF 2(1)] 2(6) `x \<le> b`
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   193
    show "b - a < \<delta>' x"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   194
      using 2(7)[OF `a \<le> x`] by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   195
  qed (auto simp add: 2)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   196
qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   197
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   198
lemma fine_single_boundaries:
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   199
  assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   200
  shows "a = d \<and> b = e"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   201
using assms proof induct
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   202
  case (2 b c  D a x)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   203
  hence "D = []" and "a = d" and "b = e" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   204
  moreover
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   205
  from `fine \<delta> (b,c) D` `D = []` have "b = c"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   206
    by (rule empty_fine_imp_eq)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   207
  ultimately show ?case by simp
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   208
qed auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   209
35328
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   210
lemma fine_listsum_eq_diff:
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   211
  fixes f :: "real \<Rightarrow> real"
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   212
  shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   213
by (induct set: fine) simp_all
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   214
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   215
text{*Lemmas about combining gauges*}
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   216
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   217
lemma gauge_min:
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   218
     "[| gauge(E) g1; gauge(E) g2 |]
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   219
      ==> gauge(E) (%x. min (g1(x)) (g2(x)))"
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   220
by (simp add: gauge_def)
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   221
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   222
lemma fine_min:
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   223
      "fine (%x. min (g1(x)) (g2(x))) (a,b) D
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   224
       ==> fine(g1) (a,b) D & fine(g2) (a,b) D"
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   225
apply (erule fine.induct)
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   226
apply (simp add: fine_Nil)
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   227
apply (simp add: fine_Cons)
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   228
done
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   229
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   230
subsection {* Riemann sum *}
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
   231
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20792
diff changeset
   232
definition
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   233
  rsum :: "[(real \<times> real \<times> real) list, real \<Rightarrow> real] \<Rightarrow> real" where
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   234
  "rsum D f = (\<Sum>(u, x, v)\<leftarrow>D. f x * (v - u))"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   235
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   236
lemma rsum_Nil [simp]: "rsum [] f = 0"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   237
unfolding rsum_def by simp
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   238
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   239
lemma rsum_Cons [simp]: "rsum ((u, x, v) # D) f = f x * (v - u) + rsum D f"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   240
unfolding rsum_def by simp
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   241
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   242
lemma rsum_zero [simp]: "rsum D (\<lambda>x. 0) = 0"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   243
by (induct D, auto)
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
   244
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   245
lemma rsum_left_distrib: "rsum D f * c = rsum D (\<lambda>x. f x * c)"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   246
by (induct D, auto simp add: algebra_simps)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   247
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   248
lemma rsum_right_distrib: "c * rsum D f = rsum D (\<lambda>x. c * f x)"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   249
by (induct D, auto simp add: algebra_simps)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   250
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   251
lemma rsum_add: "rsum D (\<lambda>x. f x + g x) =  rsum D f + rsum D g"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   252
by (induct D, auto simp add: algebra_simps)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   253
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   254
lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   255
unfolding rsum_def map_append listsum_append ..
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   256
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   257
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   258
subsection {* Gauge integrability (definite) *}
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
   259
21404
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20792
diff changeset
   260
definition
eb85850d3eb7 more robust syntax for definition/abbreviation/notation;
wenzelm
parents: 20792
diff changeset
   261
  Integral :: "[(real*real),real=>real,real] => bool" where
37765
26bdfb7b680b dropped superfluous [code del]s
haftmann
parents: 35441
diff changeset
   262
  "Integral = (%(a,b) f k. \<forall>e > 0.
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   263
                               (\<exists>\<delta>. gauge {a .. b} \<delta> &
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   264
                               (\<forall>D. fine \<delta> (a,b) D -->
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   265
                                         \<bar>rsum D f - k\<bar> < e)))"
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   266
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   267
lemma Integral_eq:
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   268
  "Integral (a, b) f k \<longleftrightarrow>
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   269
    (\<forall>e>0. \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a,b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e))"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   270
unfolding Integral_def by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   271
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   272
lemma IntegralI:
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   273
  assumes "\<And>e. 0 < e \<Longrightarrow>
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   274
    \<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   275
  shows "Integral (a, b) f k"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   276
using assms unfolding Integral_def by auto
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   277
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   278
lemma IntegralE:
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   279
  assumes "Integral (a, b) f k" and "0 < e"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   280
  obtains \<delta> where "gauge {a..b} \<delta>" and "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f - k\<bar> < e"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   281
using assms unfolding Integral_def by auto
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   282
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   283
lemma Integral_def2:
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   284
  "Integral = (%(a,b) f k. \<forall>e>0. (\<exists>\<delta>. gauge {a..b} \<delta> &
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   285
                               (\<forall>D. fine \<delta> (a,b) D -->
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   286
                                         \<bar>rsum D f - k\<bar> \<le> e)))"
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   287
unfolding Integral_def
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   288
apply (safe intro!: ext)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   289
apply (fast intro: less_imp_le)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   290
apply (drule_tac x="e/2" in spec)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   291
apply force
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   292
done
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   293
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   294
text{*The integral is unique if it exists*}
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
lemma Integral_unique:
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   297
  assumes le: "a \<le> b"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   298
  assumes 1: "Integral (a, b) f k1"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   299
  assumes 2: "Integral (a, b) f k2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   300
  shows "k1 = k2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   301
proof (rule ccontr)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   302
  assume "k1 \<noteq> k2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   303
  hence e: "0 < \<bar>k1 - k2\<bar> / 2" by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   304
  obtain d1 where "gauge {a..b} d1" and
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   305
    d1: "\<forall>D. fine d1 (a, b) D \<longrightarrow> \<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   306
    using 1 e by (rule IntegralE)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   307
  obtain d2 where "gauge {a..b} d2" and
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   308
    d2: "\<forall>D. fine d2 (a, b) D \<longrightarrow> \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   309
    using 2 e by (rule IntegralE)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   310
  have "gauge {a..b} (\<lambda>x. min (d1 x) (d2 x))"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   311
    using `gauge {a..b} d1` and `gauge {a..b} d2`
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   312
    by (rule gauge_min)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   313
  then obtain D where "fine (\<lambda>x. min (d1 x) (d2 x)) (a, b) D"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   314
    using fine_exists [OF le] by fast
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   315
  hence "fine d1 (a, b) D" and "fine d2 (a, b) D"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   316
    by (auto dest: fine_min)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   317
  hence "\<bar>rsum D f - k1\<bar> < \<bar>k1 - k2\<bar> / 2" and "\<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   318
    using d1 d2 by simp_all
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   319
  hence "\<bar>rsum D f - k1\<bar> + \<bar>rsum D f - k2\<bar> < \<bar>k1 - k2\<bar> / 2 + \<bar>k1 - k2\<bar> / 2"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   320
    by (rule add_strict_mono)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   321
  thus False by auto
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   322
qed
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   323
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   324
lemma Integral_zero: "Integral(a,a) f 0"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   325
apply (rule IntegralI)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   326
apply (rule_tac x = "\<lambda>x. 1" in exI)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   327
apply (simp add: fine_same_iff gauge_def)
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   328
done
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   329
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   330
lemma Integral_same_iff [simp]: "Integral (a, a) f k \<longleftrightarrow> k = 0"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   331
  by (auto intro: Integral_zero Integral_unique)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   332
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   333
lemma Integral_zero_fun: "Integral (a,b) (\<lambda>x. 0) 0"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   334
apply (rule IntegralI)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   335
apply (rule_tac x="\<lambda>x. 1" in exI, simp add: gauge_def)
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   336
done
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   337
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   338
lemma fine_rsum_const: "fine \<delta> (a,b) D \<Longrightarrow> rsum D (\<lambda>x. c) = (c * (b - a))"
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   339
unfolding rsum_def
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   340
by (induct set: fine, auto simp add: algebra_simps)
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   341
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   342
lemma Integral_mult_const: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. c) (c * (b - a))"
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   343
apply (cases "a = b", simp)
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   344
apply (rule IntegralI)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   345
apply (rule_tac x = "\<lambda>x. b - a" in exI)
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   346
apply (rule conjI, simp add: gauge_def)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   347
apply (clarify)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   348
apply (subst fine_rsum_const, assumption, simp)
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   349
done
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   350
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   351
lemma Integral_eq_diff_bounds: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. 1) (b - a)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   352
  using Integral_mult_const [of a b 1] by simp
15093
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)"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   356
apply (auto simp add: order_le_less)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   357
apply (cases "c = 0", simp add: Integral_zero_fun)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   358
apply (rule IntegralI)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   359
apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos)
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   360
apply (rule_tac x="\<delta>" in exI, clarify)
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   361
apply (drule_tac x="D" in spec, clarify)
31257
547bf9819d6c clean up some rsum proofs
huffman
parents: 31253
diff changeset
   362
apply (simp add: pos_less_divide_eq abs_mult [symmetric]
547bf9819d6c clean up some rsum proofs
huffman
parents: 31253
diff changeset
   363
                 algebra_simps rsum_right_distrib)
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   364
done
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   365
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   366
lemma Integral_add:
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   367
  assumes "Integral (a, b) f x1"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   368
  assumes "Integral (b, c) f x2"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   369
  assumes "a \<le> b" and "b \<le> c"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   370
  shows "Integral (a, c) f (x1 + x2)"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   371
proof (cases "a < b \<and> b < c", rule IntegralI)
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   372
  fix \<epsilon> :: real assume "0 < \<epsilon>"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   373
  hence "0 < \<epsilon> / 2" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   374
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   375
  assume "a < b \<and> b < c"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   376
  hence "a < b" and "b < c" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   377
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   378
  obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   379
    and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f - x1 \<bar> < (\<epsilon> / 2)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   380
    using IntegralE [OF `Integral (a, b) f x1` `0 < \<epsilon>/2`] by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   381
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   382
  obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   383
    and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f - x2 \<bar> < (\<epsilon> / 2)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   384
    using IntegralE [OF `Integral (b, c) f x2` `0 < \<epsilon>/2`] by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   385
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   386
  def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b - x)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   387
           else if x = b then min (\<delta>1 b) (\<delta>2 b)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   388
                         else min (\<delta>2 x) (x - b)"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   389
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   390
  have "gauge {a..c} \<delta>"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   391
    using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   392
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   393
  moreover {
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   394
    fix D :: "(real \<times> real \<times> real) list"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   395
    assume fine: "fine \<delta> (a,c) D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   396
    from fine_covers_all[OF this `a < b` `b \<le> c`]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   397
    obtain N where "N < length D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   398
      and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   399
      by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   400
    obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   401
    with * have "d < b" and "b \<le> e" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   402
    have in_D: "(d, t, e) \<in> set D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   403
      using D_eq[symmetric] using `N < length D` by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   404
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   405
    from mem_fine[OF fine in_D]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   406
    have "d < e" and "d \<le> t" and "t \<le> e" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   407
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   408
    have "t = b"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   409
    proof (rule ccontr)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   410
      assume "t \<noteq> b"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   411
      with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   412
      show False by (cases "t < b") auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   413
    qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   414
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   415
    let ?D1 = "take N D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   416
    let ?D2 = "drop N D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   417
    def D1 \<equiv> "take N D @ [(d, t, b)]"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   418
    def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   419
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   420
    have "D \<noteq> []" using `N < length D` by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   421
    from hd_drop_conv_nth[OF this `N < length D`]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   422
    have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   423
    with fine_append_split[OF _ _ append_take_drop_id[symmetric]]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   424
    have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   425
      using `N < length D` fine by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   426
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   427
    have "fine \<delta>1 (a,b) D1" unfolding D1_def
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   428
    proof (rule fine_append)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   429
      show "fine \<delta>1 (a, d) ?D1"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   430
      proof (rule fine1[THEN fine_\<delta>_expand])
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   431
        fix x assume "a \<le> x" "x \<le> d"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   432
        hence "x \<le> b" using `d < b` `x \<le> d` by auto
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   433
        thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   434
      qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   435
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   436
      have "b - d < \<delta>1 t"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   437
        using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   438
      from `d < b` `d \<le> t` `t = b` this
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   439
      show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   440
    qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   441
    note rsum1 = I1[OF this]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   442
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   443
    have drop_split: "drop N D = [D ! N] @ drop (Suc N) D"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   444
      using nth_drop'[OF `N < length D`] by simp
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   445
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   446
    have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   447
    proof (cases "drop (Suc N) D = []")
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   448
      case True
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   449
      note * = fine2[simplified drop_split True D_eq append_Nil2]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   450
      have "e = c" using fine_single_boundaries[OF * refl] by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   451
      thus ?thesis unfolding True using fine_Nil by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   452
    next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   453
      case False
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   454
      note * = fine_append_split[OF fine2 False drop_split]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   455
      from fine_single_boundaries[OF *(1)]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   456
      have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   457
      with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   458
      thus ?thesis
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   459
      proof (rule fine_\<delta>_expand)
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   460
        fix x assume "e \<le> x" and "x \<le> c"
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   461
        thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   462
      qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   463
    qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   464
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   465
    have "fine \<delta>2 (b, c) D2"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   466
    proof (cases "e = b")
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   467
      case True thus ?thesis using fine2 by (simp add: D1_def D2_def)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   468
    next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   469
      case False
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   470
      have "e - b < \<delta>2 b"
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   471
        using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   472
      with False `t = b` `b \<le> e`
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   473
      show ?thesis using D2_def
32960
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   474
        by (auto intro!: fine_append[OF _ fine2] fine_single
69916a850301 eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents: 31366
diff changeset
   475
               simp del: append_Cons)
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   476
    qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   477
    note rsum2 = I2[OF this]
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   478
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   479
    have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   480
      using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   481
    also have "\<dots> = rsum D1 f + rsum D2 f"
31366
380188f5e75e use algebra_simps instead of ring_simps
hoelzl
parents: 31364
diff changeset
   482
      by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps)
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   483
    finally have "\<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   484
      using add_strict_mono[OF rsum1 rsum2] by simp
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   485
  }
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   486
  ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and>
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   487
    (\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f - (x1 + x2)\<bar> < \<epsilon>)"
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   488
    by blast
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   489
next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   490
  case False
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   491
  hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   492
  thus ?thesis
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   493
  proof (rule disjE)
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   494
    assume "a = b" hence "x1 = 0"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   495
      using `Integral (a, b) f x1` by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   496
    thus ?thesis using `a = b` `Integral (b, c) f x2` by simp
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   497
  next
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   498
    assume "b = c" hence "x2 = 0"
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   499
      using `Integral (b, c) f x2` by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   500
    thus ?thesis using `b = c` `Integral (a, b) f x1` by simp
31364
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   501
  qed
46da73330913 Generalized Integral_add
hoelzl
parents: 31338
diff changeset
   502
qed
31259
c1b981b71dba encode gauge-fine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents: 31257
diff changeset
   503
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   504
text{*Fundamental theorem of calculus (Part I)*}
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   505
15105
e194d4d265fb fixed tex problem
nipkow
parents: 15094
diff changeset
   506
text{*"Straddle Lemma" : Swartz and Thompson: AMM 95(7) 1988 *}
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   507
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   508
lemma strad1:
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   509
       "\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow>
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   510
             \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2;
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   511
        0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk>
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   512
       \<Longrightarrow> \<forall>z. \<bar>z - x\<bar> < s -->\<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   513
apply clarify
31253
d54dc8956d48 use interval sets with gauge predicate
huffman
parents: 31252
diff changeset
   514
apply (case_tac "z = x", simp)
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   515
apply (drule_tac x = z in spec)
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   516
apply (rule_tac z1 = "\<bar>inverse (z - x)\<bar>" 
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   517
       in real_mult_le_cancel_iff2 [THEN iffD1])
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   518
 apply simp
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   519
apply (simp del: abs_inverse add: abs_mult [symmetric]
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   520
          mult_assoc [symmetric])
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   521
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
   522
                    = (f z - f x) / (z - x) - f' x")
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   523
 apply (simp add: abs_mult [symmetric] mult_ac diff_minus)
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   524
apply (subst mult_commute)
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   525
apply (simp add: left_distrib diff_minus)
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   526
apply (simp add: mult_assoc divide_inverse)
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   527
apply (simp add: left_distrib)
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   528
done
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   529
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   530
lemma lemma_straddle:
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   531
  assumes f': "\<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x)" and "0 < e"
31253
d54dc8956d48 use interval sets with gauge predicate
huffman
parents: 31252
diff changeset
   532
  shows "\<exists>g. gauge {a..b} g &
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   533
                (\<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
   534
                  --> \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   535
proof -
31253
d54dc8956d48 use interval sets with gauge predicate
huffman
parents: 31252
diff changeset
   536
  have "\<forall>x\<in>{a..b}.
15360
300e09825d8b Added "ALL x > y" and relatives.
nipkow
parents: 15251
diff changeset
   537
        (\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v - u) < d --> 
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   538
                       \<bar>(f(v) - f(u)) - (f'(x) * (v - u))\<bar> \<le> e * (v - u))"
31253
d54dc8956d48 use interval sets with gauge predicate
huffman
parents: 31252
diff changeset
   539
  proof (clarsimp)
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   540
    fix x :: real assume "a \<le> x" and "x \<le> b"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   541
    with f' have "DERIV f x :> f'(x)" by simp
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   542
    then have "\<forall>r>0. \<exists>s>0. \<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < r"
31338
d41a8ba25b67 generalize constants from Lim.thy to class metric_space
huffman
parents: 31336
diff changeset
   543
      by (simp add: DERIV_iff2 LIM_eq)
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   544
    with `0 < e` obtain s
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   545
    where "\<forall>z. z \<noteq> x \<and> \<bar>z - x\<bar> < s \<longrightarrow> \<bar>(f z - f x) / (z - x) - f' x\<bar> < e/2" and "0 < s"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   546
      by (drule_tac x="e/2" in spec, auto)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   547
    then have strad [rule_format]:
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   548
        "\<forall>z. \<bar>z - x\<bar> < s --> \<bar>f z - f x - f' x * (z - x)\<bar> \<le> e/2 * \<bar>z - x\<bar>"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   549
      using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   550
    show "\<exists>d>0. \<forall>u v. u \<le> x \<and> x \<le> v \<and> v - u < d \<longrightarrow> \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   551
    proof (safe intro!: exI)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   552
      show "0 < s" by fact
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   553
    next
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   554
      fix u v :: real assume "u \<le> x" and "x \<le> v" and "v - u < s"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   555
      have "\<bar>f v - f u - f' x * (v - u)\<bar> =
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   556
            \<bar>(f v - f x - f' x * (v - x)) + (f x - f u - f' x * (x - u))\<bar>"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   557
        by (simp add: right_diff_distrib)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   558
      also have "\<dots> \<le> \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f x - f u - f' x * (x - u)\<bar>"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   559
        by (rule abs_triangle_ineq)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   560
      also have "\<dots> = \<bar>f v - f x - f' x * (v - x)\<bar> + \<bar>f u - f x - f' x * (u - x)\<bar>"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   561
        by (simp add: right_diff_distrib)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   562
      also have "\<dots> \<le> (e/2) * \<bar>v - x\<bar> + (e/2) * \<bar>u - x\<bar>"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   563
        using `u \<le> x` `x \<le> v` `v - u < s` by (intro add_mono strad, simp_all)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   564
      also have "\<dots> \<le> e * (v - u) / 2 + e * (v - u) / 2"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   565
        using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all)
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   566
      also have "\<dots> = e * (v - u)"
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   567
        by simp
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   568
      finally show "\<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u)" .
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   569
    qed
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   570
  qed
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   571
  thus ?thesis
31253
d54dc8956d48 use interval sets with gauge predicate
huffman
parents: 31252
diff changeset
   572
    by (simp add: gauge_def) (drule bchoice, auto)
31252
5155117f9d66 clean up some proofs
huffman
parents: 30082
diff changeset
   573
qed
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   574
35328
e8888458dce3 Moved old Integration to examples.
hoelzl
parents: 33640
diff changeset
   575
lemma fundamental_theorem_of_calculus:
35441
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   576
  assumes "a \<le> b"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   577
  assumes f': "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f'(x)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   578
  shows "Integral (a, b) f' (f(b) - f(a))"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   579
proof (cases "a = b")
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   580
  assume "a = b" thus ?thesis by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   581
next
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   582
  assume "a \<noteq> b" with `a \<le> b` have "a < b" by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   583
  show ?thesis
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   584
  proof (simp add: Integral_def2, clarify)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   585
    fix e :: real assume "0 < e"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   586
    with `a < b` have "0 < e / (b - a)" by (simp add: divide_pos_pos)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   587
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   588
    from lemma_straddle [OF f' this]
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   589
    obtain \<delta> where "gauge {a..b} \<delta>"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   590
      and \<delta>: "\<And>x u v. \<lbrakk>a \<le> u; u \<le> x; x \<le> v; v \<le> b; v - u < \<delta> x\<rbrakk> \<Longrightarrow>
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   591
           \<bar>f v - f u - f' x * (v - u)\<bar> \<le> e * (v - u) / (b - a)" by auto
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   592
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   593
    have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   594
    proof (clarify)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   595
      fix D assume D: "fine \<delta> (a, b) D"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   596
      hence "(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) = f b - f a"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   597
        by (rule fine_listsum_eq_diff)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   598
      hence "\<bar>rsum D f' - (f b - f a)\<bar> = \<bar>rsum D f' - (\<Sum>(u, x, v)\<leftarrow>D. f v - f u)\<bar>"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   599
        by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   600
      also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v - f u) - rsum D f'\<bar>"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   601
        by (rule abs_minus_commute)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   602
      also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v - f u) - f' x * (v - u)\<bar>"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   603
        by (simp only: rsum_def listsum_subtractf split_def)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   604
      also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v - f u) - f' x * (v - u)\<bar>)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   605
        by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   606
      also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b - a)) * (v - u))"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   607
        apply (rule listsum_mono, clarify, rename_tac u x v)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   608
        using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3)
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   609
        done
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   610
      also have "\<dots> = e"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   611
        using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"]
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   612
        unfolding split_def listsum_const_mult
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   613
        using `a < b` by simp
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   614
      finally show "\<bar>rsum D f' - (f b - f a)\<bar> \<le> e" .
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   615
    qed
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   616
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   617
    with `gauge {a..b} \<delta>`
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   618
    show "\<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f' - (f b - f a)\<bar> \<le> e)"
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   619
      by auto
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   620
  qed
ae742caa0c5b polished and converted some proofs to Isar style
huffman
parents: 35328
diff changeset
   621
qed
13958
c1c67582c9b5 New material on integration, etc. Moving Hyperreal/ex
paulson
parents:
diff changeset
   622
15093
49ede01e9ee6 conversion of Integration and NSPrimes to Isar scripts
paulson
parents: 13958
diff changeset
   623
end