Streamlined parts of Complex/ex/DenumRat and AFP/Integration/Rats and
authornipkow
Tue Sep 02 21:31:28 2008 +0200 (2008-09-02)
changeset 2809150f2d6ba024c
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
src/HOL/Real/RComplete.thy
src/HOL/Real/Rational.thy
src/HOL/Real/RealDef.thy
     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.51 +by(simp add: Rats_eq_range_of_rat_o_nat_to_rat_surj image_def)
    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.8 +by (simp add: real_eq_of_nat)
     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"