--- 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>