author  hoelzl 
Thu, 25 Apr 2013 11:59:21 +0200  
changeset 51775  408d937c9486 
parent 51773  9328c6681f3c 
child 51956  a4d81cdebf8b 
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)" 

101 
unfolding diff_minus by (intro vanishes_add vanishes_minus X Y) 

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 

113 
show "0 < r / a" using r a by (simp add: divide_pos_pos) 

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

173 
using assms unfolding diff_minus by simp 

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 

218 
show "0 < v/b" using v b(1) by (rule divide_pos_pos) 

219 
show "0 < u/a" using u a(1) by (rule divide_pos_pos) 

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 

285 
show "0 < b * r * b" 

286 
by (simp add: `0 < r` b mult_pos_pos) 

287 
show "r = inverse b * (b * r * b) * inverse b" 

288 
using b by simp 

289 
qed 

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

291 
using cauchyD [OF X s] .. 

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

293 
proof (clarsimp) 

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

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

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

297 
by (simp add: inverse_diff_inverse nz * abs_mult) 

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

299 
by (simp add: mult_strict_mono less_imp_inverse_less 

300 
mult_pos_pos i j b * s) 

301 
finally show "\<bar>inverse (X m)  inverse (X n)\<bar> < r" unfolding r . 

302 
qed 

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

304 
qed 

305 

306 
lemma vanishes_diff_inverse: 

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

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

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

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

311 
proof (rule vanishesI) 

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

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

314 
using cauchy_not_vanishes [OF X] by fast 

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

316 
using cauchy_not_vanishes [OF Y] by fast 

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

318 
proof 

319 
show "0 < a * r * b" 

320 
using a r b by (simp add: mult_pos_pos) 

321 
show "inverse a * (a * r * b) * inverse b = r" 

322 
using a r b by simp 

323 
qed 

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

325 
using vanishesD [OF XY s] .. 

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

327 
proof (clarsimp) 

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

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

330 
using i j a b n by auto 

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

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

333 
by (simp add: inverse_diff_inverse abs_mult) 

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

335 
apply (intro mult_strict_mono' less_imp_inverse_less) 

336 
apply (simp_all add: a b i j k n mult_nonneg_nonneg) 

337 
done 

338 
also note `inverse a * s * inverse b = r` 

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

340 
qed 

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

342 
qed 

343 

344 
subsection {* Equivalence relation on Cauchy sequences *} 

345 

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

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

348 

349 
lemma realrelI [intro?]: 

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

351 
shows "realrel X Y" 

352 
using assms unfolding realrel_def by simp 

353 

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

355 
unfolding realrel_def by simp 

356 

357 
lemma symp_realrel: "symp realrel" 

358 
unfolding realrel_def 

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

360 

361 
lemma transp_realrel: "transp realrel" 

362 
unfolding realrel_def 

363 
apply (rule transpI, clarify) 

364 
apply (drule (1) vanishes_add) 

365 
apply (simp add: algebra_simps) 

366 
done 

367 

368 
lemma part_equivp_realrel: "part_equivp realrel" 

369 
by (fast intro: part_equivpI symp_realrel transp_realrel 

370 
realrel_refl cauchy_const) 

371 

372 
subsection {* The field of real numbers *} 

373 

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

375 
morphisms rep_real Real 

376 
by (rule part_equivp_realrel) 

377 

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

379 
unfolding real.pcr_cr_eq cr_real_def realrel_def by auto 

380 

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

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

383 
proof (induct x) 

384 
case (1 X) 

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

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

387 
qed 

388 

389 
lemma eq_Real: 

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

391 
using real.rel_eq_transfer 

392 
unfolding real.pcr_cr_eq cr_real_def fun_rel_def realrel_def by simp 

393 

394 
declare real.forall_transfer [transfer_rule del] 

395 

396 
lemma forall_real_transfer [transfer_rule]: (* TODO: generate automatically *) 

397 
"(fun_rel (fun_rel pcr_real op =) op =) 

398 
(transfer_bforall cauchy) transfer_forall" 

399 
using real.forall_transfer 

400 
by (simp add: realrel_def) 

401 

402 
instantiation real :: field_inverse_zero 

403 
begin 

404 

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

406 
by (simp add: realrel_refl) 

407 

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

409 
by (simp add: realrel_refl) 

410 

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

412 
unfolding realrel_def add_diff_add 

413 
by (simp only: cauchy_add vanishes_add simp_thms) 

414 

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

416 
unfolding realrel_def minus_diff_minus 

417 
by (simp only: cauchy_minus vanishes_minus simp_thms) 

418 

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

420 
unfolding realrel_def mult_diff_mult 

421 
by (subst (4) mult_commute, simp only: cauchy_mult vanishes_add 

422 
vanishes_mult_bounded cauchy_imp_bounded simp_thms) 

423 

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

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

426 
proof  

427 
fix X Y assume "realrel X Y" 

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

429 
unfolding realrel_def by simp_all 

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

431 
proof 

432 
assume "vanishes X" 

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

434 
next 

435 
assume "vanishes Y" 

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

437 
qed 

438 
thus "?thesis X Y" 

439 
unfolding realrel_def 

440 
by (simp add: vanishes_diff_inverse X Y XY) 

441 
qed 

442 

443 
definition 

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

445 

446 
definition 

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

448 

449 
lemma add_Real: 

450 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

452 
using assms plus_real.transfer 

453 
unfolding cr_real_eq fun_rel_def by simp 

454 

455 
lemma minus_Real: 

456 
assumes X: "cauchy X" 

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

458 
using assms uminus_real.transfer 

459 
unfolding cr_real_eq fun_rel_def by simp 

460 

461 
lemma diff_Real: 

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

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

464 
unfolding minus_real_def diff_minus 

465 
by (simp add: minus_Real add_Real X Y) 

466 

467 
lemma mult_Real: 

468 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

470 
using assms times_real.transfer 

471 
unfolding cr_real_eq fun_rel_def by simp 

472 

473 
lemma inverse_Real: 

474 
assumes X: "cauchy X" 

475 
shows "inverse (Real X) = 

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

477 
using assms inverse_real.transfer zero_real.transfer 

478 
unfolding cr_real_eq fun_rel_def by (simp split: split_if_asm, metis) 

479 

480 
instance proof 

481 
fix a b c :: real 

482 
show "a + b = b + a" 

483 
by transfer (simp add: add_ac realrel_def) 

484 
show "(a + b) + c = a + (b + c)" 

485 
by transfer (simp add: add_ac realrel_def) 

486 
show "0 + a = a" 

487 
by transfer (simp add: realrel_def) 

488 
show " a + a = 0" 

489 
by transfer (simp add: realrel_def) 

490 
show "a  b = a +  b" 

491 
by (rule minus_real_def) 

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

493 
by transfer (simp add: mult_ac realrel_def) 

494 
show "a * b = b * a" 

495 
by transfer (simp add: mult_ac realrel_def) 

496 
show "1 * a = a" 

497 
by transfer (simp add: mult_ac realrel_def) 

498 
show "(a + b) * c = a * c + b * c" 

499 
by transfer (simp add: distrib_right realrel_def) 

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

501 
by transfer (simp add: realrel_def) 

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

503 
apply transfer 

504 
apply (simp add: realrel_def) 

505 
apply (rule vanishesI) 

506 
apply (frule (1) cauchy_not_vanishes, clarify) 

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

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

509 
done 

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

511 
by (rule divide_real_def) 

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

513 
by transfer (simp add: realrel_def) 

514 
qed 

515 

516 
end 

517 

518 
subsection {* Positive reals *} 

519 

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

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

522 
proof  

523 
{ fix X Y 

524 
assume "realrel X Y" 

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

526 
unfolding realrel_def by simp_all 

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

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

529 
by fast 

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

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

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

533 
using vanishesD [OF XY s] .. 

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

535 
proof (clarsimp) 

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

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

538 
using i j n by simp_all 

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

540 
qed 

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

542 
} note 1 = this 

543 
fix X Y assume "realrel X Y" 

544 
hence "realrel X Y" and "realrel Y X" 

545 
using symp_realrel unfolding symp_def by auto 

546 
thus "?thesis X Y" 

547 
by (safe elim!: 1) 

548 
qed 

549 

550 
lemma positive_Real: 

551 
assumes X: "cauchy X" 

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

553 
using assms positive.transfer 

554 
unfolding cr_real_eq fun_rel_def by simp 

555 

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

557 
by transfer auto 

558 

559 
lemma positive_add: 

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

561 
apply transfer 

562 
apply (clarify, rename_tac a b i j) 

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

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

565 
apply (simp add: add_strict_mono) 

566 
done 

567 

568 
lemma positive_mult: 

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

570 
apply transfer 

571 
apply (clarify, rename_tac a b i j) 

572 
apply (rule_tac x="a * b" in exI, simp add: mult_pos_pos) 

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

574 
apply (rule mult_strict_mono, auto) 

575 
done 

576 

577 
lemma positive_minus: 

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

579 
apply transfer 

580 
apply (simp add: realrel_def) 

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

582 
done 

583 

584 
instantiation real :: linordered_field_inverse_zero 

585 
begin 

586 

587 
definition 

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

589 

590 
definition 

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

592 

593 
definition 

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

595 

596 
definition 

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

598 

599 
instance proof 

600 
fix a b c :: real 

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

602 
by (rule abs_real_def) 

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

604 
unfolding less_eq_real_def less_real_def 

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

606 
show "a \<le> a" 

607 
unfolding less_eq_real_def by simp 

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

609 
unfolding less_eq_real_def less_real_def 

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

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

612 
unfolding less_eq_real_def less_real_def 

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

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

615 
unfolding less_eq_real_def less_real_def by (auto simp: diff_minus) (* by auto *) 

616 
(* FIXME: Procedure int_combine_numerals: c + b  (c + a) \<equiv> b +  a *) 

617 
(* Should produce c + b  (c + a) \<equiv> b  a *) 

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

619 
by (rule sgn_real_def) 

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

621 
unfolding less_eq_real_def less_real_def 

622 
by (auto dest!: positive_minus) 

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

624 
unfolding less_real_def 

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

626 
qed 

627 

628 
end 

629 

630 
instantiation real :: distrib_lattice 

631 
begin 

632 

633 
definition 

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

635 

636 
definition 

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

638 

639 
instance proof 

640 
qed (auto simp add: inf_real_def sup_real_def min_max.sup_inf_distrib1) 

641 

642 
end 

643 

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

645 
apply (induct x) 

646 
apply (simp add: zero_real_def) 

647 
apply (simp add: one_real_def add_Real) 

648 
done 

649 

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

651 
apply (cases x rule: int_diff_cases) 

652 
apply (simp add: of_nat_Real diff_Real) 

653 
done 

654 

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

656 
apply (induct x) 

657 
apply (simp add: Fract_of_int_quotient of_rat_divide) 

658 
apply (simp add: of_int_Real divide_inverse) 

659 
apply (simp add: inverse_Real mult_Real) 

660 
done 

661 

662 
instance real :: archimedean_field 

663 
proof 

664 
fix x :: real 

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

666 
apply (induct x) 

667 
apply (frule cauchy_imp_bounded, clarify) 

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

669 
apply (rule less_imp_le) 

670 
apply (simp add: of_int_Real less_real_def diff_Real positive_Real) 

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

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

673 
apply (rule le_less_trans [OF abs_ge_self]) 

674 
apply (rule less_le_trans [OF _ le_of_int_ceiling]) 

675 
apply simp 

676 
done 

677 
qed 

678 

679 
instantiation real :: floor_ceiling 

680 
begin 

681 

682 
definition [code del]: 

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

684 

685 
instance proof 

686 
fix x :: real 

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

688 
unfolding floor_real_def using floor_exists1 by (rule theI') 

689 
qed 

690 

691 
end 

692 

693 
subsection {* Completeness *} 

694 

695 
lemma not_positive_Real: 

696 
assumes X: "cauchy X" 

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

698 
unfolding positive_Real [OF X] 

699 
apply (auto, unfold not_less) 

700 
apply (erule obtain_pos_sum) 

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

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

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

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

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

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

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

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

709 
done 

710 

711 
lemma le_Real: 

712 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

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

715 
apply (simp add: diff_Real not_positive_Real X Y) 

716 
apply (simp add: diff_le_eq add_ac) 

717 
done 

718 

719 
lemma le_RealI: 

720 
assumes Y: "cauchy Y" 

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

722 
proof (induct x) 

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

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

725 
by (simp add: of_rat_Real le_Real) 

726 
{ 

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

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

729 
by (rule obtain_pos_sum) 

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

731 
using cauchyD [OF Y s] .. 

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

733 
using le [OF t] .. 

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

735 
proof (clarsimp) 

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

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

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

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

740 
qed 

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

742 
} 

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

744 
by (simp add: of_rat_Real le_Real X Y) 

745 
qed 

746 

747 
lemma Real_leI: 

748 
assumes X: "cauchy X" 

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

750 
shows "Real X \<le> y" 

751 
proof  

752 
have " y \<le>  Real X" 

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

754 
thus ?thesis by simp 

755 
qed 

756 

757 
lemma less_RealD: 

758 
assumes Y: "cauchy Y" 

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

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

761 

762 
lemma of_nat_less_two_power: 

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

764 
apply (induct n) 

765 
apply simp 

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

767 
apply (drule (1) add_le_less_mono, simp) 

768 
apply simp 

769 
done 

770 

771 
lemma complete_real: 

772 
fixes S :: "real set" 

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

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

775 
proof  

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

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

778 

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

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

781 
proof 

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

783 
also have "x  1 < x" by simp 

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

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

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

787 
unfolding P_def of_rat_of_int_eq using x by fast 

788 
qed 

789 
obtain b where b: "P b" 

790 
proof 

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

792 
unfolding P_def of_rat_of_int_eq 

793 
proof 

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

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

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

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

798 
qed 

799 
qed 

800 

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

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

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

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

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

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

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

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

809 
unfolding A_def B_def C_def bisect_def split_def by simp 

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

811 
unfolding A_def B_def C_def bisect_def split_def by simp 

812 

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

814 
apply (simp add: eq_divide_eq) 

815 
apply (induct_tac n, simp) 

816 
apply (simp add: C_def avg_def algebra_simps) 

817 
done 

818 

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

820 
apply (simp add: divide_less_eq) 

821 
apply (subst mult_commute) 

822 
apply (frule_tac y=y in ex_less_of_nat_mult) 

823 
apply clarify 

824 
apply (rule_tac x=n in exI) 

825 
apply (erule less_trans) 

826 
apply (rule mult_strict_right_mono) 

827 
apply (rule le_less_trans [OF _ of_nat_less_two_power]) 

828 
apply simp 

829 
apply assumption 

830 
done 

831 

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

833 
by (induct_tac n, simp_all add: a) 

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

835 
by (induct_tac n, simp_all add: b) 

836 
have ab: "a < b" 

837 
using a b unfolding P_def 

838 
apply (clarsimp simp add: not_le) 

839 
apply (drule (1) bspec) 

840 
apply (drule (1) less_le_trans) 

841 
apply (simp add: of_rat_less) 

842 
done 

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

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

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

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

847 
apply (erule less_Suc_induct) 

848 
apply (clarsimp simp add: C_def avg_def) 

849 
apply (simp add: add_divide_distrib [symmetric]) 

850 
apply (rule AB [THEN less_imp_le]) 

851 
apply simp 

852 
done 

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

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

855 
apply (erule less_Suc_induct) 

856 
apply (clarsimp simp add: C_def avg_def) 

857 
apply (simp add: add_divide_distrib [symmetric]) 

858 
apply (rule AB [THEN less_imp_le]) 

859 
apply simp 

860 
done 

861 
have cauchy_lemma: 

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

863 
apply (rule cauchyI) 

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

865 
apply (erule exE) 

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

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

868 
apply (simp add: width) 

869 
apply (drule_tac x=n in spec) 

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

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

872 
apply (frule A_mono, drule B_mono) 

873 
apply (frule A_mono, drule B_mono) 

874 
apply arith 

875 
done 

876 
have "cauchy A" 

877 
apply (rule cauchy_lemma [rule_format]) 

878 
apply (simp add: A_mono) 

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

880 
done 

881 
have "cauchy B" 

882 
apply (rule cauchy_lemma [rule_format]) 

883 
apply (simp add: B_mono) 

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

885 
done 

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

887 
proof 

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

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

890 
using PB [unfolded P_def] `cauchy B` 

891 
by (simp add: le_RealI) 

892 
qed 

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

894 
apply clarify 

895 
apply (erule contrapos_pp) 

896 
apply (simp add: not_le) 

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

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

899 
apply (simp add: P_def not_le, clarify) 

900 
apply (erule rev_bexI) 

901 
apply (erule (1) less_trans) 

902 
apply (simp add: PA) 

903 
done 

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

905 
proof (rule vanishesI) 

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

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

908 
using twos by fast 

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

910 
proof (clarify) 

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

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

913 
by simp 

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

915 
using n by (simp add: divide_left_mono mult_pos_pos) 

916 
also note k 

917 
finally show "\<bar>(b  a) / 2 ^ n\<bar> < r" . 

918 
qed 

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

920 
qed 

921 
hence 3: "Real B = Real A" 

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

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

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

925 
qed 

926 

927 

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

928 
instantiation real :: linear_continuum 
51523  929 
begin 
930 

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

932 

933 
definition 

934 
Sup_real_def: "Sup X \<equiv> LEAST z::real. \<forall>x\<in>X. x\<le>z" 

935 

936 
definition 

937 
Inf_real_def: "Inf (X::real set) \<equiv>  Sup (uminus ` X)" 

938 

939 
instance 

940 
proof 

941 
{ fix z x :: real and X :: "real set" 

942 
assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> x \<le> z" 

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

944 
using complete_real[of X] by blast 

945 
then show "x \<le> Sup X" 

946 
unfolding Sup_real_def by (rule LeastI2_order) (auto simp: x) } 

947 
note Sup_upper = this 

948 

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

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

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

952 
using complete_real[of X] by blast 

953 
then have "Sup X = s" 

954 
unfolding Sup_real_def by (best intro: Least_equality) 

955 
also with s z have "... \<le> z" 

956 
by blast 

957 
finally show "Sup X \<le> z" . } 

958 
note Sup_least = this 

959 

960 
{ fix x z :: real and X :: "real set" 

961 
assume x: "x \<in> X" and z: "\<And>x. x \<in> X \<Longrightarrow> z \<le> x" 

962 
have "x \<le> Sup (uminus ` X)" 

963 
by (rule Sup_upper[of _ _ " z"]) (auto simp add: image_iff x z) 

964 
then show "Inf X \<le> x" 

965 
by (auto simp add: Inf_real_def) } 

966 

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

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

969 
have "Sup (uminus ` X) \<le> z" 

970 
using x z by (force intro: Sup_least) 

971 
then show "z \<le> Inf X" 

972 
by (auto simp add: 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

973 

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

974 
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

975 
using zero_neq_one by blast 
51523  976 
qed 
977 
end 

978 

979 
text {* 

980 
\medskip Completeness properties using @{text "isUb"}, @{text "isLub"}: 

981 
*} 

982 

983 
lemma reals_complete: "\<exists>X. X \<in> S \<Longrightarrow> \<exists>Y. isUb (UNIV::real set) S Y \<Longrightarrow> \<exists>t. isLub (UNIV :: real set) S t" 

984 
by (intro exI[of _ "Sup S"] isLub_cSup) (auto simp: setle_def isUb_def intro: cSup_upper) 

985 

986 

987 
subsection {* Hiding implementation details *} 

988 

989 
hide_const (open) vanishes cauchy positive Real 

990 

991 
declare Real_induct [induct del] 

992 
declare Abs_real_induct [induct del] 

993 
declare Abs_real_cases [cases del] 

994 

995 
lemmas [transfer_rule del] = 

996 
real.All_transfer real.Ex_transfer real.rel_eq_transfer forall_real_transfer 

997 
zero_real.transfer one_real.transfer plus_real.transfer uminus_real.transfer 

998 
times_real.transfer inverse_real.transfer positive.transfer real.right_unique 

999 
real.right_total 

1000 

1001 
subsection{*More Lemmas*} 

1002 

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

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

1005 

1006 
lemma real_mult_left_cancel: "(c::real) \<noteq> 0 ==> (c*a=c*b) = (a=b)" 

1007 
by simp (* redundant with mult_cancel_left *) 

1008 

1009 
lemma real_mult_right_cancel: "(c::real) \<noteq> 0 ==> (a*c=b*c) = (a=b)" 

1010 
by simp (* redundant with mult_cancel_right *) 

1011 

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

1013 
by simp (* solved by linordered_ring_less_cancel_factor simproc *) 

1014 

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

1016 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

1017 

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

1019 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

1020 

1021 

1022 
subsection {* Embedding numbers into the Reals *} 

1023 

1024 
abbreviation 

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

1026 
where 

1027 
"real_of_nat \<equiv> of_nat" 

1028 

1029 
abbreviation 

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

1031 
where 

1032 
"real_of_int \<equiv> of_int" 

1033 

1034 
abbreviation 

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

1036 
where 

1037 
"real_of_rat \<equiv> of_rat" 

1038 

1039 
consts 

1040 
(*overloaded constant for injecting other types into "real"*) 

1041 
real :: "'a => real" 

1042 

1043 
defs (overloaded) 

1044 
real_of_nat_def [code_unfold]: "real == real_of_nat" 

1045 
real_of_int_def [code_unfold]: "real == real_of_int" 

1046 

1047 
declare [[coercion_enabled]] 

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

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

1050 
declare [[coercion "int"]] 

1051 

1052 
declare [[coercion_map map]] 

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

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

1055 

1056 
lemma real_eq_of_nat: "real = of_nat" 

1057 
unfolding real_of_nat_def .. 

1058 

1059 
lemma real_eq_of_int: "real = of_int" 

1060 
unfolding real_of_int_def .. 

1061 

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

1063 
by (simp add: real_of_int_def) 

1064 

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

1066 
by (simp add: real_of_int_def) 

1067 

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

1069 
by (simp add: real_of_int_def) 

1070 

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

1072 
by (simp add: real_of_int_def) 

1073 

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

1075 
by (simp add: real_of_int_def) 

1076 

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

1078 
by (simp add: real_of_int_def) 

1079 

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

1081 
by (simp add: real_of_int_def of_int_power) 

1082 

1083 
lemmas power_real_of_int = real_of_int_power [symmetric] 

1084 

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

1086 
apply (subst real_eq_of_int)+ 

1087 
apply (rule of_int_setsum) 

1088 
done 

1089 

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

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

1092 
apply (subst real_eq_of_int)+ 

1093 
apply (rule of_int_setprod) 

1094 
done 

1095 

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

1097 
by (simp add: real_of_int_def) 

1098 

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

1100 
by (simp add: real_of_int_def) 

1101 

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

1103 
by (simp add: real_of_int_def) 

1104 

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

1106 
by (simp add: real_of_int_def) 

1107 

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

1109 
by (simp add: real_of_int_def) 

1110 

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

1112 
by (simp add: real_of_int_def) 

1113 

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

1115 
by (simp add: real_of_int_def) 

1116 

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

1118 
by (simp add: real_of_int_def) 

1119 

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

1121 
unfolding real_of_one[symmetric] real_of_int_less_iff .. 

1122 

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

1124 
unfolding real_of_one[symmetric] real_of_int_le_iff .. 

1125 

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

1127 
unfolding real_of_one[symmetric] real_of_int_less_iff .. 

1128 

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

1130 
unfolding real_of_one[symmetric] real_of_int_le_iff .. 

1131 

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

1133 
by (auto simp add: abs_if) 

1134 

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

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

1137 
apply (simp del: real_of_int_add) 

1138 
apply auto 

1139 
done 

1140 

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

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

1143 
apply (simp del: real_of_int_add) 

1144 
apply simp 

1145 
done 

1146 

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

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

1149 
proof  

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

1151 
by auto 

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

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

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

1155 
by simp 

1156 
then show ?thesis 

1157 
by (auto simp add: add_divide_distrib algebra_simps) 

1158 
qed 

1159 

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

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

1162 
apply (subst real_of_int_div_aux) 

1163 
apply simp 

1164 
apply (simp add: dvd_eq_mod_eq_0) 

1165 
done 

1166 

1167 
lemma real_of_int_div2: 

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

1169 
apply (case_tac "x = 0") 

1170 
apply simp 

1171 
apply (case_tac "0 < x") 

1172 
apply (simp add: algebra_simps) 

1173 
apply (subst real_of_int_div_aux) 

1174 
apply simp 

1175 
apply (subst zero_le_divide_iff) 

1176 
apply auto 

1177 
apply (simp add: algebra_simps) 

1178 
apply (subst real_of_int_div_aux) 

1179 
apply simp 

1180 
apply (subst zero_le_divide_iff) 

1181 
apply auto 

1182 
done 

1183 

1184 
lemma real_of_int_div3: 

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

1186 
apply (simp add: algebra_simps) 

1187 
apply (subst real_of_int_div_aux) 

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

1189 
done 

1190 

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

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

1193 

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

1195 
unfolding real_of_int_def by (rule Ints_of_int) 

1196 

1197 

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

1199 

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

1201 
by (simp add: real_of_nat_def) 

1202 

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

1204 
by (simp add: real_of_nat_def) 

1205 

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

1207 
by (simp add: real_of_nat_def) 

1208 

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

1210 
by (simp add: real_of_nat_def) 

1211 

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

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

1214 
by (simp add: real_of_nat_def) 

1215 

1216 
lemma real_of_nat_less_iff [iff]: 

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

1218 
by (simp add: real_of_nat_def) 

1219 

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

1221 
by (simp add: real_of_nat_def) 

1222 

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

1224 
by (simp add: real_of_nat_def) 

1225 

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

1227 
by (simp add: real_of_nat_def del: of_nat_Suc) 

1228 

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

1230 
by (simp add: real_of_nat_def of_nat_mult) 

1231 

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

1233 
by (simp add: real_of_nat_def of_nat_power) 

1234 

1235 
lemmas power_real_of_nat = real_of_nat_power [symmetric] 

1236 

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

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

1239 
apply (subst real_eq_of_nat)+ 

1240 
apply (rule of_nat_setsum) 

1241 
done 

1242 

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

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

1245 
apply (subst real_eq_of_nat)+ 

1246 
apply (rule of_nat_setprod) 

1247 
done 

1248 

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

1250 
apply (subst card_eq_setsum) 

1251 
apply (subst real_of_nat_setsum) 

1252 
apply simp 

1253 
done 

1254 

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

1256 
by (simp add: real_of_nat_def) 

1257 

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

1259 
by (simp add: real_of_nat_def) 

1260 

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

1262 
by (simp add: add: real_of_nat_def of_nat_diff) 

1263 

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

1265 
by (auto simp: real_of_nat_def) 

1266 

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

1268 
by (simp add: add: real_of_nat_def) 

1269 

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

1271 
by (simp add: add: real_of_nat_def) 

1272 

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

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

1275 
apply simp 

1276 
apply (auto simp add: real_of_nat_Suc) 

1277 
done 

1278 

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

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

1281 
apply (simp add: less_Suc_eq_le) 

1282 
apply (simp add: real_of_nat_Suc) 

1283 
done 

1284 

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

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

1287 
proof  

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

1289 
by auto 

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

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

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

1293 
by simp 

1294 
then show ?thesis 

1295 
by (auto simp add: add_divide_distrib algebra_simps) 

1296 
qed 

1297 

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

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

1300 
by (subst real_of_nat_div_aux) 

1301 
(auto simp add: dvd_eq_mod_eq_0 [symmetric]) 

1302 

1303 
lemma real_of_nat_div2: 

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

1305 
apply (simp add: algebra_simps) 

1306 
apply (subst real_of_nat_div_aux) 

1307 
apply simp 

1308 
apply (subst zero_le_divide_iff) 

1309 
apply simp 

1310 
done 

1311 

1312 
lemma real_of_nat_div3: 

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

1314 
apply(case_tac "x = 0") 

1315 
apply (simp) 

1316 
apply (simp add: algebra_simps) 

1317 
apply (subst real_of_nat_div_aux) 

1318 
apply simp 

1319 
done 

1320 

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

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

1323 

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

1325 
by (simp add: real_of_int_def real_of_nat_def) 

1326 

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

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

1329 
apply force 

1330 
apply (simp only: real_of_int_of_nat_eq) 

1331 
done 

1332 

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

1334 
unfolding real_of_nat_def by (rule of_nat_in_Nats) 

1335 

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

1337 
unfolding real_of_nat_def by (rule Ints_of_nat) 

1338 

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

1340 

1341 
theorem reals_Archimedean: 

1342 
assumes x_pos: "0 < x" 

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

1344 
unfolding real_of_nat_def using x_pos 

1345 
by (rule ex_inverse_of_nat_Suc_less) 

1346 

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

1348 
unfolding real_of_nat_def by (rule ex_less_of_nat) 

1349 

1350 
lemma reals_Archimedean3: 

1351 
assumes x_greater_zero: "0 < x" 

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

1353 
unfolding real_of_nat_def using `0 < x` 

1354 
by (auto intro: ex_less_of_nat_mult) 

1355 

1356 

1357 
subsection{* Rationals *} 

1358 

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

1360 
by (simp add: real_eq_of_nat) 

1361 

1362 

1363 
lemma Rats_eq_int_div_int: 

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

1365 
proof 

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

1367 
proof 

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

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

1370 
have "of_rat r : ?S" 

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

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

1373 
qed 

1374 
next 

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

1376 
proof(auto simp:Rats_def) 

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

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

1379 
by (simp add:of_rat_rat real_eq_of_int) 

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

1381 
qed 

1382 
qed 

1383 

1384 
lemma Rats_eq_int_div_nat: 

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

1386 
proof(auto simp:Rats_eq_int_div_int) 

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

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

1389 
proof cases 

1390 
assume "j>0" 

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

1392 
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) 

1393 
thus ?thesis by blast 

1394 
next 

1395 
assume "~ j>0" 

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

1397 
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) 

1398 
thus ?thesis by blast 

1399 
qed 

1400 
next 

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

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

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

1404 
qed 

1405 

1406 
lemma Rats_abs_nat_div_natE: 

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

1408 
obtains m n :: nat 

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

1410 
proof  

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

1412 
by(auto simp add: Rats_eq_int_div_nat) 

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

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

1415 
let ?gcd = "gcd m n" 

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

1417 
let ?k = "m div ?gcd" 

1418 
let ?l = "n div ?gcd" 

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

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

1421 
by (rule dvd_mult_div_cancel) 

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

1423 
by (rule dvd_mult_div_cancel) 

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

1425 
moreover 

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

1427 
proof  

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

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

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

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

1432 
finally show ?thesis .. 

1433 
qed 

1434 
moreover 

1435 
have "?gcd' = 1" 

1436 
proof  

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

1438 
by (rule gcd_mult_distrib_nat) 

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

1440 
with gcd show ?thesis by auto 

1441 
qed 

1442 
ultimately show ?thesis .. 

1443 
qed 

1444 

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

1446 

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

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

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

1450 

1451 
lemma Rats_dense_in_real: 

1452 
fixes x :: real 

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

1454 
proof  

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

1456 
with reals_Archimedean obtain q::nat 

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

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

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

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

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

1462 
unfolding r_def p_def 

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

1464 
finally have "x < r" . 

1465 
moreover have "r < y" 

1466 
unfolding r_def p_def 

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

1468 
less_ceiling_iff [symmetric]) 

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

1470 
ultimately show ?thesis by fast 

1471 
qed 

1472 

1473 

1474 

1475 
subsection{*Numerals and Arithmetic*} 

1476 

1477 
lemma [code_abbrev]: 

1478 
"real_of_int (numeral k) = numeral k" 

1479 
"real_of_int (neg_numeral k) = neg_numeral k" 

1480 
by simp_all 

1481 

1482 
text{*Collapse applications of @{term real} to @{term number_of}*} 

1483 
lemma real_numeral [simp]: 

1484 
"real (numeral v :: int) = numeral v" 

1485 
"real (neg_numeral v :: int) = neg_numeral v" 

1486 
by (simp_all add: real_of_int_def) 

1487 

1488 
lemma real_of_nat_numeral [simp]: 

1489 
"real (numeral v :: nat) = numeral v" 

1490 
by (simp add: real_of_nat_def) 

1491 

1492 
declaration {* 

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

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

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

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

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

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

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

1500 
@{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq}, 

1501 
@{thm real_of_nat_numeral}, @{thm real_numeral(1)}, @{thm real_numeral(2)}] 

1502 
#> Lin_Arith.add_inj_const (@{const_name real}, @{typ "nat \<Rightarrow> real"}) 

1503 
#> Lin_Arith.add_inj_const (@{const_name real}, @{typ "int \<Rightarrow> real"})) 

1504 
*} 

1505 

1506 

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

1508 

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

1510 
by arith 

1511 

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

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

1514 
by auto 

1515 

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

1517 
by auto 

1518 

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

1520 
by auto 

1521 

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

1523 
by auto 

1524 

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

1526 
by auto 

1527 

1528 
subsection {* Lemmas about powers *} 

1529 

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

1531 
declare abs_mult_self [simp] 

1532 

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

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

1535 
by simp 

1536 

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

1538 
apply (induct "n") 

1539 
apply (auto simp add: real_of_nat_Suc) 

1540 
apply (subst mult_2) 

1541 
apply (erule add_less_le_mono) 

1542 
apply (rule two_realpow_ge_one) 

1543 
done 

1544 

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

1546 
lemma realpow_Suc_le_self: 

1547 
fixes r :: "'a::linordered_semidom" 

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

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

1550 

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

1552 
lemma realpow_minus_mult: 

1553 
fixes x :: "'a::monoid_mult" 

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

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

1556 

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

1558 
lemma real_two_squares_add_zero_iff [simp]: 

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

1560 
by (rule sum_squares_eq_zero_iff) 

1561 

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

1563 
lemma realpow_two_sum_zero_iff [simp]: 

1564 
"(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)" 

1565 
by (rule sum_power2_eq_zero_iff) 

1566 

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

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

1569 

1570 
lemma realpow_square_minus_le [simp]: "(u ^ 2) \<le> (x::real) ^ 2" 

1571 
by (auto simp add: power2_eq_square) 

1572 

1573 

1574 
lemma numeral_power_le_real_of_nat_cancel_iff[simp]: 

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

1576 
unfolding real_of_nat_le_iff[symmetric] by simp 

1577 

1578 
lemma real_of_nat_le_numeral_power_cancel_iff[simp]: 

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

1580 
unfolding real_of_nat_le_iff[symmetric] by simp 