# HG changeset patch
# User nipkow
# Date 1220383888 -7200
# Node ID 50f2d6ba024c494b569150d64e6c7e1b999dc5e4
# Parent  29af3c712d2b7b26b99225c2cc4b126d55f7aa3f
Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
distributed them over Real/ (to do with bijections and density).
Library/NatPair became Nat_Int_Bij and made that part of Main.

diff -r 29af3c712d2b -r 50f2d6ba024c src/HOL/Main.thy
--- a/src/HOL/Main.thy	Tue Sep 02 20:38:17 2008 +0200
+++ b/src/HOL/Main.thy	Tue Sep 02 21:31:28 2008 +0200
@@ -5,7 +5,7 @@
 header {* Main HOL *}
 
 theory Main
-imports Plain Map Presburger Recdef
+imports Plain Map Nat_Int_Bij Recdef
 begin
 
 ML {* val HOL_proofs = ! Proofterm.proofs *}
diff -r 29af3c712d2b -r 50f2d6ba024c src/HOL/Real/RComplete.thy
--- 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
diff -r 29af3c712d2b -r 50f2d6ba024c src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Tue Sep 02 20:38:17 2008 +0200
+++ b/src/HOL/Real/Rational.thy	Tue Sep 02 21:31:28 2008 +0200
@@ -6,7 +6,7 @@
 header {* Rational numbers *}
 
 theory Rational
-imports "../Presburger" GCD
+imports "../Nat_Int_Bij" GCD
 uses ("rat_arith.ML")
 begin
 
@@ -791,6 +791,46 @@
   by (rule Rats_cases) auto
 
 
+subsection {* The Rationals are Countably Infinite *}
+
+definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
+"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
+                      in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
+
+lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
+unfolding surj_def
+proof
+  fix r::rat
+  show "\<exists>n. r = nat_to_rat_surj n"
+  proof(cases r)
+    fix i j assume [simp]: "r = Fract i j" and "j \<noteq> 0"
+    have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
+               in nat_to_rat_surj(nat2_to_nat (m,n)))"
+      using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
+      by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
+    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
+  qed
+qed
+
+lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
+by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
+
+context field_char_0
+begin
+
+lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
+  "\<rat> = range (of_rat o nat_to_rat_surj)"
+using surj_nat_to_rat_surj
+by (auto simp: Rats_def image_def surj_def)
+   (blast intro: arg_cong[where f = of_rat])
+
+lemma surj_of_rat_nat_to_rat_surj:
+  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
+by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
+
+end
+
+
 subsection {* Implementation of rational numbers as pairs of integers *}
 
 lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"
diff -r 29af3c712d2b -r 50f2d6ba024c src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Tue Sep 02 20:38:17 2008 +0200
+++ b/src/HOL/Real/RealDef.thy	Tue Sep 02 21:31:28 2008 +0200
@@ -847,19 +847,23 @@
 
 subsection{* Rationals *}
 
+lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
+by (simp add: real_eq_of_nat)
+
+
 lemma Rats_eq_int_div_int:
-  "Rats = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
+  "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
 proof
-  show "Rats \<subseteq> ?S"
+  show "\<rat> \<subseteq> ?S"
   proof
-    fix x::real assume "x : Rats"
+    fix x::real assume "x : \<rat>"
     then obtain r where "x = of_rat r" unfolding Rats_def ..
     have "of_rat r : ?S"
       by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
     thus "x : ?S" using `x = of_rat r` by simp
   qed
 next
-  show "?S \<subseteq> Rats"
+  show "?S \<subseteq> \<rat>"
   proof(auto simp:Rats_def)
     fix i j :: int assume "j \<noteq> 0"
     hence "real i / real j = of_rat(Fract i j)"
@@ -869,7 +873,7 @@
 qed
 
 lemma Rats_eq_int_div_nat:
-  "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
+  "\<rat> = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
 proof(auto simp:Rats_eq_int_div_int)
   fix i j::int assume "j \<noteq> 0"
   show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"