equal
deleted
inserted
replaced
499 |
499 |
500 lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" |
500 lemma floor_real_of_nat [simp]: "floor (real (n::nat)) = int n" |
501 unfolding real_of_nat_def by simp |
501 unfolding real_of_nat_def by simp |
502 |
502 |
503 lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" |
503 lemma floor_minus_real_of_nat [simp]: "floor (- real (n::nat)) = - int n" |
504 unfolding real_of_nat_def by simp |
504 unfolding real_of_nat_def by (simp add: floor_minus) |
505 |
505 |
506 lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" |
506 lemma floor_real_of_int [simp]: "floor (real (n::int)) = n" |
507 unfolding real_of_int_def by simp |
507 unfolding real_of_int_def by simp |
508 |
508 |
509 lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" |
509 lemma floor_minus_real_of_int [simp]: "floor (- real (n::int)) = - n" |
510 unfolding real_of_int_def by simp |
510 unfolding real_of_int_def by (simp add: floor_minus) |
511 |
511 |
512 lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" |
512 lemma real_lb_ub_int: " \<exists>n::int. real n \<le> r & r < real (n+1)" |
513 unfolding real_of_int_def by (rule floor_exists) |
513 unfolding real_of_int_def by (rule floor_exists) |
514 |
514 |
515 lemma lemma_floor: |
515 lemma lemma_floor: |