author  blanchet 
Thu, 28 Aug 2014 00:40:38 +0200  
changeset 58061  3d060f43accb 
parent 58055  625bdd5c70b2 
child 58097  cfd3cff9387b 
permissions  rwrr 
51523  1 
(* Title: HOL/Real.thy 
2 
Author: Jacques D. Fleuriot, University of Edinburgh, 1998 

3 
Author: Larry Paulson, University of Cambridge 

4 
Author: Jeremy Avigad, Carnegie Mellon University 

5 
Author: Florian Zuleger, Johannes Hoelzl, and Simon Funke, TU Muenchen 

6 
Conversion to Isar and new proofs by Lawrence C Paulson, 2003/4 

7 
Construction of Cauchy Reals by Brian Huffman, 2010 

8 
*) 

9 

10 
header {* Development of the Reals using Cauchy Sequences *} 

11 

12 
theory Real 

51773  13 
imports Rat Conditionally_Complete_Lattices 
51523  14 
begin 
15 

16 
text {* 

17 
This theory contains a formalization of the real numbers as 

18 
equivalence classes of Cauchy sequences of rationals. See 

19 
@{file "~~/src/HOL/ex/Dedekind_Real.thy"} for an alternative 

20 
construction using Dedekind cuts. 

21 
*} 

22 

23 
subsection {* Preliminary lemmas *} 

24 

25 
lemma add_diff_add: 

26 
fixes a b c d :: "'a::ab_group_add" 

27 
shows "(a + c)  (b + d) = (a  b) + (c  d)" 

28 
by simp 

29 

30 
lemma minus_diff_minus: 

31 
fixes a b :: "'a::ab_group_add" 

32 
shows " a   b =  (a  b)" 

33 
by simp 

34 

35 
lemma mult_diff_mult: 

36 
fixes x y a b :: "'a::ring" 

37 
shows "(x * y  a * b) = x * (y  b) + (x  a) * b" 

38 
by (simp add: algebra_simps) 

39 

40 
lemma inverse_diff_inverse: 

41 
fixes a b :: "'a::division_ring" 

42 
assumes "a \<noteq> 0" and "b \<noteq> 0" 

43 
shows "inverse a  inverse b =  (inverse a * (a  b) * inverse b)" 

44 
using assms by (simp add: algebra_simps) 

45 

46 
lemma obtain_pos_sum: 

47 
fixes r :: rat assumes r: "0 < r" 

48 
obtains s t where "0 < s" and "0 < t" and "r = s + t" 

49 
proof 

50 
from r show "0 < r/2" by simp 

51 
from r show "0 < r/2" by simp 

52 
show "r = r/2 + r/2" by simp 

53 
qed 

54 

55 
subsection {* Sequences that converge to zero *} 

56 

57 
definition 

58 
vanishes :: "(nat \<Rightarrow> rat) \<Rightarrow> bool" 

59 
where 

60 
"vanishes X = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r)" 

61 

62 
lemma vanishesI: "(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r) \<Longrightarrow> vanishes X" 

63 
unfolding vanishes_def by simp 

64 

65 
lemma vanishesD: "\<lbrakk>vanishes X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. \<bar>X n\<bar> < r" 

66 
unfolding vanishes_def by simp 

67 

68 
lemma vanishes_const [simp]: "vanishes (\<lambda>n. c) \<longleftrightarrow> c = 0" 

69 
unfolding vanishes_def 

70 
apply (cases "c = 0", auto) 

71 
apply (rule exI [where x="\<bar>c\<bar>"], auto) 

72 
done 

73 

74 
lemma vanishes_minus: "vanishes X \<Longrightarrow> vanishes (\<lambda>n.  X n)" 

75 
unfolding vanishes_def by simp 

76 

77 
lemma vanishes_add: 

78 
assumes X: "vanishes X" and Y: "vanishes Y" 

79 
shows "vanishes (\<lambda>n. X n + Y n)" 

80 
proof (rule vanishesI) 

81 
fix r :: rat assume "0 < r" 

82 
then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 

83 
by (rule obtain_pos_sum) 

84 
obtain i where i: "\<forall>n\<ge>i. \<bar>X n\<bar> < s" 

85 
using vanishesD [OF X s] .. 

86 
obtain j where j: "\<forall>n\<ge>j. \<bar>Y n\<bar> < t" 

87 
using vanishesD [OF Y t] .. 

88 
have "\<forall>n\<ge>max i j. \<bar>X n + Y n\<bar> < r" 

89 
proof (clarsimp) 

90 
fix n assume n: "i \<le> n" "j \<le> n" 

91 
have "\<bar>X n + Y n\<bar> \<le> \<bar>X n\<bar> + \<bar>Y n\<bar>" by (rule abs_triangle_ineq) 

92 
also have "\<dots> < s + t" by (simp add: add_strict_mono i j n) 

93 
finally show "\<bar>X n + Y n\<bar> < r" unfolding r . 

94 
qed 

95 
thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n + Y n\<bar> < r" .. 

96 
qed 

97 

98 
lemma vanishes_diff: 

99 
assumes X: "vanishes X" and Y: "vanishes Y" 

100 
shows "vanishes (\<lambda>n. X n  Y n)" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

101 
unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y) 
51523  102 

103 
lemma vanishes_mult_bounded: 

104 
assumes X: "\<exists>a>0. \<forall>n. \<bar>X n\<bar> < a" 

105 
assumes Y: "vanishes (\<lambda>n. Y n)" 

106 
shows "vanishes (\<lambda>n. X n * Y n)" 

107 
proof (rule vanishesI) 

108 
fix r :: rat assume r: "0 < r" 

109 
obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a" 

110 
using X by fast 

111 
obtain b where b: "0 < b" "r = a * b" 

112 
proof 

56541  113 
show "0 < r / a" using r a by simp 
51523  114 
show "r = a * (r / a)" using a by simp 
115 
qed 

116 
obtain k where k: "\<forall>n\<ge>k. \<bar>Y n\<bar> < b" 

117 
using vanishesD [OF Y b(1)] .. 

118 
have "\<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" 

119 
by (simp add: b(2) abs_mult mult_strict_mono' a k) 

120 
thus "\<exists>k. \<forall>n\<ge>k. \<bar>X n * Y n\<bar> < r" .. 

121 
qed 

122 

123 
subsection {* Cauchy sequences *} 

124 

125 
definition 

126 
cauchy :: "(nat \<Rightarrow> rat) \<Rightarrow> bool" 

127 
where 

128 
"cauchy X \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m  X n\<bar> < r)" 

129 

130 
lemma cauchyI: 

131 
"(\<And>r. 0 < r \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m  X n\<bar> < r) \<Longrightarrow> cauchy X" 

132 
unfolding cauchy_def by simp 

133 

134 
lemma cauchyD: 

135 
"\<lbrakk>cauchy X; 0 < r\<rbrakk> \<Longrightarrow> \<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m  X n\<bar> < r" 

136 
unfolding cauchy_def by simp 

137 

138 
lemma cauchy_const [simp]: "cauchy (\<lambda>n. x)" 

139 
unfolding cauchy_def by simp 

140 

141 
lemma cauchy_add [simp]: 

142 
assumes X: "cauchy X" and Y: "cauchy Y" 

143 
shows "cauchy (\<lambda>n. X n + Y n)" 

144 
proof (rule cauchyI) 

145 
fix r :: rat assume "0 < r" 

146 
then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 

147 
by (rule obtain_pos_sum) 

148 
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m  X n\<bar> < s" 

149 
using cauchyD [OF X s] .. 

150 
obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m  Y n\<bar> < t" 

151 
using cauchyD [OF Y t] .. 

152 
have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>(X m + Y m)  (X n + Y n)\<bar> < r" 

153 
proof (clarsimp) 

154 
fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n" 

155 
have "\<bar>(X m + Y m)  (X n + Y n)\<bar> \<le> \<bar>X m  X n\<bar> + \<bar>Y m  Y n\<bar>" 

156 
unfolding add_diff_add by (rule abs_triangle_ineq) 

157 
also have "\<dots> < s + t" 

158 
by (rule add_strict_mono, simp_all add: i j *) 

159 
finally show "\<bar>(X m + Y m)  (X n + Y n)\<bar> < r" unfolding r . 

160 
qed 

161 
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>(X m + Y m)  (X n + Y n)\<bar> < r" .. 

162 
qed 

163 

164 
lemma cauchy_minus [simp]: 

165 
assumes X: "cauchy X" 

166 
shows "cauchy (\<lambda>n.  X n)" 

167 
using assms unfolding cauchy_def 

168 
unfolding minus_diff_minus abs_minus_cancel . 

169 

170 
lemma cauchy_diff [simp]: 

171 
assumes X: "cauchy X" and Y: "cauchy Y" 

172 
shows "cauchy (\<lambda>n. X n  Y n)" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

173 
using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff) 
51523  174 

175 
lemma cauchy_imp_bounded: 

176 
assumes "cauchy X" shows "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b" 

177 
proof  

178 
obtain k where k: "\<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m  X n\<bar> < 1" 

179 
using cauchyD [OF assms zero_less_one] .. 

180 
show "\<exists>b>0. \<forall>n. \<bar>X n\<bar> < b" 

181 
proof (intro exI conjI allI) 

182 
have "0 \<le> \<bar>X 0\<bar>" by simp 

183 
also have "\<bar>X 0\<bar> \<le> Max (abs ` X ` {..k})" by simp 

184 
finally have "0 \<le> Max (abs ` X ` {..k})" . 

185 
thus "0 < Max (abs ` X ` {..k}) + 1" by simp 

186 
next 

187 
fix n :: nat 

188 
show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" 

189 
proof (rule linorder_le_cases) 

190 
assume "n \<le> k" 

191 
hence "\<bar>X n\<bar> \<le> Max (abs ` X ` {..k})" by simp 

192 
thus "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" by simp 

193 
next 

194 
assume "k \<le> n" 

195 
have "\<bar>X n\<bar> = \<bar>X k + (X n  X k)\<bar>" by simp 

196 
also have "\<bar>X k + (X n  X k)\<bar> \<le> \<bar>X k\<bar> + \<bar>X n  X k\<bar>" 

197 
by (rule abs_triangle_ineq) 

198 
also have "\<dots> < Max (abs ` X ` {..k}) + 1" 

199 
by (rule add_le_less_mono, simp, simp add: k `k \<le> n`) 

200 
finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" . 

201 
qed 

202 
qed 

203 
qed 

204 

205 
lemma cauchy_mult [simp]: 

206 
assumes X: "cauchy X" and Y: "cauchy Y" 

207 
shows "cauchy (\<lambda>n. X n * Y n)" 

208 
proof (rule cauchyI) 

209 
fix r :: rat assume "0 < r" 

210 
then obtain u v where u: "0 < u" and v: "0 < v" and "r = u + v" 

211 
by (rule obtain_pos_sum) 

212 
obtain a where a: "0 < a" "\<forall>n. \<bar>X n\<bar> < a" 

213 
using cauchy_imp_bounded [OF X] by fast 

214 
obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b" 

215 
using cauchy_imp_bounded [OF Y] by fast 

216 
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b" 

217 
proof 

56541  218 
show "0 < v/b" using v b(1) by simp 
219 
show "0 < u/a" using u a(1) by simp 

51523  220 
show "r = a * (u/a) + (v/b) * b" 
221 
using a(1) b(1) `r = u + v` by simp 

222 
qed 

223 
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m  X n\<bar> < s" 

224 
using cauchyD [OF X s] .. 

225 
obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>Y m  Y n\<bar> < t" 

226 
using cauchyD [OF Y t] .. 

227 
have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>X m * Y m  X n * Y n\<bar> < r" 

228 
proof (clarsimp) 

229 
fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n" 

230 
have "\<bar>X m * Y m  X n * Y n\<bar> = \<bar>X m * (Y m  Y n) + (X m  X n) * Y n\<bar>" 

231 
unfolding mult_diff_mult .. 

232 
also have "\<dots> \<le> \<bar>X m * (Y m  Y n)\<bar> + \<bar>(X m  X n) * Y n\<bar>" 

233 
by (rule abs_triangle_ineq) 

234 
also have "\<dots> = \<bar>X m\<bar> * \<bar>Y m  Y n\<bar> + \<bar>X m  X n\<bar> * \<bar>Y n\<bar>" 

235 
unfolding abs_mult .. 

236 
also have "\<dots> < a * t + s * b" 

237 
by (simp_all add: add_strict_mono mult_strict_mono' a b i j *) 

238 
finally show "\<bar>X m * Y m  X n * Y n\<bar> < r" unfolding r . 

239 
qed 

240 
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>X m * Y m  X n * Y n\<bar> < r" .. 

241 
qed 

242 

243 
lemma cauchy_not_vanishes_cases: 

244 
assumes X: "cauchy X" 

245 
assumes nz: "\<not> vanishes X" 

246 
shows "\<exists>b>0. \<exists>k. (\<forall>n\<ge>k. b <  X n) \<or> (\<forall>n\<ge>k. b < X n)" 

247 
proof  

248 
obtain r where "0 < r" and r: "\<forall>k. \<exists>n\<ge>k. r \<le> \<bar>X n\<bar>" 

249 
using nz unfolding vanishes_def by (auto simp add: not_less) 

250 
obtain s t where s: "0 < s" and t: "0 < t" and "r = s + t" 

251 
using `0 < r` by (rule obtain_pos_sum) 

252 
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m  X n\<bar> < s" 

253 
using cauchyD [OF X s] .. 

254 
obtain k where "i \<le> k" and "r \<le> \<bar>X k\<bar>" 

255 
using r by fast 

256 
have k: "\<forall>n\<ge>k. \<bar>X n  X k\<bar> < s" 

257 
using i `i \<le> k` by auto 

258 
have "X k \<le>  r \<or> r \<le> X k" 

259 
using `r \<le> \<bar>X k\<bar>` by auto 

260 
hence "(\<forall>n\<ge>k. t <  X n) \<or> (\<forall>n\<ge>k. t < X n)" 

261 
unfolding `r = s + t` using k by auto 

262 
hence "\<exists>k. (\<forall>n\<ge>k. t <  X n) \<or> (\<forall>n\<ge>k. t < X n)" .. 

263 
thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t <  X n) \<or> (\<forall>n\<ge>k. t < X n)" 

264 
using t by auto 

265 
qed 

266 

267 
lemma cauchy_not_vanishes: 

268 
assumes X: "cauchy X" 

269 
assumes nz: "\<not> vanishes X" 

270 
shows "\<exists>b>0. \<exists>k. \<forall>n\<ge>k. b < \<bar>X n\<bar>" 

271 
using cauchy_not_vanishes_cases [OF assms] 

272 
by clarify (rule exI, erule conjI, rule_tac x=k in exI, auto) 

273 

274 
lemma cauchy_inverse [simp]: 

275 
assumes X: "cauchy X" 

276 
assumes nz: "\<not> vanishes X" 

277 
shows "cauchy (\<lambda>n. inverse (X n))" 

278 
proof (rule cauchyI) 

279 
fix r :: rat assume "0 < r" 

280 
obtain b i where b: "0 < b" and i: "\<forall>n\<ge>i. b < \<bar>X n\<bar>" 

281 
using cauchy_not_vanishes [OF X nz] by fast 

282 
from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto 

283 
obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b" 

284 
proof 

56544  285 
show "0 < b * r * b" by (simp add: `0 < r` b) 
51523  286 
show "r = inverse b * (b * r * b) * inverse b" 
287 
using b by simp 

288 
qed 

289 
obtain j where j: "\<forall>m\<ge>j. \<forall>n\<ge>j. \<bar>X m  X n\<bar> < s" 

290 
using cauchyD [OF X s] .. 

291 
have "\<forall>m\<ge>max i j. \<forall>n\<ge>max i j. \<bar>inverse (X m)  inverse (X n)\<bar> < r" 

292 
proof (clarsimp) 

293 
fix m n assume *: "i \<le> m" "j \<le> m" "i \<le> n" "j \<le> n" 

294 
have "\<bar>inverse (X m)  inverse (X n)\<bar> = 

295 
inverse \<bar>X m\<bar> * \<bar>X m  X n\<bar> * inverse \<bar>X n\<bar>" 

296 
by (simp add: inverse_diff_inverse nz * abs_mult) 

297 
also have "\<dots> < inverse b * s * inverse b" 

298 
by (simp add: mult_strict_mono less_imp_inverse_less 

56544  299 
i j b * s) 
51523  300 
finally show "\<bar>inverse (X m)  inverse (X n)\<bar> < r" unfolding r . 
301 
qed 

302 
thus "\<exists>k. \<forall>m\<ge>k. \<forall>n\<ge>k. \<bar>inverse (X m)  inverse (X n)\<bar> < r" .. 

303 
qed 

304 

305 
lemma vanishes_diff_inverse: 

306 
assumes X: "cauchy X" "\<not> vanishes X" 

307 
assumes Y: "cauchy Y" "\<not> vanishes Y" 

308 
assumes XY: "vanishes (\<lambda>n. X n  Y n)" 

309 
shows "vanishes (\<lambda>n. inverse (X n)  inverse (Y n))" 

310 
proof (rule vanishesI) 

311 
fix r :: rat assume r: "0 < r" 

312 
obtain a i where a: "0 < a" and i: "\<forall>n\<ge>i. a < \<bar>X n\<bar>" 

313 
using cauchy_not_vanishes [OF X] by fast 

314 
obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>" 

315 
using cauchy_not_vanishes [OF Y] by fast 

316 
obtain s where s: "0 < s" and "inverse a * s * inverse b = r" 

317 
proof 

318 
show "0 < a * r * b" 

56544  319 
using a r b by simp 
51523  320 
show "inverse a * (a * r * b) * inverse b = r" 
321 
using a r b by simp 

322 
qed 

323 
obtain k where k: "\<forall>n\<ge>k. \<bar>X n  Y n\<bar> < s" 

324 
using vanishesD [OF XY s] .. 

325 
have "\<forall>n\<ge>max (max i j) k. \<bar>inverse (X n)  inverse (Y n)\<bar> < r" 

326 
proof (clarsimp) 

327 
fix n assume n: "i \<le> n" "j \<le> n" "k \<le> n" 

328 
have "X n \<noteq> 0" and "Y n \<noteq> 0" 

329 
using i j a b n by auto 

330 
hence "\<bar>inverse (X n)  inverse (Y n)\<bar> = 

331 
inverse \<bar>X n\<bar> * \<bar>X n  Y n\<bar> * inverse \<bar>Y n\<bar>" 

332 
by (simp add: inverse_diff_inverse abs_mult) 

333 
also have "\<dots> < inverse a * s * inverse b" 

334 
apply (intro mult_strict_mono' less_imp_inverse_less) 

56536  335 
apply (simp_all add: a b i j k n) 
51523  336 
done 
337 
also note `inverse a * s * inverse b = r` 

338 
finally show "\<bar>inverse (X n)  inverse (Y n)\<bar> < r" . 

339 
qed 

340 
thus "\<exists>k. \<forall>n\<ge>k. \<bar>inverse (X n)  inverse (Y n)\<bar> < r" .. 

341 
qed 

342 

343 
subsection {* Equivalence relation on Cauchy sequences *} 

344 

345 
definition realrel :: "(nat \<Rightarrow> rat) \<Rightarrow> (nat \<Rightarrow> rat) \<Rightarrow> bool" 

346 
where "realrel = (\<lambda>X Y. cauchy X \<and> cauchy Y \<and> vanishes (\<lambda>n. X n  Y n))" 

347 

348 
lemma realrelI [intro?]: 

349 
assumes "cauchy X" and "cauchy Y" and "vanishes (\<lambda>n. X n  Y n)" 

350 
shows "realrel X Y" 

351 
using assms unfolding realrel_def by simp 

352 

353 
lemma realrel_refl: "cauchy X \<Longrightarrow> realrel X X" 

354 
unfolding realrel_def by simp 

355 

356 
lemma symp_realrel: "symp realrel" 

357 
unfolding realrel_def 

358 
by (rule sympI, clarify, drule vanishes_minus, simp) 

359 

360 
lemma transp_realrel: "transp realrel" 

361 
unfolding realrel_def 

362 
apply (rule transpI, clarify) 

363 
apply (drule (1) vanishes_add) 

364 
apply (simp add: algebra_simps) 

365 
done 

366 

367 
lemma part_equivp_realrel: "part_equivp realrel" 

368 
by (fast intro: part_equivpI symp_realrel transp_realrel 

369 
realrel_refl cauchy_const) 

370 

371 
subsection {* The field of real numbers *} 

372 

373 
quotient_type real = "nat \<Rightarrow> rat" / partial: realrel 

374 
morphisms rep_real Real 

375 
by (rule part_equivp_realrel) 

376 

377 
lemma cr_real_eq: "pcr_real = (\<lambda>x y. cauchy x \<and> Real x = y)" 

378 
unfolding real.pcr_cr_eq cr_real_def realrel_def by auto 

379 

380 
lemma Real_induct [induct type: real]: (* TODO: generate automatically *) 

381 
assumes "\<And>X. cauchy X \<Longrightarrow> P (Real X)" shows "P x" 

382 
proof (induct x) 

383 
case (1 X) 

384 
hence "cauchy X" by (simp add: realrel_def) 

385 
thus "P (Real X)" by (rule assms) 

386 
qed 

387 

388 
lemma eq_Real: 

389 
"cauchy X \<Longrightarrow> cauchy Y \<Longrightarrow> Real X = Real Y \<longleftrightarrow> vanishes (\<lambda>n. X n  Y n)" 

390 
using real.rel_eq_transfer 

55945  391 
unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp 
51523  392 

51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51775
diff
changeset

393 
lemma Domainp_pcr_real [transfer_domain_rule]: "Domainp pcr_real = cauchy" 
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51775
diff
changeset

394 
by (simp add: real.domain_eq realrel_def) 
51523  395 

396 
instantiation real :: field_inverse_zero 

397 
begin 

398 

399 
lift_definition zero_real :: "real" is "\<lambda>n. 0" 

400 
by (simp add: realrel_refl) 

401 

402 
lift_definition one_real :: "real" is "\<lambda>n. 1" 

403 
by (simp add: realrel_refl) 

404 

405 
lift_definition plus_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n + Y n" 

406 
unfolding realrel_def add_diff_add 

407 
by (simp only: cauchy_add vanishes_add simp_thms) 

408 

409 
lift_definition uminus_real :: "real \<Rightarrow> real" is "\<lambda>X n.  X n" 

410 
unfolding realrel_def minus_diff_minus 

411 
by (simp only: cauchy_minus vanishes_minus simp_thms) 

412 

413 
lift_definition times_real :: "real \<Rightarrow> real \<Rightarrow> real" is "\<lambda>X Y n. X n * Y n" 

414 
unfolding realrel_def mult_diff_mult 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset

415 
by (subst (4) mult.commute, simp only: cauchy_mult vanishes_add 
51523  416 
vanishes_mult_bounded cauchy_imp_bounded simp_thms) 
417 

418 
lift_definition inverse_real :: "real \<Rightarrow> real" 

419 
is "\<lambda>X. if vanishes X then (\<lambda>n. 0) else (\<lambda>n. inverse (X n))" 

420 
proof  

421 
fix X Y assume "realrel X Y" 

422 
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n  Y n)" 

423 
unfolding realrel_def by simp_all 

424 
have "vanishes X \<longleftrightarrow> vanishes Y" 

425 
proof 

426 
assume "vanishes X" 

427 
from vanishes_diff [OF this XY] show "vanishes Y" by simp 

428 
next 

429 
assume "vanishes Y" 

430 
from vanishes_add [OF this XY] show "vanishes X" by simp 

431 
qed 

432 
thus "?thesis X Y" 

433 
unfolding realrel_def 

434 
by (simp add: vanishes_diff_inverse X Y XY) 

435 
qed 

436 

437 
definition 

438 
"x  y = (x::real) +  y" 

439 

440 
definition 

441 
"x / y = (x::real) * inverse y" 

442 

443 
lemma add_Real: 

444 
assumes X: "cauchy X" and Y: "cauchy Y" 

445 
shows "Real X + Real Y = Real (\<lambda>n. X n + Y n)" 

446 
using assms plus_real.transfer 

55945  447 
unfolding cr_real_eq rel_fun_def by simp 
51523  448 

449 
lemma minus_Real: 

450 
assumes X: "cauchy X" 

451 
shows " Real X = Real (\<lambda>n.  X n)" 

452 
using assms uminus_real.transfer 

55945  453 
unfolding cr_real_eq rel_fun_def by simp 
51523  454 

455 
lemma diff_Real: 

456 
assumes X: "cauchy X" and Y: "cauchy Y" 

457 
shows "Real X  Real Y = Real (\<lambda>n. X n  Y n)" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

458 
unfolding minus_real_def 
51523  459 
by (simp add: minus_Real add_Real X Y) 
460 

461 
lemma mult_Real: 

462 
assumes X: "cauchy X" and Y: "cauchy Y" 

463 
shows "Real X * Real Y = Real (\<lambda>n. X n * Y n)" 

464 
using assms times_real.transfer 

55945  465 
unfolding cr_real_eq rel_fun_def by simp 
51523  466 

467 
lemma inverse_Real: 

468 
assumes X: "cauchy X" 

469 
shows "inverse (Real X) = 

470 
(if vanishes X then 0 else Real (\<lambda>n. inverse (X n)))" 

471 
using assms inverse_real.transfer zero_real.transfer 

55945  472 
unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis) 
51523  473 

474 
instance proof 

475 
fix a b c :: real 

476 
show "a + b = b + a" 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

477 
by transfer (simp add: ac_simps realrel_def) 
51523  478 
show "(a + b) + c = a + (b + c)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

479 
by transfer (simp add: ac_simps realrel_def) 
51523  480 
show "0 + a = a" 
481 
by transfer (simp add: realrel_def) 

482 
show " a + a = 0" 

483 
by transfer (simp add: realrel_def) 

484 
show "a  b = a +  b" 

485 
by (rule minus_real_def) 

486 
show "(a * b) * c = a * (b * c)" 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

487 
by transfer (simp add: ac_simps realrel_def) 
51523  488 
show "a * b = b * a" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

489 
by transfer (simp add: ac_simps realrel_def) 
51523  490 
show "1 * a = a" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

491 
by transfer (simp add: ac_simps realrel_def) 
51523  492 
show "(a + b) * c = a * c + b * c" 
493 
by transfer (simp add: distrib_right realrel_def) 

494 
show "(0\<Colon>real) \<noteq> (1\<Colon>real)" 

495 
by transfer (simp add: realrel_def) 

496 
show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 

497 
apply transfer 

498 
apply (simp add: realrel_def) 

499 
apply (rule vanishesI) 

500 
apply (frule (1) cauchy_not_vanishes, clarify) 

501 
apply (rule_tac x=k in exI, clarify) 

502 
apply (drule_tac x=n in spec, simp) 

503 
done 

504 
show "a / b = a * inverse b" 

505 
by (rule divide_real_def) 

506 
show "inverse (0::real) = 0" 

507 
by transfer (simp add: realrel_def) 

508 
qed 

509 

510 
end 

511 

512 
subsection {* Positive reals *} 

513 

514 
lift_definition positive :: "real \<Rightarrow> bool" 

515 
is "\<lambda>X. \<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n" 

516 
proof  

517 
{ fix X Y 

518 
assume "realrel X Y" 

519 
hence XY: "vanishes (\<lambda>n. X n  Y n)" 

520 
unfolding realrel_def by simp_all 

521 
assume "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n" 

522 
then obtain r i where "0 < r" and i: "\<forall>n\<ge>i. r < X n" 

523 
by fast 

524 
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 

525 
using `0 < r` by (rule obtain_pos_sum) 

526 
obtain j where j: "\<forall>n\<ge>j. \<bar>X n  Y n\<bar> < s" 

527 
using vanishesD [OF XY s] .. 

528 
have "\<forall>n\<ge>max i j. t < Y n" 

529 
proof (clarsimp) 

530 
fix n assume n: "i \<le> n" "j \<le> n" 

531 
have "\<bar>X n  Y n\<bar> < s" and "r < X n" 

532 
using i j n by simp_all 

533 
thus "t < Y n" unfolding r by simp 

534 
qed 

535 
hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by fast 

536 
} note 1 = this 

537 
fix X Y assume "realrel X Y" 

538 
hence "realrel X Y" and "realrel Y X" 

539 
using symp_realrel unfolding symp_def by auto 

540 
thus "?thesis X Y" 

541 
by (safe elim!: 1) 

542 
qed 

543 

544 
lemma positive_Real: 

545 
assumes X: "cauchy X" 

546 
shows "positive (Real X) \<longleftrightarrow> (\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < X n)" 

547 
using assms positive.transfer 

55945  548 
unfolding cr_real_eq rel_fun_def by simp 
51523  549 

550 
lemma positive_zero: "\<not> positive 0" 

551 
by transfer auto 

552 

553 
lemma positive_add: 

554 
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x + y)" 

555 
apply transfer 

556 
apply (clarify, rename_tac a b i j) 

557 
apply (rule_tac x="a + b" in exI, simp) 

558 
apply (rule_tac x="max i j" in exI, clarsimp) 

559 
apply (simp add: add_strict_mono) 

560 
done 

561 

562 
lemma positive_mult: 

563 
"positive x \<Longrightarrow> positive y \<Longrightarrow> positive (x * y)" 

564 
apply transfer 

565 
apply (clarify, rename_tac a b i j) 

56544  566 
apply (rule_tac x="a * b" in exI, simp) 
51523  567 
apply (rule_tac x="max i j" in exI, clarsimp) 
568 
apply (rule mult_strict_mono, auto) 

569 
done 

570 

571 
lemma positive_minus: 

572 
"\<not> positive x \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> positive ( x)" 

573 
apply transfer 

574 
apply (simp add: realrel_def) 

575 
apply (drule (1) cauchy_not_vanishes_cases, safe, fast, fast) 

576 
done 

577 

578 
instantiation real :: linordered_field_inverse_zero 

579 
begin 

580 

581 
definition 

582 
"x < y \<longleftrightarrow> positive (y  x)" 

583 

584 
definition 

585 
"x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y" 

586 

587 
definition 

588 
"abs (a::real) = (if a < 0 then  a else a)" 

589 

590 
definition 

591 
"sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else  1)" 

592 

593 
instance proof 

594 
fix a b c :: real 

595 
show "\<bar>a\<bar> = (if a < 0 then  a else a)" 

596 
by (rule abs_real_def) 

597 
show "a < b \<longleftrightarrow> a \<le> b \<and> \<not> b \<le> a" 

598 
unfolding less_eq_real_def less_real_def 

599 
by (auto, drule (1) positive_add, simp_all add: positive_zero) 

600 
show "a \<le> a" 

601 
unfolding less_eq_real_def by simp 

602 
show "a \<le> b \<Longrightarrow> b \<le> c \<Longrightarrow> a \<le> c" 

603 
unfolding less_eq_real_def less_real_def 

604 
by (auto, drule (1) positive_add, simp add: algebra_simps) 

605 
show "a \<le> b \<Longrightarrow> b \<le> a \<Longrightarrow> a = b" 

606 
unfolding less_eq_real_def less_real_def 

607 
by (auto, drule (1) positive_add, simp add: positive_zero) 

608 
show "a \<le> b \<Longrightarrow> c + a \<le> c + b" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53652
diff
changeset

609 
unfolding less_eq_real_def less_real_def by auto 
51523  610 
(* FIXME: Procedure int_combine_numerals: c + b  (c + a) \<equiv> b +  a *) 
611 
(* Should produce c + b  (c + a) \<equiv> b  a *) 

612 
show "sgn a = (if a = 0 then 0 else if 0 < a then 1 else  1)" 

613 
by (rule sgn_real_def) 

614 
show "a \<le> b \<or> b \<le> a" 

615 
unfolding less_eq_real_def less_real_def 

616 
by (auto dest!: positive_minus) 

617 
show "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b" 

618 
unfolding less_real_def 

619 
by (drule (1) positive_mult, simp add: algebra_simps) 

620 
qed 

621 

622 
end 

623 

624 
instantiation real :: distrib_lattice 

625 
begin 

626 

627 
definition 

628 
"(inf :: real \<Rightarrow> real \<Rightarrow> real) = min" 

629 

630 
definition 

631 
"(sup :: real \<Rightarrow> real \<Rightarrow> real) = max" 

632 

633 
instance proof 

54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
54489
diff
changeset

634 
qed (auto simp add: inf_real_def sup_real_def max_min_distrib2) 
51523  635 

636 
end 

637 

638 
lemma of_nat_Real: "of_nat x = Real (\<lambda>n. of_nat x)" 

639 
apply (induct x) 

640 
apply (simp add: zero_real_def) 

641 
apply (simp add: one_real_def add_Real) 

642 
done 

643 

644 
lemma of_int_Real: "of_int x = Real (\<lambda>n. of_int x)" 

645 
apply (cases x rule: int_diff_cases) 

646 
apply (simp add: of_nat_Real diff_Real) 

647 
done 

648 

649 
lemma of_rat_Real: "of_rat x = Real (\<lambda>n. x)" 

650 
apply (induct x) 

651 
apply (simp add: Fract_of_int_quotient of_rat_divide) 

652 
apply (simp add: of_int_Real divide_inverse) 

653 
apply (simp add: inverse_Real mult_Real) 

654 
done 

655 

656 
instance real :: archimedean_field 

657 
proof 

658 
fix x :: real 

659 
show "\<exists>z. x \<le> of_int z" 

660 
apply (induct x) 

661 
apply (frule cauchy_imp_bounded, clarify) 

662 
apply (rule_tac x="ceiling b + 1" in exI) 

663 
apply (rule less_imp_le) 

664 
apply (simp add: of_int_Real less_real_def diff_Real positive_Real) 

665 
apply (rule_tac x=1 in exI, simp add: algebra_simps) 

666 
apply (rule_tac x=0 in exI, clarsimp) 

667 
apply (rule le_less_trans [OF abs_ge_self]) 

668 
apply (rule less_le_trans [OF _ le_of_int_ceiling]) 

669 
apply simp 

670 
done 

671 
qed 

672 

673 
instantiation real :: floor_ceiling 

674 
begin 

675 

676 
definition [code del]: 

677 
"floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" 

678 

679 
instance proof 

680 
fix x :: real 

681 
show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)" 

682 
unfolding floor_real_def using floor_exists1 by (rule theI') 

683 
qed 

684 

685 
end 

686 

687 
subsection {* Completeness *} 

688 

689 
lemma not_positive_Real: 

690 
assumes X: "cauchy X" 

691 
shows "\<not> positive (Real X) \<longleftrightarrow> (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> r)" 

692 
unfolding positive_Real [OF X] 

693 
apply (auto, unfold not_less) 

694 
apply (erule obtain_pos_sum) 

695 
apply (drule_tac x=s in spec, simp) 

696 
apply (drule_tac r=t in cauchyD [OF X], clarify) 

697 
apply (drule_tac x=k in spec, clarsimp) 

698 
apply (rule_tac x=n in exI, clarify, rename_tac m) 

699 
apply (drule_tac x=m in spec, simp) 

700 
apply (drule_tac x=n in spec, simp) 

701 
apply (drule spec, drule (1) mp, clarify, rename_tac i) 

702 
apply (rule_tac x="max i k" in exI, simp) 

703 
done 

704 

705 
lemma le_Real: 

706 
assumes X: "cauchy X" and Y: "cauchy Y" 

707 
shows "Real X \<le> Real Y = (\<forall>r>0. \<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r)" 

708 
unfolding not_less [symmetric, where 'a=real] less_real_def 

709 
apply (simp add: diff_Real not_positive_Real X Y) 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

710 
apply (simp add: diff_le_eq ac_simps) 
51523  711 
done 
712 

713 
lemma le_RealI: 

714 
assumes Y: "cauchy Y" 

715 
shows "\<forall>n. x \<le> of_rat (Y n) \<Longrightarrow> x \<le> Real Y" 

716 
proof (induct x) 

717 
fix X assume X: "cauchy X" and "\<forall>n. Real X \<le> of_rat (Y n)" 

718 
hence le: "\<And>m r. 0 < r \<Longrightarrow> \<exists>k. \<forall>n\<ge>k. X n \<le> Y m + r" 

719 
by (simp add: of_rat_Real le_Real) 

720 
{ 

721 
fix r :: rat assume "0 < r" 

722 
then obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 

723 
by (rule obtain_pos_sum) 

724 
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>Y m  Y n\<bar> < s" 

725 
using cauchyD [OF Y s] .. 

726 
obtain j where j: "\<forall>n\<ge>j. X n \<le> Y i + t" 

727 
using le [OF t] .. 

728 
have "\<forall>n\<ge>max i j. X n \<le> Y n + r" 

729 
proof (clarsimp) 

730 
fix n assume n: "i \<le> n" "j \<le> n" 

731 
have "X n \<le> Y i + t" using n j by simp 

732 
moreover have "\<bar>Y i  Y n\<bar> < s" using n i by simp 

733 
ultimately show "X n \<le> Y n + r" unfolding r by simp 

734 
qed 

735 
hence "\<exists>k. \<forall>n\<ge>k. X n \<le> Y n + r" .. 

736 
} 

737 
thus "Real X \<le> Real Y" 

738 
by (simp add: of_rat_Real le_Real X Y) 

739 
qed 

740 

741 
lemma Real_leI: 

742 
assumes X: "cauchy X" 

743 
assumes le: "\<forall>n. of_rat (X n) \<le> y" 

744 
shows "Real X \<le> y" 

745 
proof  

746 
have " y \<le>  Real X" 

747 
by (simp add: minus_Real X le_RealI of_rat_minus le) 

748 
thus ?thesis by simp 

749 
qed 

750 

751 
lemma less_RealD: 

752 
assumes Y: "cauchy Y" 

753 
shows "x < Real Y \<Longrightarrow> \<exists>n. x < of_rat (Y n)" 

754 
by (erule contrapos_pp, simp add: not_less, erule Real_leI [OF Y]) 

755 

756 
lemma of_nat_less_two_power: 

757 
"of_nat n < (2::'a::linordered_idom) ^ n" 

758 
apply (induct n) 

759 
apply simp 

760 
apply (subgoal_tac "(1::'a) \<le> 2 ^ n") 

761 
apply (drule (1) add_le_less_mono, simp) 

762 
apply simp 

763 
done 

764 

765 
lemma complete_real: 

766 
fixes S :: "real set" 

767 
assumes "\<exists>x. x \<in> S" and "\<exists>z. \<forall>x\<in>S. x \<le> z" 

768 
shows "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" 

769 
proof  

770 
obtain x where x: "x \<in> S" using assms(1) .. 

771 
obtain z where z: "\<forall>x\<in>S. x \<le> z" using assms(2) .. 

772 

773 
def P \<equiv> "\<lambda>x. \<forall>y\<in>S. y \<le> of_rat x" 

774 
obtain a where a: "\<not> P a" 

775 
proof 

776 
have "of_int (floor (x  1)) \<le> x  1" by (rule of_int_floor_le) 

777 
also have "x  1 < x" by simp 

778 
finally have "of_int (floor (x  1)) < x" . 

779 
hence "\<not> x \<le> of_int (floor (x  1))" by (simp only: not_le) 

780 
then show "\<not> P (of_int (floor (x  1)))" 

781 
unfolding P_def of_rat_of_int_eq using x by fast 

782 
qed 

783 
obtain b where b: "P b" 

784 
proof 

785 
show "P (of_int (ceiling z))" 

786 
unfolding P_def of_rat_of_int_eq 

787 
proof 

788 
fix y assume "y \<in> S" 

789 
hence "y \<le> z" using z by simp 

790 
also have "z \<le> of_int (ceiling z)" by (rule le_of_int_ceiling) 

791 
finally show "y \<le> of_int (ceiling z)" . 

792 
qed 

793 
qed 

794 

795 
def avg \<equiv> "\<lambda>x y :: rat. x/2 + y/2" 

796 
def bisect \<equiv> "\<lambda>(x, y). if P (avg x y) then (x, avg x y) else (avg x y, y)" 

797 
def A \<equiv> "\<lambda>n. fst ((bisect ^^ n) (a, b))" 

798 
def B \<equiv> "\<lambda>n. snd ((bisect ^^ n) (a, b))" 

799 
def C \<equiv> "\<lambda>n. avg (A n) (B n)" 

800 
have A_0 [simp]: "A 0 = a" unfolding A_def by simp 

801 
have B_0 [simp]: "B 0 = b" unfolding B_def by simp 

802 
have A_Suc [simp]: "\<And>n. A (Suc n) = (if P (C n) then A n else C n)" 

803 
unfolding A_def B_def C_def bisect_def split_def by simp 

804 
have B_Suc [simp]: "\<And>n. B (Suc n) = (if P (C n) then C n else B n)" 

805 
unfolding A_def B_def C_def bisect_def split_def by simp 

806 

807 
have width: "\<And>n. B n  A n = (b  a) / 2^n" 

808 
apply (simp add: eq_divide_eq) 

809 
apply (induct_tac n, simp) 

810 
apply (simp add: C_def avg_def algebra_simps) 

811 
done 

812 

813 
have twos: "\<And>y r :: rat. 0 < r \<Longrightarrow> \<exists>n. y / 2 ^ n < r" 

814 
apply (simp add: divide_less_eq) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57447
diff
changeset

815 
apply (subst mult.commute) 
51523  816 
apply (frule_tac y=y in ex_less_of_nat_mult) 
817 
apply clarify 

818 
apply (rule_tac x=n in exI) 

819 
apply (erule less_trans) 

820 
apply (rule mult_strict_right_mono) 

821 
apply (rule le_less_trans [OF _ of_nat_less_two_power]) 

822 
apply simp 

823 
apply assumption 

824 
done 

825 

826 
have PA: "\<And>n. \<not> P (A n)" 

827 
by (induct_tac n, simp_all add: a) 

828 
have PB: "\<And>n. P (B n)" 

829 
by (induct_tac n, simp_all add: b) 

830 
have ab: "a < b" 

831 
using a b unfolding P_def 

832 
apply (clarsimp simp add: not_le) 

833 
apply (drule (1) bspec) 

834 
apply (drule (1) less_le_trans) 

835 
apply (simp add: of_rat_less) 

836 
done 

837 
have AB: "\<And>n. A n < B n" 

838 
by (induct_tac n, simp add: ab, simp add: C_def avg_def) 

839 
have A_mono: "\<And>i j. i \<le> j \<Longrightarrow> A i \<le> A j" 

840 
apply (auto simp add: le_less [where 'a=nat]) 

841 
apply (erule less_Suc_induct) 

842 
apply (clarsimp simp add: C_def avg_def) 

843 
apply (simp add: add_divide_distrib [symmetric]) 

844 
apply (rule AB [THEN less_imp_le]) 

845 
apply simp 

846 
done 

847 
have B_mono: "\<And>i j. i \<le> j \<Longrightarrow> B j \<le> B i" 

848 
apply (auto simp add: le_less [where 'a=nat]) 

849 
apply (erule less_Suc_induct) 

850 
apply (clarsimp simp add: C_def avg_def) 

851 
apply (simp add: add_divide_distrib [symmetric]) 

852 
apply (rule AB [THEN less_imp_le]) 

853 
apply simp 

854 
done 

855 
have cauchy_lemma: 

856 
"\<And>X. \<forall>n. \<forall>i\<ge>n. A n \<le> X i \<and> X i \<le> B n \<Longrightarrow> cauchy X" 

857 
apply (rule cauchyI) 

858 
apply (drule twos [where y="b  a"]) 

859 
apply (erule exE) 

860 
apply (rule_tac x=n in exI, clarify, rename_tac i j) 

861 
apply (rule_tac y="B n  A n" in le_less_trans) defer 

862 
apply (simp add: width) 

863 
apply (drule_tac x=n in spec) 

864 
apply (frule_tac x=i in spec, drule (1) mp) 

865 
apply (frule_tac x=j in spec, drule (1) mp) 

866 
apply (frule A_mono, drule B_mono) 

867 
apply (frule A_mono, drule B_mono) 

868 
apply arith 

869 
done 

870 
have "cauchy A" 

871 
apply (rule cauchy_lemma [rule_format]) 

872 
apply (simp add: A_mono) 

873 
apply (erule order_trans [OF less_imp_le [OF AB] B_mono]) 

874 
done 

875 
have "cauchy B" 

876 
apply (rule cauchy_lemma [rule_format]) 

877 
apply (simp add: B_mono) 

878 
apply (erule order_trans [OF A_mono less_imp_le [OF AB]]) 

879 
done 

880 
have 1: "\<forall>x\<in>S. x \<le> Real B" 

881 
proof 

882 
fix x assume "x \<in> S" 

883 
then show "x \<le> Real B" 

884 
using PB [unfolded P_def] `cauchy B` 

885 
by (simp add: le_RealI) 

886 
qed 

887 
have 2: "\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> Real A \<le> z" 

888 
apply clarify 

889 
apply (erule contrapos_pp) 

890 
apply (simp add: not_le) 

891 
apply (drule less_RealD [OF `cauchy A`], clarify) 

892 
apply (subgoal_tac "\<not> P (A n)") 

893 
apply (simp add: P_def not_le, clarify) 

894 
apply (erule rev_bexI) 

895 
apply (erule (1) less_trans) 

896 
apply (simp add: PA) 

897 
done 

898 
have "vanishes (\<lambda>n. (b  a) / 2 ^ n)" 

899 
proof (rule vanishesI) 

900 
fix r :: rat assume "0 < r" 

901 
then obtain k where k: "\<bar>b  a\<bar> / 2 ^ k < r" 

902 
using twos by fast 

903 
have "\<forall>n\<ge>k. \<bar>(b  a) / 2 ^ n\<bar> < r" 

904 
proof (clarify) 

905 
fix n assume n: "k \<le> n" 

906 
have "\<bar>(b  a) / 2 ^ n\<bar> = \<bar>b  a\<bar> / 2 ^ n" 

907 
by simp 

908 
also have "\<dots> \<le> \<bar>b  a\<bar> / 2 ^ k" 

56544  909 
using n by (simp add: divide_left_mono) 
51523  910 
also note k 
911 
finally show "\<bar>(b  a) / 2 ^ n\<bar> < r" . 

912 
qed 

913 
thus "\<exists>k. \<forall>n\<ge>k. \<bar>(b  a) / 2 ^ n\<bar> < r" .. 

914 
qed 

915 
hence 3: "Real B = Real A" 

916 
by (simp add: eq_Real `cauchy A` `cauchy B` width) 

917 
show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" 

918 
using 1 2 3 by (rule_tac x="Real B" in exI, simp) 

919 
qed 

920 

51775
408d937c9486
revert #916271d52466; add nontopological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51773
diff
changeset

921 
instantiation real :: linear_continuum 
51523  922 
begin 
923 

924 
subsection{*Supremum of a set of reals*} 

925 

54281  926 
definition "Sup X = (LEAST z::real. \<forall>x\<in>X. x \<le> z)" 
927 
definition "Inf (X::real set) =  Sup (uminus ` X)" 

51523  928 

929 
instance 

930 
proof 

54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54230
diff
changeset

931 
{ fix x :: real and X :: "real set" 
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54230
diff
changeset

932 
assume x: "x \<in> X" "bdd_above X" 
51523  933 
then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z" 
54258
adfc759263ab
use bdd_above and bdd_below for conditionally complete lattices
hoelzl
parents:
54230
diff
changeset

934 
using complete_real[of X] unfolding bdd_above_def by blast 
51523  935 
then show "x \<le> Sup X" 
936 
unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) } 

937 
note Sup_upper = this 

938 

939 
{ fix z :: real and X :: "real set" 

940 
assume x: "X \<noteq> {}" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z" 

941 
then obtain s where s: "\<forall>y\<in>X. y \<le> s" "\<And>z. \<forall>y\<in>X. y \<le> z \<Longrightarrow> s \<le> z" 

942 
using complete_real[of X] by blast 

943 
then have "Sup X = s" 

944 
unfolding Sup_real_def by (best intro: Least_equality) 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53076
diff
changeset

945 
also from s z have "... \<le> z" 
51523  946 
by blast 
947 
finally show "Sup X \<le> z" . } 

948 
note Sup_least = this 

949 

54281  950 
{ fix x :: real and X :: "real set" assume x: "x \<in> X" "bdd_below X" then show "Inf X \<le> x" 
951 
using Sup_upper[of "x" "uminus ` X"] by (auto simp: Inf_real_def) } 

952 
{ fix z :: real and X :: "real set" assume "X \<noteq> {}" "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" then show "z \<le> Inf X" 

953 
using Sup_least[of "uminus ` X" " z"] by (force simp: Inf_real_def) } 

51775
408d937c9486
revert #916271d52466; add nontopological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51773
diff
changeset

954 
show "\<exists>a b::real. a \<noteq> b" 
408d937c9486
revert #916271d52466; add nontopological linear_continuum type class; show linear_continuum_topology is a perfect_space
hoelzl
parents:
51773
diff
changeset

955 
using zero_neq_one by blast 
51523  956 
qed 
957 
end 

958 

959 

960 
subsection {* Hiding implementation details *} 

961 

962 
hide_const (open) vanishes cauchy positive Real 

963 

964 
declare Real_induct [induct del] 

965 
declare Abs_real_induct [induct del] 

966 
declare Abs_real_cases [cases del] 

967 

53652
18fbca265e2e
use lifting_forget for deregistering numeric types as a quotient type
kuncar
parents:
53374
diff
changeset

968 
lifting_update real.lifting 
18fbca265e2e
use lifting_forget for deregistering numeric types as a quotient type
kuncar
parents:
53374
diff
changeset

969 
lifting_forget real.lifting 
51956
a4d81cdebf8b
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
kuncar
parents:
51775
diff
changeset

970 

51523  971 
subsection{*More Lemmas*} 
972 

973 
text {* BH: These lemmas should not be necessary; they should be 

974 
covered by existing simp rules and simplification procedures. *} 

975 

976 
lemma real_mult_less_iff1 [simp]: "(0::real) < z ==> (x*z < y*z) = (x < y)" 

977 
by simp (* solved by linordered_ring_less_cancel_factor simproc *) 

978 

979 
lemma real_mult_le_cancel_iff1 [simp]: "(0::real) < z ==> (x*z \<le> y*z) = (x\<le>y)" 

980 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

981 

982 
lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)" 

983 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

984 

985 

986 
subsection {* Embedding numbers into the Reals *} 

987 

988 
abbreviation 

989 
real_of_nat :: "nat \<Rightarrow> real" 

990 
where 

991 
"real_of_nat \<equiv> of_nat" 

992 

993 
abbreviation 

994 
real_of_int :: "int \<Rightarrow> real" 

995 
where 

996 
"real_of_int \<equiv> of_int" 

997 

998 
abbreviation 

999 
real_of_rat :: "rat \<Rightarrow> real" 

1000 
where 

1001 
"real_of_rat \<equiv> of_rat" 

1002 

58042
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1003 
class real_of = 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1004 
fixes real :: "'a \<Rightarrow> real" 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1005 

ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1006 
instantiation nat :: real_of 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1007 
begin 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1008 

ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1009 
definition real_nat :: "nat \<Rightarrow> real" where real_of_nat_def [code_unfold]: "real \<equiv> of_nat" 
51523  1010 

58042
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1011 
instance .. 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1012 
end 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1013 

ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1014 
instantiation int :: real_of 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1015 
begin 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1016 

ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1017 
definition real_int :: "int \<Rightarrow> real" where real_of_int_def [code_unfold]: "real \<equiv> of_int" 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1018 

ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1019 
instance .. 
ffa9e39763e3
introduce real_of typeclass for real :: 'a => real
hoelzl
parents:
58040
diff
changeset

1020 
end 
51523  1021 

1022 
declare [[coercion_enabled]] 

1023 
declare [[coercion "real::nat\<Rightarrow>real"]] 

1024 
declare [[coercion "real::int\<Rightarrow>real"]] 

1025 
declare [[coercion "int"]] 

1026 

1027 
declare [[coercion_map map]] 

1028 
declare [[coercion_map "% f g h x. g (h (f x))"]] 

1029 
declare [[coercion_map "% f g (x,y) . (f x, g y)"]] 

1030 

1031 
lemma real_eq_of_nat: "real = of_nat" 

1032 
unfolding real_of_nat_def .. 

1033 

1034 
lemma real_eq_of_int: "real = of_int" 

1035 
unfolding real_of_int_def .. 

1036 

1037 
lemma real_of_int_zero [simp]: "real (0::int) = 0" 

1038 
by (simp add: real_of_int_def) 

1039 

1040 
lemma real_of_one [simp]: "real (1::int) = (1::real)" 

1041 
by (simp add: real_of_int_def) 

1042 

1043 
lemma real_of_int_add [simp]: "real(x + y) = real (x::int) + real y" 

1044 
by (simp add: real_of_int_def) 

1045 

1046 
lemma real_of_int_minus [simp]: "real(x) = real (x::int)" 

1047 
by (simp add: real_of_int_def) 

1048 

1049 
lemma real_of_int_diff [simp]: "real(x  y) = real (x::int)  real y" 

1050 
by (simp add: real_of_int_def) 

1051 

1052 
lemma real_of_int_mult [simp]: "real(x * y) = real (x::int) * real y" 

1053 
by (simp add: real_of_int_def) 

1054 

1055 
lemma real_of_int_power [simp]: "real (x ^ n) = real (x::int) ^ n" 

1056 
by (simp add: real_of_int_def of_int_power) 

1057 

1058 
lemmas power_real_of_int = real_of_int_power [symmetric] 

1059 

1060 
lemma real_of_int_setsum [simp]: "real ((SUM x:A. f x)::int) = (SUM x:A. real(f x))" 

1061 
apply (subst real_eq_of_int)+ 

1062 
apply (rule of_int_setsum) 

1063 
done 

1064 

1065 
lemma real_of_int_setprod [simp]: "real ((PROD x:A. f x)::int) = 

1066 
(PROD x:A. real(f x))" 

1067 
apply (subst real_eq_of_int)+ 

1068 
apply (rule of_int_setprod) 

1069 
done 

1070 

1071 
lemma real_of_int_zero_cancel [simp, algebra, presburger]: "(real x = 0) = (x = (0::int))" 

1072 
by (simp add: real_of_int_def) 

1073 

1074 
lemma real_of_int_inject [iff, algebra, presburger]: "(real (x::int) = real y) = (x = y)" 

1075 
by (simp add: real_of_int_def) 

1076 

1077 
lemma real_of_int_less_iff [iff, presburger]: "(real (x::int) < real y) = (x < y)" 

1078 
by (simp add: real_of_int_def) 

1079 

1080 
lemma real_of_int_le_iff [simp, presburger]: "(real (x::int) \<le> real y) = (x \<le> y)" 

1081 
by (simp add: real_of_int_def) 

1082 

1083 
lemma real_of_int_gt_zero_cancel_iff [simp, presburger]: "(0 < real (n::int)) = (0 < n)" 

1084 
by (simp add: real_of_int_def) 

1085 

1086 
lemma real_of_int_ge_zero_cancel_iff [simp, presburger]: "(0 <= real (n::int)) = (0 <= n)" 

1087 
by (simp add: real_of_int_def) 

1088 

1089 
lemma real_of_int_lt_zero_cancel_iff [simp, presburger]: "(real (n::int) < 0) = (n < 0)" 

1090 
by (simp add: real_of_int_def) 

1091 

1092 
lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)" 

1093 
by (simp add: real_of_int_def) 

1094 

1095 
lemma one_less_real_of_int_cancel_iff: "1 < real (i :: int) \<longleftrightarrow> 1 < i" 

1096 
unfolding real_of_one[symmetric] real_of_int_less_iff .. 

1097 

1098 
lemma one_le_real_of_int_cancel_iff: "1 \<le> real (i :: int) \<longleftrightarrow> 1 \<le> i" 

1099 
unfolding real_of_one[symmetric] real_of_int_le_iff .. 

1100 

1101 
lemma real_of_int_less_one_cancel_iff: "real (i :: int) < 1 \<longleftrightarrow> i < 1" 

1102 
unfolding real_of_one[symmetric] real_of_int_less_iff .. 

1103 

1104 
lemma real_of_int_le_one_cancel_iff: "real (i :: int) \<le> 1 \<longleftrightarrow> i \<le> 1" 

1105 
unfolding real_of_one[symmetric] real_of_int_le_iff .. 

1106 

1107 
lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))" 

1108 
by (auto simp add: abs_if) 

1109 

1110 
lemma int_less_real_le: "((n::int) < m) = (real n + 1 <= real m)" 

1111 
apply (subgoal_tac "real n + 1 = real (n + 1)") 

1112 
apply (simp del: real_of_int_add) 

1113 
apply auto 

1114 
done 

1115 

1116 
lemma int_le_real_less: "((n::int) <= m) = (real n < real m + 1)" 

1117 
apply (subgoal_tac "real m + 1 = real (m + 1)") 

1118 
apply (simp del: real_of_int_add) 

1119 
apply simp 

1120 
done 

1121 

1122 
lemma real_of_int_div_aux: "(real (x::int)) / (real d) = 

1123 
real (x div d) + (real (x mod d)) / (real d)" 

1124 
proof  

1125 
have "x = (x div d) * d + x mod d" 

1126 
by auto 

1127 
then have "real x = real (x div d) * real d + real(x mod d)" 

1128 
by (simp only: real_of_int_mult [THEN sym] real_of_int_add [THEN sym]) 

1129 
then have "real x / real d = ... / real d" 

1130 
by simp 

1131 
then show ?thesis 

1132 
by (auto simp add: add_divide_distrib algebra_simps) 

1133 
qed 

1134 

1135 
lemma real_of_int_div: "(d :: int) dvd n ==> 

1136 
real(n div d) = real n / real d" 

1137 
apply (subst real_of_int_div_aux) 

1138 
apply simp 

1139 
apply (simp add: dvd_eq_mod_eq_0) 

1140 
done 

1141 

1142 
lemma real_of_int_div2: 

1143 
"0 <= real (n::int) / real (x)  real (n div x)" 

1144 
apply (case_tac "x = 0") 

1145 
apply simp 

1146 
apply (case_tac "0 < x") 

1147 
apply (simp add: algebra_simps) 

1148 
apply (subst real_of_int_div_aux) 

1149 
apply simp 

1150 
apply (simp add: algebra_simps) 

1151 
apply (subst real_of_int_div_aux) 

1152 
apply simp 

1153 
apply (subst zero_le_divide_iff) 

1154 
apply auto 

1155 
done 

1156 

1157 
lemma real_of_int_div3: 

1158 
"real (n::int) / real (x)  real (n div x) <= 1" 

1159 
apply (simp add: algebra_simps) 

1160 
apply (subst real_of_int_div_aux) 

1161 
apply (auto simp add: divide_le_eq intro: order_less_imp_le) 

1162 
done 

1163 

1164 
lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 

1165 
by (insert real_of_int_div2 [of n x], simp) 

1166 

1167 
lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints" 

1168 
unfolding real_of_int_def by (rule Ints_of_int) 

1169 

1170 

1171 
subsection{*Embedding the Naturals into the Reals*} 

1172 

1173 
lemma real_of_nat_zero [simp]: "real (0::nat) = 0" 

1174 
by (simp add: real_of_nat_def) 

1175 

1176 
lemma real_of_nat_1 [simp]: "real (1::nat) = 1" 

1177 
by (simp add: real_of_nat_def) 

1178 

1179 
lemma real_of_nat_one [simp]: "real (Suc 0) = (1::real)" 

1180 
by (simp add: real_of_nat_def) 

1181 

1182 
lemma real_of_nat_add [simp]: "real (m + n) = real (m::nat) + real n" 

1183 
by (simp add: real_of_nat_def) 

1184 

1185 
(*Not for addsimps: often the LHS is used to represent a positive natural*) 

1186 
lemma real_of_nat_Suc: "real (Suc n) = real n + (1::real)" 

1187 
by (simp add: real_of_nat_def) 

1188 

1189 
lemma real_of_nat_less_iff [iff]: 

1190 
"(real (n::nat) < real m) = (n < m)" 

1191 
by (simp add: real_of_nat_def) 

1192 

1193 
lemma real_of_nat_le_iff [iff]: "(real (n::nat) \<le> real m) = (n \<le> m)" 

1194 
by (simp add: real_of_nat_def) 

1195 

1196 
lemma real_of_nat_ge_zero [iff]: "0 \<le> real (n::nat)" 

1197 
by (simp add: real_of_nat_def) 

1198 

1199 
lemma real_of_nat_Suc_gt_zero: "0 < real (Suc n)" 

1200 
by (simp add: real_of_nat_def del: of_nat_Suc) 

1201 

1202 
lemma real_of_nat_mult [simp]: "real (m * n) = real (m::nat) * real n" 

1203 
by (simp add: real_of_nat_def of_nat_mult) 

1204 

1205 
lemma real_of_nat_power [simp]: "real (m ^ n) = real (m::nat) ^ n" 

1206 
by (simp add: real_of_nat_def of_nat_power) 

1207 

1208 
lemmas power_real_of_nat = real_of_nat_power [symmetric] 

1209 

1210 
lemma real_of_nat_setsum [simp]: "real ((SUM x:A. f x)::nat) = 

1211 
(SUM x:A. real(f x))" 

1212 
apply (subst real_eq_of_nat)+ 

1213 
apply (rule of_nat_setsum) 

1214 
done 

1215 

1216 
lemma real_of_nat_setprod [simp]: "real ((PROD x:A. f x)::nat) = 

1217 
(PROD x:A. real(f x))" 

1218 
apply (subst real_eq_of_nat)+ 

1219 
apply (rule of_nat_setprod) 

1220 
done 

1221 

1222 
lemma real_of_card: "real (card A) = setsum (%x.1) A" 

1223 
apply (subst card_eq_setsum) 

1224 
apply (subst real_of_nat_setsum) 

1225 
apply simp 

1226 
done 

1227 

1228 
lemma real_of_nat_inject [iff]: "(real (n::nat) = real m) = (n = m)" 

1229 
by (simp add: real_of_nat_def) 

1230 

1231 
lemma real_of_nat_zero_iff [iff]: "(real (n::nat) = 0) = (n = 0)" 

1232 
by (simp add: real_of_nat_def) 

1233 

1234 
lemma real_of_nat_diff: "n \<le> m ==> real (m  n) = real (m::nat)  real n" 

1235 
by (simp add: add: real_of_nat_def of_nat_diff) 

1236 

1237 
lemma real_of_nat_gt_zero_cancel_iff [simp]: "(0 < real (n::nat)) = (0 < n)" 

1238 
by (auto simp: real_of_nat_def) 

1239 

1240 
lemma real_of_nat_le_zero_cancel_iff [simp]: "(real (n::nat) \<le> 0) = (n = 0)" 

1241 
by (simp add: add: real_of_nat_def) 

1242 

1243 
lemma not_real_of_nat_less_zero [simp]: "~ real (n::nat) < 0" 

1244 
by (simp add: add: real_of_nat_def) 

1245 

1246 
lemma nat_less_real_le: "((n::nat) < m) = (real n + 1 <= real m)" 

1247 
apply (subgoal_tac "real n + 1 = real (Suc n)") 

1248 
apply simp 

1249 
apply (auto simp add: real_of_nat_Suc) 

1250 
done 

1251 

1252 
lemma nat_le_real_less: "((n::nat) <= m) = (real n < real m + 1)" 

1253 
apply (subgoal_tac "real m + 1 = real (Suc m)") 

1254 
apply (simp add: less_Suc_eq_le) 

1255 
apply (simp add: real_of_nat_Suc) 

1256 
done 

1257 

1258 
lemma real_of_nat_div_aux: "(real (x::nat)) / (real d) = 

1259 
real (x div d) + (real (x mod d)) / (real d)" 

1260 
proof  

1261 
have "x = (x div d) * d + x mod d" 

1262 
by auto 

1263 
then have "real x = real (x div d) * real d + real(x mod d)" 

1264 
by (simp only: real_of_nat_mult [THEN sym] real_of_nat_add [THEN sym]) 

1265 
then have "real x / real d = \<dots> / real d" 

1266 
by simp 

1267 
then show ?thesis 

1268 
by (auto simp add: add_divide_distrib algebra_simps) 

1269 
qed 

1270 

1271 
lemma real_of_nat_div: "(d :: nat) dvd n ==> 

1272 
real(n div d) = real n / real d" 

1273 
by (subst real_of_nat_div_aux) 

1274 
(auto simp add: dvd_eq_mod_eq_0 [symmetric]) 

1275 

1276 
lemma real_of_nat_div2: 

1277 
"0 <= real (n::nat) / real (x)  real (n div x)" 

1278 
apply (simp add: algebra_simps) 

1279 
apply (subst real_of_nat_div_aux) 

1280 
apply simp 

1281 
done 

1282 

1283 
lemma real_of_nat_div3: 

1284 
"real (n::nat) / real (x)  real (n div x) <= 1" 

1285 
apply(case_tac "x = 0") 

1286 
apply (simp) 

1287 
apply (simp add: algebra_simps) 

1288 
apply (subst real_of_nat_div_aux) 

1289 
apply simp 

1290 
done 

1291 

1292 
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 

1293 
by (insert real_of_nat_div2 [of n x], simp) 

1294 

1295 
lemma real_of_int_of_nat_eq [simp]: "real (of_nat n :: int) = real n" 

1296 
by (simp add: real_of_int_def real_of_nat_def) 

1297 

1298 
lemma real_nat_eq_real [simp]: "0 <= x ==> real(nat x) = real x" 

1299 
apply (subgoal_tac "real(int(nat x)) = real(nat x)") 

1300 
apply force 

1301 
apply (simp only: real_of_int_of_nat_eq) 

1302 
done 

1303 

1304 
lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats" 

1305 
unfolding real_of_nat_def by (rule of_nat_in_Nats) 

1306 

1307 
lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints" 

1308 
unfolding real_of_nat_def by (rule Ints_of_nat) 

1309 

1310 
subsection {* The Archimedean Property of the Reals *} 

1311 

1312 
theorem reals_Archimedean: 

1313 
assumes x_pos: "0 < x" 

1314 
shows "\<exists>n. inverse (real (Suc n)) < x" 

1315 
unfolding real_of_nat_def using x_pos 

1316 
by (rule ex_inverse_of_nat_Suc_less) 

1317 

1318 
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)" 

1319 
unfolding real_of_nat_def by (rule ex_less_of_nat) 

1320 

1321 
lemma reals_Archimedean3: 

1322 
assumes x_greater_zero: "0 < x" 

1323 
shows "\<forall>(y::real). \<exists>(n::nat). y < real n * x" 

1324 
unfolding real_of_nat_def using `0 < x` 

1325 
by (auto intro: ex_less_of_nat_mult) 

1326 

1327 

1328 
subsection{* Rationals *} 

1329 

1330 
lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>" 

1331 
by (simp add: real_eq_of_nat) 

1332 

1333 
lemma Rats_eq_int_div_int: 

1334 
"\<rat> = { real(i::int)/real(j::int) i j. j \<noteq> 0}" (is "_ = ?S") 

1335 
proof 

1336 
show "\<rat> \<subseteq> ?S" 

1337 
proof 

1338 
fix x::real assume "x : \<rat>" 

1339 
then obtain r where "x = of_rat r" unfolding Rats_def .. 

1340 
have "of_rat r : ?S" 

1341 
by (cases r)(auto simp add:of_rat_rat real_eq_of_int) 

1342 
thus "x : ?S" using `x = of_rat r` by simp 

1343 
qed 

1344 
next 

1345 
show "?S \<subseteq> \<rat>" 

1346 
proof(auto simp:Rats_def) 

1347 
fix i j :: int assume "j \<noteq> 0" 

1348 
hence "real i / real j = of_rat(Fract i j)" 

1349 
by (simp add:of_rat_rat real_eq_of_int) 

1350 
thus "real i / real j \<in> range of_rat" by blast 

1351 
qed 

1352 
qed 

1353 

1354 
lemma Rats_eq_int_div_nat: 

1355 
"\<rat> = { real(i::int)/real(n::nat) i n. n \<noteq> 0}" 

1356 
proof(auto simp:Rats_eq_int_div_int) 

1357 
fix i j::int assume "j \<noteq> 0" 

1358 
show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n" 

1359 
proof cases 

1360 
assume "j>0" 

1361 
hence "real i/real j = real i/real(nat j) \<and> 0<nat j" 

1362 
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) 

1363 
thus ?thesis by blast 

1364 
next 

1365 
assume "~ j>0" 

1366 
hence "real i/real j = real(i)/real(nat(j)) \<and> 0<nat(j)" using `j\<noteq>0` 

1367 
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) 

1368 
thus ?thesis by blast 

1369 
qed 

1370 
next 

1371 
fix i::int and n::nat assume "0 < n" 

1372 
hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp 

1373 
thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast 

1374 
qed 

1375 

1376 
lemma Rats_abs_nat_div_natE: 

1377 
assumes "x \<in> \<rat>" 

1378 
obtains m n :: nat 

1379 
where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1" 

1380 
proof  

1381 
from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n" 

1382 
by(auto simp add: Rats_eq_int_div_nat) 

1383 
hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp 

1384 
then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast 

1385 
let ?gcd = "gcd m n" 

1386 
from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by simp 

1387 
let ?k = "m div ?gcd" 

1388 
let ?l = "n div ?gcd" 

1389 
let ?gcd' = "gcd ?k ?l" 

1390 
have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m" 

1391 
by (rule dvd_mult_div_cancel) 

1392 
have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n" 

1393 
by (rule dvd_mult_div_cancel) 

1394 
from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv) 

1395 
moreover 

1396 
have "\<bar>x\<bar> = real ?k / real ?l" 

1397 
proof  

1398 
from gcd have "real ?k / real ?l = 

1399 
real (?gcd * ?k) / real (?gcd * ?l)" by simp 

1400 
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp 

1401 
also from x_rat have "\<dots> = \<bar>x\<bar>" .. 

1402 
finally show ?thesis .. 

1403 
qed 

1404 
moreover 

1405 
have "?gcd' = 1" 

1406 
proof  

1407 
have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)" 

1408 
by (rule gcd_mult_distrib_nat) 

1409 
with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp 

1410 
with gcd show ?thesis by auto 

1411 
qed 

1412 
ultimately show ?thesis .. 

1413 
qed 

1414 

1415 
subsection{*Density of the Rational Reals in the Reals*} 

1416 

1417 
text{* This density proof is due to Stefan Richter and was ported by TN. The 

1418 
original source is \emph{Real Analysis} by H.L. Royden. 

1419 
It employs the Archimedean property of the reals. *} 

1420 

1421 
lemma Rats_dense_in_real: 

1422 
fixes x :: real 

1423 
assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y" 

1424 
proof  

1425 
from `x<y` have "0 < yx" by simp 

1426 
with reals_Archimedean obtain q::nat 

1427 
where q: "inverse (real q) < yx" and "0 < q" by auto 

1428 
def p \<equiv> "ceiling (y * real q)  1" 

1429 
def r \<equiv> "of_int p / real q" 

1430 
from q have "x < y  inverse (real q)" by simp 

1431 
also have "y  inverse (real q) \<le> r" 

1432 
unfolding r_def p_def 

1433 
by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`) 

1434 
finally have "x < r" . 

1435 
moreover have "r < y" 

1436 
unfolding r_def p_def 

1437 
by (simp add: divide_less_eq diff_less_eq `0 < q` 

1438 
less_ceiling_iff [symmetric]) 

1439 
moreover from r_def have "r \<in> \<rat>" by simp 

1440 
ultimately show ?thesis by fast 

1441 
qed 

1442 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1443 
lemma of_rat_dense: 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1444 
fixes x y :: real 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1445 
assumes "x < y" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1446 
shows "\<exists>q :: rat. x < of_rat q \<and> of_rat q < y" 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1447 
using Rats_dense_in_real [OF `x < y`] 
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1448 
by (auto elim: Rats_cases) 
51523  1449 

1450 

1451 
subsection{*Numerals and Arithmetic*} 

1452 

1453 
lemma [code_abbrev]: 

1454 
"real_of_int (numeral k) = numeral k" 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54281
diff
changeset

1455 
"real_of_int ( numeral k) =  numeral k" 
51523  1456 
by simp_all 
1457 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54281
diff
changeset

1458 
text{*Collapse applications of @{const real} to @{const numeral}*} 
51523  1459 
lemma real_numeral [simp]: 
1460 
"real (numeral v :: int) = numeral v" 

54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54281
diff
changeset

1461 
"real ( numeral v :: int) =  numeral v" 
51523  1462 
by (simp_all add: real_of_int_def) 
1463 

57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1464 
lemma real_of_nat_numeral [simp]: 
51523  1465 
"real (numeral v :: nat) = numeral v" 
1466 
by (simp add: real_of_nat_def) 

1467 

1468 
declaration {* 

1469 
K (Lin_Arith.add_inj_thms [@{thm real_of_nat_le_iff} RS iffD2, @{thm real_of_nat_inject} RS iffD2] 

1470 
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: real_of_nat_less_iff RS iffD2 *) 

1471 
#> Lin_Arith.add_inj_thms [@{thm real_of_int_le_iff} RS iffD2, @{thm real_of_int_inject} RS iffD2] 

1472 
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: real_of_int_less_iff RS iffD2 *) 

1473 
#> Lin_Arith.add_simps [@{thm real_of_nat_zero}, @{thm real_of_nat_Suc}, @{thm real_of_nat_add}, 

1474 
@{thm real_of_nat_mult}, @{thm real_of_int_zero}, @{thm real_of_one}, 

1475 
@{thm real_of_int_add}, @{thm real_of_int_minus}, @{thm real_of_int_diff}, 

1476 
@{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq}, 

58040
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
57514
diff
changeset

1477 
@{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}, 
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
57514
diff
changeset

1478 
@{thm real_of_int_def[symmetric]}, @{thm real_of_nat_def[symmetric]}] 
51523  1479 
#> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \<Rightarrow> real"}) 
58040
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
57514
diff
changeset

1480 
#> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"}) 
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
57514
diff
changeset

1481 
#> Lin_Arith.add_inj_const (@{const_name of_nat}, @{typ "nat \<Rightarrow> real"}) 
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
57514
diff
changeset

1482 
#> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"})) 
51523  1483 
*} 
1484 

1485 
subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*} 

1486 

1487 
lemma real_add_minus_iff [simp]: "(x +  a = (0::real)) = (x=a)" 

1488 
by arith 

1489 

1490 
text {* FIXME: redundant with @{text add_eq_0_iff} below *} 

1491 
lemma real_add_eq_0_iff: "(x+y = (0::real)) = (y = x)" 

1492 
by auto 

1493 

1494 
lemma real_add_less_0_iff: "(x+y < (0::real)) = (y < x)" 

1495 
by auto 

1496 

1497 
lemma real_0_less_add_iff: "((0::real) < x+y) = (x < y)" 

1498 
by auto 

1499 

1500 
lemma real_add_le_0_iff: "(x+y \<le> (0::real)) = (y \<le> x)" 

1501 
by auto 

1502 

1503 
lemma real_0_le_add_iff: "((0::real) \<le> x+y) = (x \<le> y)" 

1504 
by auto 

1505 

1506 
subsection {* Lemmas about powers *} 

1507 

1508 
text {* FIXME: declare this in Rings.thy or not at all *} 

1509 
declare abs_mult_self [simp] 

1510 

1511 
(* used by Import/HOL/real.imp *) 

1512 
lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n" 

1513 
by simp 

1514 

1515 
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n" 

1516 
apply (induct "n") 

1517 
apply (auto simp add: real_of_nat_Suc) 

1518 
apply (subst mult_2) 

1519 
apply (erule add_less_le_mono) 

1520 
apply (rule two_realpow_ge_one) 

1521 
done 

1522 

1523 
text {* TODO: no longer realspecific; rename and move elsewhere *} 

1524 
lemma realpow_Suc_le_self: 

1525 
fixes r :: "'a::linordered_semidom" 

1526 
shows "[ 0 \<le> r; r \<le> 1 ] ==> r ^ Suc n \<le> r" 

1527 
by (insert power_decreasing [of 1 "Suc n" r], simp) 

1528 

1529 
text {* TODO: no longer realspecific; rename and move elsewhere *} 

1530 
lemma realpow_minus_mult: 

1531 
fixes x :: "'a::monoid_mult" 

1532 
shows "0 < n \<Longrightarrow> x ^ (n  1) * x = x ^ n" 

1533 
by (simp add: power_commutes split add: nat_diff_split) 

1534 

1535 
text {* FIXME: declare this [simp] for all types, or not at all *} 

1536 
lemma real_two_squares_add_zero_iff [simp]: 

1537 
"(x * x + y * y = 0) = ((x::real) = 0 \<and> y = 0)" 

1538 
by (rule sum_squares_eq_zero_iff) 

1539 

1540 
text {* FIXME: declare this [simp] for all types, or not at all *} 

1541 
lemma realpow_two_sum_zero_iff [simp]: 

53076  1542 
"(x\<^sup>2 + y\<^sup>2 = (0::real)) = (x = 0 & y = 0)" 
51523  1543 
by (rule sum_power2_eq_zero_iff) 
1544 

1545 
lemma real_minus_mult_self_le [simp]: "(u * u) \<le> (x * (x::real))" 

1546 
by (rule_tac y = 0 in order_trans, auto) 

1547 

53076  1548 
lemma realpow_square_minus_le [simp]: " u\<^sup>2 \<le> (x::real)\<^sup>2" 
51523  1549 
by (auto simp add: power2_eq_square) 
1550 

1551 

1552 
lemma numeral_power_le_real_of_nat_cancel_iff[simp]: 

1553 
"(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a" 

1554 
unfolding real_of_nat_le_iff[symmetric] by simp 

1555 

1556 
lemma real_of_nat_le_numeral_power_cancel_iff[simp]: 

