summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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;

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

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

--- 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 - 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