src/HOL/Library/Polynomial_Factorial.thy

 
 subsection \<open>Various facts about polynomials\<close>
 
 lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
   by (induction A) (simp_all add: one_poly_def mult_ac)
-
-lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
-proof -
-  have "smult c p = [:c:] * p" by simp
-  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
-  proof safe
-    assume A: "[:c:] * p dvd 1"
-    thus "p dvd 1" by (rule dvd_mult_right)
-    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
-    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
-    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
-    also note B [symmetric]
-    finally show "c dvd 1" by simp
-  next
-    assume "c dvd 1" "p dvd 1"
-    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
-    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
-    hence "[:c:] dvd 1" by (rule dvdI)
-    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
-  qed
-  finally show ?thesis .
-qed
-
-lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
-  using degree_mod_less[of b a] by auto
-  
-lemma smult_eq_iff:
-  assumes "(b :: 'a :: field) \<noteq> 0"
-  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
-proof
-  assume "smult a p = smult b q"
-  also from assms have "smult (inverse b) \<dots> = q" by simp
-  finally show "smult (a / b) p = q" by (simp add: field_simps)
-qed (insert assms, auto)
 
 lemma irreducible_const_poly_iff:
   fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
   shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
 proof

   by (subst (2) normalize_mult_unit_factor [symmetric, of x])
      (simp del: normalize_mult_unit_factor)
   
 lemma normalize_snd_quot_of_fract: "normalize (snd (quot_of_fract x)) = snd (quot_of_fract x)"
   by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
-
-
-subsection \<open>Content and primitive part of a polynomial\<close>
-
-definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
-  "content p = Gcd (set (coeffs p))"
-
-lemma content_0 [simp]: "content 0 = 0"
-  by (simp add: content_def)
-
-lemma content_1 [simp]: "content 1 = 1"
-  by (simp add: content_def)
-
-lemma content_const [simp]: "content [:c:] = normalize c"
-  by (simp add: content_def cCons_def)
-
-lemma const_poly_dvd_iff_dvd_content:
-  fixes c :: "'a :: semiring_Gcd"
-  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
-proof (cases "p = 0")
-  case [simp]: False
-  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
-  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
-  proof safe
-    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
-    thus "c dvd coeff p n"
-      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
-  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
-  also have "\<dots> \<longleftrightarrow> c dvd content p"
-    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
-          dvd_mult_unit_iff)
-  finally show ?thesis .
-qed simp_all
-
-lemma content_dvd [simp]: "[:content p:] dvd p"
-  by (subst const_poly_dvd_iff_dvd_content) simp_all
-  
-lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
-  by (cases "n \<le> degree p") 
-     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
-
-lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
-  by (simp add: content_def Gcd_dvd)
-
-lemma normalize_content [simp]: "normalize (content p) = content p"
-  by (simp add: content_def)
-
-lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
-proof
-  assume "is_unit (content p)"
-  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
-  thus "content p = 1" by simp
-qed auto
-
-lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
-  by (simp add: content_def coeffs_smult Gcd_mult)
-
-lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
-  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
-
-definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
-  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
-  
-lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
-  by (simp add: primitive_part_def)
-
-lemma content_times_primitive_part [simp]:
-  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
-  shows "smult (content p) (primitive_part p) = p"
-proof (cases "p = 0")
-  case False
-  thus ?thesis
-  unfolding primitive_part_def
-  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs 
-           intro: map_poly_idI)
-qed simp_all
-
-lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
-proof (cases "p = 0")
-  case False
-  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
-    by (simp add:  primitive_part_def)
-  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
-    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
-  finally show ?thesis using False by simp
-qed simp
-
-lemma content_primitive_part [simp]:
-  assumes "p \<noteq> 0"
-  shows   "content (primitive_part p) = 1"
-proof -
-  have "p = smult (content p) (primitive_part p)" by simp
-  also have "content \<dots> = content p * content (primitive_part p)" 
-    by (simp del: content_times_primitive_part)
-  finally show ?thesis using assms by simp
-qed
-
-lemma content_decompose:
-  fixes p :: "'a :: semiring_Gcd poly"
-  obtains p' where "p = smult (content p) p'" "content p' = 1"
-proof (cases "p = 0")
-  case True
-  thus ?thesis by (intro that[of 1]) simp_all
-next
-  case False
-  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule 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
-qed
-
-lemma smult_content_normalize_primitive_part [simp]:
-  "smult (content p) (normalize (primitive_part p)) = normalize p"
-proof -
-  have "smult (content p) (normalize (primitive_part p)) = 
-          normalize ([:content p:] * primitive_part p)" 
-    by (subst normalize_mult) (simp_all add: normalize_const_poly)
-  also have "[:content p:] * primitive_part p = p" by simp
-  finally 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
-  
-lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
-  by (simp add: primitive_part_def map_poly_pCons)
- 
-lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
-  by (auto simp: primitive_part_def)
-  
-lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
-proof (cases "p = 0")
-  case False
-  have "p = smult (content p) (primitive_part p)" by simp
-  also from False have "degree \<dots> = degree (primitive_part p)"
-    by (subst degree_smult_eq) simp_all
-  finally show ?thesis ..
-qed simp_all
 
 
 subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
 
 abbreviation (input) fract_poly