author  huffman 
Mon, 25 May 2009 21:55:07 0700  
changeset 31252  5155117f9d66 
parent 30082  43c5b7bfc791 
child 31253  d54dc8956d48 
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 

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

15 
{*Partitions and tagged partitions etc.*} 
13958  16 

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

17 
partition :: "[(real*real),nat => real] => bool" where 
28562  18 
[code del]: "partition = (%(a,b) D. D 0 = a & 
15360  19 
(\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) & 
19765  20 
(\<forall>n \<ge> N. D(n) = b)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

21 

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

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

23 
psize :: "(nat => real) => nat" where 
28562  24 
[code del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) & 
19765  25 
(\<forall>n \<ge> N. D(n) = D(N)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

26 

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

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

28 
tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where 
28562  29 
[code del]:"tpart = (%(a,b) (D,p). partition(a,b) D & 
19765  30 
(\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))" 
13958  31 

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

32 
{*Gauges and gaugefine divisions*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

33 

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

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

35 
gauge :: "[real => bool, real => real] => bool" where 
28562  36 
[code del]:"gauge E g = (\<forall>x. E x > 0 < g(x))" 
13958  37 

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

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

39 
fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where 
28562  40 
[code del]:"fine = (%g (D,p). \<forall>n. n < (psize D) > D(Suc n)  D(n) < g(p n))" 
13958  41 

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

42 
{*Riemann sum*} 
13958  43 

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

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

45 
rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real" where 
19765  46 
"rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n)  D(n)))" 
13958  47 

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

48 
{*Gauge integrability (definite)*} 
13958  49 

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

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

51 
Integral :: "[(real*real),real=>real,real] => bool" where 
28562  52 
[code del]: "Integral = (%(a,b) f k. \<forall>e > 0. 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

53 
(\<exists>g. gauge(%x. a \<le> x & x \<le> b) g & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

54 
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) > 
19765  55 
\<bar>rsum(D,p) f  k\<bar> < e)))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

56 

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

57 

31252  58 
lemma Integral_def2: 
59 
"Integral = (%(a,b) f k. \<forall>e>0. (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g & 

60 
(\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) > 

61 
\<bar>rsum(D,p) f  k\<bar> \<le> e)))" 

62 
unfolding Integral_def 

63 
apply (safe intro!: ext) 

64 
apply (fast intro: less_imp_le) 

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

66 
apply force 

67 
done 

68 

29353  69 
lemma psize_unique: 
70 
assumes 1: "\<forall>n < N. D(n) < D(Suc n)" 

71 
assumes 2: "\<forall>n \<ge> N. D(n) = D(N)" 

72 
shows "psize D = N" 

73 
unfolding psize_def 

74 
proof (rule some_equality) 

75 
show "(\<forall>n<N. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>N. D(n) = D(N))" using prems .. 

76 
next 

77 
fix M assume "(\<forall>n<M. D(n) < D(Suc n)) \<and> (\<forall>n\<ge>M. D(n) = D(M))" 

78 
hence 3: "\<forall>n<M. D(n) < D(Suc n)" and 4: "\<forall>n\<ge>M. D(n) = D(M)" by fast+ 

79 
show "M = N" 

80 
proof (rule linorder_cases) 

81 
assume "M < N" 

82 
hence "D(M) < D(Suc M)" by (rule 1 [rule_format]) 

83 
also have "D(Suc M) = D(M)" by (rule 4 [rule_format], simp) 

84 
finally show "M = N" by simp 

85 
next 

86 
assume "N < M" 

87 
hence "D(N) < D(Suc N)" by (rule 3 [rule_format]) 

88 
also have "D(Suc N) = D(N)" by (rule 2 [rule_format], simp) 

89 
finally show "M = N" by simp 

90 
next 

91 
assume "M = N" thus "M = N" . 

92 
qed 

93 
qed 

94 

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

95 
lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0" 
29353  96 
by (rule psize_unique, simp_all) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

97 

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

98 
lemma partition_one [simp]: "a < b ==> psize (%n. if n = 0 then a else b) = 1" 
29353  99 
by (rule psize_unique, simp_all) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

100 

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

101 
lemma partition_single [simp]: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

102 
"a \<le> b ==> partition(a,b)(%n. if n = 0 then a else b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

103 
by (auto simp add: partition_def order_le_less) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

104 

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

105 
lemma partition_lhs: "partition(a,b) D ==> (D(0) = a)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

107 

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

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

109 
"(partition(a,b) D) = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

110 
((D 0 = a) & 
15360  111 
(\<forall>n < psize D. D n < D(Suc n)) & 
112 
(\<forall>n \<ge> psize D. D n = b))" 

29353  113 
apply (simp add: partition_def) 
114 
apply (rule iffI, clarify) 

115 
apply (subgoal_tac "psize D = N", simp) 

116 
apply (rule psize_unique, assumption, simp) 

117 
apply (simp, rule_tac x="psize D" in exI, simp) 

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

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

119 

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

120 
lemma partition_rhs: "partition(a,b) D ==> (D(psize D) = b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

122 

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

123 
lemma partition_rhs2: "[partition(a,b) D; psize D \<le> n ] ==> (D n = b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

125 

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

126 
lemma lemma_partition_lt_gen [rule_format]: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

127 
"partition(a,b) D & m + Suc d \<le> n & n \<le> (psize D) > D(m) < D(m + Suc d)" 
15251  128 
apply (induct "d", auto simp add: partition) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

129 
apply (blast dest: Suc_le_lessD intro: less_le_trans order_less_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

131 

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

132 
lemma less_eq_add_Suc: "m < n ==> \<exists>d. n = m + Suc d" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

134 

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

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

136 
"[partition(a,b) D; m < n; n \<le> (psize D)] ==> D(m) < D(n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

137 
by (auto dest: less_eq_add_Suc intro: lemma_partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

138 

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

139 
lemma partition_lt: "partition(a,b) D ==> n < (psize D) ==> D(0) < D(Suc n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

140 
apply (induct "n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

143 

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

144 
lemma partition_le: "partition(a,b) D ==> a \<le> b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

145 
apply (frule partition [THEN iffD1], safe) 
15219  146 
apply (drule_tac x = "psize D" and P="%n. psize D \<le> n > ?P n" in spec, safe) 
147 
apply (case_tac "psize D = 0") 

30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29833
diff
changeset

148 
apply (drule_tac [2] n = "psize D  Suc 0" in partition_lt, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

150 

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

151 
lemma partition_gt: "[partition(a,b) D; n < (psize D)] ==> D(n) < D(psize D)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

152 
by (auto intro: partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

153 

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

154 
lemma partition_eq: "partition(a,b) D ==> ((a = b) = (psize D = 0))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

155 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

158 
apply (rule ccontr) 
30082
43c5b7bfc791
make more proofs work whether or not One_nat_def is a simp rule
huffman
parents:
29833
diff
changeset

159 
apply (drule_tac n = "psize D  Suc 0" in partition_lt) 
15219  160 
apply auto 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

162 

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

163 
lemma partition_lb: "partition(a,b) D ==> a \<le> D(r)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

164 
apply (frule partition [THEN iffD1], safe) 
15251  165 
apply (induct "r") 
166 
apply (cut_tac [2] y = "Suc r" and x = "psize D" in linorder_le_less_linear) 

167 
apply (auto intro: partition_le) 

168 
apply (drule_tac x = r in spec) 

169 
apply arith; 

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

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

171 

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

172 
lemma partition_lb_lt: "[ partition(a,b) D; psize D ~= 0 ] ==> a < D(Suc n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

173 
apply (rule_tac t = a in partition_lhs [THEN subst], assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

174 
apply (cut_tac x = "Suc n" and y = "psize D" in linorder_le_less_linear) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

175 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

176 
apply (blast intro: partition_lt less_le_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

179 
apply (erule impE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

180 
apply (erule less_imp_le) 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

181 
apply (frule partition_rhs) 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset

182 
apply (drule partition_gt[of _ _ _ 0], arith) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

185 

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

186 
lemma partition_ub: "partition(a,b) D ==> D(r) \<le> b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

187 
apply (frule partition [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

188 
apply (cut_tac x = "psize D" and y = r in linorder_le_less_linear, safe, blast) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

189 
apply (subgoal_tac "\<forall>x. D ((psize D)  x) \<le> b") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

191 
apply (drule_tac x = "psize D  r" in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

192 
apply (subgoal_tac "psize D  (psize D  r) = r") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

196 
apply (induct_tac "x") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

197 
apply (simp (no_asm), blast) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

198 
apply (case_tac "psize D  Suc n = 0") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

199 
apply (erule_tac V = "\<forall>n. psize D \<le> n > D n = b" in thin_rl) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

201 
apply (rule order_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

202 
prefer 2 apply assumption 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

203 
apply (subgoal_tac "psize D  n = Suc (psize D  Suc n)") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

204 
prefer 2 apply arith 
20432
07ec57376051
lin_arith_prover: splitting reverted because of performance loss
webertj
parents:
20256
diff
changeset

205 
apply (drule_tac x = "psize D  Suc n" in spec, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

207 

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

208 
lemma partition_ub_lt: "[ partition(a,b) D; n < psize D ] ==> D(n) < b" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

209 
by (blast intro: partition_rhs [THEN subst] partition_gt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

210 

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

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

212 
"[ partition (a, b) D1; partition (b, c) D2 ] 
15360  213 
==> (\<forall>n < psize D1 + psize D2. 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

214 
(if n < psize D1 then D1 n else D2 (n  psize D1)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

215 
< (if Suc n < psize D1 then D1 (Suc n) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

216 
else D2 (Suc n  psize D1))) & 
15360  217 
(\<forall>n \<ge> psize D1 + psize D2. 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

218 
(if n < psize D1 then D1 n else D2 (n  psize D1)) = 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

219 
(if psize D1 + psize D2 < psize D1 then D1 (psize D1 + psize D2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

220 
else D2 (psize D1 + psize D2  psize D1)))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

221 
apply (auto intro: partition_lt_gen) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

222 
apply (subgoal_tac "psize D1 = Suc n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

223 
apply (auto intro!: partition_lt_gen simp add: partition_lhs partition_ub_lt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

224 
apply (auto intro!: partition_rhs2 simp add: partition_rhs 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

227 

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

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

229 
"[ partition (a, b) D1; partition (b, c) D2; N < psize D1 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

230 
==> D1(N) < D2 (psize D2)" 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

231 
apply (rule_tac y = "D1 (psize D1)" in order_less_le_trans) 
15219  232 
apply (erule partition_gt) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

235 

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

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

237 
"[ partition (a, b) D1; partition (b, c) D2 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

238 
==> psize (%n. if n < psize D1 then D1 n else D2 (n  psize D1)) = 
29353  239 
psize D1 + psize D2" 
240 
apply (rule psize_unique) 

241 
apply (erule (1) lemma_partition_append1 [THEN conjunct1]) 

242 
apply (erule (1) lemma_partition_append1 [THEN conjunct2]) 

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

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

244 

15219  245 
lemma tpart_eq_lhs_rhs: "[psize D = 0; tpart(a,b) (D,p)] ==> a = b" 
246 
by (auto simp add: tpart_def partition_eq) 

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

247 

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

248 
lemma tpart_partition: "tpart(a,b) (D,p) ==> partition(a,b) D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

250 

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

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

252 
"[ tpart(a,b) (D1,p1); fine(g) (D1,p1); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

253 
tpart(b,c) (D2,p2); fine(g) (D2,p2) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

254 
==> \<exists>D p. tpart(a,c) (D,p) & fine(g) (D,p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

255 
apply (rule_tac x = "%n. if n < psize D1 then D1 n else D2 (n  psize D1)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

257 
apply (rule_tac x = "%n. if n < psize D1 then p1 n else p2 (n  psize D1)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

259 
apply (case_tac "psize D1 = 0") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

260 
apply (auto dest: tpart_eq_lhs_rhs) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

263 
lemma_partition_append2 [OF tpart_partition tpart_partition]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

264 
{*But must not expand @{term fine} in other subgoals*} 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

266 
apply (subgoal_tac "psize D1 = Suc n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

268 
apply (drule tpart_partition [THEN partition_rhs]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

269 
apply (drule tpart_partition [THEN partition_lhs]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

270 
apply (auto split: nat_diff_split) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

273 
apply (subgoal_tac "psize D1 = Suc n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

276 
apply (drule partition_lhs, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

277 
apply (simp split: nat_diff_split) 
15944  278 
apply (subst partition) 
279 
apply (subst (1 2) lemma_partition_append2, assumption+) 

280 
apply (rule conjI) 

281 
apply (simp add: partition_lhs) 

282 
apply (drule lemma_partition_append1) 

283 
apply assumption; 

284 
apply (simp add: partition_rhs) 

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

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

286 

15481  287 

15219  288 
text{*We can always find a division that is fine wrt any gauge*} 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

289 

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

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

291 
"[ a \<le> b; gauge(%x. a \<le> x & x \<le> b) g ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

292 
==> \<exists>D p. tpart(a,b) (D,p) & fine g (D,p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

293 
apply (cut_tac P = "%(u,v). a \<le> u & v \<le> b > 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

294 
(\<exists>D p. tpart (u,v) (D,p) & fine (g) (D,p))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

296 
apply safe 
15219  297 
apply (blast intro: order_trans)+ 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

298 
apply (auto intro: partition_append) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

299 
apply (case_tac "a \<le> x & x \<le> b") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

300 
apply (rule_tac [2] x = 1 in exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

301 
apply (rule_tac x = "g x" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

303 
apply (rule_tac x = "%n. if n = 0 then aa else ba" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

304 
apply (rule_tac x = "%n. if n = 0 then x else ba" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

307 

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

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

309 

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

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

311 
"[ gauge(E) g1; gauge(E) g2 ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

312 
==> gauge(E) (%x. if g1(x) < g2(x) then g1(x) else g2(x))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

314 

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

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

316 
"fine (%x. if g1(x) < g2(x) then g1(x) else g2(x)) (D,p) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

317 
==> fine(g1) (D,p) & fine(g2) (D,p)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

318 
by (auto simp add: fine_def split: split_if_asm) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

319 

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

320 

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

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

322 

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

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

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

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

326 
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

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

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

329 
apply (drule_tac g = "%x. if g x < ga x then g x else ga x" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

334 
apply (subgoal_tac "\<bar>(rsum (D,p) f  k2)  (rsum (D,p) f  k1)\<bar> < \<bar>k1  k2\<bar>") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

337 
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

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

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

340 

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

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

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

343 
apply (rule_tac x = "%x. 1" in exI) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

344 
apply (auto dest: partition_eq simp add: gauge_def tpart_def rsum_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

346 

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

347 
lemma sumr_partition_eq_diff_bounds [simp]: 
15539  348 
"(\<Sum>n=0..<m. D (Suc n)  D n::real) = D(m)  D 0" 
15251  349 
by (induct "m", auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

350 

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

351 
lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b  a)" 
15219  352 
apply (auto simp add: order_le_less rsum_def Integral_def) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

353 
apply (rule_tac x = "%x. b  a" in exI) 
22998  354 
apply (auto simp add: gauge_def abs_less_iff tpart_def partition) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

356 

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

357 
lemma Integral_mult_const: "a \<le> b ==> Integral(a,b) (%x. c) (c*(b  a))" 
15219  358 
apply (auto simp add: order_le_less rsum_def Integral_def) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

359 
apply (rule_tac x = "%x. b  a" in exI) 
22998  360 
apply (auto simp add: setsum_right_distrib [symmetric] gauge_def abs_less_iff 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

361 
right_diff_distrib [symmetric] partition tpart_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

363 

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

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

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

19279  368 
apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc) 
22998  369 
apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

370 
prefer 2 apply force 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

376 
apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1]) 
16924  377 
apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

379 

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

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

381 

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

383 

16588  384 
lemma choiceP: "\<forall>x. P(x) > (\<exists>y. Q x y) ==> \<exists>f. (\<forall>x. P(x) > Q x (f x))" 
385 
by (insert bchoice [of "Collect P" Q], simp) 

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

386 

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

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

388 
lemma choice2: "\<forall>x. (\<exists>y. R(y) & (\<exists>z. Q x y z)) ==> 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

389 
\<exists>f fa. (\<forall>x. R(f x) & Q x (f x) (fa x))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

391 

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

392 

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

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

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

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

398 
apply clarify 

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

399 
apply (case_tac "0 < \<bar>z  x\<bar>") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

400 
prefer 2 apply (simp add: zero_less_abs_iff) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

405 
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

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

407 
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

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

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

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

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

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

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

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

415 

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

416 
lemma lemma_straddle: 
31252  417 
assumes f': "\<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x)" and "0 < e" 
418 
shows "\<exists>g. gauge(%x. a \<le> x & x \<le> b) g & 

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

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

420 
> \<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
31252  421 
proof  
422 
have "\<forall>x. a \<le> x & x \<le> b > 

15360  423 
(\<exists>d > 0. \<forall>u v. u \<le> x & x \<le> v & (v  u) < d > 
31252  424 
\<bar>(f(v)  f(u))  (f'(x) * (v  u))\<bar> \<le> e * (v  u))" 
425 
proof (clarify) 

426 
fix x :: real assume "a \<le> x" and "x \<le> b" 

427 
with f' have "DERIV f x :> f'(x)" by simp 

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

429 
by (simp add: DERIV_iff2 LIM_def) 

430 
with `0 < e` obtain s 

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

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

433 
then have strad [rule_format]: 

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

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

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

437 
proof (safe intro!: exI) 

438 
show "0 < s" by fact 

439 
next 

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

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

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

443 
by (simp add: right_diff_distrib) 

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

445 
by (rule abs_triangle_ineq) 

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

447 
by (simp add: right_diff_distrib) 

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

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

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

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

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

453 
by simp 

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

455 
qed 

456 
qed 

457 
thus ?thesis 

458 
by (simp add: gauge_def) (drule choiceP, auto) 

459 
qed 

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 FTC1: "[a \<le> b; \<forall>x. a \<le> x & x \<le> b > DERIV f x :> f'(x) ] 
15219  462 
==> Integral(a,b) f' (f(b)  f(a))" 
31252  463 
apply (drule order_le_imp_less_or_eq, auto) 
464 
apply (auto simp add: Integral_def2) 

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

466 
apply (simp add: divide_pos_pos) 

467 
apply clarify 

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

469 
apply (clarsimp simp add: tpart_def rsum_def) 

470 
apply (subgoal_tac "(\<Sum>n=0..<psize D. f(D(Suc n))  f(D n)) = f b  f a") 

471 
prefer 2 

472 
apply (cut_tac D = "%n. f (D n)" and m = "psize D" 

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

473 
in sumr_partition_eq_diff_bounds) 
31252  474 
apply (simp add: partition_lhs partition_rhs) 
475 
apply (erule subst) 

476 
apply (subst setsum_subtractf [symmetric]) 

477 
apply (rule setsum_abs [THEN order_trans]) 

478 
apply (subgoal_tac "e = (\<Sum>n=0..<psize D. (e / (b  a)) * (D (Suc n)  (D n)))") 

479 
apply (erule ssubst) 

480 
apply (simp add: abs_minus_commute) 

481 
apply (rule setsum_mono) 

482 
apply (simp add: partition_lb partition_ub fine_def) 

483 
apply (subst setsum_right_distrib [symmetric]) 

484 
apply (subst sumr_partition_eq_diff_bounds) 

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

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

486 
done 
13958  487 

488 

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

489 
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

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

491 

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

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

493 
"[ a \<le> b; b \<le> c; Integral(a,b) f' k1; Integral(b,c) f' k2; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

494 
\<forall>x. a \<le> x & x \<le> c > DERIV f x :> f' x ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

495 
==> Integral(a,c) f' (k1 + k2)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

496 
apply (rule FTC1 [THEN Integral_subst], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

497 
apply (frule FTC1, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

498 
apply (frule_tac a = b in FTC1, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

500 
apply (drule_tac ?k2.0 = "f b  f a" in Integral_unique) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

501 
apply (drule_tac [3] ?k2.0 = "f c  f b" in Integral_unique, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

503 

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

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

505 
"partition(a,b) D ==> psize D = (LEAST n. D(n) = b)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

506 
apply (auto intro!: Least_equality [symmetric] partition_rhs) 
15219  507 
apply (auto dest: partition_ub_lt simp add: linorder_not_less [symmetric]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

509 

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

510 
lemma lemma_partition_bounded: "partition (a, c) D ==> ~ (\<exists>n. c < D(n))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

514 

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

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

516 
"partition (a, c) D ==> D = (%n. if D n < c then D n else c)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

518 
apply (auto dest!: lemma_partition_bounded) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

521 

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

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

523 
"partition (a, c) D ==> D = (%n. if D n \<le> c then D n else c)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

525 
apply (auto dest!: lemma_partition_bounded) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

526 
apply (drule_tac x = n in spec, auto) 
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 partition_lt_Suc: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

530 
"[ partition(a,b) D; n < psize D ] ==> D n < D (Suc n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

532 

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

533 
lemma tpart_tag_eq: "tpart(a,c) (D,p) ==> p = (%n. if D n < c then p n else c)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

534 
apply (rule ext) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

536 
apply (drule linorder_not_less [THEN iffD1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

537 
apply (drule_tac r = "Suc n" in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

540 

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

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

542 

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

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

544 
"[ a \<le> D n; D n < b; partition(a,b) D ] ==> n < psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

545 
by (auto simp add: partition linorder_not_less [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

546 

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

547 
lemma lemma_additivity2: "[ a \<le> D n; partition(a,D n) D ] ==> psize D \<le> n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

548 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

549 
apply (frule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

550 
apply (frule_tac r = "Suc n" in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

551 
apply (auto dest!: spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

553 

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

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

555 
"[ partition(a,b) D; psize D < m ] ==> D(m) = D(psize D)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

557 

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

558 
lemma partition_ub2: "[ partition(a,b) D; psize D < m ] ==> D(r) \<le> D(m)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

560 

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

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

562 
"[ tpart(a,b) (D,p); psize D \<le> m ] ==> p(m) = D(m)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

567 

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

568 
lemma partition_lt_cancel: "[ partition(a,b) D; D m < D n ] ==> m < n" 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
23315
diff
changeset

569 
apply (cut_tac less_linear [of n "psize D"], auto) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
23315
diff
changeset

570 
apply (cut_tac less_linear [of m n]) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
23315
diff
changeset

571 
apply (cut_tac less_linear [of m "psize D"]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

572 
apply (auto dest: partition_gt) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

574 
apply (frule partition_eq_bound) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

575 
apply (drule_tac [2] partition_gt, auto) 
29811
026b0f9f579f
fixed Proofs and dependencies ; Theory Dense_Linear_Order moved to Library
chaieb@chaieblaptop
parents:
29469
diff
changeset

576 
apply (metis linear not_less partition_rhs partition_rhs2) 
29833  577 
apply (metis lemma_additivity1 order_less_trans partition_eq_bound partition_lb partition_rhs) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

579 

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

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

581 
"[ a \<le> D n; D n < b; partition (a, b) D ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

582 
==> psize (%x. if D x < D n then D(x) else D n) = n" 
29353  583 
apply (frule (2) lemma_additivity1) 
584 
apply (rule psize_unique, auto) 

585 
apply (erule partition_lt_Suc, erule (1) less_trans) 

586 
apply (erule notE) 

587 
apply (erule (1) partition_lt_gen, erule less_imp_le) 

588 
apply (drule (1) partition_lt_cancel, simp) 

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

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

590 

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

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

592 
"partition (a, b) D 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

593 
==> psize (%x. if D x < D n then D(x) else D n) \<le> psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

594 
apply (frule_tac r = n in partition_ub) 
15219  595 
apply (drule_tac x = "D n" in order_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

596 
apply (auto simp add: lemma_partition_eq [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

597 
apply (frule_tac r = n in partition_lb) 
15219  598 
apply (drule (2) lemma_additivity4_psize_eq) 
599 
apply (rule ccontr, auto) 

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

600 
apply (frule_tac not_leE [THEN [2] partition_eq_bound]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

603 

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

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

605 
"[ partition(a,b) D; na < psize (%x. if D x < D n then D(x) else D n) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

606 
==> na < psize D" 
15219  607 
by (erule lemma_psize_left_less_psize [THEN [2] less_le_trans]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

608 

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

609 

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

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

611 
"[ partition(a,b) D; D na < D n; D n < D (Suc na); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

612 
n < psize D ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

613 
==> False" 
24742
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
23315
diff
changeset

614 
by (metis not_less_eq partition_lt_cancel real_of_nat_less_iff) 
73b8b42a36b6
removal of some "ref"s from res_axioms.ML; a sideeffect is that the ordering
paulson
parents:
23315
diff
changeset

615 

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

616 

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

617 
lemma psize_const [simp]: "psize (%x. k) = 0" 
15219  618 
by (auto simp add: psize_def) 
15093
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 lemma_additivity3a: 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

621 
"[ partition(a,b) D; D na < D n; D n < D (Suc na); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

622 
na < psize D ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

623 
==> False" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

624 
apply (frule_tac m = n in partition_lt_cancel) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

625 
apply (auto intro: lemma_additivity3) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

627 

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

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

629 
"[ partition(a,b) D; D n < b ] ==> psize (%x. D (x + n)) \<le> psize D  n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

630 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

631 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

632 
apply (simp add: partition less_diff_conv) 
15219  633 
apply (simp add: le_diff_conv partition_rhs2 split: nat_diff_split) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

635 
apply (frule partition_rhs, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

636 
apply (frule partition_lt_cancel, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

637 
apply (drule partition [THEN iffD1], safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

638 
apply (subgoal_tac "~ D (psize D  n + n) < D (Suc (psize D  n + n))") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

640 
apply (drule_tac x = "Suc (psize D)" and P="%n. ?P n \<longrightarrow> D n = D (psize D)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

641 
in spec) 
15219  642 
apply simp 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

644 

15219  645 
lemma psize_le_n: "partition (a, D n) D ==> psize D \<le> n" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

646 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

647 
apply (frule partition_lt_Suc, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

648 
apply (frule_tac r = "Suc n" in partition_ub, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

650 

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

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

652 
"partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D  n" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

653 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

654 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

657 
apply (case_tac "psize D \<le> n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

658 
apply (force intro: partition_rhs2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

660 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

661 
apply (frule psize_le_n) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

662 
apply (drule_tac x = "psize D  n" in spec, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

663 
apply (drule partition [THEN iffD1], safe) 
15219  664 
apply (drule_tac x = "Suc n" and P="%na. ?s \<le> na \<longrightarrow> D na = D n" in spec, auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

666 

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

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

668 
"partition(a,b) D ==> psize (%x. D (x + n)) \<le> psize D  n" 
15219  669 
apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

670 
apply (blast intro: better_lemma_psize_right_eq1a better_lemma_psize_right_eq1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

672 

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

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

674 
"[ partition(a,b) D; D n < b ] ==> psize (%x. D (x + n)) \<le> psize D" 
15219  675 
apply (simp add: psize_def [of "(%x. D (x + n))"]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

676 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

678 
apply (subgoal_tac "n \<le> psize D") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

680 
apply (rule ccontr, drule not_leE) 
15219  681 
apply (drule_tac less_imp_le [THEN [2] partition_rhs2], assumption, simp) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

685 

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

686 
(* should be combined with previous theorem; also proof has redundancy *) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

688 
"partition(a,D n) D ==> psize (%x. D (x + n)) \<le> psize D" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

689 
apply (simp add: psize_def [of "(%x. D (x + n))"]); 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

690 
apply (rule_tac a = "psize D  n" in someI2, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

692 
apply (case_tac "psize D \<le> n") 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

693 
apply (force intro: partition_rhs2 simp add: le_diff_conv) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

695 
apply (rule ccontr, drule not_leE) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

699 

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

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

701 
"[ partition(a,b) D ] ==> psize (%x. D (x + n)) \<le> psize D" 
15219  702 
apply (frule_tac r1 = n in partition_ub [THEN order_le_imp_less_or_eq]) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

703 
apply (blast intro: lemma_psize_right_eq1a lemma_psize_right_eq1) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

705 

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

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

707 
"[ a \<le> D n; tpart (a, b) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

708 
==> tpart(a, D n) (%x. if D x < D n then D(x) else D n, 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

709 
%x. if D x < D n then p(x) else D n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

710 
apply (frule_tac r = n in tpart_partition [THEN partition_ub]) 
15219  711 
apply (drule_tac x = "D n" in order_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

712 
apply (auto simp add: tpart_partition [THEN lemma_partition_eq, symmetric] tpart_tag_eq [symmetric]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

713 
apply (frule_tac tpart_partition [THEN [3] lemma_additivity1]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

714 
apply (auto simp add: tpart_def) 
15219  715 
apply (drule_tac [2] linorder_not_less [THEN iffD1, THEN order_le_imp_less_or_eq], auto) 
716 
prefer 3 apply (drule_tac x=na in spec, arith) 

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

717 
prefer 2 apply (blast dest: lemma_additivity3) 
15219  718 
apply (frule (2) lemma_additivity4_psize_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

719 
apply (rule partition [THEN iffD2]) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

720 
apply (frule partition [THEN iffD1]) 
15219  721 
apply safe 
722 
apply (auto simp add: partition_lt_gen) 

15197  723 
apply (drule (1) partition_lt_cancel, arith) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

725 

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

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

727 
"[ a \<le> D n; tpart (a, b) (D, p); gauge (%x. a \<le> x & x \<le> D n) g; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

728 
fine (%x. if x < D n then min (g x) ((D n  x)/ 2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

729 
else if x = D n then min (g (D n)) (ga (D n)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

730 
else min (ga x) ((x  D n)/ 2)) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

731 
==> fine g 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

732 
(%x. if D x < D n then D(x) else D n, 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

733 
%x. if D x < D n then p(x) else D n)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

734 
apply (auto simp add: fine_def tpart_def gauge_def) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

735 
apply (frule_tac [!] na=na in lemma_psize_left_less_psize2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

738 
apply (auto dest: lemma_additivity3a simp add: split_if_asm) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

740 

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

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

742 
"[ a \<le> D n; tpart (a, b) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

743 
==> tpart(D n, b) (%x. D(x + n),%x. p(x + n))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

744 
apply (simp add: tpart_def partition_def, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

745 
apply (rule_tac x = "N  n" in exI, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

747 

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

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

749 
"[ a \<le> D n; tpart (a, b) (D, p); gauge (%x. D n \<le> x & x \<le> b) ga; 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

750 
fine (%x. if x < D n then min (g x) ((D n  x)/ 2) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

751 
else if x = D n then min (g (D n)) (ga (D n)) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

752 
else min (ga x) ((x  D n)/ 2)) (D, p) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

753 
==> fine ga (%x. D(x + n),%x. p(x + n))" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

755 
apply (drule_tac x = "na + n" in spec) 
20217
25b068a99d2b
linear arithmetic splits certain operators (e.g. min, max, abs)
webertj
parents:
19765
diff
changeset

756 
apply (frule_tac n = n in tpart_partition [THEN better_lemma_psize_right_eq], auto) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

757 
apply (simp add: tpart_def, safe) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

758 
apply (subgoal_tac "D n \<le> p (na + n)") 
15219  759 
apply (drule_tac y = "p (na + n)" in order_le_imp_less_or_eq) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

761 
apply (simp split: split_if_asm, simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

764 
apply (drule_tac x = "na + n" in spec, safe) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

765 
apply (rule_tac y="D (na + n)" in order_trans) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

766 
apply (case_tac "na = 0", auto) 
23315  767 
apply (erule partition_lt_gen [THEN order_less_imp_le]) 
768 
apply arith 

769 
apply arith 

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

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

771 

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

772 
lemma rsum_add: "rsum (D, p) (%x. f x + g x) = rsum (D, p) f + rsum(D, p) g" 
15536  773 
by (simp add: rsum_def setsum_addf left_distrib) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

774 

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

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

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

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

778 
==> Integral(a,b) (%x. f x + g x) (k1 + k2)" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

782 
apply (drule gauge_min, assumption) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

783 
apply (rule_tac x = " (%x. if ga x < gaa x then ga x else gaa x)" in exI) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

787 
apply (drule_tac a = "\<bar>rsum (D, p) f  k1\<bar> * 2" and c = "\<bar>rsum (D, p) g  k2\<bar> * 2" in add_strict_mono, assumption) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

788 
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

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

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

791 

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

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

793 
"[ partition(a,b) D; r < psize D ] ==> 0 < D (Suc r)  D r" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

795 

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

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

797 
"[ \<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

798 
tpart(a,b) (D,p) 
15360  799 
] ==> \<forall>n \<le> psize D. f (p n) \<le> g (p n)" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

801 
apply (auto, frule partition [THEN iffD1], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

803 
apply (case_tac "n = 0", simp) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

804 
apply (rule partition_lt_gen [THEN order_less_le_trans, THEN order_less_imp_le], auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

805 
apply (drule le_imp_less_or_eq, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

806 
apply (drule_tac [2] x = "psize D" in spec, auto) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

807 
apply (drule_tac r = "Suc n" in partition_ub) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

810 

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

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

812 
"[ \<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

813 
tpart(a,b) (D,p) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

814 
] ==> rsum(D,p) f \<le> rsum(D,p) g" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

815 
apply (simp add: rsum_def) 
15539  816 
apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2] 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

817 
dest!: lemma_Integral_le) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

819 

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

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

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

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

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

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

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

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

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

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

830 
apply (drule_tac g = "%x. if ga x < gaa x then ga x else gaa x" 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

835 
apply (frule lemma_Integral_rsum_le, assumption) 
15094
a7d1a3fdc30d
conversion of Hyperreal/{Fact,Filter} to Isar scripts
paulson
parents:
15093
diff
changeset

836 
apply (subgoal_tac "\<bar>(rsum (D,p) f  k1)  (rsum (D,p) g  k2)\<bar> < \<bar>k1  k2\<bar>") 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

839 
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

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

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

842 

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

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

844 
"(\<exists>k. Integral(a,b) f k) ==> 
15360  845 
(\<forall>e > 0. \<exists>g. gauge (%x. a \<le> x & x \<le> b) g & 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

846 
(\<forall>D1 D2 p1 p2. 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

847 
tpart(a,b) (D1, p1) & fine g (D1,p1) & 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

848 
tpart(a,b) (D2, p2) & fine g (D2,p2) > 
15360  849 
\<bar>rsum(D1,p1) f  rsum(D2,p2) f\<bar> < e))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

853 
apply (frule_tac x = D1 in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

854 
apply (frule_tac x = D2 in spec) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

856 
apply (erule_tac V = "0 < e" in thin_rl) 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

858 
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

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

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

861 

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

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

863 
"Cauchy X = 
20563  864 
(\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m  X n\<bar> < inverse(real (Suc j))))" 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

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

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

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

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

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

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

872 

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

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

874 
"[ a \<le> b; \<forall>n. gauge (%x. a \<le> x & x \<le> b) (fa n) ] 
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

875 
==> \<forall>n. \<exists>D p. tpart (a, b) (D, p) & fine (fa n) (D, p)" 
15219  876 
by (blast dest: partition_exists) 
15093
49ede01e9ee6
conversion of Integration and NSPrimes to Isar scripts
paulson
parents:
13958
diff
changeset

877 

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

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

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

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

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

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

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

886 

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

887 
end 