src/HOL/Rat.thy
changeset 61070 b72a990adfe2
parent 60758 d8d85a8172b5
child 61144 5e94dfead1c2
     1.1 --- a/src/HOL/Rat.thy	Mon Aug 31 21:01:21 2015 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon Aug 31 21:28:08 2015 +0200
     1.3 @@ -808,58 +808,54 @@
     1.4  context field_char_0
     1.5  begin
     1.6  
     1.7 -definition
     1.8 -  Rats  :: "'a set" where
     1.9 -  "Rats = range of_rat"
    1.10 -
    1.11 -notation (xsymbols)
    1.12 -  Rats  ("\<rat>")
    1.13 +definition Rats :: "'a set" ("\<rat>")
    1.14 +  where "\<rat> = range of_rat"
    1.15  
    1.16  end
    1.17  
    1.18 -lemma Rats_of_rat [simp]: "of_rat r \<in> Rats"
    1.19 +lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
    1.20  by (simp add: Rats_def)
    1.21  
    1.22 -lemma Rats_of_int [simp]: "of_int z \<in> Rats"
    1.23 +lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
    1.24  by (subst of_rat_of_int_eq [symmetric], rule Rats_of_rat)
    1.25  
    1.26 -lemma Rats_of_nat [simp]: "of_nat n \<in> Rats"
    1.27 +lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
    1.28  by (subst of_rat_of_nat_eq [symmetric], rule Rats_of_rat)
    1.29  
    1.30 -lemma Rats_number_of [simp]: "numeral w \<in> Rats"
    1.31 +lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
    1.32  by (subst of_rat_numeral_eq [symmetric], rule Rats_of_rat)
    1.33  
    1.34 -lemma Rats_0 [simp]: "0 \<in> Rats"
    1.35 +lemma Rats_0 [simp]: "0 \<in> \<rat>"
    1.36  apply (unfold Rats_def)
    1.37  apply (rule range_eqI)
    1.38  apply (rule of_rat_0 [symmetric])
    1.39  done
    1.40  
    1.41 -lemma Rats_1 [simp]: "1 \<in> Rats"
    1.42 +lemma Rats_1 [simp]: "1 \<in> \<rat>"
    1.43  apply (unfold Rats_def)
    1.44  apply (rule range_eqI)
    1.45  apply (rule of_rat_1 [symmetric])
    1.46  done
    1.47  
    1.48 -lemma Rats_add [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a + b \<in> Rats"
    1.49 +lemma Rats_add [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a + b \<in> \<rat>"
    1.50  apply (auto simp add: Rats_def)
    1.51  apply (rule range_eqI)
    1.52  apply (rule of_rat_add [symmetric])
    1.53  done
    1.54  
    1.55 -lemma Rats_minus [simp]: "a \<in> Rats \<Longrightarrow> - a \<in> Rats"
    1.56 +lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
    1.57  apply (auto simp add: Rats_def)
    1.58  apply (rule range_eqI)
    1.59  apply (rule of_rat_minus [symmetric])
    1.60  done
    1.61  
    1.62 -lemma Rats_diff [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a - b \<in> Rats"
    1.63 +lemma Rats_diff [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a - b \<in> \<rat>"
    1.64  apply (auto simp add: Rats_def)
    1.65  apply (rule range_eqI)
    1.66  apply (rule of_rat_diff [symmetric])
    1.67  done
    1.68  
    1.69 -lemma Rats_mult [simp]: "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a * b \<in> Rats"
    1.70 +lemma Rats_mult [simp]: "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a * b \<in> \<rat>"
    1.71  apply (auto simp add: Rats_def)
    1.72  apply (rule range_eqI)
    1.73  apply (rule of_rat_mult [symmetric])
    1.74 @@ -867,7 +863,7 @@
    1.75  
    1.76  lemma nonzero_Rats_inverse:
    1.77    fixes a :: "'a::field_char_0"
    1.78 -  shows "\<lbrakk>a \<in> Rats; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> Rats"
    1.79 +  shows "\<lbrakk>a \<in> \<rat>; a \<noteq> 0\<rbrakk> \<Longrightarrow> inverse a \<in> \<rat>"
    1.80  apply (auto simp add: Rats_def)
    1.81  apply (rule range_eqI)
    1.82  apply (erule nonzero_of_rat_inverse [symmetric])
    1.83 @@ -875,7 +871,7 @@
    1.84  
    1.85  lemma Rats_inverse [simp]:
    1.86    fixes a :: "'a::{field_char_0, field}"
    1.87 -  shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
    1.88 +  shows "a \<in> \<rat> \<Longrightarrow> inverse a \<in> \<rat>"
    1.89  apply (auto simp add: Rats_def)
    1.90  apply (rule range_eqI)
    1.91  apply (rule of_rat_inverse [symmetric])
    1.92 @@ -883,7 +879,7 @@
    1.93  
    1.94  lemma nonzero_Rats_divide:
    1.95    fixes a b :: "'a::field_char_0"
    1.96 -  shows "\<lbrakk>a \<in> Rats; b \<in> Rats; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
    1.97 +  shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>; b \<noteq> 0\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
    1.98  apply (auto simp add: Rats_def)
    1.99  apply (rule range_eqI)
   1.100  apply (erule nonzero_of_rat_divide [symmetric])
   1.101 @@ -891,7 +887,7 @@
   1.102  
   1.103  lemma Rats_divide [simp]:
   1.104    fixes a b :: "'a::{field_char_0, field}"
   1.105 -  shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
   1.106 +  shows "\<lbrakk>a \<in> \<rat>; b \<in> \<rat>\<rbrakk> \<Longrightarrow> a / b \<in> \<rat>"
   1.107  apply (auto simp add: Rats_def)
   1.108  apply (rule range_eqI)
   1.109  apply (rule of_rat_divide [symmetric])
   1.110 @@ -899,7 +895,7 @@
   1.111  
   1.112  lemma Rats_power [simp]:
   1.113    fixes a :: "'a::field_char_0"
   1.114 -  shows "a \<in> Rats \<Longrightarrow> a ^ n \<in> Rats"
   1.115 +  shows "a \<in> \<rat> \<Longrightarrow> a ^ n \<in> \<rat>"
   1.116  apply (auto simp add: Rats_def)
   1.117  apply (rule range_eqI)
   1.118  apply (rule of_rat_power [symmetric])