# HG changeset patch
# User huffman
# Date 1315001999 25200
# Node ID 31d41a0f6b5d09cc362b341e2eeb282f4a699cdb
# Parent  ee5772ca7d163f3fb7d80e0539cc082d40338530
simplify proof of Rats_dense_in_real;
remove lemma Rats_dense_in_nn_real;

diff -r ee5772ca7d16 -r 31d41a0f6b5d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 02 14:27:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 02 15:19:59 2011 -0700
@@ -914,7 +914,7 @@
 lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
         (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
 unfolding eventually_within
-by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl) 
+by auto (metis dense order_le_less_trans)
 
 lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
   unfolding trivial_limit_def
diff -r ee5772ca7d16 -r 31d41a0f6b5d src/HOL/RComplete.thy
--- a/src/HOL/RComplete.thy	Fri Sep 02 14:27:55 2011 -0700
+++ b/src/HOL/RComplete.thy	Fri Sep 02 15:19:59 2011 -0700
@@ -113,50 +113,25 @@
 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"
+lemma Rats_dense_in_real:
+  fixes x :: real
+  assumes "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 diff_minus 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
+    where q: "inverse (real q) < y-x" and "0 < q" by auto
+  def p \<equiv> "ceiling (y * real q) - 1"
+  def r \<equiv> "of_int p / real q"
+  from q have "x < y - inverse (real q)" by simp
+  also have "y - inverse (real q) \<le> r"
+    unfolding r_def p_def
+    by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling `0 < q`)
+  finally have "x < r" .
+  moreover have "r < y"
+    unfolding r_def p_def
+    by (simp add: divide_less_eq diff_less_eq `0 < q`
+      less_ceiling_iff [symmetric])
+  moreover from r_def have "r \<in> \<rat>" by simp
   ultimately show ?thesis by fast
 qed