add class cancel_comm_monoid_add
authorhuffman
Fri Feb 13 14:12:00 2009 -0800 (2009-02-13)
changeset 29904856f16a3b436
parent 29900 333cbcad74c3
child 29905 26ee9656872a
add class cancel_comm_monoid_add
src/HOL/NSA/StarDef.thy
src/HOL/OrderedGroup.thy
src/HOL/Polynomial.thy
src/HOL/Ring_and_Field.thy
     1.1 --- a/src/HOL/NSA/StarDef.thy	Fri Feb 13 12:07:03 2009 -0800
     1.2 +++ b/src/HOL/NSA/StarDef.thy	Fri Feb 13 14:12:00 2009 -0800
     1.3 @@ -844,6 +844,8 @@
     1.4  instance star :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add
     1.5  by (intro_classes, transfer, rule add_imp_eq)
     1.6  
     1.7 +instance star :: (cancel_comm_monoid_add) cancel_comm_monoid_add ..
     1.8 +
     1.9  instance star :: (ab_group_add) ab_group_add
    1.10  apply (intro_classes)
    1.11  apply (transfer, rule left_minus)
     2.1 --- a/src/HOL/OrderedGroup.thy	Fri Feb 13 12:07:03 2009 -0800
     2.2 +++ b/src/HOL/OrderedGroup.thy	Fri Feb 13 14:12:00 2009 -0800
     2.3 @@ -147,6 +147,9 @@
     2.4  
     2.5  end
     2.6  
     2.7 +class cancel_comm_monoid_add = cancel_ab_semigroup_add + comm_monoid_add
     2.8 +
     2.9 +
    2.10  subsection {* Groups *}
    2.11  
    2.12  class group_add = minus + uminus + monoid_add +
    2.13 @@ -261,7 +264,7 @@
    2.14  subclass group_add
    2.15    proof qed (simp_all add: ab_left_minus ab_diff_minus)
    2.16  
    2.17 -subclass cancel_ab_semigroup_add
    2.18 +subclass cancel_comm_monoid_add
    2.19  proof
    2.20    fix a b c :: 'a
    2.21    assume "a + b = a + c"
     3.1 --- a/src/HOL/Polynomial.thy	Fri Feb 13 12:07:03 2009 -0800
     3.2 +++ b/src/HOL/Polynomial.thy	Fri Feb 13 14:12:00 2009 -0800
     3.3 @@ -293,8 +293,7 @@
     3.4  
     3.5  end
     3.6  
     3.7 -instance poly ::
     3.8 -  ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add
     3.9 +instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
    3.10  proof
    3.11    fix p q r :: "'a poly"
    3.12    assume "p + q = p + r" thus "q = r"
     4.1 --- a/src/HOL/Ring_and_Field.thy	Fri Feb 13 12:07:03 2009 -0800
     4.2 +++ b/src/HOL/Ring_and_Field.thy	Fri Feb 13 14:12:00 2009 -0800
     4.3 @@ -41,7 +41,7 @@
     4.4  
     4.5  class semiring_0 = semiring + comm_monoid_add + mult_zero
     4.6  
     4.7 -class semiring_0_cancel = semiring + comm_monoid_add + cancel_ab_semigroup_add
     4.8 +class semiring_0_cancel = semiring + cancel_comm_monoid_add
     4.9  begin
    4.10  
    4.11  subclass semiring_0
    4.12 @@ -80,7 +80,7 @@
    4.13  
    4.14  end
    4.15  
    4.16 -class comm_semiring_0_cancel = comm_semiring + comm_monoid_add + cancel_ab_semigroup_add
    4.17 +class comm_semiring_0_cancel = comm_semiring + cancel_comm_monoid_add
    4.18  begin
    4.19  
    4.20  subclass semiring_0_cancel ..
    4.21 @@ -198,8 +198,8 @@
    4.22  class no_zero_divisors = zero + times +
    4.23    assumes no_zero_divisors: "a \<noteq> 0 \<Longrightarrow> b \<noteq> 0 \<Longrightarrow> a * b \<noteq> 0"
    4.24  
    4.25 -class semiring_1_cancel = semiring + comm_monoid_add + zero_neq_one
    4.26 -  + cancel_ab_semigroup_add + monoid_mult
    4.27 +class semiring_1_cancel = semiring + cancel_comm_monoid_add
    4.28 +  + zero_neq_one + monoid_mult
    4.29  begin
    4.30  
    4.31  subclass semiring_0_cancel ..
    4.32 @@ -208,8 +208,8 @@
    4.33  
    4.34  end
    4.35  
    4.36 -class comm_semiring_1_cancel = comm_semiring + comm_monoid_add + comm_monoid_mult
    4.37 -  + zero_neq_one + cancel_ab_semigroup_add
    4.38 +class comm_semiring_1_cancel = comm_semiring + cancel_comm_monoid_add
    4.39 +  + zero_neq_one + comm_monoid_mult
    4.40  begin
    4.41  
    4.42  subclass semiring_1_cancel ..
    4.43 @@ -543,7 +543,7 @@
    4.44  end
    4.45  
    4.46  class pordered_cancel_semiring = mult_mono + pordered_ab_semigroup_add
    4.47 -  + semiring + comm_monoid_add + cancel_ab_semigroup_add
    4.48 +  + semiring + cancel_comm_monoid_add
    4.49  begin
    4.50  
    4.51  subclass semiring_0_cancel ..