author  huffman 
Sat, 19 May 2007 04:52:24 +0200  
changeset 23012  496b42cf588d 
parent 23008  c4a259f3bbcc 
child 23309  678ee30499d2 
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 

62 
obtain a where a_in_P: "a \<in> P" using not_empty_P .. 

63 
have a_pos: "0 < a" using positive_P .. 

64 
then obtain pa where "a = real_of_preal pa" 

65 
by (auto simp add: real_gt_zero_preal_Ex) 

66 
hence "pa \<in> ?pP" using a_in_P by auto 

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 .. 

71 
hence "a < sup" .. 

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 

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

483 
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" 
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) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

486 
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) 
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]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

488 
apply (simp_all add: real_of_int_real_of_nat) 
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 

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

491 
lemma floor_minus_real_of_nat [simp]: "floor ( real (n::nat)) =  int n" 
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) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

494 
apply (drule_tac [2] real_of_int_real_of_nat [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]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

497 
apply (simp_all add: real_of_int_real_of_nat) 
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) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

503 
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

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

506 

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

507 
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

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

509 
apply (rule Least_equality) 
16819  510 
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

511 
apply (drule_tac [2] real_of_int_real_of_nat [THEN ssubst]) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

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

514 

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

515 
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

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

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

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

519 
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

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

521 

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

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

523 
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

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

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

526 
have "real m < real n + 1" by (rule order_le_less_trans) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

527 
also have "... = real(n+1)" by simp 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

528 
finally have "m < n+1" by (simp only: real_of_int_less_iff) 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

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

531 

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

532 
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

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

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

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

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

538 

16819  539 
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

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

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

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

543 
apply (rule theI2) 
16819  544 
apply (rule_tac [3] theI2) 
545 
apply simp 

546 
apply (erule conjI) 

547 
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

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

549 

16819  550 
lemma floor_mono2: "x \<le> y ==> floor x \<le> floor y" 
22998  551 
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

552 

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

553 
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

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

555 

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

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

557 
"(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

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

559 
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

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

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

563 

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

564 
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

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

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

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

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

569 

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

570 
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

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

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

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

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

575 

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

576 
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

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

578 
apply (simp add: real_of_nat_Suc) 
15539  579 
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

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

581 

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

582 
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

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

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

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

586 

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

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

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

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

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

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

592 

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

595 
prefer 2 

596 
apply (rule floor_real_of_int) 

597 
apply simp 

598 
done 

599 

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

600 
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

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

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

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

604 
apply (auto intro: lemma_floor) 
16819  605 
done 
606 

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

608 
apply (simp add: floor_def Least_def) 

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

610 
apply (rule theI2) 

611 
apply (auto intro: lemma_floor) 

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

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

613 

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

614 
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

615 
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

616 
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

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

618 

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

621 
apply (auto simp del: real_of_int_floor_gt_diff_one) 

622 
done 

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

623 

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

626 
apply arith 

627 
apply (subst real_of_int_less_iff [THEN sym]) 

628 
apply simp 

16893  629 
apply (insert real_of_int_floor_add_one_gt [of x]) 
16819  630 
apply arith 
631 
done 

632 

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

634 
apply (rule order_trans) 

635 
prefer 2 

636 
apply (rule real_of_int_floor_le) 

637 
apply (subst real_of_int_le_iff) 

638 
apply assumption 

639 
done 

640 

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

642 
apply (rule iffI) 

643 
apply (erule real_le_floor) 

644 
apply (erule le_floor) 

645 
done 

646 

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

650 

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

652 
by (simp add: le_floor_eq) 

653 

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

655 
by (simp add: le_floor_eq) 

656 

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

658 
apply (subst linorder_not_le [THEN sym])+ 

659 
apply simp 

660 
apply (rule le_floor_eq) 

661 
done 

662 

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

666 

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

668 
by (simp add: floor_less_eq) 

669 

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

671 
by (simp add: floor_less_eq) 

672 

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

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

675 
apply auto 

676 
done 

677 

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

681 

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

683 
by (simp add: less_floor_eq) 

684 

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

686 
by (simp add: less_floor_eq) 

687 

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

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

690 
apply auto 

691 
done 

692 

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

696 

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

698 
by (simp add: floor_le_eq) 

699 

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

701 
by (simp add: floor_le_eq) 

702 

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

704 
apply (subst order_eq_iff) 

705 
apply (rule conjI) 

706 
prefer 2 

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

708 
apply arith 

709 
apply (subst real_of_int_less_iff [THEN sym]) 

710 
apply simp 

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

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

713 
apply arith 

714 
apply (rule real_of_int_floor_le) 

715 
apply (rule real_of_int_floor_add_one_gt) 

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

717 
apply arith 

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

723 
apply (rule real_of_int_floor_add_one_gt) 

724 
apply (rule real_of_int_floor_le) 

725 
done 

726 

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

730 
apply simp 

731 
done 

732 

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

734 
apply (subst floor_add [THEN sym]) 

735 
apply simp 

736 
done 

737 

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

739 
apply (subst diff_minus)+ 

740 
apply (subst real_of_int_minus [THEN sym]) 

741 
apply (rule floor_add) 

742 
done 

743 

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

747 
apply simp 

748 
done 

749 

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

751 
apply (subst floor_subtract [THEN sym]) 

752 
apply simp 

753 
done 

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

754 

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

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

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

757 

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

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

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

760 

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

761 
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

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

763 

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

764 
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

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

766 

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

767 
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

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

769 

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

770 
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

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

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

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

774 

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

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

777 

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

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

780 

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

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

782 
"(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

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

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

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

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

787 

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

788 
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

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

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

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

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

793 

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

794 
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

795 
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

796 

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

797 
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

798 
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

799 

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

800 
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

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

802 

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

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

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

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

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

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

808 

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

811 

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

812 
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

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

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

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

816 

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

817 
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

818 
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

819 
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

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

821 

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

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

825 
apply simp 

826 
apply (rule le_floor) 

827 
apply simp 

828 
done 

829 

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

831 
apply (unfold ceiling_def) 

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

833 
apply simp 

834 
apply (rule real_le_floor) 

835 
apply simp 

836 
done 

837 

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

839 
apply (rule iffI) 

840 
apply (erule ceiling_le_real) 

841 
apply (erule ceiling_le) 

842 
done 

843 

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

847 

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

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

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

855 
apply (subst linorder_not_le [THEN sym])+ 

856 
apply simp 

857 
apply (rule ceiling_le_eq) 

858 
done 

859 

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

863 

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

865 
by (simp add: less_ceiling_eq) 

866 

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

868 
by (simp add: less_ceiling_eq) 

869 

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

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

872 
apply auto 

873 
done 

874 

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

878 

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

880 
by (simp add: ceiling_less_eq) 

881 

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

883 
by (simp add: ceiling_less_eq) 

884 

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

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

887 
apply auto 

888 
done 

889 

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

893 

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

895 
by (simp add: le_ceiling_eq) 

896 

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

898 
by (simp add: le_ceiling_eq) 

899 

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

901 
apply (unfold ceiling_def, simp) 

902 
apply (subst real_of_int_minus [THEN sym]) 

903 
apply (subst floor_add) 

904 
apply simp 

905 
done 

906 

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

910 
apply simp 

911 
done 

912 

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

914 
apply (subst ceiling_add [THEN sym]) 

915 
apply simp 

916 
done 

917 

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

919 
apply (subst diff_minus)+ 

920 
apply (subst real_of_int_minus [THEN sym]) 

921 
apply (rule ceiling_add) 

922 
done 

923 

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

927 
apply simp 

928 
done 

929 

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

931 
apply (subst ceiling_subtract [THEN sym]) 

932 
apply simp 

933 
done 

934 

935 
subsection {* Versions for the natural numbers *} 

936 

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

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

940 

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

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

942 
natceiling :: "real => nat" where 
19765  943 
"natceiling x = nat(ceiling x)" 
16819  944 

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

946 
by (unfold natfloor_def, simp) 

947 

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

949 
by (unfold natfloor_def, simp) 

950 

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

952 
by (unfold natfloor_def, simp) 

953 

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

955 
by (unfold natfloor_def, simp) 

956 

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

958 
by (unfold natfloor_def, simp) 

959 

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

961 
by (unfold natfloor_def, simp) 

962 

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

964 
apply (unfold natfloor_def) 

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

966 
apply simp 

967 
apply (erule floor_mono2) 

968 
done 

969 

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

971 
apply (case_tac "0 <= x") 

972 
apply (subst natfloor_def)+ 

973 
apply (subst nat_le_eq_zle) 

974 
apply force 

16893  975 
apply (erule floor_mono2) 
16819  976 
apply (subst natfloor_neg) 
977 
apply simp 

978 
apply simp 

979 
done 

980 

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

982 
apply (unfold natfloor_def) 

983 
apply (subst nat_int [THEN sym]) 

984 
apply (subst nat_le_eq_zle) 

985 
apply simp 

986 
apply (rule le_floor) 

987 
apply simp 

988 
done 

989 

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

991 
apply (rule iffI) 

992 
apply (rule order_trans) 

993 
prefer 2 

994 
apply (erule real_natfloor_le) 

995 
apply (subst real_of_nat_le_iff) 

996 
apply assumption 

997 
apply (erule le_natfloor) 

998 
done 

999 

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

1003 
apply (subst le_natfloor_eq, assumption) 

1004 
apply simp 

1005 
done 

1006 

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

1010 
apply (rule iffI) 

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

1014 
apply simp 

1015 
apply simp 

1016 
done 

1017 

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

1019 
apply (unfold natfloor_def) 

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

1021 
apply (subst eq_nat_nat_iff) 

1022 
apply simp 

1023 
apply simp 

1024 
apply (rule floor_eq2) 

1025 
apply auto 

1026 
done 

1027 

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

1029 
apply (case_tac "0 <= x") 

1030 
apply (unfold natfloor_def) 

1031 
apply simp 

1032 
apply simp_all 

1033 
done 

1034 

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

1036 
apply (simp add: compare_rls) 

1037 
apply (rule real_natfloor_add_one_gt) 

1038 
done 

1039 

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

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

1042 
apply arith 

1043 
apply (rule real_natfloor_add_one_gt) 

1044 
done 

1045 

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

1047 
apply (unfold natfloor_def) 

1048 
apply (subgoal_tac "real a = real (int a)") 

1049 
apply (erule ssubst) 

1050 
apply (simp add: nat_add_distrib) 

1051 
apply simp 

1052 
done 

1053 

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

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

1058 
apply simp_all 

1059 
done 

1060 

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

1062 
apply (subst natfloor_add [THEN sym]) 

1063 
apply assumption 

1064 
apply simp 

1065 
done 

1066 

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

1070 
apply (subgoal_tac "real a = real (int a)") 

1071 
apply (erule ssubst) 

1072 
apply simp 

1073 
apply simp 

1074 
done 

1075 

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

1077 
by (unfold natceiling_def, simp) 

1078 

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

1080 
by (unfold natceiling_def, simp) 

1081 

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

1083 
by (unfold natceiling_def, simp) 

1084 

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

1086 
by (unfold natceiling_def, simp) 

1087 

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

1089 
by (unfold natceiling_def, simp) 

1090 

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

1092 
apply (unfold natceiling_def) 

1093 
apply (case_tac "x < 0") 

1094 
apply simp 

1095 
apply (subst real_nat_eq_real) 

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

1097 
apply simp 

1098 
apply (rule ceiling_mono2) 

1099 
apply simp 

1100 
apply simp 

1101 
done 

1102 

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

1104 
apply (unfold natceiling_def) 

1105 
apply simp 

1106 
done 

1107 

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

1109 
apply (case_tac "0 <= x") 

1110 
apply (subst natceiling_def)+ 

1111 
apply (subst nat_le_eq_zle) 

1112 
apply (rule disjI2) 

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

1114 
apply simp 

1115 
apply (rule order_trans) 

1116 
apply simp 

1117 
apply (erule order_trans) 

1118 
apply simp 

1119 
apply (erule ceiling_mono2) 

1120 
apply (subst natceiling_neg) 

1121 
apply simp_all 

1122 
done 

1123 

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

1125 
apply (unfold natceiling_def) 

1126 
apply (case_tac "x < 0") 

1127 
apply simp 

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

1129 
apply (subst nat_le_eq_zle) 

1130 
apply simp 

1131 
apply (rule ceiling_le) 

1132 
apply simp 

1133 
done 

1134 

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

1136 
apply (rule iffI) 

1137 
apply (rule order_trans) 

1138 
apply (rule real_natceiling_ge) 

1139 
apply (subst real_of_nat_le_iff) 

1140 
apply assumption 

1141 
apply (erule natceiling_le) 

1142 
done 

1143 

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

16819  1147 
apply (subst natceiling_le_eq, assumption) 
1148 
apply simp 

1149 
done 

1150 

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

1154 
apply assumption 

1155 
apply simp 

1156 
apply (subst natceiling_neg) 

1157 
apply simp 

1158 
apply simp 

1159 
done 

1160 

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

1162 
apply (unfold natceiling_def) 

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

1166 
apply (subst eq_nat_nat_iff) 

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

1168 
apply simp 

1169 
apply (rule ceiling_mono2) 

1170 
apply force 

1171 
apply force 

1172 
apply (rule ceiling_eq2) 

1173 
apply (simp, simp) 

1174 
apply (subst nat_add_distrib) 

1175 
apply auto 

1176 
done 

1177 

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

1181 
apply (subgoal_tac "real a = real (int a)") 

1182 
apply (erule ssubst) 

1183 
apply simp 

1184 
apply (subst nat_add_distrib) 

1185 
apply (subgoal_tac "0 = ceiling 0") 

1186 
apply (erule ssubst) 

1187 
apply (erule ceiling_mono2) 

1188 
apply simp_all 

1189 
done 

1190 

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

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

1196 
done 

1197 

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

1199 
apply (subst natceiling_add [THEN sym]) 

1200 
apply assumption 

1201 
apply simp 

1202 
done 

1203 

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

1207 
apply (subgoal_tac "real a = real (int a)") 

1208 
apply (erule ssubst) 

1209 
apply simp 

1210 
apply simp 

1211 
done 

1212 

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

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

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

1218 
by simp 

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

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

1223 
by simp 

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

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

1228 
by simp 

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

1232 
diff_divide_distrib prems) 

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

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

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

1240 
apply (rule add_nonneg_nonneg) 

1241 
apply (rule divide_nonneg_pos) 

1242 
apply simp 

1243 
apply (simp add: prems) 

1244 
apply (rule divide_nonneg_pos) 

1245 
apply (simp add: compare_rls) 

1246 
apply (rule real_natfloor_le) 

1247 
apply (insert prems, auto) 

1248 
done 

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

1252 
apply simp 

1253 
apply (rule add_nonneg_nonneg) 

1254 
apply (rule divide_nonneg_pos) 

1255 
apply force 

1256 
apply (force simp add: prems) 

1257 
apply (rule divide_nonneg_pos) 

1258 
apply (simp add: compare_rls) 

1259 
apply (rule real_natfloor_le) 

1260 
apply (auto simp add: prems) 

1261 
apply (insert prems, arith) 

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

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

1264 
apply (erule ssubst) 

1265 
apply (rule add_le_less_mono) 

1266 
apply (simp add: compare_rls) 

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

1270 
apply (subst real_of_nat_le_iff) 

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

1272 
apply arith 

1273 
apply (rule mod_less_divisor) 

1274 
apply assumption 

1275 
apply auto 

1276 
apply (simp add: compare_rls) 

1277 
apply (subst add_commute) 

1278 
apply (rule real_natfloor_add_one_gt) 

1279 
done 

1280 
finally show ?thesis 

1281 
by simp 

1282 
qed 

1283 

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

1284 
end 