src/HOL/Polynomial.thy

 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
   by (rule poly_ext, simp)
 
 lemma smult_add_right:
   "smult a (p + q) = smult a p + smult a q"
-  by (rule poly_ext, simp add: ring_simps)
+  by (rule poly_ext, simp add: algebra_simps)
 
 lemma smult_add_left:
   "smult (a + b) p = smult a p + smult b p"
-  by (rule poly_ext, simp add: ring_simps)
+  by (rule poly_ext, simp add: algebra_simps)
 
 lemma smult_minus_right [simp]:
   "smult (a::'a::comm_ring) (- p) = - smult a p"
   by (rule poly_ext, simp)
 

   "smult (- a::'a::comm_ring) p = - smult a p"
   by (rule poly_ext, simp)
 
 lemma smult_diff_right:
   "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q"
-  by (rule poly_ext, simp add: ring_simps)
+  by (rule poly_ext, simp add: algebra_simps)
 
 lemma smult_diff_left:
   "smult (a - b::'a::comm_ring) p = smult a p - smult b p"
-  by (rule poly_ext, simp add: ring_simps)
+  by (rule poly_ext, simp add: algebra_simps)
 
 lemmas smult_distribs =
   smult_add_left smult_add_right
   smult_diff_left smult_diff_right
 

 lemma mult_poly_0_right: "p * (0::'a poly) = 0"
   by (induct p, simp add: mult_poly_0_left, simp)
 
 lemma mult_pCons_right [simp]:
   "p * pCons a q = smult a p + pCons 0 (p * q)"
-  by (induct p, simp add: mult_poly_0_left, simp add: ring_simps)
+  by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps)
 
 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right
 
 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
   by (induct p, simp add: mult_poly_0, simp add: smult_add_right)

 
 lemma mult_poly_add_left:
   fixes p q r :: "'a poly"
   shows "(p + q) * r = p * r + q * r"
   by (induct r, simp add: mult_poly_0,
-                simp add: smult_distribs group_simps)
+                simp add: smult_distribs algebra_simps)
 
 instance proof
   fix p q r :: "'a poly"
   show 0: "0 * p = 0"
     by (rule mult_poly_0_left)

   from 1 have q1: "x = q1 * y + r1" and r1: "r1 = 0 \<or> degree r1 < degree y"
     unfolding pdivmod_rel_def by simp_all
   from 2 have q2: "x = q2 * y + r2" and r2: "r2 = 0 \<or> degree r2 < degree y"
     unfolding pdivmod_rel_def by simp_all
   from q1 q2 have q3: "(q1 - q2) * y = r2 - r1"
-    by (simp add: ring_simps)
+    by (simp add: algebra_simps)
   from r1 r2 have r3: "(r2 - r1) = 0 \<or> degree (r2 - r1) < degree y"
     by (auto intro: degree_diff_less)
 
   show "q1 = q2 \<and> r1 = r2"
   proof (rule ccontr)

   shows "poly (monom a n) x = a * x ^ n"
   by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac)
 
 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
   apply (induct p arbitrary: q, simp)
-  apply (case_tac q, simp, simp add: ring_simps)
+  apply (case_tac q, simp, simp add: algebra_simps)
   done
 
 lemma poly_minus [simp]:
   fixes x :: "'a::comm_ring"
   shows "poly (- p) x = - poly p x"

 
 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
   by (cases "finite A", induct set: finite, simp_all)
 
 lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
-  by (induct p, simp, simp add: ring_simps)
+  by (induct p, simp, simp add: algebra_simps)
 
 lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
-  by (induct p, simp_all, simp add: ring_simps)
+  by (induct p, simp_all, simp add: algebra_simps)
 
 lemma poly_power [simp]:
   fixes p :: "'a::{comm_semiring_1,recpower} poly"
   shows "poly (p ^ n) x = poly p x ^ n"
   by (induct n, simp, simp add: power_Suc)

 
 lemma synthetic_div_correct':
   fixes c :: "'a::comm_ring_1"
   shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p"
   using synthetic_div_correct [of p c]
-  by (simp add: group_simps)
+  by (simp add: algebra_simps)
 
 lemma poly_eq_0_iff_dvd:
   fixes c :: "'a::idom"
   shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p"
 proof