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