src/HOL/Library/Polynomial_Factorial.thy
 changeset 64795 8e7db8df16a0 parent 64794 6f7391f28197 child 64848 c50db2128048
```     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Thu Jan 05 14:49:21 2017 +0100
1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Thu Jan 05 17:11:21 2017 +0100
1.3 @@ -19,40 +19,6 @@
1.4  lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
1.5    by (induction A) (simp_all add: one_poly_def mult_ac)
1.6
1.7 -lemma is_unit_smult_iff: "smult c p dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
1.8 -proof -
1.9 -  have "smult c p = [:c:] * p" by simp
1.10 -  also have "\<dots> dvd 1 \<longleftrightarrow> c dvd 1 \<and> p dvd 1"
1.11 -  proof safe
1.12 -    assume A: "[:c:] * p dvd 1"
1.13 -    thus "p dvd 1" by (rule dvd_mult_right)
1.14 -    from A obtain q where B: "1 = [:c:] * p * q" by (erule dvdE)
1.15 -    have "c dvd c * (coeff p 0 * coeff q 0)" by simp
1.16 -    also have "\<dots> = coeff ([:c:] * p * q) 0" by (simp add: mult.assoc coeff_mult)
1.17 -    also note B [symmetric]
1.18 -    finally show "c dvd 1" by simp
1.19 -  next
1.20 -    assume "c dvd 1" "p dvd 1"
1.21 -    from \<open>c dvd 1\<close> obtain d where "1 = c * d" by (erule dvdE)
1.22 -    hence "1 = [:c:] * [:d:]" by (simp add: one_poly_def mult_ac)
1.23 -    hence "[:c:] dvd 1" by (rule dvdI)
1.24 -    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1" by simp
1.25 -  qed
1.26 -  finally show ?thesis .
1.27 -qed
1.28 -
1.29 -lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
1.30 -  using degree_mod_less[of b a] by auto
1.31 -
1.32 -lemma smult_eq_iff:
1.33 -  assumes "(b :: 'a :: field) \<noteq> 0"
1.34 -  shows   "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q"
1.35 -proof
1.36 -  assume "smult a p = smult b q"
1.37 -  also from assms have "smult (inverse b) \<dots> = q" by simp
1.38 -  finally show "smult (a / b) p = q" by (simp add: field_simps)
1.39 -qed (insert assms, auto)
1.40 -
1.41  lemma irreducible_const_poly_iff:
1.42    fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
1.43    shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
1.44 @@ -160,145 +126,6 @@
1.45    by (intro unit_factor_1_imp_normalized unit_factor_snd_quot_of_fract)
1.46
1.47
1.48 -subsection \<open>Content and primitive part of a polynomial\<close>
1.49 -
1.50 -definition content :: "('a :: semiring_Gcd poly) \<Rightarrow> 'a" where
1.51 -  "content p = Gcd (set (coeffs p))"
1.52 -
1.53 -lemma content_0 [simp]: "content 0 = 0"
1.54 -  by (simp add: content_def)
1.55 -
1.56 -lemma content_1 [simp]: "content 1 = 1"
1.57 -  by (simp add: content_def)
1.58 -
1.59 -lemma content_const [simp]: "content [:c:] = normalize c"
1.60 -  by (simp add: content_def cCons_def)
1.61 -
1.62 -lemma const_poly_dvd_iff_dvd_content:
1.63 -  fixes c :: "'a :: semiring_Gcd"
1.64 -  shows "[:c:] dvd p \<longleftrightarrow> c dvd content p"
1.65 -proof (cases "p = 0")
1.66 -  case [simp]: False
1.67 -  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)" by (rule const_poly_dvd_iff)
1.68 -  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
1.69 -  proof safe
1.70 -    fix n :: nat assume "\<forall>a\<in>set (coeffs p). c dvd a"
1.71 -    thus "c dvd coeff p n"
1.72 -      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
1.73 -  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
1.74 -  also have "\<dots> \<longleftrightarrow> c dvd content p"
1.75 -    by (simp add: content_def dvd_Gcd_iff mult.commute [of "unit_factor x" for x]
1.76 -          dvd_mult_unit_iff)
1.77 -  finally show ?thesis .
1.78 -qed simp_all
1.79 -
1.80 -lemma content_dvd [simp]: "[:content p:] dvd p"
1.81 -  by (subst const_poly_dvd_iff_dvd_content) simp_all
1.82 -
1.83 -lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
1.84 -  by (cases "n \<le> degree p")
1.85 -     (auto simp: content_def coeffs_def not_le coeff_eq_0 simp del: upt_Suc intro: Gcd_dvd)
1.86 -
1.87 -lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
1.88 -  by (simp add: content_def Gcd_dvd)
1.89 -
1.90 -lemma normalize_content [simp]: "normalize (content p) = content p"
1.91 -  by (simp add: content_def)
1.92 -
1.93 -lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
1.94 -proof
1.95 -  assume "is_unit (content p)"
1.96 -  hence "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
1.97 -  thus "content p = 1" by simp
1.98 -qed auto
1.99 -
1.100 -lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
1.101 -  by (simp add: content_def coeffs_smult Gcd_mult)
1.102 -
1.103 -lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
1.104 -  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
1.105 -
1.106 -definition primitive_part :: "'a :: {semiring_Gcd,idom_divide} poly \<Rightarrow> 'a poly" where
1.107 -  "primitive_part p = (if p = 0 then 0 else map_poly (\<lambda>x. x div content p) p)"
1.108 -
1.109 -lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
1.110 -  by (simp add: primitive_part_def)
1.111 -
1.112 -lemma content_times_primitive_part [simp]:
1.113 -  fixes p :: "'a :: {idom_divide, semiring_Gcd} poly"
1.114 -  shows "smult (content p) (primitive_part p) = p"
1.115 -proof (cases "p = 0")
1.116 -  case False
1.117 -  thus ?thesis
1.118 -  unfolding primitive_part_def
1.119 -  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
1.120 -           intro: map_poly_idI)
1.121 -qed simp_all
1.122 -
1.123 -lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
1.124 -proof (cases "p = 0")
1.125 -  case False
1.126 -  hence "primitive_part p = map_poly (\<lambda>x. x div content p) p"
1.127 -    by (simp add:  primitive_part_def)
1.128 -  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
1.129 -    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
1.130 -  finally show ?thesis using False by simp
1.131 -qed simp
1.132 -
1.133 -lemma content_primitive_part [simp]:
1.134 -  assumes "p \<noteq> 0"
1.135 -  shows   "content (primitive_part p) = 1"
1.136 -proof -
1.137 -  have "p = smult (content p) (primitive_part p)" by simp
1.138 -  also have "content \<dots> = content p * content (primitive_part p)"
1.139 -    by (simp del: content_times_primitive_part)
1.140 -  finally show ?thesis using assms by simp
1.141 -qed
1.142 -
1.143 -lemma content_decompose:
1.144 -  fixes p :: "'a :: semiring_Gcd poly"
1.145 -  obtains p' where "p = smult (content p) p'" "content p' = 1"
1.146 -proof (cases "p = 0")
1.147 -  case True
1.148 -  thus ?thesis by (intro that[of 1]) simp_all
1.149 -next
1.150 -  case False
1.151 -  from content_dvd[of p] obtain r where r: "p = [:content p:] * r" by (erule dvdE)
1.152 -  have "content p * 1 = content p * content r" by (subst r) simp
1.153 -  with False have "content r = 1" by (subst (asm) mult_left_cancel) simp_all
1.154 -  with r show ?thesis by (intro that[of r]) simp_all
1.155 -qed
1.156 -
1.157 -lemma smult_content_normalize_primitive_part [simp]:
1.158 -  "smult (content p) (normalize (primitive_part p)) = normalize p"
1.159 -proof -
1.160 -  have "smult (content p) (normalize (primitive_part p)) =
1.161 -          normalize ([:content p:] * primitive_part p)"
1.162 -    by (subst normalize_mult) (simp_all add: normalize_const_poly)
1.163 -  also have "[:content p:] * primitive_part p = p" by simp
1.164 -  finally show ?thesis .
1.165 -qed
1.166 -
1.167 -lemma content_dvd_contentI [intro]:
1.168 -  "p dvd q \<Longrightarrow> content p dvd content q"
1.169 -  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
1.170 -
1.171 -lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
1.172 -  by (simp add: primitive_part_def map_poly_pCons)
1.173 -
1.174 -lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
1.175 -  by (auto simp: primitive_part_def)
1.176 -
1.177 -lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
1.178 -proof (cases "p = 0")
1.179 -  case False
1.180 -  have "p = smult (content p) (primitive_part p)" by simp
1.181 -  also from False have "degree \<dots> = degree (primitive_part p)"
1.182 -    by (subst degree_smult_eq) simp_all
1.183 -  finally show ?thesis ..
1.184 -qed simp_all
1.185 -
1.186 -
1.187  subsection \<open>Lifting polynomial coefficients to the field of fractions\<close>
1.188
1.189  abbreviation (input) fract_poly
```