src/HOL/Real/RealDef.thy
changeset 28001 4642317e0deb
parent 27964 1e0303048c0b
child 28091 50f2d6ba024c
     1.1 --- a/src/HOL/Real/RealDef.thy	Tue Aug 26 11:42:46 2008 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Aug 26 12:07:06 2008 +0200
     1.3 @@ -558,8 +558,6 @@
     1.4  where
     1.5    "real_of_rat \<equiv> of_rat"
     1.6  
     1.7 -definition [code func del]: "Rational = range of_rat"
     1.8 -
     1.9  consts
    1.10    (*overloaded constant for injecting other types into "real"*)
    1.11    real :: "'a => real"
    1.12 @@ -705,52 +703,6 @@
    1.13  by (insert real_of_int_div2 [of n x], simp)
    1.14  
    1.15  
    1.16 -lemma Rational_eq_int_div_int:
    1.17 -  "Rational = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
    1.18 -proof
    1.19 -  show "Rational \<subseteq> ?S"
    1.20 -  proof
    1.21 -    fix x::real assume "x : Rational"
    1.22 -    then obtain r where "x = of_rat r" unfolding Rational_def ..
    1.23 -    have "of_rat r : ?S"
    1.24 -      by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
    1.25 -    thus "x : ?S" using `x = of_rat r` by simp
    1.26 -  qed
    1.27 -next
    1.28 -  show "?S \<subseteq> Rational"
    1.29 -  proof(auto simp:Rational_def)
    1.30 -    fix i j :: int assume "j \<noteq> 0"
    1.31 -    hence "real i / real j = of_rat(Fract i j)"
    1.32 -      by (simp add:of_rat_rat real_eq_of_int)
    1.33 -    thus "real i / real j \<in> range of_rat" by blast
    1.34 -  qed
    1.35 -qed
    1.36 -
    1.37 -lemma Rational_eq_int_div_nat:
    1.38 -  "Rational = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    1.39 -proof(auto simp:Rational_eq_int_div_int)
    1.40 -  fix i j::int assume "j \<noteq> 0"
    1.41 -  show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
    1.42 -  proof cases
    1.43 -    assume "j>0"
    1.44 -    hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
    1.45 -      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
    1.46 -    thus ?thesis by blast
    1.47 -  next
    1.48 -    assume "~ j>0"
    1.49 -    hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
    1.50 -      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
    1.51 -    thus ?thesis by blast
    1.52 -  qed
    1.53 -next
    1.54 -  fix i::int and n::nat assume "0 < n"
    1.55 -  moreover have "real n = real(int n)"
    1.56 -    by (simp add: real_eq_of_int real_eq_of_nat)
    1.57 -  ultimately show "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0"
    1.58 -    by (fastsimp)
    1.59 -qed
    1.60 -
    1.61 -
    1.62  subsection{*Embedding the Naturals into the Reals*}
    1.63  
    1.64  lemma real_of_nat_zero [simp]: "real (0::nat) = 0"
    1.65 @@ -892,6 +844,91 @@
    1.66    apply (simp only: real_of_int_real_of_nat)
    1.67  done
    1.68  
    1.69 +
    1.70 +subsection{* Rationals *}
    1.71 +
    1.72 +lemma Rats_eq_int_div_int:
    1.73 +  "Rats = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
    1.74 +proof
    1.75 +  show "Rats \<subseteq> ?S"
    1.76 +  proof
    1.77 +    fix x::real assume "x : Rats"
    1.78 +    then obtain r where "x = of_rat r" unfolding Rats_def ..
    1.79 +    have "of_rat r : ?S"
    1.80 +      by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
    1.81 +    thus "x : ?S" using `x = of_rat r` by simp
    1.82 +  qed
    1.83 +next
    1.84 +  show "?S \<subseteq> Rats"
    1.85 +  proof(auto simp:Rats_def)
    1.86 +    fix i j :: int assume "j \<noteq> 0"
    1.87 +    hence "real i / real j = of_rat(Fract i j)"
    1.88 +      by (simp add:of_rat_rat real_eq_of_int)
    1.89 +    thus "real i / real j \<in> range of_rat" by blast
    1.90 +  qed
    1.91 +qed
    1.92 +
    1.93 +lemma Rats_eq_int_div_nat:
    1.94 +  "Rats = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    1.95 +proof(auto simp:Rats_eq_int_div_int)
    1.96 +  fix i j::int assume "j \<noteq> 0"
    1.97 +  show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
    1.98 +  proof cases
    1.99 +    assume "j>0"
   1.100 +    hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
   1.101 +      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
   1.102 +    thus ?thesis by blast
   1.103 +  next
   1.104 +    assume "~ j>0"
   1.105 +    hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
   1.106 +      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
   1.107 +    thus ?thesis by blast
   1.108 +  qed
   1.109 +next
   1.110 +  fix i::int and n::nat assume "0 < n"
   1.111 +  hence "real i/real n = real i/real(int n) \<and> int n \<noteq> 0" by simp
   1.112 +  thus "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0" by blast
   1.113 +qed
   1.114 +
   1.115 +lemma Rats_abs_nat_div_natE:
   1.116 +  assumes "x \<in> \<rat>"
   1.117 +  obtains m n where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
   1.118 +proof -
   1.119 +  from `x \<in> \<rat>` obtain i::int and n::nat where "n \<noteq> 0" and "x = real i / real n"
   1.120 +    by(auto simp add: Rats_eq_int_div_nat)
   1.121 +  hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by simp
   1.122 +  then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
   1.123 +  let ?gcd = "gcd m n"
   1.124 +  from `n\<noteq>0` have gcd: "?gcd \<noteq> 0" by (simp add: gcd_zero)
   1.125 +  let ?k = "m div ?gcd"
   1.126 +  let ?l = "n div ?gcd"
   1.127 +  let ?gcd' = "gcd ?k ?l"
   1.128 +  have "?gcd dvd m" .. then have gcd_k: "?gcd * ?k = m"
   1.129 +    by (rule dvd_mult_div_cancel)
   1.130 +  have "?gcd dvd n" .. then have gcd_l: "?gcd * ?l = n"
   1.131 +    by (rule dvd_mult_div_cancel)
   1.132 +  from `n\<noteq>0` and gcd_l have "?l \<noteq> 0" by (auto iff del: neq0_conv)
   1.133 +  moreover
   1.134 +  have "\<bar>x\<bar> = real ?k / real ?l"
   1.135 +  proof -
   1.136 +    from gcd have "real ?k / real ?l =
   1.137 +        real (?gcd * ?k) / real (?gcd * ?l)" by simp
   1.138 +    also from gcd_k and gcd_l have "\<dots> = real m / real n" by simp
   1.139 +    also from x_rat have "\<dots> = \<bar>x\<bar>" ..
   1.140 +    finally show ?thesis ..
   1.141 +  qed
   1.142 +  moreover
   1.143 +  have "?gcd' = 1"
   1.144 +  proof -
   1.145 +    have "?gcd * ?gcd' = gcd (?gcd * ?k) (?gcd * ?l)"
   1.146 +      by (rule gcd_mult_distrib2)
   1.147 +    with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
   1.148 +    with gcd show ?thesis by simp
   1.149 +  qed
   1.150 +  ultimately show ?thesis ..
   1.151 +qed
   1.152 +
   1.153 +
   1.154  subsection{*Numerals and Arithmetic*}
   1.155  
   1.156  instantiation real :: number_ring