--- a/src/HOL/Polynomial.thy Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Polynomial.thy Wed Jan 28 16:29:16 2009 +0100
@@ -442,11 +442,11 @@
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"
@@ -458,11 +458,11 @@
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
@@ -517,7 +517,7 @@
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
@@ -531,7 +531,7 @@
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"
@@ -758,7 +758,7 @@
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)
@@ -894,7 +894,7 @@
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]:
@@ -911,10 +911,10 @@
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"
@@ -983,7 +983,7 @@
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"