author  paulson <lp15@cam.ac.uk> 
Wed, 24 Feb 2016 15:51:01 +0000  
changeset 62397  5ae24f33d343 
parent 62348  9a5f43dac883 
child 62398  a4b68bf18f8d 
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 

60758  10 
section \<open>Development of the Reals using Cauchy Sequences\<close> 
51523  11 

12 
theory Real 

51773  13 
imports Rat Conditionally_Complete_Lattices 
51523  14 
begin 
15 

60758  16 
text \<open> 
51523  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. 

60758  21 
\<close> 
51523  22 

60758  23 
subsection \<open>Preliminary lemmas\<close> 
51523  24 

61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

25 
lemma inj_add_left [simp]: 
61204  26 
fixes x :: "'a::cancel_semigroup_add" shows "inj (op+ x)" 
27 
by (meson add_left_imp_eq injI) 

28 

29 
lemma inj_mult_left [simp]: "inj (op* x) \<longleftrightarrow> x \<noteq> (0::'a::idom)" 

30 
by (metis injI mult_cancel_left the_inv_f_f zero_neq_one) 

31 

51523  32 
lemma add_diff_add: 
33 
fixes a b c d :: "'a::ab_group_add" 

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

35 
by simp 

36 

37 
lemma minus_diff_minus: 

38 
fixes a b :: "'a::ab_group_add" 

39 
shows " a   b =  (a  b)" 

40 
by simp 

41 

42 
lemma mult_diff_mult: 

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

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

45 
by (simp add: algebra_simps) 

46 

47 
lemma inverse_diff_inverse: 

48 
fixes a b :: "'a::division_ring" 

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

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

51 
using assms by (simp add: algebra_simps) 

52 

53 
lemma obtain_pos_sum: 

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

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

56 
proof 

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

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

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

60 
qed 

61 

60758  62 
subsection \<open>Sequences that converge to zero\<close> 
51523  63 

64 
definition 

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

66 
where 

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

68 

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

70 
unfolding vanishes_def by simp 

71 

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

73 
unfolding vanishes_def by simp 

74 

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

76 
unfolding vanishes_def 

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

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

79 
done 

80 

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

82 
unfolding vanishes_def by simp 

83 

84 
lemma vanishes_add: 

85 
assumes X: "vanishes X" and Y: "vanishes Y" 

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

87 
proof (rule vanishesI) 

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

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

90 
by (rule obtain_pos_sum) 

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

92 
using vanishesD [OF X s] .. 

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

94 
using vanishesD [OF Y t] .. 

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

96 
proof (clarsimp) 

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

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

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

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

101 
qed 

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

103 
qed 

104 

105 
lemma vanishes_diff: 

106 
assumes X: "vanishes X" and Y: "vanishes Y" 

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

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

108 
unfolding diff_conv_add_uminus by (intro vanishes_add vanishes_minus X Y) 
51523  109 

110 
lemma vanishes_mult_bounded: 

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

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

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

114 
proof (rule vanishesI) 

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

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

117 
using X by blast 
51523  118 
obtain b where b: "0 < b" "r = a * b" 
119 
proof 

56541  120 
show "0 < r / a" using r a by simp 
51523  121 
show "r = a * (r / a)" using a by simp 
122 
qed 

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

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

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

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

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

128 
qed 

129 

60758  130 
subsection \<open>Cauchy sequences\<close> 
51523  131 

132 
definition 

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

134 
where 

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

136 

137 
lemma cauchyI: 

138 
"(\<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" 

139 
unfolding cauchy_def by simp 

140 

141 
lemma cauchyD: 

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

143 
unfolding cauchy_def by simp 

144 

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

146 
unfolding cauchy_def by simp 

147 

148 
lemma cauchy_add [simp]: 

149 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

151 
proof (rule cauchyI) 

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

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

154 
by (rule obtain_pos_sum) 

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

156 
using cauchyD [OF X s] .. 

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

158 
using cauchyD [OF Y t] .. 

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

160 
proof (clarsimp) 

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

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

163 
unfolding add_diff_add by (rule abs_triangle_ineq) 

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

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

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

167 
qed 

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

169 
qed 

170 

171 
lemma cauchy_minus [simp]: 

172 
assumes X: "cauchy X" 

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

174 
using assms unfolding cauchy_def 

175 
unfolding minus_diff_minus abs_minus_cancel . 

176 

177 
lemma cauchy_diff [simp]: 

178 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

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

180 
using assms unfolding diff_conv_add_uminus by (simp del: add_uminus_conv_diff) 
51523  181 

182 
lemma cauchy_imp_bounded: 

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

184 
proof  

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

186 
using cauchyD [OF assms zero_less_one] .. 

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

188 
proof (intro exI conjI allI) 

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

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

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

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

193 
next 

194 
fix n :: nat 

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

196 
proof (rule linorder_le_cases) 

197 
assume "n \<le> k" 

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

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

200 
next 

201 
assume "k \<le> n" 

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

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

204 
by (rule abs_triangle_ineq) 

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

60758  206 
by (rule add_le_less_mono, simp, simp add: k \<open>k \<le> n\<close>) 
51523  207 
finally show "\<bar>X n\<bar> < Max (abs ` X ` {..k}) + 1" . 
208 
qed 

209 
qed 

210 
qed 

211 

212 
lemma cauchy_mult [simp]: 

213 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

215 
proof (rule cauchyI) 

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

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

218 
by (rule obtain_pos_sum) 

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

220 
using cauchy_imp_bounded [OF X] by blast 
51523  221 
obtain b where b: "0 < b" "\<forall>n. \<bar>Y n\<bar> < b" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

222 
using cauchy_imp_bounded [OF Y] by blast 
51523  223 
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = a * t + s * b" 
224 
proof 

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

51523  227 
show "r = a * (u/a) + (v/b) * b" 
60758  228 
using a(1) b(1) \<open>r = u + v\<close> by simp 
51523  229 
qed 
230 
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m  X n\<bar> < s" 

231 
using cauchyD [OF X s] .. 

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

233 
using cauchyD [OF Y t] .. 

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

235 
proof (clarsimp) 

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

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

238 
unfolding mult_diff_mult .. 

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

240 
by (rule abs_triangle_ineq) 

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

242 
unfolding abs_mult .. 

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

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

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

246 
qed 

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

248 
qed 

249 

250 
lemma cauchy_not_vanishes_cases: 

251 
assumes X: "cauchy X" 

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

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

254 
proof  

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

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

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

60758  258 
using \<open>0 < r\<close> by (rule obtain_pos_sum) 
51523  259 
obtain i where i: "\<forall>m\<ge>i. \<forall>n\<ge>i. \<bar>X m  X n\<bar> < s" 
260 
using cauchyD [OF X s] .. 

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

262 
using r by blast 
51523  263 
have k: "\<forall>n\<ge>k. \<bar>X n  X k\<bar> < s" 
60758  264 
using i \<open>i \<le> k\<close> by auto 
51523  265 
have "X k \<le>  r \<or> r \<le> X k" 
60758  266 
using \<open>r \<le> \<bar>X k\<bar>\<close> by auto 
51523  267 
hence "(\<forall>n\<ge>k. t <  X n) \<or> (\<forall>n\<ge>k. t < X n)" 
60758  268 
unfolding \<open>r = s + t\<close> using k by auto 
51523  269 
hence "\<exists>k. (\<forall>n\<ge>k. t <  X n) \<or> (\<forall>n\<ge>k. t < X n)" .. 
270 
thus "\<exists>t>0. \<exists>k. (\<forall>n\<ge>k. t <  X n) \<or> (\<forall>n\<ge>k. t < X n)" 

271 
using t by auto 

272 
qed 

273 

274 
lemma cauchy_not_vanishes: 

275 
assumes X: "cauchy X" 

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

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

278 
using cauchy_not_vanishes_cases [OF assms] 

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

280 

281 
lemma cauchy_inverse [simp]: 

282 
assumes X: "cauchy X" 

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

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

285 
proof (rule cauchyI) 

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

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

288 
using cauchy_not_vanishes [OF X nz] by blast 
51523  289 
from b i have nz: "\<forall>n\<ge>i. X n \<noteq> 0" by auto 
290 
obtain s where s: "0 < s" and r: "r = inverse b * s * inverse b" 

291 
proof 

60758  292 
show "0 < b * r * b" by (simp add: \<open>0 < r\<close> b) 
51523  293 
show "r = inverse b * (b * r * b) * inverse b" 
294 
using b by simp 

295 
qed 

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

297 
using cauchyD [OF X s] .. 

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

299 
proof (clarsimp) 

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

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

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

303 
by (simp add: inverse_diff_inverse nz * abs_mult) 

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

305 
by (simp add: mult_strict_mono less_imp_inverse_less 

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

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

310 
qed 

311 

312 
lemma vanishes_diff_inverse: 

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

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

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

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

317 
proof (rule vanishesI) 

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

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

320 
using cauchy_not_vanishes [OF X] by blast 
51523  321 
obtain b j where b: "0 < b" and j: "\<forall>n\<ge>j. b < \<bar>Y n\<bar>" 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

322 
using cauchy_not_vanishes [OF Y] by blast 
51523  323 
obtain s where s: "0 < s" and "inverse a * s * inverse b = r" 
324 
proof 

325 
show "0 < a * r * b" 

56544  326 
using a r b by simp 
51523  327 
show "inverse a * (a * r * b) * inverse b = r" 
328 
using a r b by simp 

329 
qed 

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

331 
using vanishesD [OF XY s] .. 

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

333 
proof (clarsimp) 

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

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

336 
using i j a b n by auto 

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

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

339 
by (simp add: inverse_diff_inverse abs_mult) 

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

341 
apply (intro mult_strict_mono' less_imp_inverse_less) 

56536  342 
apply (simp_all add: a b i j k n) 
51523  343 
done 
60758  344 
also note \<open>inverse a * s * inverse b = r\<close> 
51523  345 
finally show "\<bar>inverse (X n)  inverse (Y n)\<bar> < r" . 
346 
qed 

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

348 
qed 

349 

60758  350 
subsection \<open>Equivalence relation on Cauchy sequences\<close> 
51523  351 

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

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

354 

355 
lemma realrelI [intro?]: 

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

357 
shows "realrel X Y" 

358 
using assms unfolding realrel_def by simp 

359 

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

361 
unfolding realrel_def by simp 

362 

363 
lemma symp_realrel: "symp realrel" 

364 
unfolding realrel_def 

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

366 

367 
lemma transp_realrel: "transp realrel" 

368 
unfolding realrel_def 

369 
apply (rule transpI, clarify) 

370 
apply (drule (1) vanishes_add) 

371 
apply (simp add: algebra_simps) 

372 
done 

373 

374 
lemma part_equivp_realrel: "part_equivp realrel" 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

375 
by (blast intro: part_equivpI symp_realrel transp_realrel 
51523  376 
realrel_refl cauchy_const) 
377 

60758  378 
subsection \<open>The field of real numbers\<close> 
51523  379 

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

381 
morphisms rep_real Real 

382 
by (rule part_equivp_realrel) 

383 

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

385 
unfolding real.pcr_cr_eq cr_real_def realrel_def by auto 

386 

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

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

389 
proof (induct x) 

390 
case (1 X) 

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

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

393 
qed 

394 

395 
lemma eq_Real: 

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

397 
using real.rel_eq_transfer 

55945  398 
unfolding real.pcr_cr_eq cr_real_def rel_fun_def realrel_def by simp 
51523  399 

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

400 
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

401 
by (simp add: real.domain_eq realrel_def) 
51523  402 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59587
diff
changeset

403 
instantiation real :: field 
51523  404 
begin 
405 

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

407 
by (simp add: realrel_refl) 

408 

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

410 
by (simp add: realrel_refl) 

411 

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

413 
unfolding realrel_def add_diff_add 

414 
by (simp only: cauchy_add vanishes_add simp_thms) 

415 

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

417 
unfolding realrel_def minus_diff_minus 

418 
by (simp only: cauchy_minus vanishes_minus simp_thms) 

419 

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

421 
unfolding realrel_def mult_diff_mult 

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

422 
by (subst (4) mult.commute, simp only: cauchy_mult vanishes_add 
51523  423 
vanishes_mult_bounded cauchy_imp_bounded simp_thms) 
424 

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

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

427 
proof  

428 
fix X Y assume "realrel X Y" 

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

430 
unfolding realrel_def by simp_all 

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

432 
proof 

433 
assume "vanishes X" 

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

435 
next 

436 
assume "vanishes Y" 

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

438 
qed 

439 
thus "?thesis X Y" 

440 
unfolding realrel_def 

441 
by (simp add: vanishes_diff_inverse X Y XY) 

442 
qed 

443 

444 
definition 

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

446 

447 
definition 

60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60352
diff
changeset

448 
"x div y = (x::real) * inverse y" 
51523  449 

450 
lemma add_Real: 

451 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

453 
using assms plus_real.transfer 

55945  454 
unfolding cr_real_eq rel_fun_def by simp 
51523  455 

456 
lemma minus_Real: 

457 
assumes X: "cauchy X" 

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

459 
using assms uminus_real.transfer 

55945  460 
unfolding cr_real_eq rel_fun_def by simp 
51523  461 

462 
lemma diff_Real: 

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

464 
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

465 
unfolding minus_real_def 
51523  466 
by (simp add: minus_Real add_Real X Y) 
467 

468 
lemma mult_Real: 

469 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

471 
using assms times_real.transfer 

55945  472 
unfolding cr_real_eq rel_fun_def by simp 
51523  473 

474 
lemma inverse_Real: 

475 
assumes X: "cauchy X" 

476 
shows "inverse (Real X) = 

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

478 
using assms inverse_real.transfer zero_real.transfer 

55945  479 
unfolding cr_real_eq rel_fun_def by (simp split: split_if_asm, metis) 
51523  480 

481 
instance proof 

482 
fix a b c :: real 

483 
show "a + b = b + a" 

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

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

486 
by transfer (simp add: ac_simps realrel_def) 
51523  487 
show "0 + a = a" 
488 
by transfer (simp add: realrel_def) 

489 
show " a + a = 0" 

490 
by transfer (simp add: realrel_def) 

491 
show "a  b = a +  b" 

492 
by (rule minus_real_def) 

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

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

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

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

498 
by transfer (simp add: ac_simps realrel_def) 
51523  499 
show "(a + b) * c = a * c + b * c" 
500 
by transfer (simp add: distrib_right realrel_def) 

61076  501 
show "(0::real) \<noteq> (1::real)" 
51523  502 
by transfer (simp add: realrel_def) 
503 
show "a \<noteq> 0 \<Longrightarrow> inverse a * a = 1" 

504 
apply transfer 

505 
apply (simp add: realrel_def) 

506 
apply (rule vanishesI) 

507 
apply (frule (1) cauchy_not_vanishes, clarify) 

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

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

510 
done 

60429
d3d1e185cd63
uniform _ div _ as infix syntax for ring division
haftmann
parents:
60352
diff
changeset

511 
show "a div b = a * inverse b" 
51523  512 
by (rule divide_real_def) 
513 
show "inverse (0::real) = 0" 

514 
by transfer (simp add: realrel_def) 

515 
qed 

516 

517 
end 

518 

60758  519 
subsection \<open>Positive reals\<close> 
51523  520 

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

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

523 
proof  

524 
{ fix X Y 

525 
assume "realrel X Y" 

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

527 
unfolding realrel_def by simp_all 

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

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

530 
by blast 
51523  531 
obtain s t where s: "0 < s" and t: "0 < t" and r: "r = s + t" 
60758  532 
using \<open>0 < r\<close> by (rule obtain_pos_sum) 
51523  533 
obtain j where j: "\<forall>n\<ge>j. \<bar>X n  Y n\<bar> < s" 
534 
using vanishesD [OF XY s] .. 

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

536 
proof (clarsimp) 

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

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

539 
using i j n by simp_all 

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

541 
qed 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

542 
hence "\<exists>r>0. \<exists>k. \<forall>n\<ge>k. r < Y n" using t by blast 
51523  543 
} note 1 = this 
544 
fix X Y assume "realrel X Y" 

545 
hence "realrel X Y" and "realrel Y X" 

546 
using symp_realrel unfolding symp_def by auto 

547 
thus "?thesis X Y" 

548 
by (safe elim!: 1) 

549 
qed 

550 

551 
lemma positive_Real: 

552 
assumes X: "cauchy X" 

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

554 
using assms positive.transfer 

55945  555 
unfolding cr_real_eq rel_fun_def by simp 
51523  556 

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

558 
by transfer auto 

559 

560 
lemma positive_add: 

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

562 
apply transfer 

563 
apply (clarify, rename_tac a b i j) 

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

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

566 
apply (simp add: add_strict_mono) 

567 
done 

568 

569 
lemma positive_mult: 

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

571 
apply transfer 

572 
apply (clarify, rename_tac a b i j) 

56544  573 
apply (rule_tac x="a * b" in exI, simp) 
51523  574 
apply (rule_tac x="max i j" in exI, clarsimp) 
575 
apply (rule mult_strict_mono, auto) 

576 
done 

577 

578 
lemma positive_minus: 

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

580 
apply transfer 

581 
apply (simp add: realrel_def) 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

582 
apply (drule (1) cauchy_not_vanishes_cases, safe) 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

583 
apply blast+ 
51523  584 
done 
585 

59867
58043346ca64
given up separate type classes demanding `inverse 0 = 0`
haftmann
parents:
59587
diff
changeset

586 
instantiation real :: linordered_field 
51523  587 
begin 
588 

589 
definition 

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

591 

592 
definition 

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

594 

595 
definition 

61944  596 
"\<bar>a::real\<bar> = (if a < 0 then  a else a)" 
51523  597 

598 
definition 

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

600 

601 
instance proof 

602 
fix a b c :: real 

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

604 
by (rule abs_real_def) 

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

606 
unfolding less_eq_real_def less_real_def 

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

608 
show "a \<le> a" 

609 
unfolding less_eq_real_def by simp 

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

611 
unfolding less_eq_real_def less_real_def 

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

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

614 
unfolding less_eq_real_def less_real_def 

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

616 
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

617 
unfolding less_eq_real_def less_real_def by auto 
51523  618 
(* FIXME: Procedure int_combine_numerals: c + b  (c + a) \<equiv> b +  a *) 
619 
(* Should produce c + b  (c + a) \<equiv> b  a *) 

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

621 
by (rule sgn_real_def) 

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

623 
unfolding less_eq_real_def less_real_def 

624 
by (auto dest!: positive_minus) 

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

626 
unfolding less_real_def 

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

628 
qed 

629 

630 
end 

631 

632 
instantiation real :: distrib_lattice 

633 
begin 

634 

635 
definition 

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

637 

638 
definition 

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

640 

641 
instance proof 

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

642 
qed (auto simp add: inf_real_def sup_real_def max_min_distrib2) 
51523  643 

644 
end 

645 

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

647 
apply (induct x) 

648 
apply (simp add: zero_real_def) 

649 
apply (simp add: one_real_def add_Real) 

650 
done 

651 

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

653 
apply (cases x rule: int_diff_cases) 

654 
apply (simp add: of_nat_Real diff_Real) 

655 
done 

656 

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

658 
apply (induct x) 

659 
apply (simp add: Fract_of_int_quotient of_rat_divide) 

660 
apply (simp add: of_int_Real divide_inverse) 

661 
apply (simp add: inverse_Real mult_Real) 

662 
done 

663 

664 
instance real :: archimedean_field 

665 
proof 

666 
fix x :: real 

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

668 
apply (induct x) 

669 
apply (frule cauchy_imp_bounded, clarify) 

61942  670 
apply (rule_tac x="\<lceil>b\<rceil> + 1" in exI) 
51523  671 
apply (rule less_imp_le) 
672 
apply (simp add: of_int_Real less_real_def diff_Real positive_Real) 

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

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

675 
apply (rule le_less_trans [OF abs_ge_self]) 

676 
apply (rule less_le_trans [OF _ le_of_int_ceiling]) 

677 
apply simp 

678 
done 

679 
qed 

680 

681 
instantiation real :: floor_ceiling 

682 
begin 

683 

684 
definition [code del]: 

61942  685 
"\<lfloor>x::real\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" 
51523  686 

61942  687 
instance 
688 
proof 

51523  689 
fix x :: real 
61942  690 
show "of_int \<lfloor>x\<rfloor> \<le> x \<and> x < of_int (\<lfloor>x\<rfloor> + 1)" 
51523  691 
unfolding floor_real_def using floor_exists1 by (rule theI') 
692 
qed 

693 

694 
end 

695 

60758  696 
subsection \<open>Completeness\<close> 
51523  697 

698 
lemma not_positive_Real: 

699 
assumes X: "cauchy X" 

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

701 
unfolding positive_Real [OF X] 

702 
apply (auto, unfold not_less) 

703 
apply (erule obtain_pos_sum) 

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

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

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

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

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

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

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

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

712 
done 

713 

714 
lemma le_Real: 

715 
assumes X: "cauchy X" and Y: "cauchy Y" 

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

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

718 
apply (simp add: diff_Real not_positive_Real X Y) 

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

719 
apply (simp add: diff_le_eq ac_simps) 
51523  720 
done 
721 

722 
lemma le_RealI: 

723 
assumes Y: "cauchy Y" 

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

725 
proof (induct x) 

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

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

728 
by (simp add: of_rat_Real le_Real) 

729 
{ 

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

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

732 
by (rule obtain_pos_sum) 

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

734 
using cauchyD [OF Y s] .. 

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

736 
using le [OF t] .. 

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

738 
proof (clarsimp) 

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

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

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

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

743 
qed 

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

745 
} 

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

747 
by (simp add: of_rat_Real le_Real X Y) 

748 
qed 

749 

750 
lemma Real_leI: 

751 
assumes X: "cauchy X" 

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

753 
shows "Real X \<le> y" 

754 
proof  

755 
have " y \<le>  Real X" 

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

757 
thus ?thesis by simp 

758 
qed 

759 

760 
lemma less_RealD: 

761 
assumes Y: "cauchy Y" 

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

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

764 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

765 
lemma of_nat_less_two_power [simp]: 
51523  766 
"of_nat n < (2::'a::linordered_idom) ^ n" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

767 
apply (induct n, simp) 
60162  768 
by (metis add_le_less_mono mult_2 of_nat_Suc one_le_numeral one_le_power power_Suc) 
51523  769 

770 
lemma complete_real: 

771 
fixes S :: "real set" 

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

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

774 
proof  

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

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

777 

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

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

780 
proof 

61942  781 
have "of_int \<lfloor>x  1\<rfloor> \<le> x  1" by (rule of_int_floor_le) 
51523  782 
also have "x  1 < x" by simp 
61942  783 
finally have "of_int \<lfloor>x  1\<rfloor> < x" . 
784 
hence "\<not> x \<le> of_int \<lfloor>x  1\<rfloor>" by (simp only: not_le) 

785 
then show "\<not> P (of_int \<lfloor>x  1\<rfloor>)" 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

786 
unfolding P_def of_rat_of_int_eq using x by blast 
51523  787 
qed 
788 
obtain b where b: "P b" 

789 
proof 

61942  790 
show "P (of_int \<lceil>z\<rceil>)" 
51523  791 
unfolding P_def of_rat_of_int_eq 
792 
proof 

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

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

61942  795 
also have "z \<le> of_int \<lceil>z\<rceil>" by (rule le_of_int_ceiling) 
796 
finally show "y \<le> of_int \<lceil>z\<rceil>" . 

51523  797 
qed 
798 
qed 

799 

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

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

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

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

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

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

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

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

808 
unfolding A_def B_def C_def bisect_def split_def by simp 

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

810 
unfolding A_def B_def C_def bisect_def split_def by simp 

811 

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

813 
apply (simp add: eq_divide_eq) 

814 
apply (induct_tac n, simp) 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

815 
apply (simp add: C_def avg_def algebra_simps) 
51523  816 
done 
817 

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

819 
apply (simp add: divide_less_eq) 

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

820 
apply (subst mult.commute) 
51523  821 
apply (frule_tac y=y in ex_less_of_nat_mult) 
822 
apply clarify 

823 
apply (rule_tac x=n in exI) 

824 
apply (erule less_trans) 

825 
apply (rule mult_strict_right_mono) 

826 
apply (rule le_less_trans [OF _ of_nat_less_two_power]) 

827 
apply simp 

828 
apply assumption 

829 
done 

830 

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

832 
by (induct_tac n, simp_all add: a) 

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

834 
by (induct_tac n, simp_all add: b) 

835 
have ab: "a < b" 

836 
using a b unfolding P_def 

837 
apply (clarsimp simp add: not_le) 

838 
apply (drule (1) bspec) 

839 
apply (drule (1) less_le_trans) 

840 
apply (simp add: of_rat_less) 

841 
done 

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

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

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

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

846 
apply (erule less_Suc_induct) 

847 
apply (clarsimp simp add: C_def avg_def) 

848 
apply (simp add: add_divide_distrib [symmetric]) 

849 
apply (rule AB [THEN less_imp_le]) 

850 
apply simp 

851 
done 

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

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

854 
apply (erule less_Suc_induct) 

855 
apply (clarsimp simp add: C_def avg_def) 

856 
apply (simp add: add_divide_distrib [symmetric]) 

857 
apply (rule AB [THEN less_imp_le]) 

858 
apply simp 

859 
done 

860 
have cauchy_lemma: 

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

862 
apply (rule cauchyI) 

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

864 
apply (erule exE) 

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

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

867 
apply (simp add: width) 

868 
apply (drule_tac x=n in spec) 

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

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

871 
apply (frule A_mono, drule B_mono) 

872 
apply (frule A_mono, drule B_mono) 

873 
apply arith 

874 
done 

875 
have "cauchy A" 

876 
apply (rule cauchy_lemma [rule_format]) 

877 
apply (simp add: A_mono) 

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

879 
done 

880 
have "cauchy B" 

881 
apply (rule cauchy_lemma [rule_format]) 

882 
apply (simp add: B_mono) 

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

884 
done 

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

886 
proof 

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

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

60758  889 
using PB [unfolded P_def] \<open>cauchy B\<close> 
51523  890 
by (simp add: le_RealI) 
891 
qed 

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

893 
apply clarify 

894 
apply (erule contrapos_pp) 

895 
apply (simp add: not_le) 

60758  896 
apply (drule less_RealD [OF \<open>cauchy A\<close>], clarify) 
51523  897 
apply (subgoal_tac "\<not> P (A n)") 
898 
apply (simp add: P_def not_le, clarify) 

899 
apply (erule rev_bexI) 

900 
apply (erule (1) less_trans) 

901 
apply (simp add: PA) 

902 
done 

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

904 
proof (rule vanishesI) 

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

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

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

907 
using twos by blast 
51523  908 
have "\<forall>n\<ge>k. \<bar>(b  a) / 2 ^ n\<bar> < r" 
909 
proof (clarify) 

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

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

912 
by simp 

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

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

917 
qed 

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

919 
qed 

920 
hence 3: "Real B = Real A" 

60758  921 
by (simp add: eq_Real \<open>cauchy A\<close> \<open>cauchy B\<close> width) 
51523  922 
show "\<exists>y. (\<forall>x\<in>S. x \<le> y) \<and> (\<forall>z. (\<forall>x\<in>S. x \<le> z) \<longrightarrow> y \<le> z)" 
923 
using 1 2 3 by (rule_tac x="Real B" in exI, simp) 

924 
qed 

925 

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

926 
instantiation real :: linear_continuum 
51523  927 
begin 
928 

60758  929 
subsection\<open>Supremum of a set of reals\<close> 
51523  930 

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

51523  933 

934 
instance 

935 
proof 

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

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

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

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

942 
note Sup_upper = this 

943 

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

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

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

947 
using complete_real[of X] by blast 

948 
then have "Sup X = s" 

61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

949 
unfolding Sup_real_def by (best intro: Least_equality) 
53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53076
diff
changeset

950 
also from s z have "... \<le> z" 
51523  951 
by blast 
952 
finally show "Sup X \<le> z" . } 

953 
note Sup_least = this 

954 

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

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

958 
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

959 
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

960 
using zero_neq_one by blast 
51523  961 
qed 
962 
end 

963 

964 

60758  965 
subsection \<open>Hiding implementation details\<close> 
51523  966 

967 
hide_const (open) vanishes cauchy positive Real 

968 

969 
declare Real_induct [induct del] 

970 
declare Abs_real_induct [induct del] 

971 
declare Abs_real_cases [cases del] 

972 

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

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

974 
lifting_forget real.lifting 
61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

975 

60758  976 
subsection\<open>More Lemmas\<close> 
51523  977 

60758  978 
text \<open>BH: These lemmas should not be necessary; they should be 
979 
covered by existing simp rules and simplification procedures.\<close> 

51523  980 

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

982 
by simp (* solved by linordered_ring_less_cancel_factor simproc *) 

983 

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

985 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

986 

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

988 
by simp (* solved by linordered_ring_le_cancel_factor simproc *) 

989 

990 

60758  991 
subsection \<open>Embedding numbers into the Reals\<close> 
51523  992 

993 
abbreviation 

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

995 
where 

996 
"real_of_nat \<equiv> of_nat" 

997 

998 
abbreviation 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

999 
real :: "nat \<Rightarrow> real" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1000 
where 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1001 
"real \<equiv> of_nat" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1002 

77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1003 
abbreviation 
51523  1004 
real_of_int :: "int \<Rightarrow> real" 
1005 
where 

1006 
"real_of_int \<equiv> of_int" 

1007 

1008 
abbreviation 

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

1010 
where 

1011 
"real_of_rat \<equiv> of_rat" 

1012 

1013 
declare [[coercion_enabled]] 

59000  1014 

1015 
declare [[coercion "of_nat :: nat \<Rightarrow> int"]] 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1016 
declare [[coercion "of_nat :: nat \<Rightarrow> real"]] 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1017 
declare [[coercion "of_int :: int \<Rightarrow> real"]] 
59000  1018 

1019 
(* We do not add rat to the coerced types, this has often unpleasant side effects when writing 

1020 
inverse (Suc n) which sometimes gets two coercions: of_rat (inverse (of_nat (Suc n))) *) 

51523  1021 

1022 
declare [[coercion_map map]] 

59000  1023 
declare [[coercion_map "\<lambda>f g h x. g (h (f x))"]] 
1024 
declare [[coercion_map "\<lambda>f g (x,y). (f x, g y)"]] 

51523  1025 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1026 
declare of_int_eq_0_iff [algebra, presburger] 
61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1027 
declare of_int_eq_1_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1028 
declare of_int_eq_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1029 
declare of_int_less_0_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1030 
declare of_int_less_1_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1031 
declare of_int_less_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1032 
declare of_int_le_0_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1033 
declare of_int_le_1_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1034 
declare of_int_le_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1035 
declare of_int_0_less_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1036 
declare of_int_0_le_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1037 
declare of_int_1_less_iff [algebra, presburger] 
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1038 
declare of_int_1_le_iff [algebra, presburger] 
51523  1039 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1040 
lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1041 
proof  
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1042 
have "(0::real) \<le> 1" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1043 
by (metis less_eq_real_def zero_less_one) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1044 
thus ?thesis 
61694
6571c78c9667
Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
paulson <lp15@cam.ac.uk>
parents:
61649
diff
changeset

1045 
by (metis floor_of_int less_floor_iff) 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1046 
qed 
51523  1047 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1048 
lemma int_le_real_less: "(n \<le> m) = (real_of_int n < real_of_int m + 1)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1049 
by (meson int_less_real_le not_le) 
51523  1050 

1051 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1052 
lemma real_of_int_div_aux: "(real_of_int x) / (real_of_int d) = 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1053 
real_of_int (x div d) + (real_of_int (x mod d)) / (real_of_int d)" 
51523  1054 
proof  
1055 
have "x = (x div d) * d + x mod d" 

1056 
by auto 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1057 
then have "real_of_int x = real_of_int (x div d) * real_of_int d + real_of_int(x mod d)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1058 
by (metis of_int_add of_int_mult) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1059 
then have "real_of_int x / real_of_int d = ... / real_of_int d" 
51523  1060 
by simp 
1061 
then show ?thesis 

1062 
by (auto simp add: add_divide_distrib algebra_simps) 

1063 
qed 

1064 

58834  1065 
lemma real_of_int_div: 
1066 
fixes d n :: int 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1067 
shows "d dvd n \<Longrightarrow> real_of_int (n div d) = real_of_int n / real_of_int d" 
58834  1068 
by (simp add: real_of_int_div_aux) 
51523  1069 

1070 
lemma real_of_int_div2: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1071 
"0 <= real_of_int n / real_of_int x  real_of_int (n div x)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1072 
apply (case_tac "x = 0", simp) 
51523  1073 
apply (case_tac "0 < x") 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1074 
apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1075 
apply (metis add.left_neutral floor_correct floor_divide_of_int_eq le_diff_eq) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1076 
done 
51523  1077 

1078 
lemma real_of_int_div3: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1079 
"real_of_int (n::int) / real_of_int (x)  real_of_int (n div x) <= 1" 
51523  1080 
apply (simp add: algebra_simps) 
1081 
apply (subst real_of_int_div_aux) 

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

1083 
done 

1084 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1085 
lemma real_of_int_div4: "real_of_int (n div x) <= real_of_int (n::int) / real_of_int x" 
51523  1086 
by (insert real_of_int_div2 [of n x], simp) 
1087 

1088 

60758  1089 
subsection\<open>Embedding the Naturals into the Reals\<close> 
51523  1090 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1091 
lemma real_of_card: "real (card A) = setsum (\<lambda>x.1) A" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1092 
by simp 
51523  1093 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1094 
lemma nat_less_real_le: "(n < m) = (real n + 1 \<le> real m)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1095 
by (metis discrete of_nat_1 of_nat_add of_nat_le_iff) 
51523  1096 

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

61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

1098 
by (meson nat_less_real_le not_le) 
51523  1099 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1100 
lemma real_of_nat_div_aux: "(real x) / (real d) = 
51523  1101 
real (x div d) + (real (x mod d)) / (real d)" 
1102 
proof  

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

1104 
by auto 

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

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1106 
by (metis of_nat_add of_nat_mult) 
51523  1107 
then have "real x / real d = \<dots> / real d" 
1108 
by simp 

1109 
then show ?thesis 

1110 
by (auto simp add: add_divide_distrib algebra_simps) 

1111 
qed 

1112 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1113 
lemma real_of_nat_div: "d dvd n \<Longrightarrow> real(n div d) = real n / real d" 
51523  1114 
by (subst real_of_nat_div_aux) 
1115 
(auto simp add: dvd_eq_mod_eq_0 [symmetric]) 

1116 

1117 
lemma real_of_nat_div2: 

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

1119 
apply (simp add: algebra_simps) 

1120 
apply (subst real_of_nat_div_aux) 

1121 
apply simp 

1122 
done 

1123 

1124 
lemma real_of_nat_div3: 

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

1126 
apply(case_tac "x = 0") 

1127 
apply (simp) 

1128 
apply (simp add: algebra_simps) 

1129 
apply (subst real_of_nat_div_aux) 

1130 
apply simp 

1131 
done 

1132 

61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

1133 
lemma real_of_nat_div4: "real (n div x) <= real (n::nat) / real x" 
51523  1134 
by (insert real_of_nat_div2 [of n x], simp) 
1135 

60758  1136 
subsection \<open>The Archimedean Property of the Reals\<close> 
51523  1137 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1138 
lemmas reals_Archimedean = ex_inverse_of_nat_Suc_less (*FIXME*) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1139 
lemmas reals_Archimedean2 = ex_less_of_nat 
51523  1140 

1141 
lemma reals_Archimedean3: 

1142 
assumes x_greater_zero: "0 < x" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1143 
shows "\<forall>y. \<exists>n. y < real n * x" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1144 
using \<open>0 < x\<close> by (auto intro: ex_less_of_nat_mult) 
51523  1145 

62397
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1146 
lemma real_archimedian_rdiv_eq_0: 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1147 
assumes x0: "x \<ge> 0" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1148 
and c: "c \<ge> 0" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1149 
and xc: "\<And>m::nat. m > 0 \<Longrightarrow> real m * x \<le> c" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1150 
shows "x = 0" 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1151 
by (metis reals_Archimedean3 dual_order.order_iff_strict le0 le_less_trans not_le x0 xc) 
5ae24f33d343
Substantial new material for multivariate analysis. Also removal of some duplicates.
paulson <lp15@cam.ac.uk>
parents:
62348
diff
changeset

1152 

51523  1153 

60758  1154 
subsection\<open>Rationals\<close> 
51523  1155 

1156 
lemma Rats_eq_int_div_int: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1157 
"\<rat> = { real_of_int i / real_of_int j i j. j \<noteq> 0}" (is "_ = ?S") 
51523  1158 
proof 
1159 
show "\<rat> \<subseteq> ?S" 

1160 
proof 

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

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

1163 
have "of_rat r : ?S" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1164 
by (cases r) (auto simp add:of_rat_rat) 
60758  1165 
thus "x : ?S" using \<open>x = of_rat r\<close> by simp 
51523  1166 
qed 
1167 
next 

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

1169 
proof(auto simp:Rats_def) 

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

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1171 
hence "real_of_int i / real_of_int j = of_rat(Fract i j)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1172 
by (simp add: of_rat_rat) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1173 
thus "real_of_int i / real_of_int j \<in> range of_rat" by blast 
51523  1174 
qed 
1175 
qed 

1176 

1177 
lemma Rats_eq_int_div_nat: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1178 
"\<rat> = { real_of_int i / real n i n. n \<noteq> 0}" 
51523  1179 
proof(auto simp:Rats_eq_int_div_int) 
1180 
fix i j::int assume "j \<noteq> 0" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1181 
show "EX (i'::int) (n::nat). real_of_int i / real_of_int j = real_of_int i'/real n \<and> 0<n" 
51523  1182 
proof cases 
1183 
assume "j>0" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1184 
hence "real_of_int i / real_of_int j = real_of_int i/real(nat j) \<and> 0<nat j" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1185 
by (simp add: of_nat_nat) 
51523  1186 
thus ?thesis by blast 
1187 
next 

1188 
assume "~ j>0" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1189 
hence "real_of_int i / real_of_int j = real_of_int(i) / real(nat(j)) \<and> 0<nat(j)" using \<open>j\<noteq>0\<close> 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1190 
by (simp add: of_nat_nat) 
51523  1191 
thus ?thesis by blast 
1192 
qed 

1193 
next 

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

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1195 
hence "real_of_int i / real n = real_of_int i / real_of_int(int n) \<and> int n \<noteq> 0" by simp 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1196 
thus "\<exists>i' j. real_of_int i / real n = real_of_int i' / real_of_int j \<and> j \<noteq> 0" by blast 
51523  1197 
qed 
1198 

1199 
lemma Rats_abs_nat_div_natE: 

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

1201 
obtains m n :: nat 

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

1203 
proof  

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1204 
from \<open>x \<in> \<rat>\<close> obtain i::int and n::nat where "n \<noteq> 0" and "x = real_of_int i / real n" 
51523  1205 
by(auto simp add: Rats_eq_int_div_nat) 
61944  1206 
hence "\<bar>x\<bar> = real (nat \<bar>i\<bar>) / real n" by (simp add: of_nat_nat) 
51523  1207 
then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast 
1208 
let ?gcd = "gcd m n" 

60758  1209 
from \<open>n\<noteq>0\<close> have gcd: "?gcd \<noteq> 0" by simp 
51523  1210 
let ?k = "m div ?gcd" 
1211 
let ?l = "n div ?gcd" 

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

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

1214 
by (rule dvd_mult_div_cancel) 

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

1216 
by (rule dvd_mult_div_cancel) 

60758  1217 
from \<open>n \<noteq> 0\<close> and gcd_l 
58834  1218 
have "?gcd * ?l \<noteq> 0" by simp 
61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

1219 
then have "?l \<noteq> 0" by (blast dest!: mult_not_zero) 
51523  1220 
moreover 
1221 
have "\<bar>x\<bar> = real ?k / real ?l" 

1222 
proof  

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1223 
from gcd have "real ?k / real ?l = real (?gcd * ?k) / real (?gcd * ?l)" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1224 
by (simp add: real_of_nat_div) 
51523  1225 
also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp 
1226 
also from x_rat have "\<dots> = \<bar>x\<bar>" .. 

1227 
finally show ?thesis .. 

1228 
qed 

1229 
moreover 

1230 
have "?gcd' = 1" 

1231 
proof  

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

1233 
by (rule gcd_mult_distrib_nat) 

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

1235 
with gcd show ?thesis by auto 

1236 
qed 

1237 
ultimately show ?thesis .. 

1238 
qed 

1239 

60758  1240 
subsection\<open>Density of the Rational Reals in the Reals\<close> 
51523  1241 

60758  1242 
text\<open>This density proof is due to Stefan Richter and was ported by TN. The 
51523  1243 
original source is \emph{Real Analysis} by H.L. Royden. 
60758  1244 
It employs the Archimedean property of the reals.\<close> 
51523  1245 

1246 
lemma Rats_dense_in_real: 

1247 
fixes x :: real 

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

1249 
proof  

60758  1250 
from \<open>x<y\<close> have "0 < yx" by simp 
61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

1251 
with reals_Archimedean obtain q::nat 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1252 
where q: "inverse (real q) < yx" and "0 < q" by blast 
61942  1253 
def p \<equiv> "\<lceil>y * real q\<rceil>  1" 
51523  1254 
def r \<equiv> "of_int p / real q" 
1255 
from q have "x < y  inverse (real q)" by simp 

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

1257 
unfolding r_def p_def 

60758  1258 
by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling \<open>0 < q\<close>) 
51523  1259 
finally have "x < r" . 
1260 
moreover have "r < y" 

1261 
unfolding r_def p_def 

60758  1262 
by (simp add: divide_less_eq diff_less_eq \<open>0 < q\<close> 
51523  1263 
less_ceiling_iff [symmetric]) 
1264 
moreover from r_def have "r \<in> \<rat>" by simp 

61649
268d88ec9087
Tweaks for "real": Removal of [iff] status for some lemmas, adding [simp] for others. Plus fixes.
paulson <lp15@cam.ac.uk>
parents:
61609
diff
changeset

1265 
ultimately show ?thesis by blast 
51523  1266 
qed 
1267 

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

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

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

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

1271 
shows "\<exists>q :: rat. x < of_rat q \<and> of_rat q < y" 
60758  1272 
using Rats_dense_in_real [OF \<open>x < y\<close>] 
57447
87429bdecad5
import more stuff from the CLT proof; base the lborel measure on interval_measure; remove lebesgue measure
hoelzl
parents:
57275
diff
changeset

1273 
by (auto elim: Rats_cases) 
51523  1274 

1275 

60758  1276 
subsection\<open>Numerals and Arithmetic\<close> 
51523  1277 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1278 
lemma [code_abbrev]: (*FIXME*) 
51523  1279 
"real_of_int (numeral k) = numeral k" 
54489
03ff4d1e6784
eliminiated neg_numeral in favour of  (numeral _)
haftmann
parents:
54281
diff
changeset

1280 
"real_of_int ( numeral k) =  numeral k" 
51523  1281 
by simp_all 
1282 

60758  1283 
declaration \<open> 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1284 
K (Lin_Arith.add_inj_thms [@{thm of_nat_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1285 
(* not needed because x < (y::nat) can be rewritten as Suc x <= y: of_nat_less_iff RS iffD2 *) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1286 
#> Lin_Arith.add_inj_thms [@{thm of_int_le_iff} RS iffD2, @{thm of_nat_eq_iff} RS iffD2] 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1287 
(* not needed because x < (y::int) can be rewritten as x + 1 <= y: of_int_less_iff RS iffD2 *) 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1288 
#> Lin_Arith.add_simps [@{thm of_nat_0}, @{thm of_nat_Suc}, @{thm of_nat_add}, 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1289 
@{thm of_nat_mult}, @{thm of_int_0}, @{thm of_int_1}, 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1290 
@{thm of_int_add}, @{thm of_int_minus}, @{thm of_int_diff}, 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1291 
@{thm of_int_mult}, @{thm of_int_of_nat_eq}, 
62348  1292 
@{thm of_nat_numeral}, @{thm of_nat_numeral}, @{thm of_int_neg_numeral}] 
58040
9a867afaab5a
better linarith support for floor, ceiling, natfloor, and natceiling
hoelzl
parents:
57514
diff
changeset

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

1294 
#> Lin_Arith.add_inj_const (@{const_name of_int}, @{typ "int \<Rightarrow> real"})) 
60758  1295 
\<close> 
51523  1296 

60758  1297 
subsection\<open>Simprules combining x+y and 0: ARE THEY NEEDED?\<close> 
51523  1298 

61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

1299 
lemma real_add_minus_iff [simp]: "(x +  a = (0::real)) = (x=a)" 
51523  1300 
by arith 
1301 

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

1303 
by auto 

1304 

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

1306 
by auto 

1307 

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

1309 
by auto 

1310 

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

1312 
by auto 

1313 

60758  1314 
subsection \<open>Lemmas about powers\<close> 
51523  1315 

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

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1317 
by simp 
51523  1318 

60758  1319 
text \<open>FIXME: declare this [simp] for all types, or not at all\<close> 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1320 
declare sum_squares_eq_zero_iff [simp] sum_power2_eq_zero_iff [simp] 
51523  1321 

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

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

1324 

53076  1325 
lemma realpow_square_minus_le [simp]: " u\<^sup>2 \<le> (x::real)\<^sup>2" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1326 
by (auto simp add: power2_eq_square) 
51523  1327 

58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1328 
lemma numeral_power_eq_real_of_int_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1329 
"numeral x ^ n = real_of_int (y::int) \<longleftrightarrow> numeral x ^ n = y" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1330 
by (metis of_int_eq_iff of_int_numeral of_int_power) 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1331 

9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1332 
lemma real_of_int_eq_numeral_power_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1333 
"real_of_int (y::int) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n" 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1334 
using numeral_power_eq_real_of_int_cancel_iff[of x n y] 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1335 
by metis 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1336 

9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1337 
lemma numeral_power_eq_real_of_nat_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1338 
"numeral x ^ n = real (y::nat) \<longleftrightarrow> numeral x ^ n = y" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1339 
using of_nat_eq_iff by fastforce 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1340 

9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1341 
lemma real_of_nat_eq_numeral_power_cancel_iff[simp]: 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1342 
"real (y::nat) = numeral x ^ n \<longleftrightarrow> y = numeral x ^ n" 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1343 
using numeral_power_eq_real_of_nat_cancel_iff[of x n y] 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1344 
by metis 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1345 

51523  1346 
lemma numeral_power_le_real_of_nat_cancel_iff[simp]: 
1347 
"(numeral x::real) ^ n \<le> real a \<longleftrightarrow> (numeral x::nat) ^ n \<le> a" 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1348 
by (metis of_nat_le_iff of_nat_numeral of_nat_power) 
51523  1349 

1350 
lemma real_of_nat_le_numeral_power_cancel_iff[simp]: 

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

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1352 
by (metis of_nat_le_iff of_nat_numeral of_nat_power) 
51523  1353 

1354 
lemma numeral_power_le_real_of_int_cancel_iff[simp]: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1355 
"(numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> (numeral x::int) ^ n \<le> a" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1356 
by (metis ceiling_le_iff ceiling_of_int of_int_numeral of_int_power) 
51523  1357 

1358 
lemma real_of_int_le_numeral_power_cancel_iff[simp]: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1359 
"real_of_int a \<le> (numeral x::real) ^ n \<longleftrightarrow> a \<le> (numeral x::int) ^ n" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1360 
by (metis floor_of_int le_floor_iff of_int_numeral of_int_power) 
51523  1361 

58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1362 
lemma numeral_power_less_real_of_nat_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1363 
"(numeral x::real) ^ n < real a \<longleftrightarrow> (numeral x::nat) ^ n < a" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1364 
by (metis of_nat_less_iff of_nat_numeral of_nat_power) 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1365 

9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1366 
lemma real_of_nat_less_numeral_power_cancel_iff[simp]: 
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1367 
"real a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::nat) ^ n" 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1368 
by (metis of_nat_less_iff of_nat_numeral of_nat_power) 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1369 

9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1370 
lemma numeral_power_less_real_of_int_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1371 
"(numeral x::real) ^ n < real_of_int a \<longleftrightarrow> (numeral x::int) ^ n < a" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1372 
by (meson not_less real_of_int_le_numeral_power_cancel_iff) 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1373 

9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1374 
lemma real_of_int_less_numeral_power_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1375 
"real_of_int a < (numeral x::real) ^ n \<longleftrightarrow> a < (numeral x::int) ^ n" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1376 
by (meson not_less numeral_power_le_real_of_int_cancel_iff) 
58983
9c390032e4eb
cancel real of power of numeral also for equality and strict inequality;
immler
parents:
58889
diff
changeset

1377 

51523  1378 
lemma neg_numeral_power_le_real_of_int_cancel_iff[simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1379 
"( numeral x::real) ^ n \<le> real_of_int a \<longleftrightarrow> ( numeral x::int) ^ n \<le> a" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1380 
by (metis of_int_le_iff of_int_neg_numeral of_int_power) 
51523  1381 

1382 
lemma real_of_int_le_neg_numeral_power_cancel_iff[simp]: 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1383 
"real_of_int a \<le> ( numeral x::real) ^ n \<longleftrightarrow> a \<le> ( numeral x::int) ^ n" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1384 
by (metis of_int_le_iff of_int_neg_numeral of_int_power) 
51523  1385 

56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56571
diff
changeset

1386 

60758  1387 
subsection\<open>Density of the Reals\<close> 
51523  1388 

1389 
lemma real_lbound_gt_zero: 

1390 
"[ (0::real) < d1; 0 < d2 ] ==> \<exists>e. 0 < e & e < d1 & e < d2" 

1391 
apply (rule_tac x = " (min d1 d2) /2" in exI) 

1392 
apply (simp add: min_def) 

1393 
done 

1394 

1395 

61799  1396 
text\<open>Similar results are proved in \<open>Fields\<close>\<close> 
51523  1397 
lemma real_less_half_sum: "x < y ==> x < (x+y) / (2::real)" 
1398 
by auto 

1399 

1400 
lemma real_gt_half_sum: "x < y ==> (x+y)/(2::real) < y" 

1401 
by auto 

1402 

1403 
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" 

1404 
by simp 

1405 

60758  1406 
subsection\<open>Absolute Value Function for the Reals\<close> 
51523  1407 

61944  1408 
lemma abs_minus_add_cancel: "\<bar>x + ( y)\<bar> = \<bar>y + ( (x::real))\<bar>" 
1409 
by (simp add: abs_if) 

51523  1410 

61944  1411 
lemma abs_add_one_gt_zero: "(0::real) < 1 + \<bar>x\<bar>" 
1412 
by (simp add: abs_if) 

51523  1413 

61944  1414 
lemma abs_add_one_not_less_self: "~ \<bar>x\<bar> + (1::real) < x" 
1415 
by simp 

61284
2314c2f62eb1
real_of_nat_Suc is now a simprule
paulson <lp15@cam.ac.uk>
parents:
61204
diff
changeset

1416 

61944  1417 
lemma abs_sum_triangle_ineq: "\<bar>(x::real) + y + (l + m)\<bar> \<le> \<bar>x + l\<bar> + \<bar>y + m\<bar>" 
1418 
by simp 

51523  1419 

1420 

60758  1421 
subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close> 
51523  1422 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1423 
(* FIXME: theorems for negative numerals. Many duplicates, e.g. from Archimedean_Field.thy. *) 
51523  1424 

56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56571
diff
changeset

1425 
lemma real_of_nat_less_numeral_iff [simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1426 
"real (n::nat) < numeral w \<longleftrightarrow> n < numeral w" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1427 
by (metis of_nat_less_iff of_nat_numeral) 
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56571
diff
changeset

1428 

48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56571
diff
changeset

1429 
lemma numeral_less_real_of_nat_iff [simp]: 
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1430 
"numeral w < real (n::nat) \<longleftrightarrow> numeral w < n" 
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1431 
by (metis of_nat_less_iff of_nat_numeral) 
56889
48a745e1bde7
avoid the Complex constructor, use the more natural Re/Im view; moved csqrt to Complex.
hoelzl
parents:
56571
diff
changeset

1432 

59587
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59000
diff
changeset

1433 
lemma numeral_le_real_of_nat_iff[simp]: 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59000
diff
changeset

1434 
"(numeral n \<le> real(m::nat)) = (numeral n \<le> m)" 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59000
diff
changeset

1435 
by (metis not_le real_of_nat_less_numeral_iff) 
8ea7b22525cb
Removed the obsolete functions "natfloor" and "natceiling"
nipkow
parents:
59000
diff
changeset

1436 

61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61284
diff
changeset

1437 
declare of_int_floor_le [simp] (* FIXME*) 
51523 