352 lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" |
352 lemma real_of_int_floor_le [simp]: "real (floor r) \<le> r" |
353 apply (simp add: floor_def Least_def) |
353 apply (simp add: floor_def Least_def) |
354 apply (insert real_lb_ub_int [of r], safe) |
354 apply (insert real_lb_ub_int [of r], safe) |
355 apply (rule theI2) |
355 apply (rule theI2) |
356 apply auto |
356 apply auto |
357 apply (subst int_le_real_less, simp) |
|
358 apply (drule_tac x = n in spec) |
|
359 apply auto |
|
360 apply (subgoal_tac "n <= x") |
|
361 apply simp |
|
362 apply (subst int_le_real_less, simp) |
|
363 done |
357 done |
364 |
358 |
365 lemma floor_mono: "x < y ==> floor x \<le> floor y" |
359 lemma floor_mono: "x < y ==> floor x \<le> floor y" |
366 apply (simp add: floor_def Least_def) |
360 apply (simp add: floor_def Least_def) |
367 apply (insert real_lb_ub_int [of x]) |
361 apply (insert real_lb_ub_int [of x]) |
383 "(real (floor x) = x) = (\<exists>n::int. x = real n)" |
377 "(real (floor x) = x) = (\<exists>n::int. x = real n)" |
384 apply (simp add: floor_def Least_def) |
378 apply (simp add: floor_def Least_def) |
385 apply (insert real_lb_ub_int [of x], erule exE) |
379 apply (insert real_lb_ub_int [of x], erule exE) |
386 apply (rule theI2) |
380 apply (rule theI2) |
387 apply (auto intro: lemma_floor) |
381 apply (auto intro: lemma_floor) |
388 apply (auto simp add: order_eq_iff int_le_real_less) |
|
389 done |
382 done |
390 |
383 |
391 lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" |
384 lemma floor_eq: "[| real n < x; x < real n + 1 |] ==> floor x = n" |
392 apply (simp add: floor_def) |
385 apply (simp add: floor_def) |
393 apply (rule Least_equality) |
386 apply (rule Least_equality) |
427 lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)" |
420 lemma real_of_int_floor_ge_diff_one [simp]: "r - 1 \<le> real(floor r)" |
428 apply (simp add: floor_def Least_def) |
421 apply (simp add: floor_def Least_def) |
429 apply (insert real_lb_ub_int [of r], safe) |
422 apply (insert real_lb_ub_int [of r], safe) |
430 apply (rule theI2) |
423 apply (rule theI2) |
431 apply (auto intro: lemma_floor) |
424 apply (auto intro: lemma_floor) |
432 apply (auto simp add: order_eq_iff int_le_real_less) |
|
433 done |
425 done |
434 |
426 |
435 lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)" |
427 lemma real_of_int_floor_gt_diff_one [simp]: "r - 1 < real(floor r)" |
436 apply (simp add: floor_def Least_def) |
428 apply (simp add: floor_def Least_def) |
437 apply (insert real_lb_ub_int [of r], safe) |
429 apply (insert real_lb_ub_int [of r], safe) |
438 apply (rule theI2) |
430 apply (rule theI2) |
439 apply (auto intro: lemma_floor) |
431 apply (auto intro: lemma_floor) |
440 apply (auto simp add: order_eq_iff int_le_real_less) |
|
441 done |
432 done |
442 |
433 |
443 lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" |
434 lemma real_of_int_floor_add_one_ge [simp]: "r \<le> real(floor r) + 1" |
444 apply (insert real_of_int_floor_ge_diff_one [of r]) |
435 apply (insert real_of_int_floor_ge_diff_one [of r]) |
445 apply (auto simp del: real_of_int_floor_ge_diff_one) |
436 apply (auto simp del: real_of_int_floor_ge_diff_one) |