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