equal
deleted
inserted
replaced
790 apply (rule le_less_trans [OF abs_ge_self]) |
790 apply (rule le_less_trans [OF abs_ge_self]) |
791 apply (rule less_le_trans [OF _ le_of_int_ceiling]) |
791 apply (rule less_le_trans [OF _ le_of_int_ceiling]) |
792 apply simp |
792 apply simp |
793 done |
793 done |
794 qed |
794 qed |
|
795 |
|
796 instantiation real :: floor_ceiling |
|
797 begin |
|
798 |
|
799 definition [code del]: |
|
800 "floor (x::real) = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" |
|
801 |
|
802 instance proof |
|
803 fix x :: real |
|
804 show "of_int (floor x) \<le> x \<and> x < of_int (floor x + 1)" |
|
805 unfolding floor_real_def using floor_exists1 by (rule theI') |
|
806 qed |
|
807 |
|
808 end |
795 |
809 |
796 subsection {* Completeness *} |
810 subsection {* Completeness *} |
797 |
811 |
798 lemma not_positive_Real: |
812 lemma not_positive_Real: |
799 assumes X: "cauchy X" |
813 assumes X: "cauchy X" |