src/HOL/Rat.thy

   by (auto simp add: quotient_of_inject)
 
 
 subsubsection {* The field of rational numbers *}
 
-instantiation rat :: field
+instantiation rat :: field_inverse_zero
 begin
 
 definition
   inverse_rat_def:
   "inverse q = Abs_Rat (\<Union>x \<in> Rep_Rat q.

   then show "inverse q * q = 1" by (cases q rule: Rat_cases_nonzero)
    (simp_all add: rat_number_expand eq_rat)
 next
   fix q r :: rat
   show "q / r = q * inverse r" by (simp add: divide_rat_def)
-qed
+qed (simp add: rat_number_expand, simp add: rat_number_collapse)
 
 end
-
-instance rat :: division_ring_inverse_zero proof
-qed (simp add: rat_number_expand, simp add: rat_number_collapse)
 
 
 subsubsection {* Various *}
 
 lemma Fract_add_one: "n \<noteq> 0 ==> Fract (m + n) n = Fract m n + 1"

 instance by intro_classes
   (auto simp add: abs_rat_def sgn_rat_def min_max.sup_inf_distrib1 inf_rat_def sup_rat_def)
 
 end
 
-instance rat :: linordered_field
+instance rat :: linordered_field_inverse_zero
 proof
   fix q r s :: rat
   show "q \<le> r ==> s + q \<le> s + r"
   proof (induct q, induct r, induct s)
     fix a b c d e f :: int

 proof -
   have "Fract a b = of_int (a div b) + Fract (a mod b) b"
     by (cases "b = 0", simp, simp add: of_int_rat)
   moreover have "0 \<le> Fract (a mod b) b \<and> Fract (a mod b) b < 1"
     unfolding Fract_of_int_quotient
-    by (rule linorder_cases [of b 0])
-       (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
+    by (rule linorder_cases [of b 0]) (simp add: divide_nonpos_neg, simp, simp add: divide_nonneg_pos)
   ultimately show ?thesis by simp
 qed
 
 instance rat :: archimedean_field
 proof

 apply (rule inverse_unique [symmetric])
 apply (simp add: of_rat_mult [symmetric])
 done
 
 lemma of_rat_inverse:
-  "(of_rat (inverse a)::'a::{field_char_0,division_ring_inverse_zero}) =
+  "(of_rat (inverse a)::'a::{field_char_0, field_inverse_zero}) =
    inverse (of_rat a)"
 by (cases "a = 0", simp_all add: nonzero_of_rat_inverse)
 
 lemma nonzero_of_rat_divide:
   "b \<noteq> 0 \<Longrightarrow> of_rat (a / b) = of_rat a / of_rat b"
 by (simp add: divide_inverse of_rat_mult nonzero_of_rat_inverse)
 
 lemma of_rat_divide:
-  "(of_rat (a / b)::'a::{field_char_0,division_ring_inverse_zero})
+  "(of_rat (a / b)::'a::{field_char_0, field_inverse_zero})
    = of_rat a / of_rat b"
 by (cases "b = 0") (simp_all add: nonzero_of_rat_divide)
 
 lemma of_rat_power:
   "(of_rat (a ^ n)::'a::field_char_0) = of_rat a ^ n"

 apply (rule range_eqI)
 apply (erule nonzero_of_rat_inverse [symmetric])
 done
 
 lemma Rats_inverse [simp]:
-  fixes a :: "'a::{field_char_0,division_ring_inverse_zero}"
+  fixes a :: "'a::{field_char_0, field_inverse_zero}"
   shows "a \<in> Rats \<Longrightarrow> inverse a \<in> Rats"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_inverse [symmetric])
 done

 apply (rule range_eqI)
 apply (erule nonzero_of_rat_divide [symmetric])
 done
 
 lemma Rats_divide [simp]:
-  fixes a b :: "'a::{field_char_0,division_ring_inverse_zero}"
+  fixes a b :: "'a::{field_char_0, field_inverse_zero}"
   shows "\<lbrakk>a \<in> Rats; b \<in> Rats\<rbrakk> \<Longrightarrow> a / b \<in> Rats"
 apply (auto simp add: Rats_def)
 apply (rule range_eqI)
 apply (rule of_rat_divide [symmetric])
 done