src/HOL/Ring_and_Field.thy

--- a/src/HOL/Ring_and_Field.thy	Sun Jun 13 17:57:35 2004 +0200
+++ b/src/HOL/Ring_and_Field.thy	Mon Jun 14 14:20:55 2004 +0200
@@ -27,6 +27,8 @@
 
 axclass semiring_0 \<subseteq> semiring, comm_monoid_add
 
+axclass semiring_0_cancel \<subseteq> semiring_0, cancel_ab_semigroup_add
+
 axclass comm_semiring \<subseteq> ab_semigroup_add, ab_semigroup_mult  
   mult_commute: "a * b = b * a"
   distrib: "(a + b) * c = a * c + b * c"
@@ -45,6 +47,10 @@
 
 instance comm_semiring_0 \<subseteq> semiring_0 ..
 
+axclass comm_semiring_0_cancel \<subseteq> comm_semiring_0, cancel_ab_semigroup_add
+
+instance comm_semiring_0_cancel \<subseteq> semiring_0_cancel ..
+
 axclass axclass_0_neq_1 \<subseteq> zero, one
   zero_neq_one [simp]: "0 \<noteq> 1"
 
@@ -57,20 +63,30 @@
 axclass axclass_no_zero_divisors \<subseteq> zero, times
   no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
 
+axclass semiring_1_cancel \<subseteq> semiring_1, cancel_ab_semigroup_add
+
+instance semiring_1_cancel \<subseteq> semiring_0_cancel ..
+
 axclass comm_semiring_1_cancel \<subseteq> comm_semiring_1, cancel_ab_semigroup_add (* previously semiring *)
 
+instance comm_semiring_1_cancel \<subseteq> semiring_1_cancel ..
+
+instance comm_semiring_1_cancel \<subseteq> comm_semiring_0_cancel ..
+
 axclass ring \<subseteq> semiring, ab_group_add
 
-instance ring \<subseteq> semiring_0 ..
+instance ring \<subseteq> semiring_0_cancel ..
 
 axclass comm_ring \<subseteq> comm_semiring_0, ab_group_add
 
 instance comm_ring \<subseteq> ring ..
 
-instance comm_ring \<subseteq> comm_semiring_0 ..
+instance comm_ring \<subseteq> comm_semiring_0_cancel ..
 
 axclass ring_1 \<subseteq> ring, semiring_1
 
+instance ring_1 \<subseteq> semiring_1_cancel ..
+
 axclass comm_ring_1 \<subseteq> comm_ring, comm_semiring_1 (* previously ring *)
 
 instance comm_ring_1 \<subseteq> ring_1 ..
@@ -83,7 +99,7 @@
   left_inverse [simp]: "a \<noteq> 0 ==> inverse a * a = 1"
   divide_inverse:      "a / b = a * inverse b"
 
-lemma mult_zero_left [simp]: "0 * a = (0::'a::{semiring_0, cancel_semigroup_add})"
+lemma mult_zero_left [simp]: "0 * a = (0::'a::semiring_0_cancel)"
 proof -
   have "0*a + 0*a = 0*a + 0"
     by (simp add: left_distrib [symmetric])
@@ -91,7 +107,7 @@
     by (simp only: add_left_cancel)
 qed
 
-lemma mult_zero_right [simp]: "a * 0 = (0::'a::{semiring_0, cancel_semigroup_add})"
+lemma mult_zero_right [simp]: "a * 0 = (0::'a::semiring_0_cancel)"
 proof -
   have "a*0 + a*0 = a*0 + 0"
     by (simp add: right_distrib [symmetric])
@@ -155,10 +171,14 @@
 
 axclass pordered_cancel_semiring \<subseteq> pordered_semiring, cancel_ab_semigroup_add
 
+instance pordered_cancel_semiring \<subseteq> semiring_0_cancel ..
+
 axclass ordered_semiring_strict \<subseteq> semiring_0, ordered_cancel_ab_semigroup_add
   mult_strict_left_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> c * a < c * b"
   mult_strict_right_mono: "a < b \<Longrightarrow> 0 < c \<Longrightarrow> a * c < b * c"
 
+instance ordered_semiring_strict \<subseteq> semiring_0_cancel ..
+
 instance ordered_semiring_strict \<subseteq> pordered_cancel_semiring
 apply intro_classes
 apply (case_tac "a < b & 0 < c")
@@ -200,6 +220,10 @@
 
 axclass lordered_ring \<subseteq> pordered_ring, lordered_ab_group_abs
 
+instance lordered_ring \<subseteq> lordered_ab_group_meet ..
+
+instance lordered_ring \<subseteq> lordered_ab_group_join ..
+
 axclass axclass_abs_if \<subseteq> minus, ord, zero
   abs_if: "abs a = (if (a < 0) then (-a) else a)"