src/HOL/Fields.thy

 
 text {*
   A division ring is like a field, but without the commutativity requirement.
 *}
 
-class inverse =
+class inverse = divide +
   fixes inverse :: "'a \<Rightarrow> 'a"
-    and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
-
-
-context semiring
 begin
-
-lemma [field_simps]:
-  shows distrib_left_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b + c) = a * b + a * c"
-    and distrib_right_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a + b) * c = a * c + b * c"
-  by (rule distrib_left distrib_right)+
+  
+abbreviation inverse_divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
+where
+  "inverse_divide \<equiv> divide"
 
 end
-
-context ring
-begin
-
-lemma [field_simps]:
-  shows left_diff_distrib_NO_MATCH: "NO_MATCH (x / y) c \<Longrightarrow> (a - b) * c = a * c - b * c"
-    and right_diff_distrib_NO_MATCH: "NO_MATCH (x / y) a \<Longrightarrow> a * (b - c) = a * b - a * c"
-  by (rule left_diff_distrib right_diff_distrib)+
-
-end
-
-setup {* Sign.add_const_constraint (@{const_name "divide"}, SOME @{typ "'a::inverse \<Rightarrow> 'a \<Rightarrow> 'a"}) *}
 
 text{* Lemmas @{text divide_simps} move division to the outside and eliminates them on (in)equalities. *}
 
 named_theorems divide_simps "rewrite rules to eliminate divisions"
 

   "\<lbrakk>b \<noteq> 0; c \<noteq> 0\<rbrakk> \<Longrightarrow> (a * c) / (c * b) = a / b"
 using nonzero_mult_divide_mult_cancel_right [of b c a] by (simp add: ac_simps)
 
 lemma diff_frac_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> x / y - w / z = (x * z - w * y) / (y * z)"
+  thm field_simps
   by (simp add: field_simps)
 
 lemma frac_eq_eq:
   "y \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> (x / y = w / z) = (x * z = w * y)"
   by (simp add: field_simps)