author  bulwahn 
Thu, 16 Feb 2012 09:51:34 +0100  
changeset 46501  fe51817749d1 
parent 45605  a89b4bc311a5 
child 49962  a8cc904a6820 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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  3 

4 
Replaced by ~~/src/HOL/Multivariate_Analysis/Real_Integral.thy . 

13958  5 
*) 
6 

35328  7 
header{*Theory of Integration on real intervals*} 
8 

9 
theory Gauge_Integration 

10 
imports Complex_Main 

11 
begin 

12 

13 
text {* 

13958  14 

35328  15 
\textbf{Attention}: This theory defines the Integration on real 
16 
intervals. This is just a example theory for historical / expository interests. 

17 
A better replacement is found in the Multivariate Analysis library. This defines 

18 
the gauge integral on real vector spaces and in the Real Integral theory 

19 
is a specialization to the integral on arbitrary real intervals. The 

20 
Multivariate Analysis package also provides a better support for analysis on 

21 
integrals. 

22 

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  26 

31259
c1b981b71dba
encode gaugefine 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  30 
gauge :: "[real set, real => real] => bool" where 
37765  31 
"gauge E g = (\<forall>x\<in>E. 0 < g(x))" 
13958  32 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

33 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

34 
subsection {* Gaugefine divisions *} 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

35 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

36 
inductive 
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

38 
for 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

39 
\<delta> :: "real \<Rightarrow> real" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

40 
where 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

41 
fine_Nil: 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

42 
"fine \<delta> (a, a) []" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

43 
 fine_Cons: 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

46 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

47 
lemmas fine_induct [induct set: fine] = 
45605  48 
fine.induct [of "\<delta>" "(a,b)" "D" "split P", unfolded split_conv] for \<delta> a b D P 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

49 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

50 
lemma fine_single: 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

53 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

54 
lemma fine_append: 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

57 

c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

60 

c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

62 
apply (induct set: fine, simp) 
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

64 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

65 

35441  66 
lemma fine_Nil_iff: "fine \<delta> (a, b) [] \<longleftrightarrow> a = b" 
67 
by (auto elim: fine.cases intro: fine.intros) 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

68 

35441  69 
lemma fine_same_iff: "fine \<delta> (a, a) D \<longleftrightarrow> D = []" 
70 
proof 

71 
assume "fine \<delta> (a, a) D" thus "D = []" 

72 
by (metis nonempty_fine_imp_less less_irrefl) 

73 
next 

74 
assume "D = []" thus "fine \<delta> (a, a) D" 

75 
by (simp add: fine_Nil) 

76 
qed 

77 

78 
lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b" 

79 
by (simp add: fine_Nil_iff) 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

80 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

81 
lemma mem_fine: 
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

83 
by (induct set: fine, simp, force) 
13958  84 

31259
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

89 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

90 

c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

93 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

94 
lemma BOLZANO: 
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

96 
assumes 1: "a \<le> b" 
c1b981b71dba
encode gaugefine 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 gaugefine 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 & (ba) < d \<longrightarrow> P a b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

99 
shows "P a b" 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

102 
apply (clarify, erule (3) 2) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

103 
apply (clarify, rule 3) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

104 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

105 

c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

107 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

108 
lemma fine_exists: 
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

110 
proof  
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

111 
{ 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine 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 gaugefine 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 gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

118 
apply (rule conjI) 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

121 
apply (case_tac "u = v") 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

122 
apply (fast intro: fine_Nil) 
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

125 
done 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

126 
} 
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

128 
qed 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

129 

31364  130 
lemma fine_covers_all: 
131 
assumes "fine \<delta> (a, c) D" and "a < x" and "x \<le> c" 

132 
shows "\<exists> N < length D. \<forall> d t e. D ! N = (d,t,e) \<longrightarrow> d < x \<and> x \<le> e" 

133 
using assms 

134 
proof (induct set: fine) 

135 
case (2 b c D a t) 

136 
thus ?case 

137 
proof (cases "b < x") 

138 
case True 

139 
with 2 obtain N where *: "N < length D" 

140 
and **: "\<And> d t e. D ! N = (d,t,e) \<Longrightarrow> d < x \<and> x \<le> e" by auto 

141 
hence "Suc N < length ((a,t,b)#D) \<and> 

142 
(\<forall> d t' e. ((a,t,b)#D) ! Suc N = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto 

143 
thus ?thesis by auto 

144 
next 

145 
case False with 2 

146 
have "0 < length ((a,t,b)#D) \<and> 

147 
(\<forall> d t' e. ((a,t,b)#D) ! 0 = (d,t',e) \<longrightarrow> d < x \<and> x \<le> e)" by auto 

148 
thus ?thesis by auto 

149 
qed 

150 
qed auto 

151 

152 
lemma fine_append_split: 

153 
assumes "fine \<delta> (a,b) D" and "D2 \<noteq> []" and "D = D1 @ D2" 

154 
shows "fine \<delta> (a,fst (hd D2)) D1" (is "?fine1") 

155 
and "fine \<delta> (fst (hd D2), b) D2" (is "?fine2") 

156 
proof  

157 
from assms 

158 
have "?fine1 \<and> ?fine2" 

159 
proof (induct arbitrary: D1 D2) 

160 
case (2 b c D a' x D1 D2) 

161 
note induct = this 

162 

163 
thus ?case 

164 
proof (cases D1) 

165 
case Nil 

166 
hence "fst (hd D2) = a'" using 2 by auto 

167 
with fine_Cons[OF `fine \<delta> (b,c) D` induct(3,4,5)] Nil induct 

168 
show ?thesis by (auto intro: fine_Nil) 

169 
next 

170 
case (Cons d1 D1') 

171 
with induct(2)[OF `D2 \<noteq> []`, of D1'] induct(8) 

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 tabwidth;
wenzelm
parents:
31366
diff
changeset

173 
"d1 = (a', x, b)" by auto 
31364  174 
with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons 
175 
show ?thesis by auto 

176 
qed 

177 
qed auto 

178 
thus ?fine1 and ?fine2 by auto 

179 
qed 

180 

181 
lemma fine_\<delta>_expand: 

182 
assumes "fine \<delta> (a,b) D" 

35441  183 
and "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> \<delta> x \<le> \<delta>' x" 
31364  184 
shows "fine \<delta>' (a,b) D" 
185 
using assms proof induct 

186 
case 1 show ?case by (rule fine_Nil) 

187 
next 

188 
case (2 b c D a x) 

189 
show ?case 

190 
proof (rule fine_Cons) 

191 
show "fine \<delta>' (b,c) D" using 2 by auto 

192 
from fine_imp_le[OF 2(1)] 2(6) `x \<le> b` 

193 
show "b  a < \<delta>' x" 

194 
using 2(7)[OF `a \<le> x`] by auto 

195 
qed (auto simp add: 2) 

196 
qed 

197 

198 
lemma fine_single_boundaries: 

199 
assumes "fine \<delta> (a,b) D" and "D = [(d, t, e)]" 

200 
shows "a = d \<and> b = e" 

201 
using assms proof induct 

202 
case (2 b c D a x) 

203 
hence "D = []" and "a = d" and "b = e" by auto 

204 
moreover 

205 
from `fine \<delta> (b,c) D` `D = []` have "b = c" 

206 
by (rule empty_fine_imp_eq) 

207 
ultimately show ?case by simp 

208 
qed auto 

209 

35328  210 
lemma fine_listsum_eq_diff: 
211 
fixes f :: "real \<Rightarrow> real" 

212 
shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v  f u) = f b  f a" 

213 
by (induct set: fine) simp_all 

214 

215 
text{*Lemmas about combining gauges*} 

216 

217 
lemma gauge_min: 

218 
"[ gauge(E) g1; gauge(E) g2 ] 

219 
==> gauge(E) (%x. min (g1(x)) (g2(x)))" 

220 
by (simp add: gauge_def) 

221 

222 
lemma fine_min: 

223 
"fine (%x. min (g1(x)) (g2(x))) (a,b) D 

224 
==> fine(g1) (a,b) D & fine(g2) (a,b) D" 

225 
apply (erule fine.induct) 

226 
apply (simp add: fine_Nil) 

227 
apply (simp add: fine_Cons) 

228 
done 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

229 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

230 
subsection {* Riemann sum *} 
13958  231 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20792
diff
changeset

232 
definition 
31259
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

235 

c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

237 
unfolding rsum_def by simp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

238 

c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

240 
unfolding rsum_def by simp 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

241 

c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

243 
by (induct D, auto) 
13958  244 

31259
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

247 

c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

250 

c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

253 

31364  254 
lemma rsum_append: "rsum (D1 @ D2) f = rsum D1 f + rsum D2 f" 
255 
unfolding rsum_def map_append listsum_append .. 

256 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

257 

c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

258 
subsection {* Gauge integrability (definite) *} 
13958  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  262 
"Integral = (%(a,b) f k. \<forall>e > 0. 
31259
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine 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  267 
lemma Integral_eq: 
268 
"Integral (a, b) f k \<longleftrightarrow> 

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))" 

270 
unfolding Integral_def by simp 

271 

272 
lemma IntegralI: 

273 
assumes "\<And>e. 0 < e \<Longrightarrow> 

274 
\<exists>\<delta>. gauge {a..b} \<delta> \<and> (\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f  k\<bar> < e)" 

275 
shows "Integral (a, b) f k" 

276 
using assms unfolding Integral_def by auto 

277 

278 
lemma IntegralE: 

279 
assumes "Integral (a, b) f k" and "0 < e" 

280 
obtains \<delta> where "gauge {a..b} \<delta>" and "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f  k\<bar> < e" 

281 
using assms unfolding Integral_def by auto 

282 

31252  283 
lemma Integral_def2: 
31259
c1b981b71dba
encode gaugefine 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 gaugefine 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 gaugefine 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  287 
unfolding Integral_def 
288 
apply (safe intro!: ext) 

289 
apply (fast intro: less_imp_le) 

290 
apply (drule_tac x="e/2" in spec) 

291 
apply force 

292 
done 

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  297 
assumes le: "a \<le> b" 
298 
assumes 1: "Integral (a, b) f k1" 

299 
assumes 2: "Integral (a, b) f k2" 

300 
shows "k1 = k2" 

301 
proof (rule ccontr) 

302 
assume "k1 \<noteq> k2" 

303 
hence e: "0 < \<bar>k1  k2\<bar> / 2" by simp 

304 
obtain d1 where "gauge {a..b} d1" and 

305 
d1: "\<forall>D. fine d1 (a, b) D \<longrightarrow> \<bar>rsum D f  k1\<bar> < \<bar>k1  k2\<bar> / 2" 

306 
using 1 e by (rule IntegralE) 

307 
obtain d2 where "gauge {a..b} d2" and 

308 
d2: "\<forall>D. fine d2 (a, b) D \<longrightarrow> \<bar>rsum D f  k2\<bar> < \<bar>k1  k2\<bar> / 2" 

309 
using 2 e by (rule IntegralE) 

310 
have "gauge {a..b} (\<lambda>x. min (d1 x) (d2 x))" 

311 
using `gauge {a..b} d1` and `gauge {a..b} d2` 

312 
by (rule gauge_min) 

313 
then obtain D where "fine (\<lambda>x. min (d1 x) (d2 x)) (a, b) D" 

314 
using fine_exists [OF le] by fast 

315 
hence "fine d1 (a, b) D" and "fine d2 (a, b) D" 

316 
by (auto dest: fine_min) 

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" 

318 
using d1 d2 by simp_all 

319 
hence "\<bar>rsum D f  k1\<bar> + \<bar>rsum D f  k2\<bar> < \<bar>k1  k2\<bar> / 2 + \<bar>k1  k2\<bar> / 2" 

320 
by (rule add_strict_mono) 

321 
thus False by auto 

322 
qed 

323 

324 
lemma Integral_zero: "Integral(a,a) f 0" 

325 
apply (rule IntegralI) 

326 
apply (rule_tac x = "\<lambda>x. 1" in exI) 

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  330 
lemma Integral_same_iff [simp]: "Integral (a, a) f k \<longleftrightarrow> k = 0" 
331 
by (auto intro: Integral_zero Integral_unique) 

332 

333 
lemma Integral_zero_fun: "Integral (a,b) (\<lambda>x. 0) 0" 

334 
apply (rule IntegralI) 

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 gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

339 
unfolding rsum_def 
c1b981b71dba
encode gaugefine 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  342 
lemma Integral_mult_const: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. c) (c * (b  a))" 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

343 
apply (cases "a = b", simp) 
35441  344 
apply (rule IntegralI) 
345 
apply (rule_tac x = "\<lambda>x. b  a" in exI) 

31259
c1b981b71dba
encode gaugefine 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 gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

347 
apply (clarify) 
c1b981b71dba
encode gaugefine 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  351 
lemma Integral_eq_diff_bounds: "a \<le> b \<Longrightarrow> Integral(a,b) (\<lambda>x. 1) (b  a)" 
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  356 
apply (auto simp add: order_le_less) 
357 
apply (cases "c = 0", simp add: Integral_zero_fun) 

358 
apply (rule IntegralI) 

359 
apply (erule_tac e="e / \<bar>c\<bar>" in IntegralE, simp add: divide_pos_pos) 

31259
c1b981b71dba
encode gaugefine 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 gaugefine 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  362 
apply (simp add: pos_less_divide_eq abs_mult [symmetric] 
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  366 
lemma Integral_add: 
367 
assumes "Integral (a, b) f x1" 

368 
assumes "Integral (b, c) f x2" 

369 
assumes "a \<le> b" and "b \<le> c" 

370 
shows "Integral (a, c) f (x1 + x2)" 

35441  371 
proof (cases "a < b \<and> b < c", rule IntegralI) 
31364  372 
fix \<epsilon> :: real assume "0 < \<epsilon>" 
373 
hence "0 < \<epsilon> / 2" by auto 

374 

375 
assume "a < b \<and> b < c" 

376 
hence "a < b" and "b < c" by auto 

377 

378 
obtain \<delta>1 where \<delta>1_gauge: "gauge {a..b} \<delta>1" 

35441  379 
and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f  x1 \<bar> < (\<epsilon> / 2)" 
380 
using IntegralE [OF `Integral (a, b) f x1` `0 < \<epsilon>/2`] by auto 

31364  381 

382 
obtain \<delta>2 where \<delta>2_gauge: "gauge {b..c} \<delta>2" 

35441  383 
and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f  x2 \<bar> < (\<epsilon> / 2)" 
384 
using IntegralE [OF `Integral (b, c) f x2` `0 < \<epsilon>/2`] by auto 

31364  385 

386 
def \<delta> \<equiv> "\<lambda> x. if x < b then min (\<delta>1 x) (b  x) 

387 
else if x = b then min (\<delta>1 b) (\<delta>2 b) 

388 
else min (\<delta>2 x) (x  b)" 

389 

390 
have "gauge {a..c} \<delta>" 

391 
using \<delta>1_gauge \<delta>2_gauge unfolding \<delta>_def gauge_def by auto 

35441  392 

31364  393 
moreover { 
394 
fix D :: "(real \<times> real \<times> real) list" 

395 
assume fine: "fine \<delta> (a,c) D" 

396 
from fine_covers_all[OF this `a < b` `b \<le> c`] 

397 
obtain N where "N < length D" 

398 
and *: "\<forall> d t e. D ! N = (d, t, e) \<longrightarrow> d < b \<and> b \<le> e" 

399 
by auto 

400 
obtain d t e where D_eq: "D ! N = (d, t, e)" by (cases "D!N", auto) 

401 
with * have "d < b" and "b \<le> e" by auto 

402 
have in_D: "(d, t, e) \<in> set D" 

403 
using D_eq[symmetric] using `N < length D` by auto 

404 

405 
from mem_fine[OF fine in_D] 

406 
have "d < e" and "d \<le> t" and "t \<le> e" by auto 

407 

408 
have "t = b" 

409 
proof (rule ccontr) 

410 
assume "t \<noteq> b" 

411 
with mem_fine3[OF fine in_D] `b \<le> e` `d \<le> t` `t \<le> e` `d < b` \<delta>_def 

412 
show False by (cases "t < b") auto 

413 
qed 

414 

415 
let ?D1 = "take N D" 

416 
let ?D2 = "drop N D" 

417 
def D1 \<equiv> "take N D @ [(d, t, b)]" 

418 
def D2 \<equiv> "(if b = e then [] else [(b, t, e)]) @ drop (Suc N) D" 

419 

46501  420 
from hd_drop_conv_nth[OF `N < length D`] 
31364  421 
have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto 
422 
with fine_append_split[OF _ _ append_take_drop_id[symmetric]] 

423 
have fine1: "fine \<delta> (a,d) ?D1" and fine2: "fine \<delta> (d,c) ?D2" 

424 
using `N < length D` fine by auto 

425 

426 
have "fine \<delta>1 (a,b) D1" unfolding D1_def 

427 
proof (rule fine_append) 

428 
show "fine \<delta>1 (a, d) ?D1" 

429 
proof (rule fine1[THEN fine_\<delta>_expand]) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

430 
fix x assume "a \<le> x" "x \<le> d" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

431 
hence "x \<le> b" using `d < b` `x \<le> d` by auto 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

432 
thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto 
31364  433 
qed 
434 

435 
have "b  d < \<delta>1 t" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

436 
using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto 
31364  437 
from `d < b` `d \<le> t` `t = b` this 
438 
show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto 

439 
qed 

440 
note rsum1 = I1[OF this] 

441 

442 
have drop_split: "drop N D = [D ! N] @ drop (Suc N) D" 

443 
using nth_drop'[OF `N < length D`] by simp 

444 

445 
have fine2: "fine \<delta>2 (e,c) (drop (Suc N) D)" 

446 
proof (cases "drop (Suc N) D = []") 

447 
case True 

448 
note * = fine2[simplified drop_split True D_eq append_Nil2] 

449 
have "e = c" using fine_single_boundaries[OF * refl] by auto 

450 
thus ?thesis unfolding True using fine_Nil by auto 

451 
next 

452 
case False 

453 
note * = fine_append_split[OF fine2 False drop_split] 

454 
from fine_single_boundaries[OF *(1)] 

455 
have "fst (hd (drop (Suc N) D)) = e" using D_eq by auto 

456 
with *(2) have "fine \<delta> (e,c) (drop (Suc N) D)" by auto 

457 
thus ?thesis 

458 
proof (rule fine_\<delta>_expand) 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

459 
fix x assume "e \<le> x" and "x \<le> c" 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

460 
thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto 
31364  461 
qed 
462 
qed 

463 

464 
have "fine \<delta>2 (b, c) D2" 

465 
proof (cases "e = b") 

466 
case True thus ?thesis using fine2 by (simp add: D1_def D2_def) 

467 
next 

468 
case False 

469 
have "e  b < \<delta>2 b" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

470 
using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto 
31364  471 
with False `t = b` `b \<le> e` 
472 
show ?thesis using D2_def 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

473 
by (auto intro!: fine_append[OF _ fine2] fine_single 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
31366
diff
changeset

474 
simp del: append_Cons) 
31364  475 
qed 
476 
note rsum2 = I2[OF this] 

477 

478 
have "rsum D f = rsum (take N D) f + rsum [D ! N] f + rsum (drop (Suc N) D) f" 

479 
using rsum_append[symmetric] nth_drop'[OF `N < length D`] by auto 

480 
also have "\<dots> = rsum D1 f + rsum D2 f" 

31366  481 
by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append algebra_simps) 
31364  482 
finally have "\<bar>rsum D f  (x1 + x2)\<bar> < \<epsilon>" 
483 
using add_strict_mono[OF rsum1 rsum2] by simp 

484 
} 

485 
ultimately show "\<exists> \<delta>. gauge {a .. c} \<delta> \<and> 

486 
(\<forall>D. fine \<delta> (a,c) D \<longrightarrow> \<bar>rsum D f  (x1 + x2)\<bar> < \<epsilon>)" 

487 
by blast 

488 
next 

489 
case False 

490 
hence "a = b \<or> b = c" using `a \<le> b` and `b \<le> c` by auto 

491 
thus ?thesis 

492 
proof (rule disjE) 

493 
assume "a = b" hence "x1 = 0" 

35441  494 
using `Integral (a, b) f x1` by simp 
495 
thus ?thesis using `a = b` `Integral (b, c) f x2` by simp 

31364  496 
next 
497 
assume "b = c" hence "x2 = 0" 

35441  498 
using `Integral (b, c) f x2` by simp 
499 
thus ?thesis using `b = c` `Integral (a, b) f x1` by simp 

31364  500 
qed 
501 
qed 

31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

502 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

503 
text{*Fundamental theorem of calculus (Part I)*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

504 

15105  505 
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

506 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

507 
lemma strad1: 
31252  508 
"\<lbrakk>\<forall>z::real. z \<noteq> x \<and> \<bar>z  x\<bar> < s \<longrightarrow> 
509 
\<bar>(f z  f x) / (z  x)  f' x\<bar> < e/2; 

510 
0 < s; 0 < e; a \<le> x; x \<le> b\<rbrakk> 

511 
\<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>" 

512 
apply clarify 

31253  513 
apply (case_tac "z = x", simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

514 
apply (drule_tac x = z in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

515 
apply (rule_tac z1 = "\<bar>inverse (z  x)\<bar>" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

516 
in real_mult_le_cancel_iff2 [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

517 
apply simp 
35441  518 
apply (simp del: abs_inverse add: abs_mult [symmetric] 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

519 
mult_assoc [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

520 
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

521 
= (f z  f x) / (z  x)  f' x") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

522 
apply (simp add: abs_mult [symmetric] mult_ac diff_minus) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

523 
apply (subst mult_commute) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

524 
apply (simp add: left_distrib diff_minus) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

525 
apply (simp add: mult_assoc divide_inverse) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

526 
apply (simp add: left_distrib) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

527 
done 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

528 

49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

529 
lemma lemma_straddle: 
31252  530 
assumes f': "\<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x)" and "0 < e" 
31253  531 
shows "\<exists>g. gauge {a..b} g & 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

532 
(\<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

533 
> \<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31252  534 
proof  
31253  535 
have "\<forall>x\<in>{a..b}. 
15360  536 
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v  u) < d > 
31252  537 
\<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31253  538 
proof (clarsimp) 
31252  539 
fix x :: real assume "a \<le> x" and "x \<le> b" 
540 
with f' have "DERIV f x :> f'(x)" by simp 

541 
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

542 
by (simp add: DERIV_iff2 LIM_eq) 
31252  543 
with `0 < e` obtain s 
544 
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" 

545 
by (drule_tac x="e/2" in spec, auto) 

546 
then have strad [rule_format]: 

547 
"\<forall>z. \<bar>z  x\<bar> < s > \<bar>f z  f x  f' x * (z  x)\<bar> \<le> e/2 * \<bar>z  x\<bar>" 

548 
using `0 < e` `a \<le> x` `x \<le> b` by (rule strad1) 

549 
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)" 

550 
proof (safe intro!: exI) 

551 
show "0 < s" by fact 

552 
next 

553 
fix u v :: real assume "u \<le> x" and "x \<le> v" and "v  u < s" 

554 
have "\<bar>f v  f u  f' x * (v  u)\<bar> = 

555 
\<bar>(f v  f x  f' x * (v  x)) + (f x  f u  f' x * (x  u))\<bar>" 

556 
by (simp add: right_diff_distrib) 

557 
also have "\<dots> \<le> \<bar>f v  f x  f' x * (v  x)\<bar> + \<bar>f x  f u  f' x * (x  u)\<bar>" 

558 
by (rule abs_triangle_ineq) 

559 
also have "\<dots> = \<bar>f v  f x  f' x * (v  x)\<bar> + \<bar>f u  f x  f' x * (u  x)\<bar>" 

560 
by (simp add: right_diff_distrib) 

561 
also have "\<dots> \<le> (e/2) * \<bar>v  x\<bar> + (e/2) * \<bar>u  x\<bar>" 

562 
using `u \<le> x` `x \<le> v` `v  u < s` by (intro add_mono strad, simp_all) 

563 
also have "\<dots> \<le> e * (v  u) / 2 + e * (v  u) / 2" 

564 
using `u \<le> x` `x \<le> v` `0 < e` by (intro add_mono, simp_all) 

565 
also have "\<dots> = e * (v  u)" 

566 
by simp 

567 
finally show "\<bar>f v  f u  f' x * (v  u)\<bar> \<le> e * (v  u)" . 

568 
qed 

569 
qed 

570 
thus ?thesis 

31253  571 
by (simp add: gauge_def) (drule bchoice, auto) 
31252  572 
qed 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

573 

35328  574 
lemma fundamental_theorem_of_calculus: 
35441  575 
assumes "a \<le> b" 
576 
assumes f': "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> DERIV f x :> f'(x)" 

577 
shows "Integral (a, b) f' (f(b)  f(a))" 

578 
proof (cases "a = b") 

579 
assume "a = b" thus ?thesis by simp 

580 
next 

581 
assume "a \<noteq> b" with `a \<le> b` have "a < b" by simp 

582 
show ?thesis 

583 
proof (simp add: Integral_def2, clarify) 

584 
fix e :: real assume "0 < e" 

585 
with `a < b` have "0 < e / (b  a)" by (simp add: divide_pos_pos) 

586 

587 
from lemma_straddle [OF f' this] 

588 
obtain \<delta> where "gauge {a..b} \<delta>" 

589 
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> 

590 
\<bar>f v  f u  f' x * (v  u)\<bar> \<le> e * (v  u) / (b  a)" by auto 

591 

592 
have "\<forall>D. fine \<delta> (a, b) D \<longrightarrow> \<bar>rsum D f'  (f b  f a)\<bar> \<le> e" 

593 
proof (clarify) 

594 
fix D assume D: "fine \<delta> (a, b) D" 

595 
hence "(\<Sum>(u, x, v)\<leftarrow>D. f v  f u) = f b  f a" 

596 
by (rule fine_listsum_eq_diff) 

597 
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>" 

598 
by simp 

599 
also have "\<dots> = \<bar>(\<Sum>(u, x, v)\<leftarrow>D. f v  f u)  rsum D f'\<bar>" 

600 
by (rule abs_minus_commute) 

601 
also have "\<dots> = \<bar>\<Sum>(u, x, v)\<leftarrow>D. (f v  f u)  f' x * (v  u)\<bar>" 

602 
by (simp only: rsum_def listsum_subtractf split_def) 

603 
also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. \<bar>(f v  f u)  f' x * (v  u)\<bar>)" 

604 
by (rule ord_le_eq_trans [OF listsum_abs], simp add: o_def split_def) 

605 
also have "\<dots> \<le> (\<Sum>(u, x, v)\<leftarrow>D. (e / (b  a)) * (v  u))" 

606 
apply (rule listsum_mono, clarify, rename_tac u x v) 

607 
using D apply (simp add: \<delta> mem_fine mem_fine2 mem_fine3) 

608 
done 

609 
also have "\<dots> = e" 

610 
using fine_listsum_eq_diff [OF D, where f="\<lambda>x. x"] 

611 
unfolding split_def listsum_const_mult 

612 
using `a < b` by simp 

613 
finally show "\<bar>rsum D f'  (f b  f a)\<bar> \<le> e" . 

614 
qed 

615 

616 
with `gauge {a..b} \<delta>` 

617 
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)" 

618 
by auto 

619 
qed 

620 
qed 

13958  621 

15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

622 
end 