1.1 --- a/src/HOL/Real/Rational.thy	Tue Aug 26 23:49:46 2008 +0200
     1.2 +++ b/src/HOL/Real/Rational.thy	Wed Aug 27 01:27:33 2008 +0200
     1.3 @@ -673,6 +673,7 @@
     1.4  where
     1.5    "rat_of_int \<equiv> of_int"
     1.6  
     1.7 +subsection {* The Set of Rational Numbers *}
     1.8  
     1.9  context field_char_0
    1.10  begin
    1.11 @@ -686,6 +687,109 @@
    1.12  
    1.13  end
    1.14  
    1.15 +lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
    1.16 +by (simp add: Rats_def)
    1.17 +
    1.18 +lemma Rats_of_int [simp]: "of_int z \<in> Rats"
    1.19 +by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
    1.20 +
    1.21 +lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
    1.22 +by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
    1.23 +
    1.24 +lemma Rats_number_of [simp]:
    1.25 +  "(number_of w::'a::{number_ring,field_char_0}) \<in> Rats"
    1.26 +by (subst of_rat_number_of_eq [symmetric], rule Rats_of_rat)
    1.27 +
    1.28 +lemma Rats_0 [simp]: "0 \<in> Rats"
    1.29 +apply (unfold Rats_def)
    1.30 +apply (rule range_eqI)
    1.31 +apply (rule of_rat_0 [symmetric])
    1.32 +done
    1.33 +
    1.34 +lemma Rats_1 [simp]: "1 \<in> Rats"
    1.35 +apply (unfold Rats_def)
    1.36 +apply (rule range_eqI)
    1.37 +apply (rule of_rat_1 [symmetric])
    1.38 +done
    1.39 +
    1.40 +lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
    1.41 +apply (auto simp add: Rats_def)
    1.42 +apply (rule range_eqI)
    1.43 +apply (rule of_rat_add [symmetric])
    1.44 +done
    1.45 +
    1.46 +lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
    1.47 +apply (auto simp add: Rats_def)
    1.48 +apply (rule range_eqI)
    1.49 +apply (rule of_rat_minus [symmetric])
    1.50 +done
    1.51 +
    1.52 +lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
    1.53 +apply (auto simp add: Rats_def)
    1.54 +apply (rule range_eqI)
    1.55 +apply (rule of_rat_diff [symmetric])
    1.56 +done
    1.57 +
    1.58 +lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
    1.59 +apply (auto simp add: Rats_def)
    1.60 +apply (rule range_eqI)
    1.61 +apply (rule of_rat_mult [symmetric])
    1.62 +done
    1.63 +
    1.64 +lemma nonzero_Rats_inverse:
    1.65 +  fixes a :: "'a::field_char_0"
    1.66 +  shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
    1.67 +apply (auto simp add: Rats_def)
    1.68 +apply (rule range_eqI)
    1.69 +apply (erule nonzero_of_rat_inverse [symmetric])
    1.70 +done
    1.71 +
    1.72 +lemma Rats_inverse [simp]:
    1.73 +  fixes a :: "'a::{field_char_0,division_by_zero}"
    1.74 +  shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
    1.75 +apply (auto simp add: Rats_def)
    1.76 +apply (rule range_eqI)
    1.77 +apply (rule of_rat_inverse [symmetric])
    1.78 +done
    1.79 +
    1.80 +lemma nonzero_Rats_divide:
    1.81 +  fixes a b :: "'a::field_char_0"
    1.82 +  shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
    1.83 +apply (auto simp add: Rats_def)
    1.84 +apply (rule range_eqI)
    1.85 +apply (erule nonzero_of_rat_divide [symmetric])
    1.86 +done
    1.87 +
    1.88 +lemma Rats_divide [simp]:
    1.89 +  fixes a b :: "'a::{field_char_0,division_by_zero}"
    1.90 +  shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
    1.91 +apply (auto simp add: Rats_def)
    1.92 +apply (rule range_eqI)
    1.93 +apply (rule of_rat_divide [symmetric])
    1.94 +done
    1.95 +
    1.96 +lemma Rats_power [simp]:
    1.97 +  fixes a :: "'a::{field_char_0,recpower}"
    1.98 +  shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
    1.99 +apply (auto simp add: Rats_def)
   1.100 +apply (rule range_eqI)
   1.101 +apply (rule of_rat_power [symmetric])
   1.102 +done
   1.103 +
   1.104 +lemma Rats_cases [cases set: Rats]:
   1.105 +  assumes "q \<in> \<rat>"
   1.106 +  obtains (of_rat) r where "q = of_rat r"
   1.107 +  unfolding Rats_def
   1.108 +proof -
   1.109 +  from `q \<in> \<rat>` have "q \<in> range of_rat" unfolding Rats_def .
   1.110 +  then obtain r where "q = of_rat r" ..
   1.111 +  then show thesis ..
   1.112 +qed
   1.113 +
   1.114 +lemma Rats_induct [case_names of_rat, induct set: Rats]:
   1.115 +  "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
   1.116 +  by (rule Rats_cases) auto
   1.117 +
   1.118  
   1.119  subsection {* Implementation of rational numbers as pairs of integers *}
   1.120