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;

remove lemma Rats_dense_in_nn_real;

src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy | file | annotate | diff | revisions | |

src/HOL/RComplete.thy | file | annotate | diff | revisions |

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