simplify proof of Rats_dense_in_real;
authorhuffman
Fri Sep 02 15:19:59 2011 -0700 (2011-09-02)
changeset 4466831d41a0f6b5d
parent 44667 ee5772ca7d16
child 44669 8e6cdb9c00a7
simplify proof of Rats_dense_in_real;
remove lemma Rats_dense_in_nn_real;
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/RComplete.thy
     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.9  
    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.6  
     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
    2.69