summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Wed, 22 Aug 2018 13:33:50 +0000 | |

changeset 68790 | 851a9d9746c6 |

parent 68789 | 9270af426282 |

child 68792 | d2470f3a768b |

prefer constructive primitive_part over implicit content_decompose

src/HOL/Computational_Algebra/Polynomial.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Computational_Algebra/Polynomial_Factorial.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Computational_Algebra/Polynomial.thy Wed Aug 22 16:41:29 2018 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed Aug 22 13:33:50 2018 +0000 @@ -4546,22 +4546,20 @@ qed lemma content_decompose: - obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1" + obtains p' :: "'a::semiring_gcd poly" + where "p = smult (content p) p'" "content p' = 1" proof (cases "p = 0") case True - then show ?thesis by (intro that[of 1]) simp_all + then have "p = smult (content p) 1" "content 1 = 1" + by simp_all + then show ?thesis .. next case False - from content_dvd[of p] obtain r where r: "p = [:content p:] * r" - by (rule dvdE) - have "content p * 1 = content p * content r" - by (subst r) simp - with False have "content r = 1" - by (subst (asm) mult_left_cancel) simp_all - with r show ?thesis - by (intro that[of r]) simp_all + then have "p = smult (content p) (primitive_part p)" "content (primitive_part p) = 1" + by simp_all + then show ?thesis .. qed - + lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q" using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast @@ -4594,53 +4592,61 @@ finally show ?thesis . qed +context +begin + +private + +lemma content_1_mult: + fixes f g :: "'a :: {semiring_gcd, factorial_semiring} poly" + assumes "content f = 1" "content g = 1" + shows "content (f * g) = 1" +proof (cases "f * g = 0") + case False + from assms have "f \<noteq> 0" "g \<noteq> 0" by auto + + hence "f * g \<noteq> 0" by auto + { + assume "\<not>is_unit (content (f * g))" + with False have "\<exists>p. p dvd content (f * g) \<and> prime p" + by (intro prime_divisor_exists) simp_all + then obtain p where "p dvd content (f * g)" "prime p" by blast + from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g" + by (simp add: const_poly_dvd_iff_dvd_content) + moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) + ultimately have "[:p:] dvd f \<or> [:p:] dvd g" + by (simp add: prime_elem_dvd_mult_iff) + with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) + with \<open>prime p\<close> have False by simp + } + hence "is_unit (content (f * g))" by blast + hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content) + thus ?thesis by simp +qed (insert assms, auto) + lemma content_mult: - fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" + fixes p q :: "'a :: {factorial_semiring, semiring_gcd} poly" shows "content (p * q) = content p * content q" -proof - - from content_decompose[of p] guess p' . note p = this - from content_decompose[of q] guess q' . note q = this - have "content (p * q) = content p * content q * content (p' * q')" - by (subst p, subst q) (simp add: mult_ac normalize_mult) - also have "content (p' * q') = 1" - proof (cases "p' * q' = 0") - case True - with \<open>content p' = 1\<close> \<open>content q' = 1\<close> show ?thesis - by auto - next - case False - from \<open>content p' = 1\<close> \<open>content q' = 1\<close> - have "p' \<noteq> 0" "q' \<noteq> 0" - by auto - then have "p' * q' \<noteq> 0" - by auto - have "is_unit (content (p' * q'))" - proof (rule ccontr) - assume "\<not> is_unit (content (p' * q'))" - with False have "\<exists>p. p dvd content (p' * q') \<and> prime p" - by (intro prime_divisor_exists) simp_all - then obtain p where "p dvd content (p' * q')" "prime p" - by blast - from \<open>p dvd content (p' * q')\<close> have "[:p:] dvd p' * q'" - by (simp add: const_poly_dvd_iff_dvd_content) - moreover from \<open>prime p\<close> have "prime_elem [:p:]" - by (simp add: lift_prime_elem_poly) - ultimately have "[:p:] dvd p' \<or> [:p:] dvd q'" - by (simp add: prime_elem_dvd_mult_iff) - with \<open>content p' = 1\<close> \<open>content q' = 1\<close> have "is_unit p" - by (simp add: const_poly_dvd_iff_dvd_content) - with \<open>prime p\<close> show False - by simp - qed - then have "normalize (content (p' * q')) = 1" - by (simp add: is_unit_normalize del: normalize_content) - then show ?thesis - by simp - qed - finally show ?thesis +proof (cases "p * q = 0") + case False + then have "p \<noteq> 0" and "q \<noteq> 0" + by simp_all + then have *: "content (primitive_part p * primitive_part q) = 1" + by (auto intro: content_1_mult) + have "p * q = smult (content p) (primitive_part p) * smult (content q) (primitive_part q)" by simp + also have "\<dots> = smult (content p * content q) (primitive_part p * primitive_part q)" + by (metis mult.commute mult_smult_right smult_smult) + with * show ?thesis + by (simp add: normalize_mult) +next + case True + then show ?thesis + by auto qed +end + lemma primitive_part_mult: fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" shows "primitive_part (p * q) = primitive_part p * primitive_part q"

--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Wed Aug 22 16:41:29 2018 +0200 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Wed Aug 22 13:33:50 2018 +0000 @@ -346,48 +346,6 @@ qed (insert A, auto simp: prime_elem_def is_unit_poly_iff) qed (auto intro: lift_prime_elem_poly) -context -begin - -private lemma content_1_mult: - fixes f g :: "'a :: {semiring_Gcd,factorial_semiring} poly" - assumes "content f = 1" "content g = 1" - shows "content (f * g) = 1" -proof (cases "f * g = 0") - case False - from assms have "f \<noteq> 0" "g \<noteq> 0" by auto - - hence "f * g \<noteq> 0" by auto - { - assume "\<not>is_unit (content (f * g))" - with False have "\<exists>p. p dvd content (f * g) \<and> prime p" - by (intro prime_divisor_exists) simp_all - then obtain p where "p dvd content (f * g)" "prime p" by blast - from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g" - by (simp add: const_poly_dvd_iff_dvd_content) - moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) - ultimately have "[:p:] dvd f \<or> [:p:] dvd g" - by (simp add: prime_elem_dvd_mult_iff) - with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) - with \<open>prime p\<close> have False by simp - } - hence "is_unit (content (f * g))" by blast - hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content) - thus ?thesis by simp -qed (insert assms, auto) - -lemma content_mult: - fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" - shows "content (p * q) = content p * content q" -proof - - from content_decompose[of p] guess p' . note p = this - from content_decompose[of q] guess q' . note q = this - have "content (p * q) = content p * content q * content (p' * q')" - by (subst p, subst q) (simp add: mult_ac normalize_mult) - also from p q have "content (p' * q') = 1" by (intro content_1_mult) - finally show ?thesis by simp -qed - lemma fract_poly_dvdD: fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly" assumes "fract_poly p dvd fract_poly q" "content p = 1" @@ -407,8 +365,6 @@ thus ?thesis by (rule dvdI) qed -end - subsection \<open>Polynomials over a field are a Euclidean ring\<close>