author  haftmann 
Wed, 03 Dec 2008 15:58:44 +0100  
changeset 28952  15a4b2cf8c34 
parent 28562  src/HOL/Real/RComplete.thy@4e74209f113e 
child 29667  53103fc8ffa3 
permissions  rwrr 
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28562
diff
changeset

1 
(* Title : HOL/RComplete.thy 
16893  2 
Author : Jacques D. Fleuriot, University of Edinburgh 
3 
Author : Larry Paulson, University of Cambridge 

4 
Author : Jeremy Avigad, Carnegie Mellon University 

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

6 
*) 

5078  7 

16893  8 
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

9 

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

13 

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

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

16 

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

17 

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

20 
text {* 

21 
Supremum property for the set of positive reals 

22 

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

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

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

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

26 

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

29 

30 
lemma posreal_complete: 

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

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

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

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

35 
proof (rule exI, rule allI) 

36 
fix y 

37 
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

38 

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

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

42 
show ?thesis 

43 
proof 

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

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

46 
using neg_y by (rule real_less_all_real2) 

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

48 
next 

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

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

51 
hence "0 < x" using positive_P by simp 

52 
hence "y < x" using neg_y by simp 

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

54 
qed 

55 
next 

56 
assume pos_y: "0 < y" 

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

57 

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

60 

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

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

23389  65 
hence "pa \<in> ?pP" using `a \<in> P` by auto 
16893  66 
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

67 

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

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

73 
by (auto simp add: real_gt_zero_preal_Ex) 

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

75 
using sup by (auto simp add: real_of_preal_lessI) 

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

77 
by (rule preal_complete) 

78 

79 
show ?thesis 

80 
proof 

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

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

83 
hence "0 < x" using pos_y by arith 

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

85 
by (auto simp add: real_gt_zero_preal_Ex) 

86 

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

88 
proof 

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

90 
by (simp add: real_of_preal_lessI) 

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

92 
qed 

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

93 

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

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

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

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

99 
next 

100 
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

101 

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

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

105 
using psup by auto 

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

107 
by (simp add: real_gt_zero_preal_Ex) 

108 
hence "y < x" using py_less_X and y_is_py 

109 
by (simp add: real_of_preal_lessI) 

110 

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

112 

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

114 
qed 

115 
qed 

116 
qed 

117 

118 
text {* 

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

120 
*} 

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

121 

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

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

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

126 
done 

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

127 

5078  128 

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

131 
*} 

132 

133 
lemma posreals_complete: 

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

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

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

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

138 
proof 

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

140 

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

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

143 

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

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

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

147 
hence "0 < u" using x_gt_zero by arith 

148 

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

150 
by (auto simp add: real_gt_zero_preal_Ex) 

151 

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

153 
proof 

154 
fix pa 

155 
assume "pa \<in> ?pS" 

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

157 
by simp 

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

159 
ultimately show "pa \<le> pu" 

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

161 
qed 

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

162 

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

165 
fix y 

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

167 
hence "0 < y" using positive_S by simp 

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

169 
by (auto simp add: real_gt_zero_preal_Ex) 

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

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

172 
by (rule preal_psup_le) 

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

174 
using y_is_py by (simp add: real_of_preal_le_iff) 

175 
qed 

176 

177 
moreover { 

178 
fix x 

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

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

181 
proof  

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

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

184 

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

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

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

188 

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

190 
hence "0 < x" using s_pos by simp 

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

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

193 

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

195 
proof 

196 
fix pe 

197 
assume "pe \<in> ?pS" 

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

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

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

201 
qed 

202 

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

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

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

206 
qed 

207 
} 

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

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

210 
qed 

211 

212 
text {* 

213 
\medskip reals Completeness (again!) 

214 
*} 

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

215 

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

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

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

220 
proof  

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

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

223 
using exists_Ub .. 

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

225 

226 
{ 

227 
fix x 

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

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

230 
by (simp add: isUb_def setle_def) 

231 
{ 

232 
fix s 

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

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

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

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

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

238 
} 

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

240 
by (auto simp add: isUb_def setle_def) 

241 
} note S_Ub_is_SHIFT_Ub = this 

242 

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

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

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

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

247 
using X_in_S and Y_isUb by auto 

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

249 
using posreals_complete [of ?SHIFT] by blast 

250 

251 
show ?thesis 

252 
proof 

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

254 
proof (rule isLubI2) 

255 
{ 

256 
fix x 

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

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

259 
using S_Ub_is_SHIFT_Ub by simp 

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

261 
using t_is_Lub by (simp add: isLub_le_isUb) 

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

263 
} 

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

265 
by (simp add: setgeI) 

266 
next 

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

268 
proof  

269 
{ 

270 
fix y 

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

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

273 
proof  

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

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

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

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

278 

279 
show ?thesis 

280 
proof cases 

281 
assume "y \<le> x" 

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

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

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

285 
next 

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

287 
hence x_less_y: "x < y" by arith 

288 

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

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

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

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

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

294 
thus ?thesis by simp 

295 
qed 

296 
qed 

297 
} 

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

299 
qed 

300 
qed 

301 
qed 

302 
qed 

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

303 

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

304 

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

307 
theorem reals_Archimedean: 

308 
assumes x_pos: "0 < x" 

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

310 
proof (rule ccontr) 

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

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

313 
proof 

314 
fix n 

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

316 
by (simp add: linorder_not_less) 

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

318 
by (simp add: inverse_eq_divide) 

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

320 
by (rule real_of_nat_ge_zero) 

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

322 
by (rule mult_right_mono) 

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

324 
qed 

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

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

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

328 
by (simp add: isUbI) 

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

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

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

332 
by (simp add: reals_complete) 

333 
then obtain "t" where 

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

335 

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

337 
proof 

338 
fix n 

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

340 
by (simp add: isLubD2) 

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

342 
by (simp add: right_distrib real_of_nat_Suc) 

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

344 
qed 

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

345 

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

348 
by (auto simp add: setle_def) 

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

350 
by (simp add: isUbI) 

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

352 
using t_is_Lub by (simp add: isLub_le_isUb) 

353 
thus False using x_pos by arith 

354 
qed 

355 

356 
text {* 

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

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

359 
*} 

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

360 

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

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

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

365 
thus ?thesis .. 

366 
next 

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

368 
hence x_greater_zero: "0 < x" by simp 

369 
hence "0 < inverse x" by simp 

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

371 
using reals_Archimedean by blast 

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

373 
using x_greater_zero by (rule mult_strict_right_mono) 

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

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

378 
hence "x < real (Suc n)" 

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23389
diff
changeset

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

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

382 

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

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

386 
proof 

387 
fix y 

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

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

390 
using reals_Archimedean2 .. 

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

392 
using x_greater_zero by (simp add: mult_strict_right_mono) 

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

23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23389
diff
changeset

394 
by (simp add: ring_simps) 
16893  395 
hence "y < real (n::nat) * x" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23389
diff
changeset

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

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

399 

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

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

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

406 
apply (rename_tac x') 

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

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

16819  410 
done 
411 

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

16893  413 
by (drule reals_Archimedean6) auto 
16819  414 

415 
lemma reals_Archimedean_6b_int: 

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

417 
apply (drule reals_Archimedean6a, auto) 

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

419 
apply (simp add: real_of_int_real_of_nat real_of_nat_Suc) 

420 
done 

421 

422 
lemma reals_Archimedean_6c_int: 

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

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

425 
apply (rename_tac n) 

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

429 
done 

430 

431 

28091
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

432 
subsection{*Density of the Rational Reals in the Reals*} 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

433 

50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

434 
text{* This density proof is due to Stefan Richter and was ported by TN. The 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

435 
original source is \emph{Real Analysis} by H.L. Royden. 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

436 
It employs the Archimedean property of the reals. *} 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

437 

50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

438 
lemma Rats_dense_in_nn_real: fixes x::real 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

439 
assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>. x<r \<and> r<y" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

440 
proof  
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

441 
from `x<y` have "0 < yx" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

442 
with reals_Archimedean obtain q::nat 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

443 
where q: "inverse (real q) < yx" and "0 < real q" by auto 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

444 
def p \<equiv> "LEAST n. y \<le> real (Suc n)/real q" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

445 
from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

446 
with `0 < real q` have ex: "y \<le> real n/real q" (is "?P n") 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

447 
by (simp add: pos_less_divide_eq[THEN sym]) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

448 
also from assms have "\<not> y \<le> real (0::nat) / real q" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

449 
ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

450 
by (unfold p_def) (rule Least_Suc) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

451 
also from ex have "?P (LEAST x. ?P x)" by (rule LeastI) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

452 
ultimately have suc: "y \<le> real (Suc p) / real q" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

453 
def r \<equiv> "real p/real q" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

454 
have "x = y(yx)" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

455 
also from suc q have "\<dots> < real (Suc p)/real q  inverse (real q)" by arith 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

456 
also have "\<dots> = real p / real q" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

457 
by (simp only: inverse_eq_divide real_diff_def real_of_nat_Suc 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

458 
minus_divide_left add_divide_distrib[THEN sym]) simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

459 
finally have "x<r" by (unfold r_def) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

460 
have "p<Suc p" .. also note main[THEN sym] 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

461 
finally have "\<not> ?P p" by (rule not_less_Least) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

462 
hence "r<y" by (simp add: r_def) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

463 
from r_def have "r \<in> \<rat>" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

464 
with `x<r` `r<y` show ?thesis by fast 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

465 
qed 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

466 

50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

467 
theorem Rats_dense_in_real: fixes x y :: real 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

468 
assumes "x<y" shows "\<exists>r \<in> \<rat>. x<r \<and> r<y" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

469 
proof  
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

470 
from reals_Archimedean2 obtain n::nat where "x < real n" by auto 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

471 
hence "0 \<le> x + real n" by arith 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

472 
also from `x<y` have "x + real n < y + real n" by arith 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

473 
ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

474 
by(rule Rats_dense_in_nn_real) 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

475 
then obtain r where "r \<in> \<rat>" and r2: "x + real n < r" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

476 
and r3: "r < y + real n" 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

477 
by blast 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

478 
have "r  real n = r + real (int n)/real (1::int)" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

479 
also from `r\<in>\<rat>` have "r + real (int n)/real (1::int) \<in> \<rat>" by simp 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

480 
also from r2 have "x < r  real n" by arith 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

481 
moreover from r3 have "r  real n < y" by arith 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

482 
ultimately show ?thesis by fast 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

483 
qed 
50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

484 

50f2d6ba024c
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
nipkow
parents:
27435
diff
changeset

485 

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

486 
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

487 

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

489 
floor :: "real => int" where 
28562  490 
[code del]: "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

491 

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

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

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

495 

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

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

499 

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

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

503 

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

504 

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

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

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

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

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

509 
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

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

511 

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

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

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

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

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

516 
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

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

518 

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

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

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

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

522 

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

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

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

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

526 

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

527 
lemma floor_zero [simp]: "floor 0 = 0" 
16819  528 
apply (simp add: floor_def del: real_of_int_add) 
529 
apply (rule Least_equality) 

530 
apply simp_all 

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

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

532 

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

533 
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

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

535 

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

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

538 
apply (rule Least_equality) 
23309  539 
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

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

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

543 

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

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

546 
apply (rule Least_equality) 
23309  547 
apply (drule_tac [2] real_of_int_of_nat_eq [THEN ssubst]) 
16819  548 
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

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

551 
done 
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 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

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

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

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

558 

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

559 
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

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

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

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

565 

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

566 
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

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

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

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

570 
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

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

572 

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

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

574 
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

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

576 
proof  
23389  577 
have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) 
578 
also have "... = real (n + 1)" by simp 

579 
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

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

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

582 

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

583 
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

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

585 
apply (insert real_lb_ub_int [of r], safe) 
16819  586 
apply (rule theI2) 
587 
apply auto 

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

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

589 

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

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

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

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

594 
apply (rule theI2) 
16819  595 
apply (rule_tac [3] theI2) 
596 
apply simp 

597 
apply (erule conjI) 

598 
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

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

600 

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

603 

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

604 
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

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

606 

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

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

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

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

610 
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

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

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

614 

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

615 
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

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

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

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

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

620 

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

621 
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

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

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

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

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

626 

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

627 
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

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

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

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

632 

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

633 
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

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

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

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

637 

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

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

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

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

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

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

643 

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

646 
prefer 2 

647 
apply (rule floor_real_of_int) 

648 
apply simp 

649 
done 

650 

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

651 
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

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

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

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

655 
apply (auto intro: lemma_floor) 
16819  656 
done 
657 

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

659 
apply (simp add: floor_def Least_def) 

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

661 
apply (rule theI2) 

662 
apply (auto intro: lemma_floor) 

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

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

664 

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

665 
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

666 
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

667 
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

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

669 

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

672 
apply (auto simp del: real_of_int_floor_gt_diff_one) 

673 
done 

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

674 

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

677 
apply arith 

678 
apply (subst real_of_int_less_iff [THEN sym]) 

679 
apply simp 

16893  680 
apply (insert real_of_int_floor_add_one_gt [of x]) 
16819  681 
apply arith 
682 
done 

683 

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

685 
apply (rule order_trans) 

686 
prefer 2 

687 
apply (rule real_of_int_floor_le) 

688 
apply (subst real_of_int_le_iff) 

689 
apply assumption 

690 
done 

691 

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

693 
apply (rule iffI) 

694 
apply (erule real_le_floor) 

695 
apply (erule le_floor) 

696 
done 

697 

16893  698 
lemma le_floor_eq_number_of [simp]: 
16819  699 
"(number_of n <= floor x) = (number_of n <= x)" 
700 
by (simp add: le_floor_eq) 

701 

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

703 
by (simp add: le_floor_eq) 

704 

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

706 
by (simp add: le_floor_eq) 

707 

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

709 
apply (subst linorder_not_le [THEN sym])+ 

710 
apply simp 

711 
apply (rule le_floor_eq) 

712 
done 

713 

16893  714 
lemma floor_less_eq_number_of [simp]: 
16819  715 
"(floor x < number_of n) = (x < number_of n)" 
716 
by (simp add: floor_less_eq) 

717 

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

719 
by (simp add: floor_less_eq) 

720 

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

722 
by (simp add: floor_less_eq) 

723 

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

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

726 
apply auto 

727 
done 

728 

16893  729 
lemma less_floor_eq_number_of [simp]: 
16819  730 
"(number_of n < floor x) = (number_of n + 1 <= x)" 
731 
by (simp add: less_floor_eq) 

732 

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

734 
by (simp add: less_floor_eq) 

735 

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

737 
by (simp add: less_floor_eq) 

738 

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

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

741 
apply auto 

742 
done 

743 

16893  744 
lemma floor_le_eq_number_of [simp]: 
16819  745 
"(floor x <= number_of n) = (x < number_of n + 1)" 
746 
by (simp add: floor_le_eq) 

747 

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

749 
by (simp add: floor_le_eq) 

750 

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

752 
by (simp add: floor_le_eq) 

753 

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

755 
apply (subst order_eq_iff) 

756 
apply (rule conjI) 

757 
prefer 2 

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

759 
apply arith 

760 
apply (subst real_of_int_less_iff [THEN sym]) 

761 
apply simp 

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

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

764 
apply arith 

765 
apply (rule real_of_int_floor_le) 

766 
apply (rule real_of_int_floor_add_one_gt) 

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

768 
apply arith 

16893  769 
apply (subst real_of_int_less_iff [THEN sym]) 
16819  770 
apply simp 
16893  771 
apply (subgoal_tac "real(floor(x + real a)) <= x + real a") 
16819  772 
apply (subgoal_tac "x < real(floor x) + 1") 
773 
apply arith 

774 
apply (rule real_of_int_floor_add_one_gt) 

775 
apply (rule real_of_int_floor_le) 

776 
done 

777 

16893  778 
lemma floor_add_number_of [simp]: 
16819  779 
"floor (x + number_of n) = floor x + number_of n" 
780 
apply (subst floor_add [THEN sym]) 

781 
apply simp 

782 
done 

783 

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

785 
apply (subst floor_add [THEN sym]) 

786 
apply simp 

787 
done 

788 

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

790 
apply (subst diff_minus)+ 

791 
apply (subst real_of_int_minus [THEN sym]) 

792 
apply (rule floor_add) 

793 
done 

794 

16893  795 
lemma floor_subtract_number_of [simp]: "floor (x  number_of n) = 
16819  796 
floor x  number_of n" 
797 
apply (subst floor_subtract [THEN sym]) 

798 
apply simp 

799 
done 

800 

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

802 
apply (subst floor_subtract [THEN sym]) 

803 
apply simp 

804 
done 

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

805 

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

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

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

808 

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

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

811 

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

812 
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

813 
by auto 
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 ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

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

817 

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

818 
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

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

820 

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

821 
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

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

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

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

825 

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

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

828 

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

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

831 

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

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

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

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

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

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

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

838 

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

839 
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

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

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

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

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

844 

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

845 
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

846 
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

847 

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

848 
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

849 
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

850 

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

851 
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

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

853 

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

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

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

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

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

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

859 

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

862 

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

863 
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

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

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

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

867 

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

868 
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

869 
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

870 
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

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

872 

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

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

876 
apply simp 

877 
apply (rule le_floor) 

878 
apply simp 

879 
done 

880 

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

882 
apply (unfold ceiling_def) 

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

884 
apply simp 

885 
apply (rule real_le_floor) 

886 
apply simp 

887 
done 

888 

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

890 
apply (rule iffI) 

891 
apply (erule ceiling_le_real) 

892 
apply (erule ceiling_le) 

893 
done 

894 

16893  895 
lemma ceiling_le_eq_number_of [simp]: 
16819  896 
"(ceiling x <= number_of n) = (x <= number_of n)" 
897 
by (simp add: ceiling_le_eq) 

898 

16893  899 
lemma ceiling_le_zero_eq [simp]: "(ceiling x <= 0) = (x <= 0)" 
16819  900 
by (simp add: ceiling_le_eq) 
901 

16893  902 
lemma ceiling_le_eq_one [simp]: "(ceiling x <= 1) = (x <= 1)" 
16819  903 
by (simp add: ceiling_le_eq) 
904 

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

906 
apply (subst linorder_not_le [THEN sym])+ 

907 
apply simp 

908 
apply (rule ceiling_le_eq) 

909 
done 

910 

16893  911 
lemma less_ceiling_eq_number_of [simp]: 
16819  912 
"(number_of n < ceiling x) = (number_of n < x)" 
913 
by (simp add: less_ceiling_eq) 

914 

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

916 
by (simp add: less_ceiling_eq) 

917 

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

919 
by (simp add: less_ceiling_eq) 

920 

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

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

923 
apply auto 

924 
done 

925 

16893  926 
lemma ceiling_less_eq_number_of [simp]: 
16819  927 
"(ceiling x < number_of n) = (x <= number_of n  1)" 
928 
by (simp add: ceiling_less_eq) 

929 

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

931 
by (simp add: ceiling_less_eq) 

932 

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

934 
by (simp add: ceiling_less_eq) 

935 

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

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

938 
apply auto 

939 
done 

940 

16893  941 
lemma le_ceiling_eq_number_of [simp]: 
16819  942 
"(number_of n <= ceiling x) = (number_of n  1 < x)" 
943 
by (simp add: le_ceiling_eq) 

944 

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

946 
by (simp add: le_ceiling_eq) 

947 

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

949 
by (simp add: le_ceiling_eq) 

950 

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

952 
apply (unfold ceiling_def, simp) 

953 
apply (subst real_of_int_minus [THEN sym]) 

954 
apply (subst floor_add) 

955 
apply simp 

956 
done 

957 

16893  958 
lemma ceiling_add_number_of [simp]: "ceiling (x + number_of n) = 
16819  959 
ceiling x + number_of n" 
960 
apply (subst ceiling_add [THEN sym]) 

961 
apply simp 

962 
done 

963 

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

965 
apply (subst ceiling_add [THEN sym]) 

966 
apply simp 

967 
done 

968 

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

970 
apply (subst diff_minus)+ 

971 
apply (subst real_of_int_minus [THEN sym]) 

972 
apply (rule ceiling_add) 

973 
done 

974 

16893  975 
lemma ceiling_subtract_number_of [simp]: "ceiling (x  number_of n) = 
16819  976 
ceiling x  number_of n" 
977 
apply (subst ceiling_subtract [THEN sym]) 

978 
apply simp 

979 
done 

980 

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

982 
apply (subst ceiling_subtract [THEN sym]) 

983 
apply simp 

984 
done 

985 

986 
subsection {* Versions for the natural numbers *} 

987 

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

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

991 

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

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

993 
natceiling :: "real => nat" where 
19765  994 
"natceiling x = nat(ceiling x)" 
16819  995 

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

997 
by (unfold natfloor_def, simp) 

998 

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

1000 
by (unfold natfloor_def, simp) 

1001 

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

1003 
by (unfold natfloor_def, simp) 

1004 

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

1006 
by (unfold natfloor_def, simp) 

1007 

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

1009 
by (unfold natfloor_def, simp) 

1010 

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

1012 
by (unfold natfloor_def, simp) 

1013 

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

1015 
apply (unfold natfloor_def) 

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

1017 
apply simp 

1018 
apply (erule floor_mono2) 

1019 
done 

1020 

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

1022 
apply (case_tac "0 <= x") 

1023 
apply (subst natfloor_def)+ 

1024 
apply (subst nat_le_eq_zle) 

1025 
apply force 

16893  1026 
apply (erule floor_mono2) 
16819  1027 
apply (subst natfloor_neg) 
1028 
apply simp 

1029 
apply simp 

1030 
done 

1031 

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

1033 
apply (unfold natfloor_def) 

1034 
apply (subst nat_int [THEN sym]) 

1035 
apply (subst nat_le_eq_zle) 

1036 
apply simp 

1037 
apply (rule le_floor) 

1038 
apply simp 

1039 
done 

1040 

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

1042 
apply (rule iffI) 

1043 
apply (rule order_trans) 

1044 
prefer 2 

1045 
apply (erule real_natfloor_le) 

1046 
apply (subst real_of_nat_le_iff) 

1047 
apply assumption 

1048 
apply (erule le_natfloor) 

1049 
done 

1050 

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

1054 
apply (subst le_natfloor_eq, assumption) 

1055 
apply simp 

1056 
done 

1057 

16820  1058 
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" 
16819  1059 
apply (case_tac "0 <= x") 
1060 
apply (subst le_natfloor_eq, assumption, simp) 

1061 
apply (rule iffI) 

16893  1062 
apply (subgoal_tac "natfloor x <= natfloor 0") 
16819  1063 
apply simp 
1064 
apply (rule natfloor_mono) 

1065 
apply simp 

1066 
apply simp 

1067 
done 

1068 

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

1070 
apply (unfold natfloor_def) 

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

1072 
apply (subst eq_nat_nat_iff) 

1073 
apply simp 

1074 
apply simp 

1075 
apply (rule floor_eq2) 

1076 
apply auto 

1077 
done 

1078 

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

1080 
apply (case_tac "0 <= x") 

1081 
apply (unfold natfloor_def) 

1082 
apply simp 

1083 
apply simp_all 

1084 
done 

1085 

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

1087 
apply (simp add: compare_rls) 

1088 
apply (rule real_natfloor_add_one_gt) 

1089 
done 

1090 

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

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

1093 
apply arith 

1094 
apply (rule real_natfloor_add_one_gt) 

1095 
done 

1096 

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

1098 
apply (unfold natfloor_def) 

24355  1099 
apply (subgoal_tac "real a = real (int a)") 
16819  1100 
apply (erule ssubst) 
23309  1101 
apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq) 
16819  1102 
apply simp 
1103 
done 

1104 

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

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

1109 
apply simp_all 

1110 
done 

1111 

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

1113 
apply (subst natfloor_add [THEN sym]) 

1114 
apply assumption 

1115 
apply simp 

1116 
done 

1117 

16893  1118 
lemma natfloor_subtract [simp]: "real a <= x ==> 
16819  1119 
natfloor(x  real a) = natfloor x  a" 
1120 
apply (unfold natfloor_def) 

24355  1121 
apply (subgoal_tac "real a = real (int a)") 
16819  1122 
apply (erule ssubst) 
23309  1123 
apply (simp del: real_of_int_of_nat_eq) 
16819  1124 
apply simp 
1125 
done 

1126 

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

1128 
by (unfold natceiling_def, simp) 

1129 

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

1131 
by (unfold natceiling_def, simp) 

1132 

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

1134 
by (unfold natceiling_def, simp) 

1135 

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

1137 
by (unfold natceiling_def, simp) 

1138 

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

1140 
by (unfold natceiling_def, simp) 

1141 

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

1143 
apply (unfold natceiling_def) 

1144 
apply (case_tac "x < 0") 

1145 
apply simp 

1146 
apply (subst real_nat_eq_real) 

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

1148 
apply simp 

1149 
apply (rule ceiling_mono2) 

1150 
apply simp 

1151 
apply simp 

1152 
done 

1153 

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

1155 
apply (unfold natceiling_def) 

1156 
apply simp 

1157 
done 

1158 

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

1160 
apply (case_tac "0 <= x") 

1161 
apply (subst natceiling_def)+ 

1162 
apply (subst nat_le_eq_zle) 

1163 
apply (rule disjI2) 

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

1165 
apply simp 

1166 
apply (rule order_trans) 

1167 
apply simp 

1168 
apply (erule order_trans) 

1169 
apply simp 

1170 
apply (erule ceiling_mono2) 

1171 
apply (subst natceiling_neg) 

1172 
apply simp_all 

1173 
done 

1174 

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

1176 
apply (unfold natceiling_def) 

1177 
apply (case_tac "x < 0") 

1178 
apply simp 

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

1180 
apply (subst nat_le_eq_zle) 

1181 
apply simp 

1182 
apply (rule ceiling_le) 

1183 
apply simp 

1184 
done 

1185 

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

1187 
apply (rule iffI) 

1188 
apply (rule order_trans) 

1189 
apply (rule real_natceiling_ge) 

1190 
apply (subst real_of_nat_le_iff) 

1191 
apply assumption 

1192 
apply (erule natceiling_le) 

1193 
done 

1194 

16893  1195 
lemma natceiling_le_eq_number_of [simp]: 
16820  1196 
"~ neg((number_of n)::int) ==> 0 <= x ==> 
1197 
(natceiling x <= number_of n) = (x <= number_of n)" 

16819  1198 
apply (subst natceiling_le_eq, assumption) 
1199 
apply simp 

1200 
done 

1201 

16820  1202 
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" 
16819  1203 
apply (case_tac "0 <= x") 
1204 
apply (subst natceiling_le_eq) 

1205 
apply assumption 

1206 
apply simp 

1207 
apply (subst natceiling_neg) 

1208 
apply simp 

1209 
apply simp 

1210 
done 

1211 

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

1213 
apply (unfold natceiling_def) 

19850  1214 
apply (simplesubst nat_int [THEN sym]) back back 
16819  1215 
apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") 
1216 
apply (erule ssubst) 

1217 
apply (subst eq_nat_nat_iff) 

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

1219 
apply simp 

1220 
apply (rule ceiling_mono2) 

1221 
apply force 

1222 
apply force 

1223 
apply (rule ceiling_eq2) 

1224 
apply (simp, simp) 

1225 
apply (subst nat_add_distrib) 

1226 
apply auto 

1227 
done 

1228 

16893  1229 
lemma natceiling_add [simp]: "0 <= x ==> 
16819  1230 
natceiling (x + real a) = natceiling x + a" 
1231 
apply (unfold natceiling_def) 

24355  1232 
apply (subgoal_tac "real a = real (int a)") 
16819  1233 
apply (erule ssubst) 
23309  1234 
apply (simp del: real_of_int_of_nat_eq) 
16819  1235 
apply (subst nat_add_distrib) 
1236 
apply (subgoal_tac "0 = ceiling 0") 

1237 
apply (erule ssubst) 

1238 
apply (erule ceiling_mono2) 

1239 
apply simp_all 

1240 
done 

1241 

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

16820  1244 
natceiling (x + number_of n) = natceiling x + number_of n" 
16819  1245 
apply (subst natceiling_add [THEN sym]) 
1246 
apply simp_all 

1247 
done 

1248 

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

1250 
apply (subst natceiling_add [THEN sym]) 

1251 
apply assumption 

1252 
apply simp 

1253 
done 

1254 

16893  1255 
lemma natceiling_subtract [simp]: "real a <= x ==> 
16819  1256 
natceiling(x  real a) = natceiling x  a" 
1257 
apply (unfold natceiling_def) 

24355  1258 
apply (subgoal_tac "real a = real (int a)") 
16819  1259 
apply (erule ssubst) 
23309  1260 
apply (simp del: real_of_int_of_nat_eq) 
16819  1261 
apply simp 
1262 
done 

1263 

25162  1264 
lemma natfloor_div_nat: "1 <= x ==> y > 0 ==> 
16819  1265 
natfloor (x / real y) = natfloor x div y" 
1266 
proof  

25162  1267 
assume "1 <= (x::real)" and "(y::nat) > 0" 
16819  1268 
have "natfloor x = (natfloor x) div y * y + (natfloor x) mod y" 
1269 
by simp 

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

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

1274 
by simp 

16893  1275 
then have "x = real ((natfloor x) div y) * real y + 
16819  1276 
real((natfloor x) mod y) + (x  real(natfloor x))" 
1277 
by (simp add: a) 

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

1279 
by simp 

16893  1280 
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 
16819  1281 
real y + (x  real(natfloor x)) / real y" 
23477
f4b83f03cac9
tuned and renamed group_eq_simps and ring_eq_simps
nipkow
parents:
23389
diff
changeset

1282 
by (auto simp add: ring_simps add_divide_distrib 
16819  1283 
diff_divide_distrib prems) 
1284 
finally have "natfloor (x / real y) = natfloor(...)" by simp 

16893  1285 
also have "... = natfloor(real((natfloor x) mod y) / 
16819  1286 
real y + (x  real(natfloor x)) / real y + real((natfloor x) div y))" 
1287 
by (simp add: add_ac) 

16893  1288 
also have "... = natfloor(real((natfloor x) mod y) / 
16819  1289 
real y + (x  real(natfloor x)) / real y) + (natfloor x) div y" 
1290 
apply (rule natfloor_add) 

1291 
apply (rule add_nonneg_nonneg) 

1292 
apply (rule divide_nonneg_pos) 

1293 
apply simp 

1294 
apply (simp add: prems) 

1295 
apply (rule divide_nonneg_pos) 

1296 
apply (simp add: compare_rls) 

1297 
apply (rule real_natfloor_le) 

1298 
apply (insert prems, auto) 

1299 
done 

16893  1300 
also have "natfloor(real((natfloor x) mod y) / 
16819  1301 
real y + (x  real(natfloor x)) / real y) = 0" 