author nipkow Tue Sep 02 21:31:28 2008 +0200 (2008-09-02) changeset 28091 50f2d6ba024c parent 28090 29af3c712d2b child 28092 5886e9359aa8
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.
 src/HOL/Main.thy file | annotate | diff | revisions src/HOL/Real/RComplete.thy file | annotate | diff | revisions src/HOL/Real/Rational.thy file | annotate | diff | revisions src/HOL/Real/RealDef.thy file | annotate | diff | revisions
     1.1 --- a/src/HOL/Main.thy	Tue Sep 02 20:38:17 2008 +0200
1.2 +++ b/src/HOL/Main.thy	Tue Sep 02 21:31:28 2008 +0200
1.3 @@ -5,7 +5,7 @@
1.4  header {* Main HOL *}
1.5
1.6  theory Main
1.7 -imports Plain Map Presburger Recdef
1.8 +imports Plain Map Nat_Int_Bij Recdef
1.9  begin
1.10
1.11  ML {* val HOL_proofs = ! Proofterm.proofs *}

     2.1 --- a/src/HOL/Real/RComplete.thy	Tue Sep 02 20:38:17 2008 +0200
2.2 +++ b/src/HOL/Real/RComplete.thy	Tue Sep 02 21:31:28 2008 +0200
2.3 @@ -430,6 +430,60 @@
2.4  done
2.5
2.6
2.7 +subsection{*Density of the Rational Reals in the Reals*}
2.8 +
2.9 +text{* This density proof is due to Stefan Richter and was ported by TN.  The
2.10 +original source is \emph{Real Analysis} by H.L. Royden.
2.11 +It employs the Archimedean property of the reals. *}
2.12 +
2.13 +lemma Rats_dense_in_nn_real: fixes x::real
2.14 +assumes "0\<le>x" and "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
2.15 +proof -
2.16 +  from x<y have "0 < y-x" by simp
2.17 +  with reals_Archimedean obtain q::nat
2.18 +    where q: "inverse (real q) < y-x" and "0 < real q" by auto
2.19 +  def p \<equiv> "LEAST n.  y \<le> real (Suc n)/real q"
2.20 +  from reals_Archimedean2 obtain n::nat where "y * real q < real n" by auto
2.21 +  with 0 < real q have ex: "y \<le> real n/real q" (is "?P n")
2.22 +    by (simp add: pos_less_divide_eq[THEN sym])
2.23 +  also from assms have "\<not> y \<le> real (0::nat) / real q" by simp
2.24 +  ultimately have main: "(LEAST n. y \<le> real n/real q) = Suc p"
2.25 +    by (unfold p_def) (rule Least_Suc)
2.26 +  also from ex have "?P (LEAST x. ?P x)" by (rule LeastI)
2.27 +  ultimately have suc: "y \<le> real (Suc p) / real q" by simp
2.28 +  def r \<equiv> "real p/real q"
2.29 +  have "x = y-(y-x)" by simp
2.30 +  also from suc q have "\<dots> < real (Suc p)/real q - inverse (real q)" by arith
2.31 +  also have "\<dots> = real p / real q"
2.32 +    by (simp only: inverse_eq_divide real_diff_def real_of_nat_Suc
2.33 +    minus_divide_left add_divide_distrib[THEN sym]) simp
2.34 +  finally have "x<r" by (unfold r_def)
2.35 +  have "p<Suc p" .. also note main[THEN sym]
2.36 +  finally have "\<not> ?P p"  by (rule not_less_Least)
2.37 +  hence "r<y" by (simp add: r_def)
2.38 +  from r_def have "r \<in> \<rat>" by simp
2.39 +  with x<r r<y show ?thesis by fast
2.40 +qed
2.41 +
2.42 +theorem Rats_dense_in_real: fixes x y :: real
2.43 +assumes "x<y" shows "\<exists>r \<in> \<rat>.  x<r \<and> r<y"
2.44 +proof -
2.45 +  from reals_Archimedean2 obtain n::nat where "-x < real n" by auto
2.46 +  hence "0 \<le> x + real n" by arith
2.47 +  also from x<y have "x + real n < y + real n" by arith
2.48 +  ultimately have "\<exists>r \<in> \<rat>. x + real n < r \<and> r < y + real n"
2.49 +    by(rule Rats_dense_in_nn_real)
2.50 +  then obtain r where "r \<in> \<rat>" and r2: "x + real n < r"
2.51 +    and r3: "r < y + real n"
2.52 +    by blast
2.53 +  have "r - real n = r + real (int n)/real (-1::int)" by simp
2.54 +  also from r\<in>\<rat> have "r + real (int n)/real (-1::int) \<in> \<rat>" by simp
2.55 +  also from r2 have "x < r - real n" by arith
2.56 +  moreover from r3 have "r - real n < y" by arith
2.57 +  ultimately show ?thesis by fast
2.58 +qed
2.59 +
2.60 +
2.61  subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
2.62
2.63  definition

     3.1 --- a/src/HOL/Real/Rational.thy	Tue Sep 02 20:38:17 2008 +0200
3.2 +++ b/src/HOL/Real/Rational.thy	Tue Sep 02 21:31:28 2008 +0200
3.3 @@ -6,7 +6,7 @@
3.4  header {* Rational numbers *}
3.5
3.6  theory Rational
3.7 -imports "../Presburger" GCD
3.8 +imports "../Nat_Int_Bij" GCD
3.9  uses ("rat_arith.ML")
3.10  begin
3.11
3.12 @@ -791,6 +791,46 @@
3.13    by (rule Rats_cases) auto
3.14
3.15
3.16 +subsection {* The Rationals are Countably Infinite *}
3.17 +
3.18 +definition nat_to_rat_surj :: "nat \<Rightarrow> rat" where
3.19 +"nat_to_rat_surj n = (let (a,b) = nat_to_nat2 n
3.20 +                      in Fract (nat_to_int_bij a) (nat_to_int_bij b))"
3.21 +
3.22 +lemma surj_nat_to_rat_surj: "surj nat_to_rat_surj"
3.23 +unfolding surj_def
3.24 +proof
3.25 +  fix r::rat
3.26 +  show "\<exists>n. r = nat_to_rat_surj n"
3.27 +  proof(cases r)
3.28 +    fix i j assume [simp]: "r = Fract i j" and "j \<noteq> 0"
3.29 +    have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
3.30 +               in nat_to_rat_surj(nat2_to_nat (m,n)))"
3.31 +      using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]
3.32 +      by(simp add:Let_def nat_to_rat_surj_def nat_to_nat2_def)
3.33 +    thus "\<exists>n. r = nat_to_rat_surj n" by(auto simp:Let_def)
3.34 +  qed
3.35 +qed
3.36 +
3.37 +lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
3.38 +by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
3.39 +
3.40 +context field_char_0
3.41 +begin
3.42 +
3.43 +lemma Rats_eq_range_of_rat_o_nat_to_rat_surj:
3.44 +  "\<rat> = range (of_rat o nat_to_rat_surj)"
3.45 +using surj_nat_to_rat_surj
3.46 +by (auto simp: Rats_def image_def surj_def)
3.47 +   (blast intro: arg_cong[where f = of_rat])
3.48 +
3.49 +lemma surj_of_rat_nat_to_rat_surj:
3.50 +  "r\<in>\<rat> \<Longrightarrow> \<exists>n. r = of_rat(nat_to_rat_surj n)"
3.52 +
3.53 +end
3.54 +
3.55 +
3.56  subsection {* Implementation of rational numbers as pairs of integers *}
3.57
3.58  lemma Fract_norm: "Fract (a div zgcd a b) (b div zgcd a b) = Fract a b"

     4.1 --- a/src/HOL/Real/RealDef.thy	Tue Sep 02 20:38:17 2008 +0200
4.2 +++ b/src/HOL/Real/RealDef.thy	Tue Sep 02 21:31:28 2008 +0200
4.3 @@ -847,19 +847,23 @@
4.4
4.5  subsection{* Rationals *}
4.6
4.7 +lemma Rats_real_nat[simp]: "real(n::nat) \<in> \<rat>"
4.9 +
4.10 +
4.11  lemma Rats_eq_int_div_int:
4.12 -  "Rats = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
4.13 +  "\<rat> = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
4.14  proof
4.15 -  show "Rats \<subseteq> ?S"
4.16 +  show "\<rat> \<subseteq> ?S"
4.17    proof
4.18 -    fix x::real assume "x : Rats"
4.19 +    fix x::real assume "x : \<rat>"
4.20      then obtain r where "x = of_rat r" unfolding Rats_def ..
4.21      have "of_rat r : ?S"
4.22        by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
4.23      thus "x : ?S" using x = of_rat r by simp
4.24    qed
4.25  next
4.26 -  show "?S \<subseteq> Rats"
4.27 +  show "?S \<subseteq> \<rat>"
4.28    proof(auto simp:Rats_def)
4.29      fix i j :: int assume "j \<noteq> 0"
4.30      hence "real i / real j = of_rat(Fract i j)"
4.31 @@ -869,7 +873,7 @@
4.32  qed
4.33
4.34  lemma Rats_eq_int_div_nat:
4.35 -  "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
4.36 +  "\<rat> = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
4.37  proof(auto simp:Rats_eq_int_div_int)
4.38    fix i j::int assume "j \<noteq> 0"
4.39    show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"