4544 with assms show ?thesis |
4544 with assms show ?thesis |
4545 by simp |
4545 by simp |
4546 qed |
4546 qed |
4547 |
4547 |
4548 lemma content_decompose: |
4548 lemma content_decompose: |
4549 obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1" |
4549 obtains p' :: "'a::semiring_gcd poly" |
|
4550 where "p = smult (content p) p'" "content p' = 1" |
4550 proof (cases "p = 0") |
4551 proof (cases "p = 0") |
4551 case True |
4552 case True |
4552 then show ?thesis by (intro that[of 1]) simp_all |
4553 then have "p = smult (content p) 1" "content 1 = 1" |
|
4554 by simp_all |
|
4555 then show ?thesis .. |
4553 next |
4556 next |
4554 case False |
4557 case False |
4555 from content_dvd[of p] obtain r where r: "p = [:content p:] * r" |
4558 then have "p = smult (content p) (primitive_part p)" "content (primitive_part p) = 1" |
4556 by (rule dvdE) |
4559 by simp_all |
4557 have "content p * 1 = content p * content r" |
4560 then show ?thesis .. |
4558 by (subst r) simp |
4561 qed |
4559 with False have "content r = 1" |
4562 |
4560 by (subst (asm) mult_left_cancel) simp_all |
|
4561 with r show ?thesis |
|
4562 by (intro that[of r]) simp_all |
|
4563 qed |
|
4564 |
|
4565 lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q" |
4563 lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q" |
4566 using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast |
4564 using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast |
4567 |
4565 |
4568 lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]" |
4566 lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]" |
4569 by (simp add: primitive_part_def map_poly_pCons) |
4567 by (simp add: primitive_part_def map_poly_pCons) |
4592 by (subst normalize_mult) (simp_all add: normalize_const_poly) |
4590 by (subst normalize_mult) (simp_all add: normalize_const_poly) |
4593 also have "[:content p:] * primitive_part p = p" by simp |
4591 also have "[:content p:] * primitive_part p = p" by simp |
4594 finally show ?thesis . |
4592 finally show ?thesis . |
4595 qed |
4593 qed |
4596 |
4594 |
|
4595 context |
|
4596 begin |
|
4597 |
|
4598 private |
|
4599 |
|
4600 lemma content_1_mult: |
|
4601 fixes f g :: "'a :: {semiring_gcd, factorial_semiring} poly" |
|
4602 assumes "content f = 1" "content g = 1" |
|
4603 shows "content (f * g) = 1" |
|
4604 proof (cases "f * g = 0") |
|
4605 case False |
|
4606 from assms have "f \<noteq> 0" "g \<noteq> 0" by auto |
|
4607 |
|
4608 hence "f * g \<noteq> 0" by auto |
|
4609 { |
|
4610 assume "\<not>is_unit (content (f * g))" |
|
4611 with False have "\<exists>p. p dvd content (f * g) \<and> prime p" |
|
4612 by (intro prime_divisor_exists) simp_all |
|
4613 then obtain p where "p dvd content (f * g)" "prime p" by blast |
|
4614 from \<open>p dvd content (f * g)\<close> have "[:p:] dvd f * g" |
|
4615 by (simp add: const_poly_dvd_iff_dvd_content) |
|
4616 moreover from \<open>prime p\<close> have "prime_elem [:p:]" by (simp add: lift_prime_elem_poly) |
|
4617 ultimately have "[:p:] dvd f \<or> [:p:] dvd g" |
|
4618 by (simp add: prime_elem_dvd_mult_iff) |
|
4619 with assms have "is_unit p" by (simp add: const_poly_dvd_iff_dvd_content) |
|
4620 with \<open>prime p\<close> have False by simp |
|
4621 } |
|
4622 hence "is_unit (content (f * g))" by blast |
|
4623 hence "normalize (content (f * g)) = 1" by (simp add: is_unit_normalize del: normalize_content) |
|
4624 thus ?thesis by simp |
|
4625 qed (insert assms, auto) |
|
4626 |
4597 lemma content_mult: |
4627 lemma content_mult: |
4598 fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly" |
4628 fixes p q :: "'a :: {factorial_semiring, semiring_gcd} poly" |
4599 shows "content (p * q) = content p * content q" |
4629 shows "content (p * q) = content p * content q" |
4600 proof - |
4630 proof (cases "p * q = 0") |
4601 from content_decompose[of p] guess p' . note p = this |
4631 case False |
4602 from content_decompose[of q] guess q' . note q = this |
4632 then have "p \<noteq> 0" and "q \<noteq> 0" |
4603 have "content (p * q) = content p * content q * content (p' * q')" |
4633 by simp_all |
4604 by (subst p, subst q) (simp add: mult_ac normalize_mult) |
4634 then have *: "content (primitive_part p * primitive_part q) = 1" |
4605 also have "content (p' * q') = 1" |
4635 by (auto intro: content_1_mult) |
4606 proof (cases "p' * q' = 0") |
4636 have "p * q = smult (content p) (primitive_part p) * smult (content q) (primitive_part q)" |
4607 case True |
|
4608 with \<open>content p' = 1\<close> \<open>content q' = 1\<close> show ?thesis |
|
4609 by auto |
|
4610 next |
|
4611 case False |
|
4612 from \<open>content p' = 1\<close> \<open>content q' = 1\<close> |
|
4613 have "p' \<noteq> 0" "q' \<noteq> 0" |
|
4614 by auto |
|
4615 then have "p' * q' \<noteq> 0" |
|
4616 by auto |
|
4617 have "is_unit (content (p' * q'))" |
|
4618 proof (rule ccontr) |
|
4619 assume "\<not> is_unit (content (p' * q'))" |
|
4620 with False have "\<exists>p. p dvd content (p' * q') \<and> prime p" |
|
4621 by (intro prime_divisor_exists) simp_all |
|
4622 then obtain p where "p dvd content (p' * q')" "prime p" |
|
4623 by blast |
|
4624 from \<open>p dvd content (p' * q')\<close> have "[:p:] dvd p' * q'" |
|
4625 by (simp add: const_poly_dvd_iff_dvd_content) |
|
4626 moreover from \<open>prime p\<close> have "prime_elem [:p:]" |
|
4627 by (simp add: lift_prime_elem_poly) |
|
4628 ultimately have "[:p:] dvd p' \<or> [:p:] dvd q'" |
|
4629 by (simp add: prime_elem_dvd_mult_iff) |
|
4630 with \<open>content p' = 1\<close> \<open>content q' = 1\<close> have "is_unit p" |
|
4631 by (simp add: const_poly_dvd_iff_dvd_content) |
|
4632 with \<open>prime p\<close> show False |
|
4633 by simp |
|
4634 qed |
|
4635 then have "normalize (content (p' * q')) = 1" |
|
4636 by (simp add: is_unit_normalize del: normalize_content) |
|
4637 then show ?thesis |
|
4638 by simp |
|
4639 qed |
|
4640 finally show ?thesis |
|
4641 by simp |
4637 by simp |
4642 qed |
4638 also have "\<dots> = smult (content p * content q) (primitive_part p * primitive_part q)" |
|
4639 by (metis mult.commute mult_smult_right smult_smult) |
|
4640 with * show ?thesis |
|
4641 by (simp add: normalize_mult) |
|
4642 next |
|
4643 case True |
|
4644 then show ?thesis |
|
4645 by auto |
|
4646 qed |
|
4647 |
|
4648 end |
4643 |
4649 |
4644 lemma primitive_part_mult: |
4650 lemma primitive_part_mult: |
4645 fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" |
4651 fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly" |
4646 shows "primitive_part (p * q) = primitive_part p * primitive_part q" |
4652 shows "primitive_part (p * q) = primitive_part p * primitive_part q" |
4647 proof - |
4653 proof - |