# HG changeset patch
# User huffman
# Date 1232052221 28800
# Node ID 8858d197a9b6d00ba9f2747a3a33fa3e73f6ac8b
# Parent  abfe2af6883e6e35002058b50e188bf61d2e837f
more instance declarations for poly

diff -r abfe2af6883e -r 8858d197a9b6 src/HOL/Polynomial.thy
--- a/src/HOL/Polynomial.thy	Thu Jan 15 12:43:12 2009 -0800
+++ b/src/HOL/Polynomial.thy	Thu Jan 15 12:43:41 2009 -0800
@@ -293,6 +293,14 @@
 
 end
 
+instance poly ::
+  ("{cancel_ab_semigroup_add,comm_monoid_add}") cancel_ab_semigroup_add
+proof
+  fix p q r :: "'a poly"
+  assume "p + q = p + r" thus "q = r"
+    by (simp add: expand_poly_eq)
+qed
+
 instantiation poly :: (ab_group_add) ab_group_add
 begin
 
@@ -541,6 +549,8 @@
 
 end
 
+instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..
+
 lemma coeff_mult:
   "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))"
 proof (induct p arbitrary: n)
@@ -582,6 +592,8 @@
 
 end
 
+instance poly :: (comm_semiring_1_cancel) comm_semiring_1_cancel ..
+
 lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
   unfolding one_poly_def
   by (simp add: coeff_pCons split: nat.split)