author  haftmann 
Tue, 19 Nov 2013 10:05:53 +0100  
changeset 54489  03ff4d1e6784 
parent 54281  b01057e72233 
child 54863  82acc20ded73 
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 

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

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 

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 

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

394 
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

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

397 
instantiation real :: field_inverse_zero 

398 
begin 

399 

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

401 
by (simp add: realrel_refl) 

402 

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

404 
by (simp add: realrel_refl) 

405 

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

407 
unfolding realrel_def add_diff_add 

408 
by (simp only: cauchy_add vanishes_add simp_thms) 

409 

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

411 
unfolding realrel_def minus_diff_minus 

412 
by (simp only: cauchy_minus vanishes_minus simp_thms) 

413 

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

415 
unfolding realrel_def mult_diff_mult 

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

417 
vanishes_mult_bounded cauchy_imp_bounded simp_thms) 

418 

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

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

421 
proof  

422 
fix X Y assume "realrel X Y" 

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

424 
unfolding realrel_def by simp_all 

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

426 
proof 

427 
assume "vanishes X" 

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

429 
next 

430 
assume "vanishes Y" 

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

432 
qed 

433 
thus "?thesis X Y" 

434 
unfolding realrel_def 

435 
by (simp add: vanishes_diff_inverse X Y XY) 

436 
qed 

437 

438 
definition 

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

440 

441 
definition 

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

443 

444 
lemma add_Real: 

445 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

447 
using assms plus_real.transfer 

448 
unfolding cr_real_eq fun_rel_def by simp 

449 

450 
lemma minus_Real: 

451 
assumes X: "cauchy X" 

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

453 
using assms uminus_real.transfer 

454 
unfolding cr_real_eq fun_rel_def by simp 

455 

456 
lemma diff_Real: 

457 
assumes X: "cauchy X" and Y: "cauchy Y" 

458 
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

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

462 
lemma mult_Real: 

463 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

465 
using assms times_real.transfer 

466 
unfolding cr_real_eq fun_rel_def by simp 

467 

468 
lemma inverse_Real: 

469 
assumes X: "cauchy X" 

470 
shows "inverse (Real X) = 

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

472 
using assms inverse_real.transfer zero_real.transfer 

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

474 

475 
instance proof 

476 
fix a b c :: real 

477 
show "a + b = b + a" 

478 
by transfer (simp add: add_ac realrel_def) 

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

480 
by transfer (simp add: add_ac realrel_def) 

481 
show "0 + a = a" 

482 
by transfer (simp add: realrel_def) 

483 
show " a + a = 0" 

484 
by transfer (simp add: realrel_def) 

485 
show "a  b = a +  b" 

486 
by (rule minus_real_def) 

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

488 
by transfer (simp add: mult_ac realrel_def) 

489 
show "a * b = b * a" 

490 
by transfer (simp add: mult_ac realrel_def) 

491 
show "1 * a = a" 

492 
by transfer (simp add: mult_ac realrel_def) 

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

494 
by transfer (simp add: distrib_right realrel_def) 

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

496 
by transfer (simp add: realrel_def) 

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

498 
apply transfer 

499 
apply (simp add: realrel_def) 

500 
apply (rule vanishesI) 

501 
apply (frule (1) cauchy_not_vanishes, clarify) 

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

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

504 
done 

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

506 
by (rule divide_real_def) 

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

508 
by transfer (simp add: realrel_def) 

509 
qed 

510 

511 
end 

512 

513 
subsection {* Positive reals *} 

514 

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

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

517 
proof  

518 
{ fix X Y 

519 
assume "realrel X Y" 

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

521 
unfolding realrel_def by simp_all 

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

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

524 
by fast 

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

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

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

528 
using vanishesD [OF XY s] .. 

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

530 
proof (clarsimp) 

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

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

533 
using i j n by simp_all 

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

535 
qed 

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

537 
} note 1 = this 

538 
fix X Y assume "realrel X Y" 

539 
hence "realrel X Y" and "realrel Y X" 

540 
using symp_realrel unfolding symp_def by auto 

541 
thus "?thesis X Y" 

542 
by (safe elim!: 1) 

543 
qed 

544 

545 
lemma positive_Real: 

546 
assumes X: "cauchy X" 

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

548 
using assms positive.transfer 

549 
unfolding cr_real_eq fun_rel_def by simp 

550 

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

552 
by transfer auto 

553 

554 
lemma positive_add: 

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

556 
apply transfer 

557 
apply (clarify, rename_tac a b i j) 

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

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

560 
apply (simp add: add_strict_mono) 

561 
done 

562 

563 
lemma positive_mult: 

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

565 
apply transfer 

566 
apply (clarify, rename_tac a b i j) 

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

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

569 
apply (rule mult_strict_mono, auto) 

570 
done 

571 

572 
lemma positive_minus: 

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

574 
apply transfer 

575 
apply (simp add: realrel_def) 

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

577 
done 

578 

579 
instantiation real :: linordered_field_inverse_zero 

580 
begin 

581 

582 
definition 

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

584 

585 
definition 

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

587 

588 
definition 

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

590 

591 
definition 

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

593 

594 
instance proof 

595 
fix a b c :: real 

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

597 
by (rule abs_real_def) 

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

599 
unfolding less_eq_real_def less_real_def 

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

601 
show "a \<le> a" 

602 
unfolding less_eq_real_def by simp 

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

604 
unfolding less_eq_real_def less_real_def 

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

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

607 
unfolding less_eq_real_def less_real_def 

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

609 
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

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

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

614 
by (rule sgn_real_def) 

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

616 
unfolding less_eq_real_def less_real_def 

617 
by (auto dest!: positive_minus) 

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

619 
unfolding less_real_def 

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

621 
qed 

622 

623 
end 

624 

625 
instantiation real :: distrib_lattice 

626 
begin 

627 

628 
definition 

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

630 

631 
definition 

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

633 

634 
instance proof 

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

636 

637 
end 

638 

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

640 
apply (induct x) 

641 
apply (simp add: zero_real_def) 

642 
apply (simp add: one_real_def add_Real) 

643 
done 

644 

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

646 
apply (cases x rule: int_diff_cases) 

647 
apply (simp add: of_nat_Real diff_Real) 

648 
done 

649 

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

651 
apply (induct x) 

652 
apply (simp add: Fract_of_int_quotient of_rat_divide) 

653 
apply (simp add: of_int_Real divide_inverse) 

654 
apply (simp add: inverse_Real mult_Real) 

655 
done 

656 

657 
instance real :: archimedean_field 

658 
proof 

659 
fix x :: real 

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

661 
apply (induct x) 

662 
apply (frule cauchy_imp_bounded, clarify) 

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

664 
apply (rule less_imp_le) 

665 
apply (simp add: of_int_Real less_real_def diff_Real positive_Real) 

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

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

668 
apply (rule le_less_trans [OF abs_ge_self]) 

669 
apply (rule less_le_trans [OF _ le_of_int_ceiling]) 

670 
apply simp 

671 
done 

672 
qed 

673 

674 
instantiation real :: floor_ceiling 

675 
begin 

676 

677 
definition [code del]: 

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

679 

680 
instance proof 

681 
fix x :: real 

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

683 
unfolding floor_real_def using floor_exists1 by (rule theI') 

684 
qed 

685 

686 
end 

687 

688 
subsection {* Completeness *} 

689 

690 
lemma not_positive_Real: 

691 
assumes X: "cauchy X" 

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

693 
unfolding positive_Real [OF X] 

694 
apply (auto, unfold not_less) 

695 
apply (erule obtain_pos_sum) 

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

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

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

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

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

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

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

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

704 
done 

705 

706 
lemma le_Real: 

707 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

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

710 
apply (simp add: diff_Real not_positive_Real X Y) 

711 
apply (simp add: diff_le_eq add_ac) 

712 
done 

713 

714 
lemma le_RealI: 

715 
assumes Y: "cauchy Y" 

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

717 
proof (induct x) 

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

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

720 
by (simp add: of_rat_Real le_Real) 

721 
{ 

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

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

724 
by (rule obtain_pos_sum) 

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

726 
using cauchyD [OF Y s] .. 

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

728 
using le [OF t] .. 

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

730 
proof (clarsimp) 

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

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

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

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

735 
qed 

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

737 
} 

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

739 
by (simp add: of_rat_Real le_Real X Y) 

740 
qed 

741 

742 
lemma Real_leI: 

743 
assumes X: "cauchy X" 

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

745 
shows "Real X \<le> y" 

746 
proof  

747 
have " y \<le>  Real X" 

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

749 
thus ?thesis by simp 

750 
qed 

751 

752 
lemma less_RealD: 

753 
assumes Y: "cauchy Y" 

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

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

756 

757 
lemma of_nat_less_two_power: 

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

759 
apply (induct n) 

760 
apply simp 

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

762 
apply (drule (1) add_le_less_mono, simp) 

763 
apply simp 

764 
done 

765 

766 
lemma complete_real: 

767 
fixes S :: "real set" 

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

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

770 
proof  

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

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

773 

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

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

776 
proof 

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

778 
also have "x  1 < x" by simp 

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

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

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

782 
unfolding P_def of_rat_of_int_eq using x by fast 

783 
qed 

784 
obtain b where b: "P b" 

785 
proof 

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

787 
unfolding P_def of_rat_of_int_eq 

788 
proof 

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

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

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

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

793 
qed 

794 
qed 

795 

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

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

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

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

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

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

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

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

804 
unfolding A_def B_def C_def bisect_def split_def by simp 

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

806 
unfolding A_def B_def C_def bisect_def split_def by simp 

807 

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

809 
apply (simp add: eq_divide_eq) 

810 
apply (induct_tac n, simp) 

811 
apply (simp add: C_def avg_def algebra_simps) 

812 
done 

813 

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

815 
apply (simp add: divide_less_eq) 

816 
apply (subst mult_commute) 

817 
apply (frule_tac y=y in ex_less_of_nat_mult) 

818 
apply clarify 

819 
apply (rule_tac x=n in exI) 

820 
apply (erule less_trans) 

821 
apply (rule mult_strict_right_mono) 

822 
apply (rule le_less_trans [OF _ of_nat_less_two_power]) 

823 
apply simp 

824 
apply assumption 

825 
done 

826 

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

828 
by (induct_tac n, simp_all add: a) 

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

830 
by (induct_tac n, simp_all add: b) 

831 
have ab: "a < b" 

832 
using a b unfolding P_def 

833 
apply (clarsimp simp add: not_le) 

834 
apply (drule (1) bspec) 

835 
apply (drule (1) less_le_trans) 

836 
apply (simp add: of_rat_less) 

837 
done 

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

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

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

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

842 
apply (erule less_Suc_induct) 

843 
apply (clarsimp simp add: C_def avg_def) 

844 
apply (simp add: add_divide_distrib [symmetric]) 

845 
apply (rule AB [THEN less_imp_le]) 

846 
apply simp 

847 
done 

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

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

850 
apply (erule less_Suc_induct) 

851 
apply (clarsimp simp add: C_def avg_def) 

852 
apply (simp add: add_divide_distrib [symmetric]) 

853 
apply (rule AB [THEN less_imp_le]) 

854 
apply simp 

855 
done 

856 
have cauchy_lemma: 

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

858 
apply (rule cauchyI) 

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

860 
apply (erule exE) 

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

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

863 
apply (simp add: width) 

864 
apply (drule_tac x=n in spec) 

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

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

867 
apply (frule A_mono, drule B_mono) 

868 
apply (frule A_mono, drule B_mono) 

869 
apply arith 

870 
done 

871 
have "cauchy A" 

872 
apply (rule cauchy_lemma [rule_format]) 

873 
apply (simp add: A_mono) 

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

875 
done 

876 
have "cauchy B" 

877 
apply (rule cauchy_lemma [rule_format]) 

878 
apply (simp add: B_mono) 

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

880 
done 

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

882 
proof 

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

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

885 
using PB [unfolded P_def] `cauchy B` 

886 
by (simp add: le_RealI) 

887 
qed 

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

889 
apply clarify 

890 
apply (erule contrapos_pp) 

891 
apply (simp add: not_le) 

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

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

894 
apply (simp add: P_def not_le, clarify) 

895 
apply (erule rev_bexI) 

896 
apply (erule (1) less_trans) 

897 
apply (simp add: PA) 

898 
done 

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

900 
proof (rule vanishesI) 

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

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

903 
using twos by fast 

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

905 
proof (clarify) 

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

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

908 
by simp 

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

910 
using n by (simp add: divide_left_mono mult_pos_pos) 

911 
also note k 

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

913 
qed 

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

915 
qed 

916 
hence 3: "Real B = Real A" 

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

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

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

920 
qed 

921 

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

922 
instantiation real :: linear_continuum 
51523  923 
begin 
924 

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

926 

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

51523  929 

930 
instance 

931 
proof 

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

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

933 
assume x: "x \<in> X" "bdd_above X" 
51523  934 
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

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

938 
note Sup_upper = this 

939 

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

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

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

943 
using complete_real[of X] by blast 

944 
then have "Sup X = s" 

945 
unfolding Sup_real_def by (best intro: Least_equality) 

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

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

949 
note Sup_least = this 

950 

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

953 
{ 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" 

954 
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

955 
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

956 
using zero_neq_one by blast 
51523  957 
qed 
958 
end 

959 

960 

961 
subsection {* Hiding implementation details *} 

962 

963 
hide_const (open) vanishes cauchy positive Real 

964 

965 
declare Real_induct [induct del] 

966 
declare Abs_real_induct [induct del] 

967 
declare Abs_real_cases [cases del] 

968 

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

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

970 
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

971 

51523  972 
subsection{*More Lemmas*} 
973 

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

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

976 

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

978 
by simp (* redundant with mult_cancel_left *) 

979 

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

981 
by simp (* redundant with mult_cancel_right *) 

982 

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

984 
by simp (* solved by linordered_ring_less_cancel_factor simproc *) 

985 

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

987 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

988 

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

990 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

991 

992 

993 
subsection {* Embedding numbers into the Reals *} 

994 

995 
abbreviation 

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

997 
where 

998 
"real_of_nat \<equiv> of_nat" 

999 

1000 
abbreviation 

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

1002 
where 

1003 
"real_of_int \<equiv> of_int" 

1004 

1005 
abbreviation 

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

1007 
where 

1008 
"real_of_rat \<equiv> of_rat" 

1009 

1010 
consts 

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

1012 
real :: "'a => real" 

1013 

1014 
defs (overloaded) 

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

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

1017 

1018 
declare [[coercion_enabled]] 

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

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

1021 
declare [[coercion "int"]] 

1022 

1023 
declare [[coercion_map map]] 

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

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

1026 

1027 
lemma real_eq_of_nat: "real = of_nat" 

1028 
unfolding real_of_nat_def .. 

1029 

1030 
lemma real_eq_of_int: "real = of_int" 

1031 
unfolding real_of_int_def .. 

1032 

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

1034 
by (simp add: real_of_int_def) 

1035 

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

1037 
by (simp add: real_of_int_def) 

1038 

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

1040 
by (simp add: real_of_int_def) 

1041 

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

1043 
by (simp add: real_of_int_def) 

1044 

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

1046 
by (simp add: real_of_int_def) 

1047 

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

1049 
by (simp add: real_of_int_def) 

1050 

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

1052 
by (simp add: real_of_int_def of_int_power) 

1053 

1054 
lemmas power_real_of_int = real_of_int_power [symmetric] 

1055 

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

1057 
apply (subst real_eq_of_int)+ 

1058 
apply (rule of_int_setsum) 

1059 
done 

1060 

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

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

1063 
apply (subst real_eq_of_int)+ 

1064 
apply (rule of_int_setprod) 

1065 
done 

1066 

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

1068 
by (simp add: real_of_int_def) 

1069 

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

1071 
by (simp add: real_of_int_def) 

1072 

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

1074 
by (simp add: real_of_int_def) 

1075 

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

1077 
by (simp add: real_of_int_def) 

1078 

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

1080 
by (simp add: real_of_int_def) 

1081 

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

1083 
by (simp add: real_of_int_def) 

1084 

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

1086 
by (simp add: real_of_int_def) 

1087 

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

1089 
by (simp add: real_of_int_def) 

1090 

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

1092 
unfolding real_of_one[symmetric] real_of_int_less_iff .. 

1093 

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

1095 
unfolding real_of_one[symmetric] real_of_int_le_iff .. 

1096 

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

1098 
unfolding real_of_one[symmetric] real_of_int_less_iff .. 

1099 

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

1101 
unfolding real_of_one[symmetric] real_of_int_le_iff .. 

1102 

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

1104 
by (auto simp add: abs_if) 

1105 

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

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

1108 
apply (simp del: real_of_int_add) 

1109 
apply auto 

1110 
done 

1111 

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

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

1114 
apply (simp del: real_of_int_add) 

1115 
apply simp 

1116 
done 

1117 

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

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

1120 
proof  

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

1122 
by auto 

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

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

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

1126 
by simp 

1127 
then show ?thesis 

1128 
by (auto simp add: add_divide_distrib algebra_simps) 

1129 
qed 

1130 

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

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

1133 
apply (subst real_of_int_div_aux) 

1134 
apply simp 

1135 
apply (simp add: dvd_eq_mod_eq_0) 

1136 
done 

1137 

1138 
lemma real_of_int_div2: 

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

1140 
apply (case_tac "x = 0") 

1141 
apply simp 

1142 
apply (case_tac "0 < x") 

1143 
apply (simp add: algebra_simps) 

1144 
apply (subst real_of_int_div_aux) 

1145 
apply simp 

1146 
apply (subst zero_le_divide_iff) 

1147 
apply auto 

1148 
apply (simp add: algebra_simps) 

1149 
apply (subst real_of_int_div_aux) 

1150 
apply simp 

1151 
apply (subst zero_le_divide_iff) 

1152 
apply auto 

1153 
done 

1154 

1155 
lemma real_of_int_div3: 

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

1157 
apply (simp add: algebra_simps) 

1158 
apply (subst real_of_int_div_aux) 

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

1160 
done 

1161 

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

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

1164 

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

1166 
unfolding real_of_int_def by (rule Ints_of_int) 

1167 

1168 

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

1170 

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

1172 
by (simp add: real_of_nat_def) 

1173 

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

1175 
by (simp add: real_of_nat_def) 

1176 

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

1178 
by (simp add: real_of_nat_def) 

1179 

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

1181 
by (simp add: real_of_nat_def) 

1182 

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

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

1185 
by (simp add: real_of_nat_def) 

1186 

1187 
lemma real_of_nat_less_iff [iff]: 

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

1189 
by (simp add: real_of_nat_def) 

1190 

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

1192 
by (simp add: real_of_nat_def) 

1193 

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

1195 
by (simp add: real_of_nat_def) 

1196 

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

1198 
by (simp add: real_of_nat_def del: of_nat_Suc) 

1199 

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

1201 
by (simp add: real_of_nat_def of_nat_mult) 

1202 

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

1204 
by (simp add: real_of_nat_def of_nat_power) 

1205 

1206 
lemmas power_real_of_nat = real_of_nat_power [symmetric] 

1207 

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

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

1210 
apply (subst real_eq_of_nat)+ 

1211 
apply (rule of_nat_setsum) 

1212 
done 

1213 

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

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

1216 
apply (subst real_eq_of_nat)+ 

1217 
apply (rule of_nat_setprod) 

1218 
done 

1219 

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

1221 
apply (subst card_eq_setsum) 

1222 
apply (subst real_of_nat_setsum) 

1223 
apply simp 

1224 
done 

1225 

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

1227 
by (simp add: real_of_nat_def) 

1228 

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

1230 
by (simp add: real_of_nat_def) 

1231 

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

1233 
by (simp add: add: real_of_nat_def of_nat_diff) 

1234 

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

1236 
by (auto simp: real_of_nat_def) 

1237 

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

1239 
by (simp add: add: real_of_nat_def) 

1240 

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

1242 
by (simp add: add: real_of_nat_def) 

1243 

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

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

1246 
apply simp 

1247 
apply (auto simp add: real_of_nat_Suc) 

1248 
done 

1249 

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

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

1252 
apply (simp add: less_Suc_eq_le) 

1253 
apply (simp add: real_of_nat_Suc) 

1254 
done 

1255 

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

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

1258 
proof  

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

1260 
by auto 

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

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

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

1264 
by simp 

1265 
then show ?thesis 

1266 
by (auto simp add: add_divide_distrib algebra_simps) 

1267 
qed 

1268 

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

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

1271 
by (subst real_of_nat_div_aux) 

1272 
(auto simp add: dvd_eq_mod_eq_0 [symmetric]) 

1273 

1274 
lemma real_of_nat_div2: 

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

1276 
apply (simp add: algebra_simps) 

1277 
apply (subst real_of_nat_div_aux) 

1278 
apply simp 

1279 
apply (subst zero_le_divide_iff) 

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 

1334 
lemma Rats_eq_int_div_int: 

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

1336 
proof 

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

1338 
proof 

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

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

1341 
have "of_rat r : ?S" 

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

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

1344 
qed 

1345 
next 

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

1347 
proof(auto simp:Rats_def) 

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

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

1350 
by (simp add:of_rat_rat real_eq_of_int) 

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

1352 
qed 

1353 
qed 

1354 

1355 
lemma Rats_eq_int_div_nat: 

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

1357 
proof(auto simp:Rats_eq_int_div_int) 

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

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

1360 
proof cases 

1361 
assume "j>0" 

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

1363 
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) 

1364 
thus ?thesis by blast 

1365 
next 

1366 
assume "~ j>0" 

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

1368 
by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat) 

1369 
thus ?thesis by blast 

1370 
qed 

1371 
next 

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

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

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

1375 
qed 

1376 

1377 
lemma Rats_abs_nat_div_natE: 

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

1379 
obtains m n :: nat 

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

1381 
proof  

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

1383 
by(auto simp add: Rats_eq_int_div_nat) 

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

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

1386 
let ?gcd = "gcd m n" 

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

1388 
let ?k = "m div ?gcd" 

1389 
let ?l = "n div ?gcd" 

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

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

1392 
by (rule dvd_mult_div_cancel) 

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

1394 
by (rule dvd_mult_div_cancel) 

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

1396 
moreover 

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

1398 
proof  

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

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

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

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

1403 
finally show ?thesis .. 

1404 
qed 

1405 
moreover 

1406 
have "?gcd' = 1" 

1407 
proof  

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

1409 
by (rule gcd_mult_distrib_nat) 

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

1411 
with gcd show ?thesis by auto 

1412 
qed 

1413 
ultimately show ?thesis .. 

1414 
qed 

1415 

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

1417 

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

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

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

1421 

1422 
lemma Rats_dense_in_real: 

1423 
fixes x :: real 

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

1425 
proof  

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

1427 
with reals_Archimedean obtain q::nat 

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

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

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

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

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

1433 
unfolding r_def p_def 

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

1435 
finally have "x < r" . 

1436 
moreover have "r < y" 

1437 
unfolding r_def p_def 

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

1439 
less_ceiling_iff [symmetric]) 

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

1441 
ultimately show ?thesis by fast 

1442 
qed 

1443 

1444 

1445 

1446 
subsection{*Numerals and Arithmetic*} 

1447 

1448 
lemma [code_abbrev]: 

1449 
"real_of_int (numeral k) = numeral k" 

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

1450 
"real_of_int ( numeral k) =  numeral k" 
51523  1451 
by simp_all 
1452 

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

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

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

1456 
"real ( numeral v :: int) =  numeral v" 
51523  1457 
by (simp_all add: real_of_int_def) 
1458 

1459 
lemma real_of_nat_numeral [simp]: 

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

1461 
by (simp add: real_of_nat_def) 

1462 

1463 
declaration {* 

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

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

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

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

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

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

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

1471 
@{thm real_of_int_mult}, @{thm real_of_int_of_nat_eq}, 

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

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

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

1475 
*} 

1476 

1477 

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

1479 

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

1481 
by arith 

1482 

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

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

1485 
by auto 

1486 

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

1488 
by auto 

1489 

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

1491 
by auto 

1492 

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

1494 
by auto 

1495 

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

1497 
by auto 

1498 

1499 
subsection {* Lemmas about powers *} 

1500 

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

1502 
declare abs_mult_self [simp] 

1503 

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

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

1506 
by simp 

1507 

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

1509 
apply (induct "n") 

1510 
apply (auto simp add: real_of_nat_Suc) 

1511 
apply (subst mult_2) 

1512 
apply (erule add_less_le_mono) 

1513 
apply (rule two_realpow_ge_one) 

1514 
done 

1515 

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

1517 
lemma realpow_Suc_le_self: 

1518 
fixes r :: "'a::linordered_semidom" 

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

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

1521 

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

1523 
lemma realpow_minus_mult: 

1524 
fixes x :: "'a::monoid_mult" 

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

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

1527 

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

1529 
lemma real_two_squares_add_zero_iff [simp]: 

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

1531 
by (rule sum_squares_eq_zero_iff) 

1532 

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

1534 
lemma realpow_two_sum_zero_iff [simp]: 

53076  1535 
"(x\<^sup>2 + y\<^sup>2 = (0::real)) = (x = 0 & y = 0)" 
51523  1536 
by (rule sum_power2_eq_zero_iff) 
1537 

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

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

1540 

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

1544 

1545 
lemma numeral_power_le_real_of_nat_cancel_iff[simp]: 

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

1547 
unfolding real_of_nat_le_iff[symmetric] by simp 

1548 

1549 
lemma real_of_nat_le_numeral_power_cancel_iff[simp]: 

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

1551 
unfolding real_of_nat_le_iff[symmetric] by simp 

1552 

1553 
lemma numeral_power_le_real_of_int_cancel_iff[simp]: 

1554 
"(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::int) ^ n \<le> a" 

1555 
unfolding real_of_int_le_iff[symmetric] by simp 

1556 

1557 
lemma real_of_int_le_numeral_power_cancel_iff[simp]: 

1558 
"real a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n" 

1559 
unfolding real_of_int_le_iff[symmetric] by simp 

1560 

1561 
lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]: 

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

1562 
"( numeral x::real) ^ n \<le> real a \<longleftrightarrow> ( numeral x::int) ^ n \<le> a" 
51523  1563 
unfolding real_of_int_le_iff[symmetric] by simp 
1564 

1565 
lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]: 

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

1566 
"real a \<le> ( numeral x::real) ^ n \<longleftrightarrow> a \<le> ( numeral x::int) ^ n" 
51523  1567 
unfolding real_of_int_le_iff[symmetric] by simp 
1568 

1569 
subsection{*Density of the Reals*} 

1570 

1571 
lemma real_lbound_gt_zero: 