# HG changeset patch # User haftmann # Date 1492439941 -7200 # Node ID d801126a14cb510f8c5ff435685b3bf5abe662eb # Parent 8c7bc3a13513d5a96e2de799f3e4a1e90ffa6480 more systematic treatment of polynomial 1 diff -r 8c7bc3a13513 -r d801126a14cb src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy --- 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: "\x. poly p x \ 0" by simp from k dp(2) have "q ^ (degree p) = p * [:1/k:]" - by (simp add: one_poly_def) + by simp then have th2: "p dvd (q ^ (degree p))" .. from dp(1) th1 th2 show ?thesis by blast diff -r 8c7bc3a13513 -r d801126a14cb src/HOL/Computational_Algebra/Polynomial.thy --- 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 "\n. of_bool (n = 0)" + by (rule MOST_SucD) simp + +lemma coeff_1 [simp]: + "coeff 1 n = of_bool (n = 0)" + by (simp add: one_poly.rep_eq) + +lemma one_pCons: + "1 = [:1:]" + by (simp add: poly_eq_iff coeff_pCons split: nat.splits) + +lemma pCons_one: + "[:1:] = 1" + by (simp add: one_pCons) instance -proof - show "1 * p = p" for p :: "'a poly" - by (simp add: one_poly_def) - show "0 \ (1::'a poly)" - by (simp add: one_poly_def) -qed + by standard (simp_all add: one_pCons) end +lemma poly_1 [simp]: + "poly 1 x = 1" + by (simp add: one_pCons) + +lemma one_poly_eq_simps [simp]: + "1 = [:1:] \ True" + "[:1:] = 1 \ True" + by (simp_all add: one_pCons) + +lemma degree_1 [simp]: + "degree 1 = 0" + by (simp add: one_pCons) + +lemma coeffs_1_eq [simp, code abstract]: + "coeffs 1 = [1]" + by (simp add: one_pCons) + +lemma smult_one [simp]: + "smult c 1 = [:c:]" + by (simp add: one_pCons) + +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 \ c = 1 \ 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 \ c = 1 \ 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]" - by (simp add: one_poly_def) - lemma degree_power_le: "degree (p ^ n) \ 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" - by (simp add: one_poly_def) - 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 @@ by (simp add: map_poly_def) lemma map_poly_1' [simp]: "f 1 = 1 \ 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 \p dvd 1\] 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 @@ by (simp add: reflect_poly_def) 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 @@ by (simp add: pderiv.simps) 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 \ 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" diff -r 8c7bc3a13513 -r d801126a14cb src/HOL/Computational_Algebra/Polynomial_FPS.thy --- 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]) - (simp add: one_poly_def) + by (simp add: fps_eq_iff) 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]) diff -r 8c7bc3a13513 -r d801126a14cb src/HOL/Computational_Algebra/Polynomial_Factorial.thy --- 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 @@ subsection \Various facts about polynomials\ lemma prod_mset_const_poly: " (\x\#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 \ b' dvd 1" by (rule irreducibleD) - with ab' show "a dvd 1 \ b dvd 1" by (auto simp: one_poly_def) + with ab' show "a dvd 1 \ 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 \ 0" and "\ 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 \ [:b:] dvd 1" by (rule irreducibleD) - thus "a dvd 1 \ b dvd 1" by (simp add: one_poly_def) - qed (insert A, auto simp: irreducible_def one_poly_def) + then show "a dvd 1 \ b dvd 1" + by (auto simp add: is_unit_const_poly_iff) + qed qed @@ -141,7 +145,7 @@ by (simp add: poly_eqI coeff_map_poly) lemma fract_poly_1 [simp]: "fract_poly 1 = 1" - by (simp add: one_poly_def map_poly_pCons) + by (simp add: map_poly_pCons) lemma fract_poly_add [simp]: "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 \ [:c:] dvd b" by blast -qed (insert assms, simp_all add: prime_elem_def one_poly_def) + then show "[:c:] dvd a \ [:c:] dvd b" by blast +next + from assms show "[:c:] \ 0" and "\ [: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"