author huffman Fri, 02 Sep 2011 15:19:59 -0700 changeset 44668 31d41a0f6b5d parent 44667 ee5772ca7d16 child 44669 8e6cdb9c00a7
simplify proof of Rats_dense_in_real; remove lemma Rats_dense_in_nn_real;
--- 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
--- 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
-  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