src/HOL/Real/RComplete.thy

 apply (rename_tac n)
 apply (drule order_le_imp_less_or_eq, auto)
 apply (rule_tac x = "- n - 1" in exI)
 apply (rule_tac [2] x = "- n" in exI, auto)
 done
+
+
+subsection{*Density of the Rational Reals in the Reals*}
+
+text{* This density proof is due to Stefan Richter and was ported by TN.  The
+original source is \emph{Real Analysis} by H.L. Royden.
+It employs the Archimedean property of the reals. *}
+
+lemma Rats_dense_in_nn_real: fixes x::real
+assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
+proof -
+  from `x<y` have "0 < y-x" by simp
+  with reals_Archimedean obtain q::nat 
+    where q: "inverse (real q) < y-x" and "0 < real q" by auto  
+  def p \<equiv> "LEAST n.  y \<le> real (Suc n)/real q"  
+  from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto
+  with `0 < real q` have ex: "y \<le> real n/real q" (is "?P n")
+    by (simp add: pos_less_divide_eq[THEN sym])
+  also from assms have "\<not> y \<le> real (0::nat) / real q" by simp
+  ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"
+    by (unfold p_def) (rule Least_Suc)
+  also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)
+  ultimately have suc: "y \<le> real (Suc p) / real q" by simp
+  def r \<equiv> "real p/real q"
+  have "x = y-(y-x)" by simp
+  also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
+  also have "\<dots> = real p / real q"
+    by (simp only: inverse_eq_divide real_diff_def real_of_nat_Suc 
+    minus_divide_left add_divide_distrib[THEN sym]) simp
+  finally have "x<r" by (unfold r_def)
+  have "p<Suc p" .. also note main[THEN sym]
+  finally have "\<not> ?P p"  by (rule not_less_Least)
+  hence "r<y" by (simp add: r_def)
+  from r_def have "r \<in> \<rat>" by simp
+  with `x<r` `r<y` show ?thesis by fast
+qed
+
+theorem Rats_dense_in_real: fixes x y :: real
+assumes "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
+proof -
+  from reals_Archimedean2 obtain n::nat where "-x < real n" by auto
+  hence "0 \<le> x + real n" by arith
+  also from `x<y` have "x + real n < y + real n" by arith
+  ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"
+    by(rule Rats_dense_in_nn_real)
+  then obtain r where "r \<in> \<rat>" and r2: "x + real n < r" 
+    and r3: "r < y + real n"
+    by blast
+  have "r - real n = r + real (int n)/real (-1::int)" by simp
+  also from `r\<in>\<rat>` have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp
+  also from r2 have "x < r - real n" by arith
+  moreover from r3 have "r - real n < y" by arith
+  ultimately show ?thesis by fast
+qed
 
 
 subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
 
 definition