author huffman Fri Sep 02 15:19:59 2011 -0700 (2011-09-02) changeset 44668 31d41a0f6b5d parent 44667 ee5772ca7d16 child 44669 8e6cdb9c00a7
simplify proof of Rats_dense_in_real;
remove lemma Rats_dense_in_nn_real;
1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 02 14:27:55 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Sep 02 15:19:59 2011 -0700
1.3 @@ -914,7 +914,7 @@
1.4  lemma eventually_within_le: "eventually P (at a within S) \<longleftrightarrow>
1.5          (\<exists>d>0. \<forall>x\<in>S. 0 < dist x a \<and> dist x a <= d \<longrightarrow> P x)" (is "?lhs = ?rhs")
1.6  unfolding eventually_within
1.7 -by auto (metis Rats_dense_in_nn_real order_le_less_trans order_refl)
1.8 +by auto (metis dense order_le_less_trans)
1.10  lemma eventually_happens: "eventually P net ==> trivial_limit net \<or> (\<exists>x. P x)"
1.11    unfolding trivial_limit_def
2.1 --- a/src/HOL/RComplete.thy	Fri Sep 02 14:27:55 2011 -0700
2.2 +++ b/src/HOL/RComplete.thy	Fri Sep 02 15:19:59 2011 -0700
2.3 @@ -113,50 +113,25 @@
2.4  original source is \emph{Real Analysis} by H.L. Royden.
2.5  It employs the Archimedean property of the reals. *}
2.7 -lemma Rats_dense_in_nn_real: fixes x::real
2.8 -assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
2.9 +lemma Rats_dense_in_real:
2.10 +  fixes x :: real
2.11 +  assumes "x < y" shows "\<exists>r\<in>\<rat>. x < r \<and> r < y"
2.12  proof -
2.13    from x<y have "0 < y-x" by simp
2.14    with reals_Archimedean obtain q::nat
2.15 -    where q: "inverse (real q) < y-x" and "0 < real q" by auto
2.16 -  def p \<equiv> "LEAST n.  y \<le> real (Suc n)/real q"
2.17 -  from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto
2.18 -  with 0 < real q have ex: "y \<le> real n/real q" (is "?P n")
2.19 -    by (simp add: pos_less_divide_eq[THEN sym])
2.20 -  also from assms have "\<not> y \<le> real (0::nat) / real q" by simp
2.21 -  ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"
2.22 -    by (unfold p_def) (rule Least_Suc)
2.23 -  also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)
2.24 -  ultimately have suc: "y \<le> real (Suc p) / real q" by simp
2.25 -  def r \<equiv> "real p/real q"
2.26 -  have "x = y-(y-x)" by simp
2.27 -  also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
2.28 -  also have "\<dots> = real p / real q"
2.29 -    by (simp only: inverse_eq_divide diff_minus real_of_nat_Suc
2.30 -    minus_divide_left add_divide_distrib[THEN sym]) simp
2.31 -  finally have "x<r" by (unfold r_def)
2.32 -  have "p<Suc p" .. also note main[THEN sym]
2.33 -  finally have "\<not> ?P p"  by (rule not_less_Least)
2.34 -  hence "r<y" by (simp add: r_def)
2.35 -  from r_def have "r \<in> \<rat>" by simp
2.36 -  with x<r r<y show ?thesis by fast
2.37 -qed
2.38 -
2.39 -theorem Rats_dense_in_real: fixes x y :: real
2.40 -assumes "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
2.41 -proof -
2.42 -  from reals_Archimedean2 obtain n::nat where "-x < real n" by auto
2.43 -  hence "0 \<le> x + real n" by arith
2.44 -  also from x<y have "x + real n < y + real n" by arith
2.45 -  ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"
2.46 -    by(rule Rats_dense_in_nn_real)
2.47 -  then obtain r where "r \<in> \<rat>" and r2: "x + real n < r"
2.48 -    and r3: "r < y + real n"
2.49 -    by blast
2.50 -  have "r - real n = r + real (int n)/real (-1::int)" by simp
2.51 -  also from r\<in>\<rat> have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp
2.52 -  also from r2 have "x < r - real n" by arith
2.53 -  moreover from r3 have "r - real n < y" by arith
2.54 +    where q: "inverse (real q) < y-x" and "0 < q" by auto
2.55 +  def p \<equiv> "ceiling (y * real q) - 1"
2.56 +  def r \<equiv> "of_int p / real q"
2.57 +  from q have "x < y - inverse (real q)" by simp
2.58 +  also have "y - inverse (real q) \<le> r"
2.59 +    unfolding r_def p_def
2.60 +    by (simp add: le_divide_eq left_diff_distrib le_of_int_ceiling 0 < q)
2.61 +  finally have "x < r" .
2.62 +  moreover have "r < y"
2.63 +    unfolding r_def p_def
2.64 +    by (simp add: divide_less_eq diff_less_eq 0 < q
2.65 +      less_ceiling_iff [symmetric])
2.66 +  moreover from r_def have "r \<in> \<rat>" by simp
2.67    ultimately show ?thesis by fast
2.68  qed