author haftmann Mon, 17 Apr 2017 16:39:01 +0200 changeset 65486 d801126a14cb parent 65485 8c7bc3a13513 child 65502 c05bec5d01ad
more systematic treatment of polynomial 1
```--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Mon Apr 17 16:39:01 2017 +0200
@@ -1025,7 +1025,7 @@
then have th1: "\<forall>x. poly p x \<noteq> 0"
by simp
from k dp(2) have "q ^ (degree p) = p * [:1/k:]"
+      by simp
then have th2: "p dvd (q ^ (degree p))" ..
from dp(1) th1 th2 show ?thesis
by blast```
```--- a/src/HOL/Computational_Algebra/Polynomial.thy	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy	Mon Apr 17 16:39:01 2017 +0200
@@ -998,41 +998,65 @@
instantiation poly :: (comm_semiring_1) comm_semiring_1
begin

-definition one_poly_def: "1 = pCons 1 0"
+lift_definition one_poly :: "'a poly"
+  is "\<lambda>n. of_bool (n = 0)"
+  by (rule MOST_SucD) simp
+
+lemma coeff_1 [simp]:
+  "coeff 1 n = of_bool (n = 0)"
+
+lemma one_pCons:
+  "1 = [:1:]"
+  by (simp add: poly_eq_iff coeff_pCons split: nat.splits)
+
+lemma pCons_one:
+  "[:1:] = 1"

instance
-proof
-  show "1 * p = p" for p :: "'a poly"
-  show "0 \<noteq> (1::'a poly)"
-qed
+  by standard (simp_all add: one_pCons)

end

+lemma poly_1 [simp]:
+  "poly 1 x = 1"
+
+lemma one_poly_eq_simps [simp]:
+  "1 = [:1:] \<longleftrightarrow> True"
+  "[:1:] = 1 \<longleftrightarrow> True"
+
+lemma degree_1 [simp]:
+  "degree 1 = 0"
+
+lemma coeffs_1_eq [simp, code abstract]:
+  "coeffs 1 = [1]"
+
+lemma smult_one [simp]:
+  "smult c 1 = [:c:]"
+
+lemma monom_eq_1 [simp]:
+  "monom 1 0 = 1"
+  by (simp add: monom_0 one_pCons)
+
+lemma monom_eq_1_iff:
+  "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
+  using monom_eq_const_iff [of c n 1] by auto
+
+lemma monom_altdef:
+  "monom c n = smult c ([:0, 1:] ^ n)"
+  by (induct n) (simp_all add: monom_0 monom_Suc)
+
instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors ..
instance poly :: (comm_ring) comm_ring ..
instance poly :: (comm_ring_1) comm_ring_1 ..
instance poly :: (comm_ring_1) comm_semiring_1_cancel ..

-lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)"
-  by (simp add: one_poly_def coeff_pCons split: nat.split)
-
-lemma monom_eq_1 [simp]: "monom 1 0 = 1"
-  by (simp add: monom_0 one_poly_def)
-
-lemma monom_eq_1_iff: "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0"
-  using monom_eq_const_iff[of c n 1] by (auto simp: one_poly_def)
-
-lemma monom_altdef: "monom c n = smult c ([:0, 1:]^n)"
-  by (induct n) (simp_all add: monom_0 monom_Suc one_poly_def)
-
-lemma degree_1 [simp]: "degree 1 = 0"
-  unfolding one_poly_def by (rule degree_pCons_0)
-
-lemma coeffs_1_eq [simp, code abstract]: "coeffs 1 = [1]"
-
lemma degree_power_le: "degree (p ^ n) \<le> degree p * n"
by (induct n) (auto intro: order_trans degree_mult_le)

@@ -1045,9 +1069,6 @@
lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
by (induct p) (simp_all add: algebra_simps)

-lemma poly_1 [simp]: "poly 1 x = 1"
-
lemma poly_power [simp]: "poly (p ^ n) x = poly p x ^ n"
for p :: "'a::comm_semiring_1 poly"
by (induct n) simp_all
@@ -1113,7 +1134,7 @@

lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1"
-  by (simp add: map_poly_def one_poly_def)
+  by (simp add: map_poly_def one_pCons)

lemma coeff_map_poly:
assumes "f 0 = 0"
@@ -1217,7 +1238,7 @@

lemma of_nat_poly:
"of_nat n = [:of_nat n:]"
-  by (induct n) (simp_all add: one_poly_def)
+  by (induct n) (simp_all add: one_pCons)

lemma of_nat_monom:
"of_nat n = monom (of_nat n) 0"
@@ -1328,7 +1349,7 @@
from this(1) obtain d where "1 = c * d"
by (rule dvdE)
then have "1 = [:c:] * [:d:]"
-      by (simp add: one_poly_def mult_ac)
+      by (simp add: one_pCons ac_simps)
then have "[:c:] dvd 1"
by (rule dvdI)
from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1"
@@ -1952,7 +1973,7 @@

lemma pcompose_1: "pcompose 1 p = 1"
for p :: "'a::comm_semiring_1 poly"
-  by (auto simp: one_poly_def pcompose_pCons)
+  by (auto simp: one_pCons pcompose_pCons)

lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)"
by (induct p) (simp_all add: pcompose_pCons)
@@ -2225,7 +2246,7 @@

lemma reflect_poly_1 [simp]: "reflect_poly 1 = 1"
-  by (simp add: reflect_poly_def one_poly_def)
+  by (simp add: reflect_poly_def one_pCons)

lemma coeff_reflect_poly:
"coeff (reflect_poly p) n = (if n > degree p then 0 else coeff p (degree p - n))"
@@ -2351,7 +2372,7 @@

lemma pderiv_1 [simp]: "pderiv 1 = 0"
-  by (simp add: one_poly_def pderiv_pCons)
+  by (simp add: one_pCons pderiv_pCons)

lemma pderiv_of_nat [simp]: "pderiv (of_nat n) = 0"
and pderiv_numeral [simp]: "pderiv (numeral m) = 0"
@@ -3242,7 +3263,7 @@

lemma is_unit_const_poly_iff: "[:c:] dvd 1 \<longleftrightarrow> c dvd 1"
for c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
-  by (auto simp: one_poly_def)
+  by (auto simp: one_pCons)

lemma is_unit_polyE:
fixes p :: "'a :: {comm_semiring_1,semiring_no_zero_divisors} poly"```
```--- a/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_FPS.thy	Mon Apr 17 16:39:01 2017 +0200
@@ -27,8 +27,7 @@
by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp

lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1"
-  by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric])

lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1"
by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric])```
```--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Apr 17 07:44:21 2017 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Mon Apr 17 16:39:01 2017 +0200
@@ -17,7 +17,7 @@

lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
-  by (induct A) (simp_all add: one_poly_def ac_simps)
+  by (induct A) (simp_all add: ac_simps)

lemma irreducible_const_poly_iff:
fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
@@ -35,17 +35,21 @@
from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
hence "c = a' * b'" by (simp add: ab' mult_ac)
from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
-    with ab' show "a dvd 1 \<or> b dvd 1" by (auto simp: one_poly_def)
+    with ab' show "a dvd 1 \<or> b dvd 1"
+      by (auto simp add: is_unit_const_poly_iff)
qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
next
assume A: "irreducible [:c:]"
-  show "irreducible c"
+  then have "c \<noteq> 0" and "\<not> c dvd 1"
+    by (auto simp add: irreducible_def is_unit_const_poly_iff)
+  then show "irreducible c"
proof (rule irreducibleI)
fix a b assume ab: "c = a * b"
hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
-    thus "a dvd 1 \<or> b dvd 1" by (simp add: one_poly_def)
-  qed (insert A, auto simp: irreducible_def one_poly_def)
+    then show "a dvd 1 \<or> b dvd 1"
+      by (auto simp add: is_unit_const_poly_iff)
+  qed
qed

@@ -141,7 +145,7 @@

lemma fract_poly_1 [simp]: "fract_poly 1 = 1"
-  by (simp add: one_poly_def map_poly_pCons)

"fract_poly (p + q) = fract_poly p + fract_poly q"
@@ -363,8 +367,11 @@
qed
hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
}
-  thus "[:c:] dvd a \<or> [:c:] dvd b" by blast
-qed (insert assms, simp_all add: prime_elem_def one_poly_def)
+  then show "[:c:] dvd a \<or> [:c:] dvd b" by blast
+next
+  from assms show "[:c:] \<noteq> 0" and "\<not> [:c:] dvd 1"
+    by (simp_all add: prime_elem_def is_unit_const_poly_iff)
+qed

lemma prime_elem_const_poly_iff:
fixes c :: "'a :: semidom"```