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
```