src/HOL/Rat.thy
changeset 36409 d323e7773aa8
parent 36349 39be26d1bc28
child 36415 a168ac750096
     1.1 --- a/src/HOL/Rat.thy	Mon Apr 26 11:34:19 2010 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon Apr 26 15:37:50 2010 +0200
     1.3 @@ -411,7 +411,7 @@
     1.4  
     1.5  subsubsection {* The field of rational numbers *}
     1.6  
     1.7 -instantiation rat :: field
     1.8 +instantiation rat :: field_inverse_zero
     1.9  begin
    1.10  
    1.11  definition
    1.12 @@ -440,13 +440,10 @@
    1.13  next
    1.14    fix q r :: rat
    1.15    show "q / r = q * inverse r" by (simp add: divide_rat_def)
    1.16 -qed
    1.17 +qed (simp add: rat_number_expand, simp add: rat_number_collapse)
    1.18  
    1.19  end
    1.20  
    1.21 -instance rat :: division_ring_inverse_zero proof
    1.22 -qed (simp add: rat_number_expand, simp add: rat_number_collapse)
    1.23 -
    1.24  
    1.25  subsubsection {* Various *}
    1.26  
    1.27 @@ -624,7 +621,7 @@
    1.28  
    1.29  end
    1.30  
    1.31 -instance rat :: linordered_field
    1.32 +instance rat :: linordered_field_inverse_zero
    1.33  proof
    1.34    fix q r s :: rat
    1.35    show "q \<le> r ==> s + q \<le> s + r"
    1.36 @@ -724,8 +721,7 @@
    1.37      by (cases "b = 0", simp, simp add: of_int_rat)
    1.38    moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
    1.39      unfolding Fract_of_int_quotient
    1.40 -    by (rule linorder_cases [of b 0])
    1.41 -       (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
    1.42 +    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
    1.43    ultimately show ?thesis by simp
    1.44  qed
    1.45  
    1.46 @@ -818,7 +814,7 @@
    1.47  done
    1.48  
    1.49  lemma of_rat_inverse:
    1.50 -  "(of_rat (inverse a)::'a::{field_char_0,division_ring_inverse_zero}) =
    1.51 +  "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
    1.52     inverse (of_rat a)"
    1.53  by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
    1.54  
    1.55 @@ -827,7 +823,7 @@
    1.56  by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
    1.57  
    1.58  lemma of_rat_divide:
    1.59 -  "(of_rat (a / b)::'a::{field_char_0,division_ring_inverse_zero})
    1.60 +  "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero})
    1.61     = of_rat a / of_rat b"
    1.62  by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
    1.63  
    1.64 @@ -968,7 +964,7 @@
    1.65  done
    1.66  
    1.67  lemma Rats_inverse [simp]:
    1.68 -  fixes a :: "'a::{field_char_0,division_ring_inverse_zero}"
    1.69 +  fixes a :: "'a::{field_char_0, field_inverse_zero}"
    1.70    shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
    1.71  apply (auto simp add: Rats_def)
    1.72  apply (rule range_eqI)
    1.73 @@ -984,7 +980,7 @@
    1.74  done
    1.75  
    1.76  lemma Rats_divide [simp]:
    1.77 -  fixes a b :: "'a::{field_char_0,division_ring_inverse_zero}"
    1.78 +  fixes a b :: "'a::{field_char_0, field_inverse_zero}"
    1.79    shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
    1.80  apply (auto simp add: Rats_def)
    1.81  apply (rule range_eqI)