author  hoelzl 
Tue, 02 Jun 2009 14:00:24 +0200  
changeset 31364  46da73330913 
parent 31338  d41a8ba25b67 
child 31366  380188f5e75e 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

1 
(* Author : Jacques D. Fleuriot 
13958  2 
Copyright : 2000 University of Edinburgh 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

3 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
13958  4 
*) 
5 

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

6 
header{*Theory of Integration*} 
13958  7 

15131  8 
theory Integration 
29469  9 
imports Deriv ATP_Linkup 
15131  10 
begin 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

11 

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

12 
text{*We follow John Harrison in formalizing the Gauge integral.*} 
13958  13 

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

14 
subsection {* Gauges *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

15 

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

16 
definition 
31253  17 
gauge :: "[real set, real => real] => bool" where 
18 
[code del]:"gauge E g = (\<forall>x\<in>E. 0 < g(x))" 

13958  19 

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

20 

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

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

22 

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

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

24 
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

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

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

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

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

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

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

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

32 
\<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

33 

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

34 
lemmas fine_induct [induct set: fine] = 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

36 

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

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

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

39 
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

40 

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

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

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

43 
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

44 

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

45 
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

46 
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

47 

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

48 
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

49 
apply (induct set: fine, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

50 
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

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

52 

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

53 
lemma empty_fine_imp_eq: "\<lbrakk>fine \<delta> (a, b) D; D = []\<rbrakk> \<Longrightarrow> a = b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

54 
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

55 

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

56 
lemma fine_eq: "fine \<delta> (a, b) D \<Longrightarrow> a = b \<longleftrightarrow> D = []" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

57 
apply (cases "D = []") 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

58 
apply (drule (1) empty_fine_imp_eq, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

59 
apply (drule (1) nonempty_fine_imp_less, simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

61 

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

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

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

64 
by (induct set: fine, simp, force) 
13958  65 

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

66 
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

67 
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

68 
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

69 
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

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

71 

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

72 
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

73 
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

74 

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

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

76 
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

77 
assumes 1: "a \<le> b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

78 
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

79 
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

80 
shows "P a b" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

81 
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

82 
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

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

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

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

86 

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

87 
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

88 

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

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

90 
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

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

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

93 
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

94 
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

95 
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

96 
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

97 
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

98 
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

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

100 
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

101 
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

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

103 
apply (fast intro: fine_Nil) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

104 
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

105 
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

106 
done 
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 
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

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

110 

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

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

114 
using assms 

115 
proof (induct set: fine) 

116 
case (2 b c D a t) 

117 
thus ?case 

118 
proof (cases "b < x") 

119 
case True 

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

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

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

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

124 
thus ?thesis by auto 

125 
next 

126 
case False with 2 

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

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

129 
thus ?thesis by auto 

130 
qed 

131 
qed auto 

132 

133 
lemma fine_append_split: 

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

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

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

137 
proof  

138 
from assms 

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

140 
proof (induct arbitrary: D1 D2) 

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

142 
note induct = this 

143 

144 
thus ?case 

145 
proof (cases D1) 

146 
case Nil 

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

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

149 
show ?thesis by (auto intro: fine_Nil) 

150 
next 

151 
case (Cons d1 D1') 

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

153 
have "fine \<delta> (b, fst (hd D2)) D1'" and "fine \<delta> (fst (hd D2), c) D2" and 

154 
"d1 = (a', x, b)" by auto 

155 
with fine_Cons[OF this(1) induct(3,4,5), OF induct(6)] Cons 

156 
show ?thesis by auto 

157 
qed 

158 
qed auto 

159 
thus ?fine1 and ?fine2 by auto 

160 
qed 

161 

162 
lemma fine_\<delta>_expand: 

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

164 
and "\<And> x. \<lbrakk> a \<le> x ; x \<le> b \<rbrakk> \<Longrightarrow> \<delta> x \<le> \<delta>' x" 

165 
shows "fine \<delta>' (a,b) D" 

166 
using assms proof induct 

167 
case 1 show ?case by (rule fine_Nil) 

168 
next 

169 
case (2 b c D a x) 

170 
show ?case 

171 
proof (rule fine_Cons) 

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

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

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

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

176 
qed (auto simp add: 2) 

177 
qed 

178 

179 
lemma fine_single_boundaries: 

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

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

182 
using assms proof induct 

183 
case (2 b c D a x) 

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

185 
moreover 

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

187 
by (rule empty_fine_imp_eq) 

188 
ultimately show ?case by simp 

189 
qed auto 

190 

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

191 

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

192 
subsection {* Riemann sum *} 
13958  193 

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

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

195 
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

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

197 

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

198 
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

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

200 

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

201 
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

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

203 

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

204 
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

205 
by (induct D, auto) 
13958  206 

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

207 
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

208 
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

209 

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

210 
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

211 
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

212 

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

213 
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

214 
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

215 

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

218 

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

219 

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

220 
subsection {* Gauge integrability (definite) *} 
13958  221 

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

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

223 
Integral :: "[(real*real),real=>real,real] => bool" where 
28562  224 
[code del]: "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

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

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

227 
\<bar>rsum D f  k\<bar> < e)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

228 

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

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

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

232 
\<bar>rsum D f  k\<bar> \<le> e)))" 
31252  233 
unfolding Integral_def 
234 
apply (safe intro!: ext) 

235 
apply (fast intro: less_imp_le) 

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

237 
apply force 

238 
done 

239 

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

240 
text{*Lemmas about combining gauges*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

241 

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

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

243 
"[ gauge(E) g1; gauge(E) g2 ] 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

244 
==> gauge(E) (%x. min (g1(x)) (g2(x)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

245 
by (simp add: gauge_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

246 

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

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

248 
"fine (%x. min (g1(x)) (g2(x))) (a,b) D 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

249 
==> fine(g1) (a,b) D & fine(g2) (a,b) D" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

250 
apply (erule fine.induct) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

251 
apply (simp add: fine_Nil) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

252 
apply (simp add: fine_Cons) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

254 

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

255 
text{*The integral is unique if it exists*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

256 

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

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

258 
"[ 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

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

260 
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

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

262 
apply (drule gauge_min, assumption) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

263 
apply (drule_tac \<delta> = "%x. min (\<delta> x) (\<delta>' x)" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

264 
in fine_exists, assumption, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

265 
apply (drule fine_min) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

266 
apply (drule spec)+ 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

268 
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

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

270 
apply (drule add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

271 
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

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

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

274 

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

275 
lemma Integral_zero [simp]: "Integral(a,a) f 0" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

277 
apply (rule_tac x = "%x. 1" in exI) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

278 
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

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

280 

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

281 
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

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

283 
by (induct set: fine, auto simp add: algebra_simps) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

284 

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

285 
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b  a)" 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

286 
apply (cases "a = b", simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

287 
apply (simp add: Integral_def, clarify) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

288 
apply (rule_tac x = "%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

289 
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

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

291 
apply (subst fine_rsum_const, assumption, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

293 

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

294 
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%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

295 
apply (cases "a = b", simp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

296 
apply (simp add: Integral_def, clarify) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

297 
apply (rule_tac x = "%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

298 
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

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

300 
apply (subst fine_rsum_const, assumption, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

302 

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

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

304 
"[ a \<le> b; Integral(a,b) f k ] ==> Integral(a,b) (%x. c * f x) (c * k)" 
15221  305 
apply (auto simp add: order_le_less 
306 
dest: Integral_unique [OF order_refl Integral_zero]) 

31257  307 
apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc) 
308 
apply (case_tac "c = 0", force) 

309 
apply (drule_tac x = "e/abs c" in spec) 

310 
apply (simp add: divide_pos_pos) 

311 
apply clarify 

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

312 
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

313 
apply (drule_tac x="D" in spec, clarify) 
31257  314 
apply (simp add: pos_less_divide_eq abs_mult [symmetric] 
315 
algebra_simps rsum_right_distrib) 

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

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

317 

31364  318 
lemma Integral_add: 
319 
assumes "Integral (a, b) f x1" 

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

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

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

323 
proof (cases "a < b \<and> b < c", simp only: Integral_def split_conv, rule allI, rule impI) 

324 
fix \<epsilon> :: real assume "0 < \<epsilon>" 

325 
hence "0 < \<epsilon> / 2" by auto 

326 

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

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

329 

330 
from `Integral (a, b) f x1`[simplified Integral_def split_conv, 

331 
rule_format, OF `0 < \<epsilon>/2`] 

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

333 
and I1: "\<And> D. fine \<delta>1 (a,b) D \<Longrightarrow> \<bar> rsum D f  x1 \<bar> < (\<epsilon> / 2)" by auto 

334 

335 
from `Integral (b, c) f x2`[simplified Integral_def split_conv, 

336 
rule_format, OF `0 < \<epsilon>/2`] 

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

338 
and I2: "\<And> D. fine \<delta>2 (b,c) D \<Longrightarrow> \<bar> rsum D f  x2 \<bar> < (\<epsilon> / 2)" by auto 

339 

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

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

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

343 

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

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

346 
moreover { 

347 
fix D :: "(real \<times> real \<times> real) list" 

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

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

350 
obtain N where "N < length D" 

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

352 
by auto 

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

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

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

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

357 

358 
from mem_fine[OF fine in_D] 

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

360 

361 
have "t = b" 

362 
proof (rule ccontr) 

363 
assume "t \<noteq> b" 

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

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

366 
qed 

367 

368 
let ?D1 = "take N D" 

369 
let ?D2 = "drop N D" 

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

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

372 

373 
have "D \<noteq> []" using `N < length D` by auto 

374 
from hd_drop_conv_nth[OF this `N < length D`] 

375 
have "fst (hd ?D2) = d" using `D ! N = (d, t, e)` by auto 

376 
with fine_append_split[OF _ _ append_take_drop_id[symmetric]] 

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

378 
using `N < length D` fine by auto 

379 

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

381 
proof (rule fine_append) 

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

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

384 
fix x assume "a \<le> x" "x \<le> d" 

385 
hence "x \<le> b" using `d < b` `x \<le> d` by auto 

386 
thus "\<delta> x \<le> \<delta>1 x" unfolding \<delta>_def by auto 

387 
qed 

388 

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

390 
using mem_fine3[OF fine in_D] \<delta>_def `b \<le> e` `t = b` by auto 

391 
from `d < b` `d \<le> t` `t = b` this 

392 
show "fine \<delta>1 (d, b) [(d, t, b)]" using fine_single by auto 

393 
qed 

394 
note rsum1 = I1[OF this] 

395 

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

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

398 

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

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

401 
case True 

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

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

404 
thus ?thesis unfolding True using fine_Nil by auto 

405 
next 

406 
case False 

407 
note * = fine_append_split[OF fine2 False drop_split] 

408 
from fine_single_boundaries[OF *(1)] 

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

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

411 
thus ?thesis 

412 
proof (rule fine_\<delta>_expand) 

413 
fix x assume "e \<le> x" and "x \<le> c" 

414 
thus "\<delta> x \<le> \<delta>2 x" using `b \<le> e` unfolding \<delta>_def by auto 

415 
qed 

416 
qed 

417 

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

419 
proof (cases "e = b") 

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

421 
next 

422 
case False 

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

424 
using mem_fine3[OF fine in_D] \<delta>_def `d < b` `t = b` by auto 

425 
with False `t = b` `b \<le> e` 

426 
show ?thesis using D2_def 

427 
by (auto intro!: fine_append[OF _ fine2] fine_single 

428 
simp del: append_Cons) 

429 
qed 

430 
note rsum2 = I2[OF this] 

431 

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

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

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

435 
by (cases "b = e", auto simp add: D1_def D2_def D_eq rsum_append ring_simps) 

436 
finally have "\<bar>rsum D f  (x1 + x2)\<bar> < \<epsilon>" 

437 
using add_strict_mono[OF rsum1 rsum2] by simp 

438 
} 

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

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

441 
by blast 

442 
next 

443 
case False 

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

445 
thus ?thesis 

446 
proof (rule disjE) 

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

448 
using `Integral (a, b) f x1` Integral_zero Integral_unique[of a b] by auto 

449 
thus ?thesis using `a = b` `Integral (b, c) f x2` by auto 

450 
next 

451 
assume "b = c" hence "x2 = 0" 

452 
using `Integral (b, c) f x2` Integral_zero Integral_unique[of b c] by auto 

453 
thus ?thesis using `b = c` `Integral (a, b) f x1` by auto 

454 
qed 

455 
qed 

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

456 

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

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

458 

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

460 

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

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

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

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

466 
apply clarify 

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

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

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

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

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

472 
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

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

474 
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

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

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

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

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

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

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

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

482 

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

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

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

487 
> \<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31252  488 
proof  
31253  489 
have "\<forall>x\<in>{a..b}. 
15360  490 
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v  u) < d > 
31252  491 
\<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31253  492 
proof (clarsimp) 
31252  493 
fix x :: real assume "a \<le> x" and "x \<le> b" 
494 
with f' have "DERIV f x :> f'(x)" by simp 

495 
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

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

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

500 
then have strad [rule_format]: 

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

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

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

504 
proof (safe intro!: exI) 

505 
show "0 < s" by fact 

506 
next 

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

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

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

510 
by (simp add: right_diff_distrib) 

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

512 
by (rule abs_triangle_ineq) 

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

514 
by (simp add: right_diff_distrib) 

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

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

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

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

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

520 
by simp 

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

522 
qed 

523 
qed 

524 
thus ?thesis 

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

527 

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

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

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

530 
shows "fine \<delta> (a, b) D \<Longrightarrow> (\<Sum>(u, x, v)\<leftarrow>D. f v  f u) = f b  f a" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

531 
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

532 

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

533 
lemma FTC1: "[a \<le> b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
15219  534 
==> Integral(a,b) f' (f(b)  f(a))" 
31252  535 
apply (drule order_le_imp_less_or_eq, auto) 
536 
apply (auto simp add: Integral_def2) 

537 
apply (drule_tac e = "e / (b  a)" in lemma_straddle) 

538 
apply (simp add: divide_pos_pos) 

539 
apply clarify 

540 
apply (rule_tac x="g" in exI, clarify) 

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

541 
apply (clarsimp simp add: rsum_def) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

542 
apply (frule fine_listsum_eq_diff [where f=f]) 
31252  543 
apply (erule subst) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

544 
apply (subst listsum_subtractf [symmetric]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

545 
apply (rule listsum_abs [THEN order_trans]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

546 
apply (subst map_compose [symmetric, unfolded o_def]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

547 
apply (subgoal_tac "e = (\<Sum>(u, x, v)\<leftarrow>D. (e / (b  a)) * (v  u))") 
31252  548 
apply (erule ssubst) 
549 
apply (simp add: abs_minus_commute) 

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

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

551 
apply (clarify, rename_tac u x v) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

552 
apply ((drule spec)+, erule mp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

553 
apply (simp add: mem_fine mem_fine2 mem_fine3) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

554 
apply (frule fine_listsum_eq_diff [where f="\<lambda>x. x"]) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

555 
apply (simp only: split_def) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

556 
apply (subst listsum_const_mult) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

558 
done 
13958  559 

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

560 
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

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

562 

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

563 
subsection {* Additivity Theorem of Gauge Integral *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

564 

15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

565 
text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

567 
"[ 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

568 
==> Integral(a,b) (%x. f x + g x) (k1 + k2)" 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

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

571 
apply (drule_tac x = "e/2" in spec)+ 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

573 
apply (rule_tac x = "\<lambda>x. min (\<delta> x) (\<delta>' x)" in exI) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

574 
apply (rule conjI, erule (1) gauge_min) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

576 
apply (drule fine_min) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

577 
apply (drule_tac x=D in spec, simp)+ 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

578 
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

579 
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

580 
mult_2_right [symmetric] real_mult_less_iff1) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

582 

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

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

584 
"[ \<forall>x. a \<le> x & x \<le> b > f x \<le> g x; 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

586 
] ==> rsum D f \<le> rsum D g" 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

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

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

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

591 
apply (drule spec, erule mp) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

592 
apply (frule (1) mem_fine) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

593 
apply (frule (1) mem_fine2) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

595 
apply (frule (1) mem_fine) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

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

598 

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

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

600 
"[ a \<le> b; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

601 
\<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

602 
Integral(a,b) f k1; Integral(a,b) g k2 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

603 
] ==> k1 \<le> k2" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

605 
apply (rotate_tac 2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

606 
apply (drule_tac x = "\<bar>k1  k2\<bar> /2" in spec) 
15221  607 
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

608 
apply (drule gauge_min, assumption) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

609 
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

610 
apply (drule fine_min) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

611 
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

612 
apply (frule lemma_Integral_rsum_le, assumption) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

613 
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

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

615 
apply (drule add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

616 
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

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

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

619 

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

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

621 
"(\<exists>k. Integral(a,b) f k) ==> 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

623 
(\<forall>D1 D2. 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

624 
fine \<delta> (a,b) D1 & 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

626 
\<bar>rsum D1 f  rsum D2 f\<bar> < e))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

627 
apply (simp add: Integral_def, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

628 
apply (drule_tac x = "e/2" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

629 
apply (rule exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

630 
apply (frule_tac x = D1 in spec) 
31259
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

631 
apply (drule_tac x = D2 in spec) 
c1b981b71dba
encode gaugefine partitions with lists instead of functions; remove lots of unnecessary lemmas
huffman
parents:
31257
diff
changeset

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

633 
apply (thin_tac "0 < e") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

634 
apply (drule add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

635 
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

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

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

638 

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

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

640 
"Cauchy X = 
20563  641 
(\<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

642 
apply (simp add: Cauchy_iff, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

643 
apply (drule reals_Archimedean, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

645 
apply (rule_tac x = M in exI, auto) 
15360  646 
apply (drule_tac x = m in spec, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

649 

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

650 
lemma monotonic_anti_derivative: 
20792  651 
fixes f g :: "real => real" shows 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

652 
"[ 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

653 
\<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

654 
==> f b  f a \<le> g b  g a" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

655 
apply (rule Integral_le, assumption) 
15219  656 
apply (auto intro: FTC1) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

658 

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

659 
end 