author  huffman 
Thu, 26 Feb 2009 06:21:31 0800  
changeset 30102  799b687e4aac 
parent 30097  57df8626c23b 
child 30122  1c912a9d8200 
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)" 

29667  379 
by (simp add: algebra_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 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

383 
instance real :: archimedean_field 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

384 
proof 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

385 
fix r :: real 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

386 
obtain n :: nat where "r < real n" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

387 
using reals_Archimedean2 .. 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

388 
then have "r \<le> of_int (int n)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

389 
unfolding real_eq_of_nat by simp 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

390 
then show "\<exists>z. r \<le> of_int z" .. 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

391 
qed 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

392 

16893  393 
lemma reals_Archimedean3: 
394 
assumes x_greater_zero: "0 < x" 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

396 
unfolding real_of_nat_def using `0 < x` 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

397 
by (auto intro: ex_less_of_nat_mult) 
14365
3d4df8c166ae
replacing HOL/Real/PRat, PNat by the rational number development
paulson
parents:
9429
diff
changeset

398 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

401 
unfolding real_of_nat_def 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

402 
apply (rule exI [where x="nat (floor r + 1)"]) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

403 
apply (insert floor_correct [of r]) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

404 
apply (simp add: nat_add_distrib of_nat_nat) 
16819  405 
done 
406 

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

16893  408 
by (drule reals_Archimedean6) auto 
16819  409 

410 
lemma reals_Archimedean_6b_int: 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

412 
unfolding real_of_int_def by (rule floor_exists) 
16819  413 

414 
lemma reals_Archimedean_6c_int: 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

416 
unfolding real_of_int_def by (rule floor_exists) 
16819  417 

418 

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

419 
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

420 

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

421 
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

422 
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

423 
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

424 

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

425 
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

426 
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

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

428 
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

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

430 
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

431 
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

432 
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

433 
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

434 
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

435 
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

436 
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

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

438 
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

439 
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

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

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

442 
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

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

444 
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

445 
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

446 
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

447 
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

448 
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

449 
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

450 
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

451 
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

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

453 

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

454 
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

455 
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

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

457 
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

458 
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

459 
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

460 
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

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

462 
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

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

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

465 
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

466 
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

467 
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

468 
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

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

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

471 

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

472 

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

473 
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

474 

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

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

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

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

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

479 
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

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

481 

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

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

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

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

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

486 
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

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

488 

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

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

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

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

492 

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

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

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

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

496 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

497 
lemma floor_real_of_nat_zero: "floor (real (0::nat)) = 0" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

498 
by auto (* delete? *) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

499 

24355  500 
lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

501 
unfolding real_of_nat_def by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

502 

24355  503 
lemma floor_minus_real_of_nat [simp]: "floor ( real (n::nat)) =  int n" 
30102  504 
unfolding real_of_nat_def by (simp add: floor_minus) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

505 

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

506 
lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

507 
unfolding real_of_int_def by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

508 

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

509 
lemma floor_minus_real_of_int [simp]: "floor ( real (n::int)) =  n" 
30102  510 
unfolding real_of_int_def by (simp add: floor_minus) 
14641
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 real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

513 
unfolding real_of_int_def by (rule floor_exists) 
14641
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 lemma_floor: 
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

516 
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

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

518 
proof  
23389  519 
have "real m < real n + 1" using a1 a2 by (rule order_le_less_trans) 
520 
also have "... = real (n + 1)" by simp 

521 
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

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

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

524 

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

525 
lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

526 
unfolding real_of_int_def by (rule of_int_floor_le) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

527 

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

528 
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

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

530 

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

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

532 
"(real (floor x) = x) = (\<exists>n::int. x = real n)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

533 
using floor_real_of_int by metis 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

534 

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

535 
lemma floor_eq: "[ real n < x; x < real n + 1 ] ==> floor x = n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

536 
unfolding real_of_int_def using floor_unique [of n x] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

537 

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

538 
lemma floor_eq2: "[ real n \<le> x; x < real n + 1 ] ==> floor x = n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

539 
unfolding real_of_int_def by (rule floor_unique) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

540 

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

541 
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

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

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

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

546 

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

547 
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

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

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

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

551 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

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

553 
"floor(number_of n :: real) = (number_of n :: int)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

554 
by (rule floor_number_of) (* already declared [simp] *) 
16819  555 

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

556 
lemma real_of_int_floor_ge_diff_one [simp]: "r  1 \<le> real(floor r)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

557 
unfolding real_of_int_def using floor_correct [of r] by simp 
16819  558 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

560 
unfolding real_of_int_def using floor_correct [of r] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

561 

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

562 
lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

563 
unfolding real_of_int_def using floor_correct [of r] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

564 

16819  565 
lemma real_of_int_floor_add_one_gt [simp]: "r < real(floor r) + 1" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

566 
unfolding real_of_int_def using floor_correct [of r] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

567 

16819  568 
lemma le_floor: "real a <= x ==> a <= floor x" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

569 
unfolding real_of_int_def by (simp add: le_floor_iff) 
16819  570 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

572 
unfolding real_of_int_def by (simp add: le_floor_iff) 
16819  573 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

575 
unfolding real_of_int_def by (rule le_floor_iff) 
16819  576 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

577 
lemma le_floor_eq_number_of: 
16819  578 
"(number_of n <= floor x) = (number_of n <= x)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

579 
by (rule number_of_le_floor) (* already declared [simp] *) 
16819  580 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

581 
lemma le_floor_eq_zero: "(0 <= floor x) = (0 <= x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

582 
by (rule zero_le_floor) (* already declared [simp] *) 
16819  583 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

584 
lemma le_floor_eq_one: "(1 <= floor x) = (1 <= x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

585 
by (rule one_le_floor) (* already declared [simp] *) 
16819  586 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

588 
unfolding real_of_int_def by (rule floor_less_iff) 
16819  589 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

590 
lemma floor_less_eq_number_of: 
16819  591 
"(floor x < number_of n) = (x < number_of n)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

592 
by (rule floor_less_number_of) (* already declared [simp] *) 
16819  593 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

594 
lemma floor_less_eq_zero: "(floor x < 0) = (x < 0)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

595 
by (rule floor_less_zero) (* already declared [simp] *) 
16819  596 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

597 
lemma floor_less_eq_one: "(floor x < 1) = (x < 1)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

598 
by (rule floor_less_one) (* already declared [simp] *) 
16819  599 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

601 
unfolding real_of_int_def by (rule less_floor_iff) 
16819  602 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

603 
lemma less_floor_eq_number_of: 
16819  604 
"(number_of n < floor x) = (number_of n + 1 <= x)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

605 
by (rule number_of_less_floor) (* already declared [simp] *) 
16819  606 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

607 
lemma less_floor_eq_zero: "(0 < floor x) = (1 <= x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

608 
by (rule zero_less_floor) (* already declared [simp] *) 
16819  609 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

610 
lemma less_floor_eq_one: "(1 < floor x) = (2 <= x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

611 
by (rule one_less_floor) (* already declared [simp] *) 
16819  612 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

614 
unfolding real_of_int_def by (rule floor_le_iff) 
16819  615 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

616 
lemma floor_le_eq_number_of: 
16819  617 
"(floor x <= number_of n) = (x < number_of n + 1)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

618 
by (rule floor_le_number_of) (* already declared [simp] *) 
16819  619 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

620 
lemma floor_le_eq_zero: "(floor x <= 0) = (x < 1)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

621 
by (rule floor_le_zero) (* already declared [simp] *) 
16819  622 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

623 
lemma floor_le_eq_one: "(floor x <= 1) = (x < 2)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

624 
by (rule floor_le_one) (* already declared [simp] *) 
16819  625 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

627 
unfolding real_of_int_def by (rule floor_add_of_int) 
16819  628 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

630 
unfolding real_of_int_def by (rule floor_diff_of_int) 
16819  631 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

632 
lemma floor_subtract_number_of: "floor (x  number_of n) = 
16819  633 
floor x  number_of n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

634 
by (rule floor_diff_number_of) (* already declared [simp] *) 
16819  635 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

636 
lemma floor_subtract_one: "floor (x  1) = floor x  1" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

637 
by (rule floor_diff_one) (* already declared [simp] *) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

638 

24355  639 
lemma ceiling_real_of_nat [simp]: "ceiling (real (n::nat)) = int n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

640 
unfolding real_of_nat_def by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

641 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

642 
lemma ceiling_real_of_nat_zero: "ceiling (real (0::nat)) = 0" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

643 
by auto (* delete? *) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

644 

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

645 
lemma ceiling_floor [simp]: "ceiling (real (floor r)) = floor r" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

646 
unfolding real_of_int_def by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

647 

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

648 
lemma floor_ceiling [simp]: "floor (real (ceiling r)) = ceiling r" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

649 
unfolding real_of_int_def by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

650 

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

651 
lemma real_of_int_ceiling_ge [simp]: "r \<le> real (ceiling r)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

652 
unfolding real_of_int_def by (rule le_of_int_ceiling) 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

653 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

654 
lemma ceiling_real_of_int [simp]: "ceiling (real (n::int)) = n" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

655 
unfolding real_of_int_def by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

656 

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

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

658 
"(real (ceiling x) = x) = (\<exists>n::int. x = real n)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

659 
using ceiling_real_of_int by metis 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

660 

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

661 
lemma ceiling_eq: "[ real n < x; x < real n + 1 ] ==> ceiling x = n + 1" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

662 
unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

663 

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

664 
lemma ceiling_eq2: "[ real n < x; x \<le> real n + 1 ] ==> ceiling x = n + 1" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

665 
unfolding real_of_int_def using ceiling_unique [of "n + 1" x] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

666 

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

667 
lemma ceiling_eq3: "[ real n  1 < x; x \<le> real n ] ==> ceiling x = n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

668 
unfolding real_of_int_def using ceiling_unique [of n x] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

669 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

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

671 
"ceiling (number_of n :: real) = (number_of n)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

672 
by (rule ceiling_number_of) (* already declared [simp] *) 
16819  673 

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

674 
lemma real_of_int_ceiling_diff_one_le [simp]: "real (ceiling r)  1 \<le> r" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

675 
unfolding real_of_int_def using ceiling_correct [of r] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

676 

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

677 
lemma real_of_int_ceiling_le_add_one [simp]: "real (ceiling r) \<le> r + 1" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

678 
unfolding real_of_int_def using ceiling_correct [of r] by simp 
14641
79b7bd936264
moved Complex/NSInduct and Hyperreal/IntFloor to more appropriate
paulson
parents:
14476
diff
changeset

679 

16819  680 
lemma ceiling_le: "x <= real a ==> ceiling x <= a" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

681 
unfolding real_of_int_def by (simp add: ceiling_le_iff) 
16819  682 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

684 
unfolding real_of_int_def by (simp add: ceiling_le_iff) 
16819  685 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

687 
unfolding real_of_int_def by (rule ceiling_le_iff) 
16819  688 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

689 
lemma ceiling_le_eq_number_of: 
16819  690 
"(ceiling x <= number_of n) = (x <= number_of n)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

691 
by (rule ceiling_le_number_of) (* already declared [simp] *) 
16819  692 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

693 
lemma ceiling_le_zero_eq: "(ceiling x <= 0) = (x <= 0)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

694 
by (rule ceiling_le_zero) (* already declared [simp] *) 
16819  695 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

696 
lemma ceiling_le_eq_one: "(ceiling x <= 1) = (x <= 1)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

697 
by (rule ceiling_le_one) (* already declared [simp] *) 
16819  698 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

700 
unfolding real_of_int_def by (rule less_ceiling_iff) 
16819  701 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

702 
lemma less_ceiling_eq_number_of: 
16819  703 
"(number_of n < ceiling x) = (number_of n < x)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

704 
by (rule number_of_less_ceiling) (* already declared [simp] *) 
16819  705 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

706 
lemma less_ceiling_eq_zero: "(0 < ceiling x) = (0 < x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

707 
by (rule zero_less_ceiling) (* already declared [simp] *) 
16819  708 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

709 
lemma less_ceiling_eq_one: "(1 < ceiling x) = (1 < x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

710 
by (rule one_less_ceiling) (* already declared [simp] *) 
16819  711 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

713 
unfolding real_of_int_def by (rule ceiling_less_iff) 
16819  714 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

715 
lemma ceiling_less_eq_number_of: 
16819  716 
"(ceiling x < number_of n) = (x <= number_of n  1)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

717 
by (rule ceiling_less_number_of) (* already declared [simp] *) 
16819  718 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

719 
lemma ceiling_less_eq_zero: "(ceiling x < 0) = (x <= 1)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

720 
by (rule ceiling_less_zero) (* already declared [simp] *) 
16819  721 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

722 
lemma ceiling_less_eq_one: "(ceiling x < 1) = (x <= 0)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

723 
by (rule ceiling_less_one) (* already declared [simp] *) 
16819  724 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

726 
unfolding real_of_int_def by (rule le_ceiling_iff) 
16819  727 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

728 
lemma le_ceiling_eq_number_of: 
16819  729 
"(number_of n <= ceiling x) = (number_of n  1 < x)" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

730 
by (rule number_of_le_ceiling) (* already declared [simp] *) 
16819  731 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

732 
lemma le_ceiling_eq_zero: "(0 <= ceiling x) = (1 < x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

733 
by (rule zero_le_ceiling) (* already declared [simp] *) 
16819  734 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

735 
lemma le_ceiling_eq_one: "(1 <= ceiling x) = (0 < x)" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

736 
by (rule one_le_ceiling) (* already declared [simp] *) 
16819  737 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

739 
unfolding real_of_int_def by (rule ceiling_add_of_int) 
16819  740 

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

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

742 
unfolding real_of_int_def by (rule ceiling_diff_of_int) 
16819  743 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

744 
lemma ceiling_subtract_number_of: "ceiling (x  number_of n) = 
16819  745 
ceiling x  number_of n" 
30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

746 
by (rule ceiling_diff_number_of) (* already declared [simp] *) 
16819  747 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

748 
lemma ceiling_subtract_one: "ceiling (x  1) = ceiling x  1" 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

749 
by (rule ceiling_diff_one) (* already declared [simp] *) 
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

750 

16819  751 

752 
subsection {* Versions for the natural numbers *} 

753 

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

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

757 

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

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

759 
natceiling :: "real => nat" where 
19765  760 
"natceiling x = nat(ceiling x)" 
16819  761 

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

763 
by (unfold natfloor_def, simp) 

764 

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

766 
by (unfold natfloor_def, simp) 

767 

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

769 
by (unfold natfloor_def, simp) 

770 

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

772 
by (unfold natfloor_def, simp) 

773 

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

775 
by (unfold natfloor_def, simp) 

776 

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

778 
by (unfold natfloor_def, simp) 

779 

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

781 
apply (unfold natfloor_def) 

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

783 
apply simp 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

784 
apply (erule floor_mono) 
16819  785 
done 
786 

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

788 
apply (case_tac "0 <= x") 

789 
apply (subst natfloor_def)+ 

790 
apply (subst nat_le_eq_zle) 

791 
apply force 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

792 
apply (erule floor_mono) 
16819  793 
apply (subst natfloor_neg) 
794 
apply simp 

795 
apply simp 

796 
done 

797 

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

799 
apply (unfold natfloor_def) 

800 
apply (subst nat_int [THEN sym]) 

801 
apply (subst nat_le_eq_zle) 

802 
apply simp 

803 
apply (rule le_floor) 

804 
apply simp 

805 
done 

806 

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

808 
apply (rule iffI) 

809 
apply (rule order_trans) 

810 
prefer 2 

811 
apply (erule real_natfloor_le) 

812 
apply (subst real_of_nat_le_iff) 

813 
apply assumption 

814 
apply (erule le_natfloor) 

815 
done 

816 

16893  817 
lemma le_natfloor_eq_number_of [simp]: 
16819  818 
"~ neg((number_of n)::int) ==> 0 <= x ==> 
819 
(number_of n <= natfloor x) = (number_of n <= x)" 

820 
apply (subst le_natfloor_eq, assumption) 

821 
apply simp 

822 
done 

823 

16820  824 
lemma le_natfloor_eq_one [simp]: "(1 <= natfloor x) = (1 <= x)" 
16819  825 
apply (case_tac "0 <= x") 
826 
apply (subst le_natfloor_eq, assumption, simp) 

827 
apply (rule iffI) 

16893  828 
apply (subgoal_tac "natfloor x <= natfloor 0") 
16819  829 
apply simp 
830 
apply (rule natfloor_mono) 

831 
apply simp 

832 
apply simp 

833 
done 

834 

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

836 
apply (unfold natfloor_def) 

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

838 
apply (subst eq_nat_nat_iff) 

839 
apply simp 

840 
apply simp 

841 
apply (rule floor_eq2) 

842 
apply auto 

843 
done 

844 

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

846 
apply (case_tac "0 <= x") 

847 
apply (unfold natfloor_def) 

848 
apply simp 

849 
apply simp_all 

850 
done 

851 

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

29667  853 
using real_natfloor_add_one_gt by (simp add: algebra_simps) 
16819  854 

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

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

857 
apply arith 

858 
apply (rule real_natfloor_add_one_gt) 

859 
done 

860 

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

862 
apply (unfold natfloor_def) 

24355  863 
apply (subgoal_tac "real a = real (int a)") 
16819  864 
apply (erule ssubst) 
23309  865 
apply (simp add: nat_add_distrib del: real_of_int_of_nat_eq) 
16819  866 
apply simp 
867 
done 

868 

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

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

873 
apply simp_all 

874 
done 

875 

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

877 
apply (subst natfloor_add [THEN sym]) 

878 
apply assumption 

879 
apply simp 

880 
done 

881 

16893  882 
lemma natfloor_subtract [simp]: "real a <= x ==> 
16819  883 
natfloor(x  real a) = natfloor x  a" 
884 
apply (unfold natfloor_def) 

24355  885 
apply (subgoal_tac "real a = real (int a)") 
16819  886 
apply (erule ssubst) 
23309  887 
apply (simp del: real_of_int_of_nat_eq) 
16819  888 
apply simp 
889 
done 

890 

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

892 
by (unfold natceiling_def, simp) 

893 

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

895 
by (unfold natceiling_def, simp) 

896 

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

898 
by (unfold natceiling_def, simp) 

899 

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

901 
by (unfold natceiling_def, simp) 

902 

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

904 
by (unfold natceiling_def, simp) 

905 

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

907 
apply (unfold natceiling_def) 

908 
apply (case_tac "x < 0") 

909 
apply simp 

910 
apply (subst real_nat_eq_real) 

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

912 
apply simp 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

913 
apply (rule ceiling_mono) 
16819  914 
apply simp 
915 
apply simp 

916 
done 

917 

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

919 
apply (unfold natceiling_def) 

920 
apply simp 

921 
done 

922 

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

924 
apply (case_tac "0 <= x") 

925 
apply (subst natceiling_def)+ 

926 
apply (subst nat_le_eq_zle) 

927 
apply (rule disjI2) 

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

929 
apply simp 

930 
apply (rule order_trans) 

931 
apply simp 

932 
apply (erule order_trans) 

933 
apply simp 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

934 
apply (erule ceiling_mono) 
16819  935 
apply (subst natceiling_neg) 
936 
apply simp_all 

937 
done 

938 

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

940 
apply (unfold natceiling_def) 

941 
apply (case_tac "x < 0") 

942 
apply simp 

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

944 
apply (subst nat_le_eq_zle) 

945 
apply simp 

946 
apply (rule ceiling_le) 

947 
apply simp 

948 
done 

949 

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

951 
apply (rule iffI) 

952 
apply (rule order_trans) 

953 
apply (rule real_natceiling_ge) 

954 
apply (subst real_of_nat_le_iff) 

955 
apply assumption 

956 
apply (erule natceiling_le) 

957 
done 

958 

16893  959 
lemma natceiling_le_eq_number_of [simp]: 
16820  960 
"~ neg((number_of n)::int) ==> 0 <= x ==> 
961 
(natceiling x <= number_of n) = (x <= number_of n)" 

16819  962 
apply (subst natceiling_le_eq, assumption) 
963 
apply simp 

964 
done 

965 

16820  966 
lemma natceiling_le_eq_one: "(natceiling x <= 1) = (x <= 1)" 
16819  967 
apply (case_tac "0 <= x") 
968 
apply (subst natceiling_le_eq) 

969 
apply assumption 

970 
apply simp 

971 
apply (subst natceiling_neg) 

972 
apply simp 

973 
apply simp 

974 
done 

975 

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

977 
apply (unfold natceiling_def) 

19850  978 
apply (simplesubst nat_int [THEN sym]) back back 
16819  979 
apply (subgoal_tac "nat(int n) + 1 = nat(int n + 1)") 
980 
apply (erule ssubst) 

981 
apply (subst eq_nat_nat_iff) 

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

983 
apply simp 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

984 
apply (rule ceiling_mono) 
16819  985 
apply force 
986 
apply force 

987 
apply (rule ceiling_eq2) 

988 
apply (simp, simp) 

989 
apply (subst nat_add_distrib) 

990 
apply auto 

991 
done 

992 

16893  993 
lemma natceiling_add [simp]: "0 <= x ==> 
16819  994 
natceiling (x + real a) = natceiling x + a" 
995 
apply (unfold natceiling_def) 

24355  996 
apply (subgoal_tac "real a = real (int a)") 
16819  997 
apply (erule ssubst) 
23309  998 
apply (simp del: real_of_int_of_nat_eq) 
16819  999 
apply (subst nat_add_distrib) 
1000 
apply (subgoal_tac "0 = ceiling 0") 

1001 
apply (erule ssubst) 

30097
57df8626c23b
generalize floor/ceiling to work with real and rat; rename floor_mono2 to floor_mono
huffman
parents:
29667
diff
changeset

1002 
apply (erule ceiling_mono) 
16819  1003 
apply simp_all 
1004 
done 

1005 

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

16820  1008 
natceiling (x + number_of n) = natceiling x + number_of n" 
16819  1009 
apply (subst natceiling_add [THEN sym]) 
1010 
apply simp_all 

1011 
done 

1012 

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

1014 
apply (subst natceiling_add [THEN sym]) 

1015 
apply assumption 

1016 
apply simp 

1017 
done 

1018 

16893  1019 
lemma natceiling_subtract [simp]: "real a <= x ==> 
16819  1020 
natceiling(x  real a) = natceiling x  a" 
1021 
apply (unfold natceiling_def) 

24355  1022 
apply (subgoal_tac "real a = real (int a)") 
16819  1023 
apply (erule ssubst) 
23309  1024 
apply (simp del: real_of_int_of_nat_eq) 
16819  1025 
apply simp 
1026 
done 

1027 

25162  1028 
lemma natfloor_div_nat: "1 <= x ==> y > 0 ==> 
16819  1029 
natfloor (x / real y) = natfloor x div y" 
1030 
proof  

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

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

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

1038 
by simp 

16893  1039 
then have "x = real ((natfloor x) div y) * real y + 
16819  1040 
real((natfloor x) mod y) + (x  real(natfloor x))" 
1041 
by (simp add: a) 

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

1043 
by simp 

16893  1044 
also have "... = real((natfloor x) div y) + real((natfloor x) mod y) / 
16819  1045 
real y + (x  real(natfloor x)) / real y" 
29667  1046 
by (auto simp add: algebra_simps add_divide_distrib 
16819  1047 
diff_divide_distrib prems) 
1048 
finally have "natfloor (x / real y) = natfloor(...)" by simp 

16893  1049 
also have "... = natfloor(real((natfloor x) mod y) / 
16819  1050 
real y + (x  real(natfloor x)) / real y + real((natfloor x) div y))" 
1051 
by (simp add: add_ac) 

16893  1052 
also have "... = natfloor(real((natfloor x) mod y) / 
16819  1053 
real y + (x  real(natfloor x)) / real y) + (natfloor x) div y" 
1054 
apply (rule natfloor_add) 

1055 
apply (rule add_nonneg_nonneg) 

1056 
apply (rule divide_nonneg_pos) 

1057 
apply simp 

1058 
apply (simp add: prems) 

1059 
apply (rule divide_nonneg_pos) 

29667  1060 
apply (simp add: algebra_simps) 
16819  1061 
apply (rule real_natfloor_le) 
1062 
apply (insert prems, auto) 

1063 
done 

16893  1064 
also have "natfloor(real((natfloor x) mod y) / 
16819  1065 
real y + (x  real(natfloor x)) / real y) = 0" 
1066 
apply (rule natfloor_eq) 

1067 
apply simp 

1068 
apply (rule add_nonneg_nonneg) 

1069 
apply (rule divide_nonneg_pos) 

1070 
apply force 

1071 
apply (force simp add: prems) 

1072 
apply (rule divide_nonneg_pos) 

29667  1073 
apply (simp add: algebra_simps) 
16819  1074 
apply (rule real_natfloor_le) 
1075 
apply (auto simp add: prems) 

1076 
apply (insert prems, arith) 

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

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

1079 
apply (erule ssubst) 

1080 
apply (rule add_le_less_mono) 

29667  1081 
apply (simp add: algebra_simps) 
1082 
apply (subgoal_tac "1 + real(natfloor x mod y) = 

16819  1083 
real(natfloor x mod y + 1)") 
1084 
apply (erule ssubst) 

1085 
apply (subst real_of_nat_le_iff) 

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

1087 
apply arith 

1088 
apply (rule mod_less_divisor) 

1089 
apply auto 

29667  1090 
using real_natfloor_add_one_gt 
1091 
apply (simp add: algebra_simps) 

16819  1092 
done 
25140  1093 
finally show ?thesis by simp 
16819  1094 
qed 
1095 

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

1096 
end 