--- a/src/HOL/NSA/StarDef.thy Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/NSA/StarDef.thy Fri Feb 13 14:12:00 2009 -0800
@@ -844,6 +844,8 @@
instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
by (intro_classes, transfer, rule add_imp_eq)
+instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
+
instance star :: (ab_group_add) ab_group_add
apply (intro_classes)
apply (transfer, rule left_minus)
--- a/src/HOL/OrderedGroup.thy Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/OrderedGroup.thy Fri Feb 13 14:12:00 2009 -0800
@@ -147,6 +147,9 @@
end
+class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
+
+
subsection {* Groups *}
class group_add = minus + uminus + monoid_add +
@@ -261,7 +264,7 @@
subclass group_add
proof qed (simp_all add: ab_left_minus ab_diff_minus)
-subclass cancel_ab_semigroup_add
+subclass cancel_comm_monoid_add
proof
fix a b c :: 'a
assume "a + b = a + c"
--- a/src/HOL/Polynomial.thy Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/Polynomial.thy Fri Feb 13 14:12:00 2009 -0800
@@ -293,8 +293,7 @@
end
-instance poly ::
- ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add
+instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
proof
fix p q r :: "'a poly"
assume "p + q = p + r" thus "q = r"
--- a/src/HOL/Ring_and_Field.thy Fri Feb 13 12:07:03 2009 -0800
+++ b/src/HOL/Ring_and_Field.thy Fri Feb 13 14:12:00 2009 -0800
@@ -41,7 +41,7 @@
class semiring_0 = semiring + comm_monoid_add + mult_zero
-class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
+class semiring_0_cancel = semiring + cancel_comm_monoid_add
begin
subclass semiring_0
@@ -80,7 +80,7 @@
end
-class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
+class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
begin
subclass semiring_0_cancel ..
@@ -198,8 +198,8 @@
class no_zero_divisors = zero + times +
assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
-class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
- + cancel_ab_semigroup_add + monoid_mult
+class semiring_1_cancel = semiring + cancel_comm_monoid_add
+ + zero_neq_one + monoid_mult
begin
subclass semiring_0_cancel ..
@@ -208,8 +208,8 @@
end
-class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
- + zero_neq_one + cancel_ab_semigroup_add
+class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
+ + zero_neq_one + comm_monoid_mult
begin
subclass semiring_1_cancel ..
@@ -543,7 +543,7 @@
end
class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
- + semiring + comm_monoid_add + cancel_ab_semigroup_add
+ + semiring + cancel_comm_monoid_add
begin
subclass semiring_0_cancel ..