remove unused, unnecessary lemmas
authorhuffman
Fri Sep 02 14:27:55 2011 -0700 (2011-09-02)
changeset 44667ee5772ca7d16
parent 44666 8670a39d4420
child 44668 31d41a0f6b5d
remove unused, unnecessary lemmas
src/HOL/RComplete.thy
     1.1 --- a/src/HOL/RComplete.thy	Fri Sep 02 13:57:12 2011 -0700
     1.2 +++ b/src/HOL/RComplete.thy	Fri Sep 02 14:27:55 2011 -0700
     1.3 @@ -106,27 +106,6 @@
     1.4    unfolding real_of_nat_def using `0 < x`
     1.5    by (auto intro: ex_less_of_nat_mult)
     1.6  
     1.7 -lemma reals_Archimedean6:
     1.8 -     "0 \<le> r ==> \<exists>(n::nat). real (n - 1) \<le> r & r < real (n)"
     1.9 -unfolding real_of_nat_def
    1.10 -apply (rule exI [where x="nat (floor r + 1)"])
    1.11 -apply (insert floor_correct [of r])
    1.12 -apply (simp add: nat_add_distrib of_nat_nat)
    1.13 -done
    1.14 -
    1.15 -lemma reals_Archimedean6a: "0 \<le> r ==> \<exists>n. real (n) \<le> r & r < real (Suc n)"
    1.16 -  by (drule reals_Archimedean6) auto
    1.17 -
    1.18 -text {* TODO: delete *}
    1.19 -lemma reals_Archimedean_6b_int:
    1.20 -     "0 \<le> r ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    1.21 -  unfolding real_of_int_def by (rule floor_exists)
    1.22 -
    1.23 -text {* TODO: delete *}
    1.24 -lemma reals_Archimedean_6c_int:
    1.25 -     "r < 0 ==> \<exists>n::int. real n \<le> r & r < real (n+1)"
    1.26 -  unfolding real_of_int_def by (rule floor_exists)
    1.27 -
    1.28  
    1.29  subsection{*Density of the Rational Reals in the Reals*}
    1.30