src/HOL/Real/RealDef.thy
changeset 27964 1e0303048c0b
parent 27833 29151fa7c58e
child 28001 4642317e0deb
     1.1 --- a/src/HOL/Real/RealDef.thy	Sat Aug 23 19:42:17 2008 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Sat Aug 23 21:06:32 2008 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4  definition
     1.5    real_add_def [code func del]: "z + w =
     1.6         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
     1.7 -		 { Abs_Real(realrel``{(x+u, y+v)}) })"
     1.8 +                 { Abs_Real(realrel``{(x+u, y+v)}) })"
     1.9  
    1.10  definition
    1.11    real_minus_def [code func del]: "- r =  contents (\<Union>(x,y) \<in> Rep_Real(r). { Abs_Real(realrel``{(y,x)}) })"
    1.12 @@ -49,7 +49,7 @@
    1.13    real_mult_def [code func del]:
    1.14      "z * w =
    1.15         contents (\<Union>(x,y) \<in> Rep_Real(z). \<Union>(u,v) \<in> Rep_Real(w).
    1.16 -		 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    1.17 +                 { Abs_Real(realrel``{(x*u + y*v, x*v + y*u)}) })"
    1.18  
    1.19  definition
    1.20    real_inverse_def [code func del]: "inverse (R::real) = (THE S. (R = 0 & S = 0) | S * R = 1)"
    1.21 @@ -558,6 +558,8 @@
    1.22  where
    1.23    "real_of_rat \<equiv> of_rat"
    1.24  
    1.25 +definition [code func del]: "Rational = range of_rat"
    1.26 +
    1.27  consts
    1.28    (*overloaded constant for injecting other types into "real"*)
    1.29    real :: "'a => real"
    1.30 @@ -700,7 +702,54 @@
    1.31  done
    1.32  
    1.33  lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
    1.34 -  by (insert real_of_int_div2 [of n x], simp)
    1.35 +by (insert real_of_int_div2 [of n x], simp)
    1.36 +
    1.37 +
    1.38 +lemma Rational_eq_int_div_int:
    1.39 +  "Rational = { real(i::int)/real(j::int) |i j. j \<noteq> 0}" (is "_ = ?S")
    1.40 +proof
    1.41 +  show "Rational \<subseteq> ?S"
    1.42 +  proof
    1.43 +    fix x::real assume "x : Rational"
    1.44 +    then obtain r where "x = of_rat r" unfolding Rational_def ..
    1.45 +    have "of_rat r : ?S"
    1.46 +      by (cases r)(auto simp add:of_rat_rat real_eq_of_int)
    1.47 +    thus "x : ?S" using `x = of_rat r` by simp
    1.48 +  qed
    1.49 +next
    1.50 +  show "?S \<subseteq> Rational"
    1.51 +  proof(auto simp:Rational_def)
    1.52 +    fix i j :: int assume "j \<noteq> 0"
    1.53 +    hence "real i / real j = of_rat(Fract i j)"
    1.54 +      by (simp add:of_rat_rat real_eq_of_int)
    1.55 +    thus "real i / real j \<in> range of_rat" by blast
    1.56 +  qed
    1.57 +qed
    1.58 +
    1.59 +lemma Rational_eq_int_div_nat:
    1.60 +  "Rational = { real(i::int)/real(n::nat) |i n. n \<noteq> 0}"
    1.61 +proof(auto simp:Rational_eq_int_div_int)
    1.62 +  fix i j::int assume "j \<noteq> 0"
    1.63 +  show "EX (i'::int) (n::nat). real i/real j = real i'/real n \<and> 0<n"
    1.64 +  proof cases
    1.65 +    assume "j>0"
    1.66 +    hence "real i/real j = real i/real(nat j) \<and> 0<nat j"
    1.67 +      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
    1.68 +    thus ?thesis by blast
    1.69 +  next
    1.70 +    assume "~ j>0"
    1.71 +    hence "real i/real j = real(-i)/real(nat(-j)) \<and> 0<nat(-j)" using `j\<noteq>0`
    1.72 +      by (simp add: real_eq_of_int real_eq_of_nat of_nat_nat)
    1.73 +    thus ?thesis by blast
    1.74 +  qed
    1.75 +next
    1.76 +  fix i::int and n::nat assume "0 < n"
    1.77 +  moreover have "real n = real(int n)"
    1.78 +    by (simp add: real_eq_of_int real_eq_of_nat)
    1.79 +  ultimately show "\<exists>(i'::int) j::int. real i/real n = real i'/real j \<and> j \<noteq> 0"
    1.80 +    by (fastsimp)
    1.81 +qed
    1.82 +
    1.83  
    1.84  subsection{*Embedding the Naturals into the Reals*}
    1.85