summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Real/RComplete.thy

changeset 28091 | 50f2d6ba024c |

parent 27435 | b3f8e9bdf9a7 |

child 28562 | 4e74209f113e |

--- a/src/HOL/Real/RComplete.thy Tue Sep 02 20:38:17 2008 +0200 +++ b/src/HOL/Real/RComplete.thy Tue Sep 02 21:31:28 2008 +0200 @@ -430,6 +430,60 @@ done +subsection{*Density of the Rational Reals in the Reals*} + +text{* This density proof is due to Stefan Richter and was ported by TN. The +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" +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 real_diff_def 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 + ultimately show ?thesis by fast +qed + + subsection{*Floor and Ceiling Functions from the Reals to the Integers*} definition