author  wenzelm 
Thu, 14 Jun 2007 18:33:31 +0200  
changeset 23389  aaca6a8e5414 
parent 23309  678ee30499d2 
child 23477  f4b83f03cac9 
permissions  rwrr 
16893  1 
(* Title : HOL/Real/RComplete.thy 
7219  2 
ID : $Id$ 
16893  3 
Author : Jacques D. Fleuriot, University of Edinburgh 
4 
Author : Larry Paulson, University of Cambridge 

5 
Author : Jeremy Avigad, Carnegie Mellon University 

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

7 
*) 

5078  8 

16893  9 
header {* Completeness of the Reals; Floor and Ceiling Functions *} 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

10 

15131  11 
theory RComplete 
15140  12 
imports Lubs RealDef 
15131  13 
begin 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

14 

3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

15 
lemma real_sum_of_halves: "x/2 + x/2 = (x::real)" 
16893  16 
by simp 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

17 

3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

18 

16893  19 
subsection {* Completeness of Positive Reals *} 
20 

21 
text {* 

22 
Supremum property for the set of positive reals 

23 

24 
Let @{text "P"} be a nonempty set of positive reals, with an upper 

25 
bound @{text "y"}. Then @{text "P"} has a least upper bound 

26 
(written @{text "S"}). 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

27 

16893  28 
FIXME: Can the premise be weakened to @{text "\<forall>x \<in> P. x\<le> y"}? 
29 
*} 

30 

31 
lemma posreal_complete: 

32 
assumes positive_P: "\<forall>x \<in> P. (0::real) < x" 

33 
and not_empty_P: "\<exists>x. x \<in> P" 

34 
and upper_bound_Ex: "\<exists>y. \<forall>x \<in> P. x<y" 

35 
shows "\<exists>S. \<forall>y. (\<exists>x \<in> P. y < x) = (y < S)" 

36 
proof (rule exI, rule allI) 

37 
fix y 

38 
let ?pP = "{w. real_of_preal w \<in> P}" 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

39 

16893  40 
show "(\<exists>x\<in>P. y < x) = (y < real_of_preal (psup ?pP))" 
41 
proof (cases "0 < y") 

42 
assume neg_y: "\<not> 0 < y" 

43 
show ?thesis 

44 
proof 

45 
assume "\<exists>x\<in>P. y < x" 

46 
have "\<forall>x. y < real_of_preal x" 

47 
using neg_y by (rule real_less_all_real2) 

48 
thus "y < real_of_preal (psup ?pP)" .. 

49 
next 

50 
assume "y < real_of_preal (psup ?pP)" 

51 
obtain "x" where x_in_P: "x \<in> P" using not_empty_P .. 

52 
hence "0 < x" using positive_P by simp 

53 
hence "y < x" using neg_y by simp 

54 
thus "\<exists>x \<in> P. y < x" using x_in_P .. 

55 
qed 

56 
next 

57 
assume pos_y: "0 < y" 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

58 

16893  59 
then obtain py where y_is_py: "y = real_of_preal py" 
60 
by (auto simp add: real_gt_zero_preal_Ex) 

61 

23389  62 
obtain a where "a \<in> P" using not_empty_P .. 
63 
with positive_P have a_pos: "0 < a" .. 

16893  64 
then obtain pa where "a = real_of_preal pa" 
65 
by (auto simp add: real_gt_zero_preal_Ex) 

23389  66 
hence "pa \<in> ?pP" using `a \<in> P` by auto 
16893  67 
hence pP_not_empty: "?pP \<noteq> {}" by auto 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

68 

16893  69 
obtain sup where sup: "\<forall>x \<in> P. x < sup" 
70 
using upper_bound_Ex .. 

23389  71 
from this and `a \<in> P` have "a < sup" .. 
16893  72 
hence "0 < sup" using a_pos by arith 
73 
then obtain possup where "sup = real_of_preal possup" 

74 
by (auto simp add: real_gt_zero_preal_Ex) 

75 
hence "\<forall>X \<in> ?pP. X \<le> possup" 

76 
using sup by (auto simp add: real_of_preal_lessI) 

77 
with pP_not_empty have psup: "\<And>Z. (\<exists>X \<in> ?pP. Z < X) = (Z < psup ?pP)" 

78 
by (rule preal_complete) 

79 

80 
show ?thesis 

81 
proof 

82 
assume "\<exists>x \<in> P. y < x" 

83 
then obtain x where x_in_P: "x \<in> P" and y_less_x: "y < x" .. 

84 
hence "0 < x" using pos_y by arith 

85 
then obtain px where x_is_px: "x = real_of_preal px" 

86 
by (auto simp add: real_gt_zero_preal_Ex) 

87 

88 
have py_less_X: "\<exists>X \<in> ?pP. py < X" 

89 
proof 

90 
show "py < px" using y_is_py and x_is_px and y_less_x 

91 
by (simp add: real_of_preal_lessI) 

92 
show "px \<in> ?pP" using x_in_P and x_is_px by simp 

93 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

94 

16893  95 
have "(\<exists>X \<in> ?pP. py < X) ==> (py < psup ?pP)" 
96 
using psup by simp 

97 
hence "py < psup ?pP" using py_less_X by simp 

98 
thus "y < real_of_preal (psup {w. real_of_preal w \<in> P})" 

99 
using y_is_py and pos_y by (simp add: real_of_preal_lessI) 

100 
next 

101 
assume y_less_psup: "y < real_of_preal (psup ?pP)" 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

102 

16893  103 
hence "py < psup ?pP" using y_is_py 
104 
by (simp add: real_of_preal_lessI) 

105 
then obtain "X" where py_less_X: "py < X" and X_in_pP: "X \<in> ?pP" 

106 
using psup by auto 

107 
then obtain x where x_is_X: "x = real_of_preal X" 

108 
by (simp add: real_gt_zero_preal_Ex) 

109 
hence "y < x" using py_less_X and y_is_py 

110 
by (simp add: real_of_preal_lessI) 

111 

112 
moreover have "x \<in> P" using x_is_X and X_in_pP by simp 

113 

114 
ultimately show "\<exists> x \<in> P. y < x" .. 

115 
qed 

116 
qed 

117 
qed 

118 

119 
text {* 

120 
\medskip Completeness properties using @{text "isUb"}, @{text "isLub"} etc. 

121 
*} 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

122 

3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

123 
lemma real_isLub_unique: "[ isLub R S x; isLub R S y ] ==> x = (y::real)" 
16893  124 
apply (frule isLub_isUb) 
125 
apply (frule_tac x = y in isLub_isUb) 

126 
apply (blast intro!: order_antisym dest!: isLub_le_isUb) 

127 
done 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

128 

5078  129 

16893  130 
text {* 
131 
\medskip Completeness theorem for the positive reals (again). 

132 
*} 

133 

134 
lemma posreals_complete: 

135 
assumes positive_S: "\<forall>x \<in> S. 0 < x" 

136 
and not_empty_S: "\<exists>x. x \<in> S" 

137 
and upper_bound_Ex: "\<exists>u. isUb (UNIV::real set) S u" 

138 
shows "\<exists>t. isLub (UNIV::real set) S t" 

139 
proof 

140 
let ?pS = "{w. real_of_preal w \<in> S}" 

141 

142 
obtain u where "isUb UNIV S u" using upper_bound_Ex .. 

143 
hence sup: "\<forall>x \<in> S. x \<le> u" by (simp add: isUb_def setle_def) 

144 

145 
obtain x where x_in_S: "x \<in> S" using not_empty_S .. 

146 
hence x_gt_zero: "0 < x" using positive_S by simp 

147 
have "x \<le> u" using sup and x_in_S .. 

148 
hence "0 < u" using x_gt_zero by arith 

149 

150 
then obtain pu where u_is_pu: "u = real_of_preal pu" 

151 
by (auto simp add: real_gt_zero_preal_Ex) 

152 

153 
have pS_less_pu: "\<forall>pa \<in> ?pS. pa \<le> pu" 

154 
proof 

155 
fix pa 

156 
assume "pa \<in> ?pS" 

157 
then obtain a where "a \<in> S" and "a = real_of_preal pa" 

158 
by simp 

159 
moreover hence "a \<le> u" using sup by simp 

160 
ultimately show "pa \<le> pu" 

161 
using sup and u_is_pu by (simp add: real_of_preal_le_iff) 

162 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

163 

16893  164 
have "\<forall>y \<in> S. y \<le> real_of_preal (psup ?pS)" 
165 
proof 

166 
fix y 

167 
assume y_in_S: "y \<in> S" 

168 
hence "0 < y" using positive_S by simp 

169 
then obtain py where y_is_py: "y = real_of_preal py" 

170 
by (auto simp add: real_gt_zero_preal_Ex) 

171 
hence py_in_pS: "py \<in> ?pS" using y_in_S by simp 

172 
with pS_less_pu have "py \<le> psup ?pS" 

173 
by (rule preal_psup_le) 

174 
thus "y \<le> real_of_preal (psup ?pS)" 

175 
using y_is_py by (simp add: real_of_preal_le_iff) 

176 
qed 

177 

178 
moreover { 

179 
fix x 

180 
assume x_ub_S: "\<forall>y\<in>S. y \<le> x" 

181 
have "real_of_preal (psup ?pS) \<le> x" 

182 
proof  

183 
obtain "s" where s_in_S: "s \<in> S" using not_empty_S .. 

184 
hence s_pos: "0 < s" using positive_S by simp 

185 

186 
hence "\<exists> ps. s = real_of_preal ps" by (simp add: real_gt_zero_preal_Ex) 

187 
then obtain "ps" where s_is_ps: "s = real_of_preal ps" .. 

188 
hence ps_in_pS: "ps \<in> {w. real_of_preal w \<in> S}" using s_in_S by simp 

189 

190 
from x_ub_S have "s \<le> x" using s_in_S .. 

191 
hence "0 < x" using s_pos by simp 

192 
hence "\<exists> px. x = real_of_preal px" by (simp add: real_gt_zero_preal_Ex) 

193 
then obtain "px" where x_is_px: "x = real_of_preal px" .. 

194 

195 
have "\<forall>pe \<in> ?pS. pe \<le> px" 

196 
proof 

197 
fix pe 

198 
assume "pe \<in> ?pS" 

199 
hence "real_of_preal pe \<in> S" by simp 

200 
hence "real_of_preal pe \<le> x" using x_ub_S by simp 

201 
thus "pe \<le> px" using x_is_px by (simp add: real_of_preal_le_iff) 

202 
qed 

203 

204 
moreover have "?pS \<noteq> {}" using ps_in_pS by auto 

205 
ultimately have "(psup ?pS) \<le> px" by (simp add: psup_le_ub) 

206 
thus "real_of_preal (psup ?pS) \<le> x" using x_is_px by (simp add: real_of_preal_le_iff) 

207 
qed 

208 
} 

209 
ultimately show "isLub UNIV S (real_of_preal (psup ?pS))" 

210 
by (simp add: isLub_def leastP_def isUb_def setle_def setge_def) 

211 
qed 

212 

213 
text {* 

214 
\medskip reals Completeness (again!) 

215 
*} 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

216 

16893  217 
lemma reals_complete: 
218 
assumes notempty_S: "\<exists>X. X \<in> S" 

219 
and exists_Ub: "\<exists>Y. isUb (UNIV::real set) S Y" 

220 
shows "\<exists>t. isLub (UNIV :: real set) S t" 

221 
proof  

222 
obtain X where X_in_S: "X \<in> S" using notempty_S .. 

223 
obtain Y where Y_isUb: "isUb (UNIV::real set) S Y" 

224 
using exists_Ub .. 

225 
let ?SHIFT = "{z. \<exists>x \<in>S. z = x + (X) + 1} \<inter> {x. 0 < x}" 

226 

227 
{ 

228 
fix x 

229 
assume "isUb (UNIV::real set) S x" 

230 
hence S_le_x: "\<forall> y \<in> S. y <= x" 

231 
by (simp add: isUb_def setle_def) 

232 
{ 

233 
fix s 

234 
assume "s \<in> {z. \<exists>x\<in>S. z = x +  X + 1}" 

235 
hence "\<exists> x \<in> S. s = x + X + 1" .. 

236 
then obtain x1 where "x1 \<in> S" and "s = x1 + (X) + 1" .. 

237 
moreover hence "x1 \<le> x" using S_le_x by simp 

238 
ultimately have "s \<le> x +  X + 1" by arith 

239 
} 

240 
then have "isUb (UNIV::real set) ?SHIFT (x + (X) + 1)" 

241 
by (auto simp add: isUb_def setle_def) 

242 
} note S_Ub_is_SHIFT_Ub = this 

243 

244 
hence "isUb UNIV ?SHIFT (Y + (X) + 1)" using Y_isUb by simp 

245 
hence "\<exists>Z. isUb UNIV ?SHIFT Z" .. 

246 
moreover have "\<forall>y \<in> ?SHIFT. 0 < y" by auto 

247 
moreover have shifted_not_empty: "\<exists>u. u \<in> ?SHIFT" 

248 
using X_in_S and Y_isUb by auto 

249 
ultimately obtain t where t_is_Lub: "isLub UNIV ?SHIFT t" 

250 
using posreals_complete [of ?SHIFT] by blast 

251 

252 
show ?thesis 

253 
proof 

254 
show "isLub UNIV S (t + X + (1))" 

255 
proof (rule isLubI2) 

256 
{ 

257 
fix x 

258 
assume "isUb (UNIV::real set) S x" 

259 
hence "isUb (UNIV::real set) (?SHIFT) (x + (X) + 1)" 

260 
using S_Ub_is_SHIFT_Ub by simp 

261 
hence "t \<le> (x + (X) + 1)" 

262 
using t_is_Lub by (simp add: isLub_le_isUb) 

263 
hence "t + X + 1 \<le> x" by arith 

264 
} 

265 
then show "(t + X + 1) <=* Collect (isUb UNIV S)" 

266 
by (simp add: setgeI) 

267 
next 

268 
show "isUb UNIV S (t + X + 1)" 

269 
proof  

270 
{ 

271 
fix y 

272 
assume y_in_S: "y \<in> S" 

273 
have "y \<le> t + X + 1" 

274 
proof  

275 
obtain "u" where u_in_shift: "u \<in> ?SHIFT" using shifted_not_empty .. 

276 
hence "\<exists> x \<in> S. u = x +  X + 1" by simp 

277 
then obtain "x" where x_and_u: "u = x +  X + 1" .. 

278 
have u_le_t: "u \<le> t" using u_in_shift and t_is_Lub by (simp add: isLubD2) 

279 

280 
show ?thesis 

281 
proof cases 

282 
assume "y \<le> x" 

283 
moreover have "x = u + X +  1" using x_and_u by arith 

284 
moreover have "u + X +  1 \<le> t + X + 1" using u_le_t by arith 

285 
ultimately show "y \<le> t + X + 1" by arith 

286 
next 

287 
assume "~(y \<le> x)" 

288 
hence x_less_y: "x < y" by arith 

289 

290 
have "x + (X) + 1 \<in> ?SHIFT" using x_and_u and u_in_shift by simp 

291 
hence "0 < x + (X) + 1" by simp 

292 
hence "0 < y + (X) + 1" using x_less_y by arith 

293 
hence "y + (X) + 1 \<in> ?SHIFT" using y_in_S by simp 

294 
hence "y + (X) + 1 \<le> t" using t_is_Lub by (simp add: isLubD2) 

295 
thus ?thesis by simp 

296 
qed 

297 
qed 

298 
} 

299 
then show ?thesis by (simp add: isUb_def setle_def) 

300 
qed 

301 
qed 

302 
qed 

303 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

304 

3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

305 

16893  306 
subsection {* The Archimedean Property of the Reals *} 
307 

308 
theorem reals_Archimedean: 

309 
assumes x_pos: "0 < x" 

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

311 
proof (rule ccontr) 

312 
assume contr: "\<not> ?thesis" 

313 
have "\<forall>n. x * real (Suc n) <= 1" 

314 
proof 

315 
fix n 

316 
from contr have "x \<le> inverse (real (Suc n))" 

317 
by (simp add: linorder_not_less) 

318 
hence "x \<le> (1 / (real (Suc n)))" 

319 
by (simp add: inverse_eq_divide) 

320 
moreover have "0 \<le> real (Suc n)" 

321 
by (rule real_of_nat_ge_zero) 

322 
ultimately have "x * real (Suc n) \<le> (1 / real (Suc n)) * real (Suc n)" 

323 
by (rule mult_right_mono) 

324 
thus "x * real (Suc n) \<le> 1" by simp 

325 
qed 

326 
hence "{z. \<exists>n. z = x * (real (Suc n))} *<= 1" 

327 
by (simp add: setle_def, safe, rule spec) 

328 
hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (real (Suc n))} 1" 

329 
by (simp add: isUbI) 

330 
hence "\<exists>Y. isUb (UNIV::real set) {z. \<exists>n. z = x* (real (Suc n))} Y" .. 

331 
moreover have "\<exists>X. X \<in> {z. \<exists>n. z = x* (real (Suc n))}" by auto 

332 
ultimately have "\<exists>t. isLub UNIV {z. \<exists>n. z = x * real (Suc n)} t" 

333 
by (simp add: reals_complete) 

334 
then obtain "t" where 

335 
t_is_Lub: "isLub UNIV {z. \<exists>n. z = x * real (Suc n)} t" .. 

336 

337 
have "\<forall>n::nat. x * real n \<le> t +  x" 

338 
proof 

339 
fix n 

340 
from t_is_Lub have "x * real (Suc n) \<le> t" 

341 
by (simp add: isLubD2) 

342 
hence "x * (real n) + x \<le> t" 

343 
by (simp add: right_distrib real_of_nat_Suc) 

344 
thus "x * (real n) \<le> t +  x" by arith 

345 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

346 

16893  347 
hence "\<forall>m. x * real (Suc m) \<le> t +  x" by simp 
348 
hence "{z. \<exists>n. z = x * (real (Suc n))} *<= (t +  x)" 

349 
by (auto simp add: setle_def) 

350 
hence "isUb (UNIV::real set) {z. \<exists>n. z = x * (real (Suc n))} (t + (x))" 

351 
by (simp add: isUbI) 

352 
hence "t \<le> t +  x" 

353 
using t_is_Lub by (simp add: isLub_le_isUb) 

354 
thus False using x_pos by arith 

355 
qed 

356 

357 
text {* 

358 
There must be other proofs, e.g. @{text "Suc"} of the largest 

359 
integer in the cut representing @{text "x"}. 

360 
*} 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

361 

3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

362 
lemma reals_Archimedean2: "\<exists>n. (x::real) < real (n::nat)" 
16893  363 
proof cases 
364 
assume "x \<le> 0" 

365 
hence "x < real (1::nat)" by simp 

366 
thus ?thesis .. 

367 
next 

368 
assume "\<not> x \<le> 0" 

369 
hence x_greater_zero: "0 < x" by simp 

370 
hence "0 < inverse x" by simp 

371 
then obtain n where "inverse (real (Suc n)) < inverse x" 

372 
using reals_Archimedean by blast 

373 
hence "inverse (real (Suc n)) * x < inverse x * x" 

374 
using x_greater_zero by (rule mult_strict_right_mono) 

375 
hence "inverse (real (Suc n)) * x < 1" 

23008  376 
using x_greater_zero by simp 
16893  377 
hence "real (Suc n) * (inverse (real (Suc n)) * x) < real (Suc n) * 1" 
378 
by (rule mult_strict_left_mono) simp 

379 
hence "x < real (Suc n)" 

23008  380 
by (simp add: ring_eq_simps) 
16893  381 
thus "\<exists>(n::nat). x < real n" .. 
382 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

383 

16893  384 
lemma reals_Archimedean3: 
385 
assumes x_greater_zero: "0 < x" 

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

387 
proof 

388 
fix y 

389 
have x_not_zero: "x \<noteq> 0" using x_greater_zero by simp 

390 
obtain n where "y * inverse x < real (n::nat)" 

391 
using reals_Archimedean2 .. 

392 
hence "y * inverse x * x < real n * x" 

393 
using x_greater_zero by (simp add: mult_strict_right_mono) 

394 
hence "x * inverse x * y < x * real n" 

23008  395 
by (simp add: ring_eq_simps) 
16893  396 
hence "y < real (n::nat) * x" 
23008  397 
using x_not_zero by (simp add: ring_eq_simps) 
16893  398 
thus "\<exists>(n::nat). y < real n * x" .. 
399 
qed 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

400 

16819  401 
lemma reals_Archimedean6: 
402 
"0 \<le> r ==> \<exists>(n::nat). real (n  1) \<le> r & r < real (n)" 

403 
apply (insert reals_Archimedean2 [of r], safe) 

23012  404 
apply (subgoal_tac "\<exists>x::nat. r < real x \<and> (\<forall>y. r < real y \<longrightarrow> x \<le> y)", auto) 
16819  405 
apply (rule_tac x = x in exI) 
406 
apply (case_tac x, simp) 

407 
apply (rename_tac x') 

408 
apply (drule_tac x = x' in spec, simp) 

23012  409 
apply (rule_tac x="LEAST n. r < real n" in exI, safe) 
410 
apply (erule LeastI, erule Least_le) 

16819  411 
done 
412 

413 
lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)" 

16893  414 
by (drule reals_Archimedean6) auto 
16819  415 

416 
lemma reals_Archimedean_6b_int: 

417 
"0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)" 

418 
apply (drule reals_Archimedean6a, auto) 

419 
apply (rule_tac x = "int n" in exI) 

420 
apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) 

421 
done 

422 

423 
lemma reals_Archimedean_6c_int: 

424 
"r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)" 

425 
apply (rule reals_Archimedean_6b_int [of "r", THEN exE], simp, auto) 

426 
apply (rename_tac n) 

22998  427 
apply (drule order_le_imp_less_or_eq, auto) 
16819  428 
apply (rule_tac x = " n  1" in exI) 
429 
apply (rule_tac [2] x = " n" in exI, auto) 

430 
done 

431 

432 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

433 
subsection{*Floor and Ceiling Functions from the Reals to the Integers*} 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

434 

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

436 
floor :: "real => int" where 
19765  437 
"floor r = (LEAST n::int. r < real (n+1))" 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

438 

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

439 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

440 
ceiling :: "real => int" where 
19765  441 
"ceiling r =  floor ( r)" 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

442 

21210  443 
notation (xsymbols) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

444 
floor ("\<lfloor>_\<rfloor>") and 
19765  445 
ceiling ("\<lceil>_\<rceil>") 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

446 

21210  447 
notation (HTML output) 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

448 
floor ("\<lfloor>_\<rfloor>") and 
19765  449 
ceiling ("\<lceil>_\<rceil>") 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

450 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

451 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

452 
lemma number_of_less_real_of_int_iff [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

453 
"((number_of n) < real (m::int)) = (number_of n < m)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

454 
apply auto 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

455 
apply (rule real_of_int_less_iff [THEN iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

456 
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

457 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

458 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

459 
lemma number_of_less_real_of_int_iff2 [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

460 
"(real (m::int) < (number_of n)) = (m < number_of n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

461 
apply auto 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

462 
apply (rule real_of_int_less_iff [THEN iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

463 
apply (drule_tac [2] real_of_int_less_iff [THEN iffD2], auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

464 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

465 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

466 
lemma number_of_le_real_of_int_iff [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

467 
"((number_of n) \<le> real (m::int)) = (number_of n \<le> m)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

468 
by (simp add: linorder_not_less [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

469 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

470 
lemma number_of_le_real_of_int_iff2 [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

471 
"(real (m::int) \<le> (number_of n)) = (m \<le> number_of n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

472 
by (simp add: linorder_not_less [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

473 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

474 
lemma floor_zero [simp]: "floor 0 = 0" 
16819  475 
apply (simp add: floor_def del: real_of_int_add) 
476 
apply (rule Least_equality) 

477 
apply simp_all 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

478 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

479 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

480 
lemma floor_real_of_nat_zero [simp]: "floor (real (0::nat)) = 0" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

481 
by auto 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

482 

23309  483 
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int_of_nat n" 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

484 
apply (simp only: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

485 
apply (rule Least_equality) 
23309  486 
apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst]) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

487 
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) 
23309  488 
apply simp_all 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

489 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

490 

23309  491 
lemma floor_minus_real_of_nat [simp]: "floor ( real (n::nat)) =  int_of_nat n" 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

492 
apply (simp only: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

493 
apply (rule Least_equality) 
23309  494 
apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst]) 
16819  495 
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst]) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

496 
apply (drule_tac [2] real_of_int_less_iff [THEN iffD1]) 
23309  497 
apply simp_all 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

498 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

499 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

500 
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

501 
apply (simp only: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

502 
apply (rule Least_equality) 
23309  503 
apply auto 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

504 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

505 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

506 
lemma floor_minus_real_of_int [simp]: "floor ( real (n::int)) =  n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

507 
apply (simp only: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

508 
apply (rule Least_equality) 
16819  509 
apply (drule_tac [2] real_of_int_minus [THEN sym, THEN subst]) 
23309  510 
apply auto 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

511 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

512 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

513 
lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

514 
apply (case_tac "r < 0") 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

515 
apply (blast intro: reals_Archimedean_6c_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

516 
apply (simp only: linorder_not_less) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

517 
apply (blast intro: reals_Archimedean_6b_int reals_Archimedean_6c_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

518 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

519 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

520 
lemma lemma_floor: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

521 
assumes a1: "real m \<le> r" and a2: "r < real n + 1" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

522 
shows "m \<le> (n::int)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

523 
proof  
23389  524 
have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) 
525 
also have "... = real (n + 1)" by simp 

526 
finally have "m < n + 1" by (simp only: real_of_int_less_iff) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

527 
thus ?thesis by arith 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

528 
qed 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

529 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

530 
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

531 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

532 
apply (insert real_lb_ub_int [of r], safe) 
16819  533 
apply (rule theI2) 
534 
apply auto 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

535 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

536 

16819  537 
lemma floor_mono: "x < y ==> floor x \<le> floor y" 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

538 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

539 
apply (insert real_lb_ub_int [of x]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

540 
apply (insert real_lb_ub_int [of y], safe) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

541 
apply (rule theI2) 
16819  542 
apply (rule_tac [3] theI2) 
543 
apply simp 

544 
apply (erule conjI) 

545 
apply (auto simp add: order_eq_iff int_le_real_less) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

546 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

547 

16819  548 
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y" 
22998  549 
by (auto dest: order_le_imp_less_or_eq simp add: floor_mono) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

550 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

551 
lemma lemma_floor2: "real n < real (x::int) + 1 ==> n \<le> x" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

552 
by (auto intro: lemma_floor) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

553 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

554 
lemma real_of_int_floor_cancel [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

555 
"(real (floor x) = x) = (\<exists>n::int. x = real n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

556 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

557 
apply (insert real_lb_ub_int [of x], erule exE) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

558 
apply (rule theI2) 
16893  559 
apply (auto intro: lemma_floor) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

560 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

561 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

562 
lemma floor_eq: "[ real n < x; x < real n + 1 ] ==> floor x = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

563 
apply (simp add: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

564 
apply (rule Least_equality) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

565 
apply (auto intro: lemma_floor) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

566 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

567 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

568 
lemma floor_eq2: "[ real n \<le> x; x < real n + 1 ] ==> floor x = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

569 
apply (simp add: floor_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

570 
apply (rule Least_equality) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

571 
apply (auto intro: lemma_floor) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

572 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

573 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

574 
lemma floor_eq3: "[ real n < x; x < real (Suc n) ] ==> nat(floor x) = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

575 
apply (rule inj_int [THEN injD]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

576 
apply (simp add: real_of_nat_Suc) 
15539  577 
apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"]) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

578 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

579 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

580 
lemma floor_eq4: "[ real n \<le> x; x < real (Suc n) ] ==> nat(floor x) = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

581 
apply (drule order_le_imp_less_or_eq) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

582 
apply (auto intro: floor_eq3) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

583 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

584 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

585 
lemma floor_number_of_eq [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

586 
"floor(number_of n :: real) = (number_of n :: int)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

587 
apply (subst real_number_of [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

588 
apply (rule floor_real_of_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

589 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

590 

16819  591 
lemma floor_one [simp]: "floor 1 = 1" 
592 
apply (rule trans) 

593 
prefer 2 

594 
apply (rule floor_real_of_int) 

595 
apply simp 

596 
done 

597 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

598 
lemma real_of_int_floor_ge_diff_one [simp]: "r  1 \<le> real(floor r)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

599 
apply (simp add: floor_def Least_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

600 
apply (insert real_lb_ub_int [of r], safe) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

601 
apply (rule theI2) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

602 
apply (auto intro: lemma_floor) 
16819  603 
done 
604 

605 
lemma real_of_int_floor_gt_diff_one [simp]: "r  1 < real(floor r)" 

606 
apply (simp add: floor_def Least_def) 

607 
apply (insert real_lb_ub_int [of r], safe) 

608 
apply (rule theI2) 

609 
apply (auto intro: lemma_floor) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

610 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

611 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

612 
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

613 
apply (insert real_of_int_floor_ge_diff_one [of r]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

614 
apply (auto simp del: real_of_int_floor_ge_diff_one) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

615 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

616 

16819  617 
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" 
618 
apply (insert real_of_int_floor_gt_diff_one [of r]) 

619 
apply (auto simp del: real_of_int_floor_gt_diff_one) 

620 
done 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

621 

16819  622 
lemma le_floor: "real a <= x ==> a <= floor x" 
623 
apply (subgoal_tac "a < floor x + 1") 

624 
apply arith 

625 
apply (subst real_of_int_less_iff [THEN sym]) 

626 
apply simp 

16893  627 
apply (insert real_of_int_floor_add_one_gt [of x]) 
16819  628 
apply arith 
629 
done 

630 

631 
lemma real_le_floor: "a <= floor x ==> real a <= x" 

632 
apply (rule order_trans) 

633 
prefer 2 

634 
apply (rule real_of_int_floor_le) 

635 
apply (subst real_of_int_le_iff) 

636 
apply assumption 

637 
done 

638 

639 
lemma le_floor_eq: "(a <= floor x) = (real a <= x)" 

640 
apply (rule iffI) 

641 
apply (erule real_le_floor) 

642 
apply (erule le_floor) 

643 
done 

644 

16893  645 
lemma le_floor_eq_number_of [simp]: 
16819  646 
"(number_of n <= floor x) = (number_of n <= x)" 
647 
by (simp add: le_floor_eq) 

648 

649 
lemma le_floor_eq_zero [simp]: "(0 <= floor x) = (0 <= x)" 

650 
by (simp add: le_floor_eq) 

651 

652 
lemma le_floor_eq_one [simp]: "(1 <= floor x) = (1 <= x)" 

653 
by (simp add: le_floor_eq) 

654 

655 
lemma floor_less_eq: "(floor x < a) = (x < real a)" 

656 
apply (subst linorder_not_le [THEN sym])+ 

657 
apply simp 

658 
apply (rule le_floor_eq) 

659 
done 

660 

16893  661 
lemma floor_less_eq_number_of [simp]: 
16819  662 
"(floor x < number_of n) = (x < number_of n)" 
663 
by (simp add: floor_less_eq) 

664 

665 
lemma floor_less_eq_zero [simp]: "(floor x < 0) = (x < 0)" 

666 
by (simp add: floor_less_eq) 

667 

668 
lemma floor_less_eq_one [simp]: "(floor x < 1) = (x < 1)" 

669 
by (simp add: floor_less_eq) 

670 

671 
lemma less_floor_eq: "(a < floor x) = (real a + 1 <= x)" 

672 
apply (insert le_floor_eq [of "a + 1" x]) 

673 
apply auto 

674 
done 

675 

16893  676 
lemma less_floor_eq_number_of [simp]: 
16819  677 
"(number_of n < floor x) = (number_of n + 1 <= x)" 
678 
by (simp add: less_floor_eq) 

679 

680 
lemma less_floor_eq_zero [simp]: "(0 < floor x) = (1 <= x)" 

681 
by (simp add: less_floor_eq) 

682 

683 
lemma less_floor_eq_one [simp]: "(1 < floor x) = (2 <= x)" 

684 
by (simp add: less_floor_eq) 

685 

686 
lemma floor_le_eq: "(floor x <= a) = (x < real a + 1)" 

687 
apply (insert floor_less_eq [of x "a + 1"]) 

688 
apply auto 

689 
done 

690 

16893  691 
lemma floor_le_eq_number_of [simp]: 
16819  692 
"(floor x <= number_of n) = (x < number_of n + 1)" 
693 
by (simp add: floor_le_eq) 

694 

695 
lemma floor_le_eq_zero [simp]: "(floor x <= 0) = (x < 1)" 

696 
by (simp add: floor_le_eq) 

697 

698 
lemma floor_le_eq_one [simp]: "(floor x <= 1) = (x < 2)" 

699 
by (simp add: floor_le_eq) 

700 

701 
lemma floor_add [simp]: "floor (x + real a) = floor x + a" 

702 
apply (subst order_eq_iff) 

703 
apply (rule conjI) 

704 
prefer 2 

705 
apply (subgoal_tac "floor x + a < floor (x + real a) + 1") 

706 
apply arith 

707 
apply (subst real_of_int_less_iff [THEN sym]) 

708 
apply simp 

709 
apply (subgoal_tac "x + real a < real(floor(x + real a)) + 1") 

710 
apply (subgoal_tac "real (floor x) <= x") 

711 
apply arith 

712 
apply (rule real_of_int_floor_le) 

713 
apply (rule real_of_int_floor_add_one_gt) 

714 
apply (subgoal_tac "floor (x + real a) < floor x + a + 1") 

715 
apply arith 

16893  716 
apply (subst real_of_int_less_iff [THEN sym]) 
16819  717 
apply simp 
16893  718 
apply (subgoal_tac "real(floor(x + real a)) <= x + real a") 
16819  719 
apply (subgoal_tac "x < real(floor x) + 1") 
720 
apply arith 

721 
apply (rule real_of_int_floor_add_one_gt) 

722 
apply (rule real_of_int_floor_le) 

723 
done 

724 

16893  725 
lemma floor_add_number_of [simp]: 
16819  726 
"floor (x + number_of n) = floor x + number_of n" 
727 
apply (subst floor_add [THEN sym]) 

728 
apply simp 

729 
done 

730 

731 
lemma floor_add_one [simp]: "floor (x + 1) = floor x + 1" 

732 
apply (subst floor_add [THEN sym]) 

733 
apply simp 

734 
done 

735 

736 
lemma floor_subtract [simp]: "floor (x  real a) = floor x  a" 

737 
apply (subst diff_minus)+ 

738 
apply (subst real_of_int_minus [THEN sym]) 

739 
apply (rule floor_add) 

740 
done 

741 

16893  742 
lemma floor_subtract_number_of [simp]: "floor (x  number_of n) = 
16819  743 
floor x  number_of n" 
744 
apply (subst floor_subtract [THEN sym]) 

745 
apply simp 

746 
done 

747 

748 
lemma floor_subtract_one [simp]: "floor (x  1) = floor x  1" 

749 
apply (subst floor_subtract [THEN sym]) 

750 
apply simp 

751 
done 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

752 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

753 
lemma ceiling_zero [simp]: "ceiling 0 = 0" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

754 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

755 

23309  756 
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int_of_nat n" 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

757 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

758 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

759 
lemma ceiling_real_of_nat_zero [simp]: "ceiling (real (0::nat)) = 0" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

760 
by auto 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

761 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

762 
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

763 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

764 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

765 
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

766 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

767 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

768 
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

769 
apply (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

770 
apply (subst le_minus_iff, simp) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

771 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

772 

16819  773 
lemma ceiling_mono: "x < y ==> ceiling x \<le> ceiling y" 
774 
by (simp add: floor_mono ceiling_def) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

775 

16819  776 
lemma ceiling_mono2: "x \<le> y ==> ceiling x \<le> ceiling y" 
777 
by (simp add: floor_mono2 ceiling_def) 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

778 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

779 
lemma real_of_int_ceiling_cancel [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

780 
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

781 
apply (auto simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

782 
apply (drule arg_cong [where f = uminus], auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

783 
apply (rule_tac x = "n" in exI, auto) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

784 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

785 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

786 
lemma ceiling_eq: "[ real n < x; x < real n + 1 ] ==> ceiling x = n + 1" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

787 
apply (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

788 
apply (rule minus_equation_iff [THEN iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

789 
apply (simp add: floor_eq [where n = "(n+1)"]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

790 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

791 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

792 
lemma ceiling_eq2: "[ real n < x; x \<le> real n + 1 ] ==> ceiling x = n + 1" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

793 
by (simp add: ceiling_def floor_eq2 [where n = "(n+1)"]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

794 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

795 
lemma ceiling_eq3: "[ real n  1 < x; x \<le> real n ] ==> ceiling x = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

796 
by (simp add: ceiling_def floor_eq2 [where n = "n"]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

797 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

798 
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

799 
by (simp add: ceiling_def) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

800 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

801 
lemma ceiling_number_of_eq [simp]: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

802 
"ceiling (number_of n :: real) = (number_of n)" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

803 
apply (subst real_number_of [symmetric]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

804 
apply (rule ceiling_real_of_int) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

805 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

806 

16819  807 
lemma ceiling_one [simp]: "ceiling 1 = 1" 
808 
by (unfold ceiling_def, simp) 

809 

14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

810 
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r)  1 \<le> r" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

811 
apply (rule neg_le_iff_le [THEN iffD1]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

812 
apply (simp add: ceiling_def diff_minus) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

813 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

814 

79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

815 
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

816 
apply (insert real_of_int_ceiling_diff_one_le [of r]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

817 
apply (simp del: real_of_int_ceiling_diff_one_le) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

818 
done 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

819 

16819  820 
lemma ceiling_le: "x <= real a ==> ceiling x <= a" 
821 
apply (unfold ceiling_def) 

822 
apply (subgoal_tac "a <= floor( x)") 

823 
apply simp 

824 
apply (rule le_floor) 

825 
apply simp 

826 
done 

827 

828 
lemma ceiling_le_real: "ceiling x <= a ==> x <= real a" 

829 
apply (unfold ceiling_def) 

830 
apply (subgoal_tac "real( a) <=  x") 

831 
apply simp 

832 
apply (rule real_le_floor) 

833 
apply simp 

834 
done 

835 

836 
lemma ceiling_le_eq: "(ceiling x <= a) = (x <= real a)" 

837 
apply (rule iffI) 

838 
apply (erule ceiling_le_real) 

839 
apply (erule ceiling_le) 

840 
done 

841 

16893  842 
lemma ceiling_le_eq_number_of [simp]: 
16819  843 
"(ceiling x <= number_of n) = (x <= number_of n)" 
844 
by (simp add: ceiling_le_eq) 

845 

16893  846 
lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" 
16819  847 
by (simp add: ceiling_le_eq) 
848 

16893  849 
lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" 
16819  850 
by (simp add: ceiling_le_eq) 
851 

852 
lemma less_ceiling_eq: "(a < ceiling x) = (real a < x)" 

853 
apply (subst linorder_not_le [THEN sym])+ 

854 
apply simp 

855 
apply (rule ceiling_le_eq) 

856 
done 

857 

16893  858 
lemma less_ceiling_eq_number_of [simp]: 
16819  859 
"(number_of n < ceiling x) = (number_of n < x)" 
860 
by (simp add: less_ceiling_eq) 

861 

862 
lemma less_ceiling_eq_zero [simp]: "(0 < ceiling x) = (0 < x)" 

863 
by (simp add: less_ceiling_eq) 

864 

865 
lemma less_ceiling_eq_one [simp]: "(1 < ceiling x) = (1 < x)" 

866 
by (simp add: less_ceiling_eq) 

867 

868 
lemma ceiling_less_eq: "(ceiling x < a) = (x <= real a  1)" 

869 
apply (insert ceiling_le_eq [of x "a  1"]) 

870 
apply auto 

871 
done 

872 

16893  873 
lemma ceiling_less_eq_number_of [simp]: 
16819  874 
"(ceiling x < number_of n) = (x <= number_of n  1)" 
875 
by (simp add: ceiling_less_eq) 

876 

877 
lemma ceiling_less_eq_zero [simp]: "(ceiling x < 0) = (x <= 1)" 

878 
by (simp add: ceiling_less_eq) 

879 

880 
lemma ceiling_less_eq_one [simp]: "(ceiling x < 1) = (x <= 0)" 

881 
by (simp add: ceiling_less_eq) 

882 

883 
lemma le_ceiling_eq: "(a <= ceiling x) = (real a  1 < x)" 

884 
apply (insert less_ceiling_eq [of "a  1" x]) 

885 
apply auto 

886 
done 

887 

16893  888 
lemma le_ceiling_eq_number_of [simp]: 
16819  889 
"(number_of n <= ceiling x) = (number_of n  1 < x)" 
890 
by (simp add: le_ceiling_eq) 

891 

892 
lemma le_ceiling_eq_zero [simp]: "(0 <= ceiling x) = (1 < x)" 

893 
by (simp add: le_ceiling_eq) 

894 

895 
lemma le_ceiling_eq_one [simp]: "(1 <= ceiling x) = (0 < x)" 

896 
by (simp add: le_ceiling_eq) 

897 

898 
lemma ceiling_add [simp]: "ceiling (x + real a) = ceiling x + a" 

899 
apply (unfold ceiling_def, simp) 

900 
apply (subst real_of_int_minus [THEN sym]) 

901 
apply (subst floor_add) 

902 
apply simp 

903 
done 

904 

16893  905 
lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = 
16819  906 
ceiling x + number_of n" 
907 
apply (subst ceiling_add [THEN sym]) 

908 
apply simp 

909 
done 

910 

911 
lemma ceiling_add_one [simp]: "ceiling (x + 1) = ceiling x + 1" 

912 
apply (subst ceiling_add [THEN sym]) 

913 
apply simp 

914 
done 

915 

916 
lemma ceiling_subtract [simp]: "ceiling (x  real a) = ceiling x  a" 

917 
apply (subst diff_minus)+ 

918 
apply (subst real_of_int_minus [THEN sym]) 

919 
apply (rule ceiling_add) 

920 
done 

921 

16893  922 
lemma ceiling_subtract_number_of [simp]: "ceiling (x  number_of n) = 
16819  923 
ceiling x  number_of n" 
924 
apply (subst ceiling_subtract [THEN sym]) 

925 
apply simp 

926 
done 

927 

928 
lemma ceiling_subtract_one [simp]: "ceiling (x  1) = ceiling x  1" 

929 
apply (subst ceiling_subtract [THEN sym]) 

930 
apply simp 

931 
done 

932 

933 
subsection {* Versions for the natural numbers *} 

934 

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

936 
natfloor :: "real => nat" where 
19765  937 
"natfloor x = nat(floor x)" 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

938 

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

939 
definition 
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21210
diff
changeset

940 
natceiling :: "real => nat" where 
19765  941 
"natceiling x = nat(ceiling x)" 
16819  942 

943 
lemma natfloor_zero [simp]: "natfloor 0 = 0" 

944 
by (unfold natfloor_def, simp) 

945 

946 
lemma natfloor_one [simp]: "natfloor 1 = 1" 

947 
by (unfold natfloor_def, simp) 

948 

949 
lemma zero_le_natfloor [simp]: "0 <= natfloor x" 

950 
by (unfold natfloor_def, simp) 

951 

952 
lemma natfloor_number_of_eq [simp]: "natfloor (number_of n) = number_of n" 

953 
by (unfold natfloor_def, simp) 

954 

955 
lemma natfloor_real_of_nat [simp]: "natfloor(real n) = n" 

956 
by (unfold natfloor_def, simp) 

957 

958 
lemma real_natfloor_le: "0 <= x ==> real(natfloor x) <= x" 

959 
by (unfold natfloor_def, simp) 

960 

961 
lemma natfloor_neg: "x <= 0 ==> natfloor x = 0" 

962 
apply (unfold natfloor_def) 

963 
apply (subgoal_tac "floor x <= floor 0") 

964 
apply simp 

965 
apply (erule floor_mono2) 

966 
done 

967 

968 
lemma natfloor_mono: "x <= y ==> natfloor x <= natfloor y" 

969 
apply (case_tac "0 <= x") 

970 
apply (subst natfloor_def)+ 

971 
apply (subst nat_le_eq_zle) 

972 
apply force 

16893  973 
apply (erule floor_mono2) 
16819  974 
apply (subst natfloor_neg) 
975 
apply simp 

976 
apply simp 

977 
done 

978 

979 
lemma le_natfloor: "real x <= a ==> x <= natfloor a" 

980 
apply (unfold natfloor_def) 

981 
apply (subst nat_int [THEN sym]) 

982 
apply (subst nat_le_eq_zle) 

983 
apply simp 

984 
apply (rule le_floor) 

985 
apply simp 

986 
done 

987 

988 
lemma le_natfloor_eq: "0 <= x ==> (a <= natfloor x) = (real a <= x)" 

989 
apply (rule iffI) 

990 
apply (rule order_trans) 

991 
prefer 2 

992 
apply (erule real_natfloor_le) 

993 
apply (subst real_of_nat_le_iff) 

994 
apply assumption 

995 
apply (erule le_natfloor) 

996 
done 

997 

16893  998 
lemma le_natfloor_eq_number_of [simp]: 
16819  999 
"~ neg((number_of n)::int) ==> 0 <= x ==> 
1000 
(number_of n <= natfloor x) = (number_of n <= x)" 

1001 
apply (subst le_natfloor_eq, assumption) 

1002 
apply simp 

1003 
done 

1004 

16820  1005 
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" 
16819  1006 
apply (case_tac "0 <= x") 
1007 
apply (subst le_natfloor_eq, assumption, simp) 

1008 
apply (rule iffI) 

16893  1009 
apply (subgoal_tac "natfloor x <= natfloor 0") 
16819  1010 
apply simp 
1011 
apply (rule natfloor_mono) 

1012 
apply simp 

1013 
apply simp 

1014 
done 

1015 

1016 
lemma natfloor_eq: "real n <= x ==> x < real n + 1 ==> natfloor x = n" 

1017 
apply (unfold natfloor_def) 

1018 
apply (subst nat_int [THEN sym]);back; 

1019 
apply (subst eq_nat_nat_iff) 

1020 
apply simp 

1021 
apply simp 

1022 
apply (rule floor_eq2) 

1023 
apply auto 

1024 
done 

1025 

1026 
lemma real_natfloor_add_one_gt: "x < real(natfloor x) + 1" 

1027 
apply (case_tac "0 <= x") 

1028 
apply (unfold natfloor_def) 

1029 
apply simp 

1030 
apply simp_all 

1031 
done 

1032 

1033 
lemma real_natfloor_gt_diff_one: "x  1 < real(natfloor x)" 

1034 
apply (simp add: compare_rls) 

1035 
apply (rule real_natfloor_add_one_gt) 

1036 
done 

1037 

1038 
lemma ge_natfloor_plus_one_imp_gt: "natfloor z + 1 <= n ==> z < real n" 

1039 
apply (subgoal_tac "z < real(natfloor z) + 1") 

1040 
apply arith 

1041 
apply (rule real_natfloor_add_one_gt) 

1042 
done 

1043 

1044 
lemma natfloor_add [simp]: "0 <= x ==> natfloor (x + real a) = natfloor x + a" 

1045 
apply (unfold natfloor_def) 

23309  1046 
apply (subgoal_tac "real a = real (int_of_nat a)") 
16819  1047 
apply (erule ssubst) 
23309  1048 
apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq) 
16819  1049 
apply simp 
1050 
done 

1051 

16893  1052 
lemma natfloor_add_number_of [simp]: 
1053 
"~neg ((number_of n)::int) ==> 0 <= x ==> 

16819  1054 
natfloor (x + number_of n) = natfloor x + number_of n" 
1055 
apply (subst natfloor_add [THEN sym]) 

1056 
apply simp_all 

1057 
done 

1058 

1059 
lemma natfloor_add_one: "0 <= x ==> natfloor(x + 1) = natfloor x + 1" 

1060 
apply (subst natfloor_add [THEN sym]) 

1061 
apply assumption 

1062 
apply simp 

1063 
done 

1064 

16893  1065 
lemma natfloor_subtract [simp]: "real a <= x ==> 
16819  1066 
natfloor(x  real a) = natfloor x  a" 
1067 
apply (unfold natfloor_def) 

23309  1068 
apply (subgoal_tac "real a = real (int_of_nat a)") 
16819  1069 
apply (erule ssubst) 
23309  1070 
apply (simp del: real_of_int_of_nat_eq) 
16819  1071 
apply simp 
1072 
done 

1073 

1074 
lemma natceiling_zero [simp]: "natceiling 0 = 0" 

1075 
by (unfold natceiling_def, simp) 

1076 

1077 
lemma natceiling_one [simp]: "natceiling 1 = 1" 

1078 
by (unfold natceiling_def, simp) 

1079 

1080 
lemma zero_le_natceiling [simp]: "0 <= natceiling x" 

1081 
by (unfold natceiling_def, simp) 

1082 

1083 
lemma natceiling_number_of_eq [simp]: "natceiling (number_of n) = number_of n" 

1084 
by (unfold natceiling_def, simp) 

1085 

1086 
lemma natceiling_real_of_nat [simp]: "natceiling(real n) = n" 

1087 
by (unfold natceiling_def, simp) 

1088 

1089 
lemma real_natceiling_ge: "x <= real(natceiling x)" 

1090 
apply (unfold natceiling_def) 

1091 
apply (case_tac "x < 0") 

1092 
apply simp 

1093 
apply (subst real_nat_eq_real) 

1094 
apply (subgoal_tac "ceiling 0 <= ceiling x") 

1095 
apply simp 

1096 
apply (rule ceiling_mono2) 

1097 
apply simp 

1098 
apply simp 

1099 
done 

1100 

1101 
lemma natceiling_neg: "x <= 0 ==> natceiling x = 0" 

1102 
apply (unfold natceiling_def) 

1103 
apply simp 

1104 
done 

1105 

1106 
lemma natceiling_mono: "x <= y ==> natceiling x <= natceiling y" 

1107 
apply (case_tac "0 <= x") 

1108 
apply (subst natceiling_def)+ 

1109 
apply (subst nat_le_eq_zle) 

1110 
apply (rule disjI2) 

1111 
apply (subgoal_tac "real (0::int) <= real(ceiling y)") 

1112 
apply simp 

1113 
apply (rule order_trans) 

1114 
apply simp 

1115 
apply (erule order_trans) 

1116 
apply simp 

1117 
apply (erule ceiling_mono2) 

1118 
apply (subst natceiling_neg) 

1119 
apply simp_all 

1120 
done 

1121 

1122 
lemma natceiling_le: "x <= real a ==> natceiling x <= a" 

1123 
apply (unfold natceiling_def) 

1124 
apply (case_tac "x < 0") 

1125 
apply simp 

1126 
apply (subst nat_int [THEN sym]);back; 

1127 
apply (subst nat_le_eq_zle) 

1128 
apply simp 

1129 
apply (rule ceiling_le) 

1130 
apply simp 

1131 
done 

1132 

1133 
lemma natceiling_le_eq: "0 <= x ==> (natceiling x <= a) = (x <= real a)" 

1134 
apply (rule iffI) 

1135 
apply (rule order_trans) 

1136 
apply (rule real_natceiling_ge) 

1137 
apply (subst real_of_nat_le_iff) 

1138 
apply assumption 

1139 
apply (erule natceiling_le) 

1140 
done 

1141 

16893  1142 
lemma natceiling_le_eq_number_of [simp]: 
16820  1143 
"~ neg((number_of n)::int) ==> 0 <= x ==> 
1144 
(natceiling x <= number_of n) = (x <= number_of n)" 

16819  1145 
apply (subst natceiling_le_eq, assumption) 
1146 
apply simp 

1147 
done 

1148 

16820  1149 
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" 
16819  1150 
apply (case_tac "0 <= x") 
1151 
apply (subst natceiling_le_eq) 

1152 
apply assumption 

1153 
apply simp 

1154 
apply (subst natceiling_neg) 

1155 
apply simp 

1156 
apply simp 

1157 
done 

1158 

1159 
lemma natceiling_eq: "real n < x ==> x <= real n + 1 ==> natceiling x = n + 1" 

1160 
apply (unfold natceiling_def) 

19850  1161 
apply (simplesubst nat_int [THEN sym]) back back 
16819  1162 
apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") 
1163 
apply (erule ssubst) 

1164 
apply (subst eq_nat_nat_iff) 

1165 
apply (subgoal_tac "ceiling 0 <= ceiling x") 

1166 
apply simp 

1167 
apply (rule ceiling_mono2) 

1168 
apply force 

1169 
apply force 

1170 
apply (rule ceiling_eq2) 

1171 
apply (simp, simp) 

1172 
apply (subst nat_add_distrib) 

1173 
apply auto 

1174 
done 

1175 

16893  1176 
lemma natceiling_add [simp]: "0 <= x ==> 
16819  1177 
natceiling (x + real a) = natceiling x + a" 
1178 
apply (unfold natceiling_def) 

23309  1179 
apply (subgoal_tac "real a = real (int_of_nat a)") 
16819  1180 
apply (erule ssubst) 
23309  1181 
apply (simp del: real_of_int_of_nat_eq) 
16819  1182 
apply (subst nat_add_distrib) 
1183 
apply (subgoal_tac "0 = ceiling 0") 

1184 
apply (erule ssubst) 

1185 
apply (erule ceiling_mono2) 

1186 
apply simp_all 

1187 
done 

1188 

16893  1189 
lemma natceiling_add_number_of [simp]: 
1190 
"~ neg ((number_of n)::int) ==> 0 <= x ==> 

16820  1191 
natceiling (x + number_of n) = natceiling x + number_of n" 
16819  1192 
apply (subst natceiling_add [THEN sym]) 
1193 
apply simp_all 

1194 
done 

1195 

1196 
lemma natceiling_add_one: "0 <= x ==> natceiling(x + 1) = natceiling x + 1" 

1197 
apply (subst natceiling_add [THEN sym]) 

1198 
apply assumption 

1199 
apply simp 

1200 
done 

1201 

16893  1202 
lemma natceiling_subtract [simp]: "real a <= x ==> 
16819  1203 
natceiling(x  real a) = natceiling x  a" 
1204 
apply (unfold natceiling_def) 

23309  1205 
apply (subgoal_tac "real a = real (int_of_nat a)") 
16819  1206 
apply (erule ssubst) 
23309  1207 
apply (simp del: real_of_int_of_nat_eq) 
16819  1208 
apply simp 
1209 
done 

1210 

16893  1211 
lemma natfloor_div_nat: "1 <= x ==> 0 < y ==> 
16819  1212 
natfloor (x / real y) = natfloor x div y" 
1213 
proof  

1214 
assume "1 <= (x::real)" and "0 < (y::nat)" 

1215 
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" 

1216 
by simp 

16893  1217 
then have a: "real(natfloor x) = real ((natfloor x) div y) * real y + 
16819  1218 
real((natfloor x) mod y)" 
1219 
by (simp only: real_of_nat_add [THEN sym] real_of_nat_mult [THEN sym]) 

1220 
have "x = real(natfloor x) + (x  real(natfloor x))" 

1221 
by simp 

16893  1222 
then have "x = real ((natfloor x) div y) * real y + 
16819  1223 
real((natfloor x) mod y) + (x  real(natfloor x))" 
1224 
by (simp add: a) 

1225 
then have "x / real y = ... / real y" 

1226 
by simp 

16893  1227 
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 
16819  1228 
real y + (x  real(natfloor x)) / real y" 
1229 
by (auto simp add: ring_distrib ring_eq_simps add_divide_distrib 

1230 
diff_divide_distrib prems) 

1231 
finally have "natfloor (x / real y) = natfloor(...)" by simp 

16893  1232 
also have "... = natfloor(real((natfloor x) mod y) / 
16819  1233 
real y + (x  real(natfloor x)) / real y + real((natfloor x) div y))" 
1234 
by (simp add: add_ac) 

16893  1235 
also have "... = natfloor(real((natfloor x) mod y) / 
16819  1236 
real y + (x  real(natfloor x)) / real y) + (natfloor x) div y" 
1237 
apply (rule natfloor_add) 

1238 
apply (rule add_nonneg_nonneg) 

1239 
apply (rule divide_nonneg_pos) 

1240 
apply simp 

1241 
apply (simp add: prems) 

1242 
apply (rule divide_nonneg_pos) 

1243 
apply (simp add: compare_rls) 

1244 
apply (rule real_natfloor_le) 

1245 
apply (insert prems, auto) 

1246 
done 

16893  1247 
also have "natfloor(real((natfloor x) mod y) / 
16819  1248 
real y + (x  real(natfloor x)) / real y) = 0" 
1249 
apply (rule natfloor_eq) 

1250 
apply simp 

1251 
apply (rule add_nonneg_nonneg) 

1252 
apply (rule divide_nonneg_pos) 

1253 
apply force 

1254 
apply (force simp add: prems) 

1255 
apply (rule divide_nonneg_pos) 

1256 
apply (simp add: compare_rls) 

1257 
apply (rule real_natfloor_le) 

1258 
apply (auto simp add: prems) 

1259 
apply (insert prems, arith) 

1260 
apply (simp add: add_divide_distrib [THEN sym]) 

1261 
apply (subgoal_tac "real y = real y  1 + 1") 

1262 
apply (erule ssubst) 

1263 
apply (rule add_le_less_mono) 

1264 
apply (simp add: compare_rls) 

16893  1265 
apply (subgoal_tac "real(natfloor x mod y) + 1 = 
16819  1266 
real(natfloor x mod y + 1)") 
1267 
apply (erule ssubst) 

1268 
apply (subst real_of_nat_le_iff) 

1269 
apply (subgoal_tac "natfloor x mod y < y") 

1270 
apply arith 

1271 
apply (rule mod_less_divisor) 

1272 
apply assumption 

1273 
apply auto 

1274 
apply (simp add: compare_rls) 

1275 
apply (subst add_commute) 

1276 
apply (rule real_natfloor_add_one_gt) 

1277 
done 

1278 
finally show ?thesis 

1279 
by simp 

1280 
qed 

1281 

14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

1282 
end 