src/HOL/Library/Univ_Poly.thy
 changeset 29667 53103fc8ffa3 parent 29504 4c3441f2f619 child 29879 4425849f5db7
```--- a/src/HOL/Library/Univ_Poly.thy	Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Library/Univ_Poly.thy	Wed Jan 28 16:29:16 2009 +0100
@@ -217,7 +217,7 @@
from Cons.hyps[rule_format, of x]
obtain q r where qr: "x#xs = [r] +++ [- a, 1] *** q" by blast
have "h#x#xs = [a*r + h] +++ [-a, 1] *** (r#q)"
-      using qr by(cases q, simp_all add: ring_simps diff_def[symmetric]
+      using qr by(cases q, simp_all add: algebra_simps diff_def[symmetric]
minus_mult_left[symmetric] right_minus)
hence "\<exists>q r. h#x#xs = [r] +++ [-a, 1] *** q" by blast}
thus ?case by blast
@@ -303,7 +303,7 @@
from C[of ?i] obtain y where y: "poly p y = 0" "\<forall>m\<le> Suc n. y \<noteq> ?i m"
by blast
from y have "y = a \<or> poly q y = 0"
with i[rule_format, of y] y(1) y(2) have False apply auto
apply (erule_tac x="m" in allE)
apply auto
@@ -414,8 +414,8 @@

lemma (in idom_char_0) poly_entire:
"poly (p *** q) = poly [] \<longleftrightarrow> poly p = poly [] \<or> poly q = poly []"
-using poly_entire_lemma2[of p q]
-by auto (rule ext, simp add: poly_mult)+
+using poly_entire_lemma2[of p q]
+by (auto simp add: expand_fun_eq poly_mult)

lemma (in idom_char_0) poly_entire_neg: "(poly (p *** q) \<noteq> poly []) = ((poly p \<noteq> poly []) & (poly q \<noteq> poly []))"
@@ -424,7 +424,7 @@
by (auto intro!: ext)

lemma (in comm_ring_1) poly_add_minus_zero_iff: "(poly (p +++ -- q) = poly []) = (poly p = poly q)"

lemma (in comm_ring_1) poly_add_minus_mult_eq: "poly (p *** q +++ --(p *** r)) = poly (p *** (q +++ -- r))"
by (auto simp add: poly_add poly_minus_def fun_eq poly_mult poly_cmult right_distrib minus_mult_left[symmetric] minus_mult_right[symmetric])
@@ -550,7 +550,7 @@
"[| p divides q; p divides (q +++ r) |] ==> p divides r"
apply (rule_tac x = "padd qaa (poly_minus qa)" in exI)
done

lemma (in comm_ring_1) poly_divides_diff2: "[| p divides r; p divides (q +++ r) |] ==> p divides q"
@@ -892,15 +892,15 @@
proof
assume eq: ?lhs
hence "\<And>x. poly ((c#cs) +++ -- (d#ds)) x = 0"
-    by (simp only: poly_minus poly_add ring_simps) simp
-  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by - (rule ext, simp)
+    by (simp only: poly_minus poly_add algebra_simps) simp
+  hence "poly ((c#cs) +++ -- (d#ds)) = poly []" by(simp add:expand_fun_eq)
hence "c = d \<and> list_all (\<lambda>x. x=0) ((cs +++ -- ds))"
-    unfolding poly_zero by (simp add: poly_minus_def ring_simps minus_mult_left[symmetric])
+    unfolding poly_zero by (simp add: poly_minus_def algebra_simps)
hence "c = d \<and> (\<forall>x. poly (cs +++ -- ds) x = 0)"
unfolding poly_zero[symmetric] by simp
-  thus ?rhs  apply (simp add: poly_minus poly_add ring_simps) apply (rule ext, simp) done
next
-  assume ?rhs then show ?lhs  by -  (rule ext,simp)
+  assume ?rhs then show ?lhs by(simp add:expand_fun_eq)
qed

lemma (in idom_char_0) pnormalize_unique: "poly p = poly q \<Longrightarrow> pnormalize p = pnormalize q"
@@ -1008,7 +1008,7 @@
from p have ap: "poly ([a,1] *** p) \<noteq> poly []"
using poly_mult_not_eq_poly_Nil unfolding poly_entire by auto
have eq: "poly ([a,1] %^(Suc n) *** p) = poly ([a,1]%^n *** ([a,1] *** p))"