src/HOL/Library/Polynomial_Factorial.thy
changeset 63830 2ea3725a34bd
parent 63764 f3ad26c4b2d9
child 63905 1c3dcb5fe6cb
     1.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 09 14:15:16 2016 +0200
     1.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Fri Sep 09 15:12:40 2016 +0200
     1.3 @@ -16,11 +16,11 @@
     1.4  
     1.5  subsection \<open>Prelude\<close>
     1.6  
     1.7 -lemma msetprod_mult: 
     1.8 -  "msetprod (image_mset (\<lambda>x. f x * g x) A) = msetprod (image_mset f A) * msetprod (image_mset g A)"
     1.9 +lemma prod_mset_mult: 
    1.10 +  "prod_mset (image_mset (\<lambda>x. f x * g x) A) = prod_mset (image_mset f A) * prod_mset (image_mset g A)"
    1.11    by (induction A) (simp_all add: mult_ac)
    1.12    
    1.13 -lemma msetprod_const: "msetprod (image_mset (\<lambda>_. c) A) = c ^ size A"
    1.14 +lemma prod_mset_const: "prod_mset (image_mset (\<lambda>_. c) A) = c ^ size A"
    1.15    by (induction A) (simp_all add: mult_ac)
    1.16    
    1.17  lemma dvd_field_iff: "x dvd y \<longleftrightarrow> (x = 0 \<longrightarrow> y = (0::'a::field))"
    1.18 @@ -341,7 +341,7 @@
    1.19  
    1.20  subsection \<open>Various facts about polynomials\<close>
    1.21  
    1.22 -lemma msetprod_const_poly: "msetprod (image_mset (\<lambda>x. [:f x:]) A) = [:msetprod (image_mset f A):]"
    1.23 +lemma prod_mset_const_poly: "prod_mset (image_mset (\<lambda>x. [:f x:]) A) = [:prod_mset (image_mset f A):]"
    1.24    by (induction A) (simp_all add: one_poly_def mult_ac)
    1.25  
    1.26  lemma degree_mod_less': "b \<noteq> 0 \<Longrightarrow> a mod b \<noteq> 0 \<Longrightarrow> degree (a mod b) < degree b"
    1.27 @@ -679,8 +679,8 @@
    1.28  lemma fract_poly_dvd: "p dvd q \<Longrightarrow> fract_poly p dvd fract_poly q"
    1.29    by (auto elim!: dvdE)
    1.30  
    1.31 -lemma msetprod_fract_poly: 
    1.32 -  "msetprod (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (msetprod (image_mset f A))"
    1.33 +lemma prod_mset_fract_poly: 
    1.34 +  "prod_mset (image_mset (\<lambda>x. fract_poly (f x)) A) = fract_poly (prod_mset (image_mset f A))"
    1.35    by (induction A) (simp_all add: mult_ac)
    1.36    
    1.37  lemma is_unit_fract_poly_iff:
    1.38 @@ -961,9 +961,9 @@
    1.39    shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
    1.40    by (auto elim!: dvdE simp: primitive_part_mult)
    1.41  
    1.42 -lemma content_msetprod: 
    1.43 +lemma content_prod_mset: 
    1.44    fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
    1.45 -  shows "content (msetprod A) = msetprod (image_mset content A)"
    1.46 +  shows "content (prod_mset A) = prod_mset (image_mset content A)"
    1.47    by (induction A) (simp_all add: content_mult mult_ac)
    1.48  
    1.49  lemma fract_poly_dvdD:
    1.50 @@ -1046,14 +1046,14 @@
    1.51        comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
    1.52  qed
    1.53  
    1.54 -lemma field_poly_msetprod_prime_factorization:
    1.55 +lemma field_poly_prod_mset_prime_factorization:
    1.56    assumes "(x :: 'a :: field poly) \<noteq> 0"
    1.57 -  shows   "msetprod (field_poly.prime_factorization x) = normalize_field_poly x"
    1.58 +  shows   "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x"
    1.59  proof -
    1.60    have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
    1.61 -  have "comm_monoid_mult.msetprod op * (1 :: 'a poly) = msetprod"
    1.62 -    by (intro ext) (simp add: comm_monoid_mult.msetprod_def[OF A] msetprod_def)
    1.63 -  with field_poly.msetprod_prime_factorization[OF assms] show ?thesis by simp
    1.64 +  have "comm_monoid_mult.prod_mset op * (1 :: 'a poly) = prod_mset"
    1.65 +    by (intro ext) (simp add: comm_monoid_mult.prod_mset_def[OF A] prod_mset_def)
    1.66 +  with field_poly.prod_mset_prime_factorization[OF assms] show ?thesis by simp
    1.67  qed
    1.68  
    1.69  lemma field_poly_in_prime_factorization_imp_prime:
    1.70 @@ -1248,32 +1248,32 @@
    1.71  private lemma poly_prime_factorization_exists_content_1:
    1.72    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
    1.73    assumes "p \<noteq> 0" "content p = 1"
    1.74 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
    1.75 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
    1.76  proof -
    1.77    let ?P = "field_poly.prime_factorization (fract_poly p)"
    1.78 -  define c where "c = msetprod (image_mset fract_content ?P)"
    1.79 +  define c where "c = prod_mset (image_mset fract_content ?P)"
    1.80    define c' where "c' = c * to_fract (lead_coeff p)"
    1.81 -  define e where "e = msetprod (image_mset primitive_part_fract ?P)"
    1.82 +  define e where "e = prod_mset (image_mset primitive_part_fract ?P)"
    1.83    define A where "A = image_mset (normalize \<circ> primitive_part_fract) ?P"
    1.84    have "content e = (\<Prod>x\<in>#field_poly.prime_factorization (map_poly to_fract p). 
    1.85                        content (primitive_part_fract x))"
    1.86 -    by (simp add: e_def content_msetprod multiset.map_comp o_def)
    1.87 +    by (simp add: e_def content_prod_mset multiset.map_comp o_def)
    1.88    also have "image_mset (\<lambda>x. content (primitive_part_fract x)) ?P = image_mset (\<lambda>_. 1) ?P"
    1.89      by (intro image_mset_cong content_primitive_part_fract) auto
    1.90 -  finally have content_e: "content e = 1" by (simp add: msetprod_const)    
    1.91 +  finally have content_e: "content e = 1" by (simp add: prod_mset_const)    
    1.92    
    1.93    have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
    1.94            normalize_field_poly (fract_poly p)" by simp
    1.95    also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
    1.96      by (simp add: unit_factor_field_poly_def lead_coeff_def monom_0 degree_map_poly coeff_map_poly)
    1.97 -  also from assms have "normalize_field_poly (fract_poly p) = msetprod ?P" 
    1.98 -    by (subst field_poly_msetprod_prime_factorization) simp_all
    1.99 -  also have "\<dots> = msetprod (image_mset id ?P)" by simp
   1.100 +  also from assms have "normalize_field_poly (fract_poly p) = prod_mset ?P" 
   1.101 +    by (subst field_poly_prod_mset_prime_factorization) simp_all
   1.102 +  also have "\<dots> = prod_mset (image_mset id ?P)" by simp
   1.103    also have "image_mset id ?P = 
   1.104                 image_mset (\<lambda>x. [:fract_content x:] * fract_poly (primitive_part_fract x)) ?P"
   1.105      by (intro image_mset_cong) (auto simp: content_times_primitive_part_fract)
   1.106 -  also have "msetprod \<dots> = smult c (fract_poly e)"
   1.107 -    by (subst msetprod_mult) (simp_all add: msetprod_fract_poly msetprod_const_poly c_def e_def)
   1.108 +  also have "prod_mset \<dots> = smult c (fract_poly e)"
   1.109 +    by (subst prod_mset_mult) (simp_all add: prod_mset_fract_poly prod_mset_const_poly c_def e_def)
   1.110    also have "[:to_fract (lead_coeff p):] * \<dots> = smult c' (fract_poly e)"
   1.111      by (simp add: c'_def)
   1.112    finally have eq: "fract_poly p = smult c' (fract_poly e)" .
   1.113 @@ -1291,28 +1291,28 @@
   1.114    hence "p = [:b:] * e" by simp
   1.115    with b have "normalize p = normalize e" 
   1.116      by (simp only: normalize_mult) (simp add: is_unit_normalize is_unit_poly_iff)
   1.117 -  also have "normalize e = msetprod A"
   1.118 -    by (simp add: multiset.map_comp e_def A_def normalize_msetprod)
   1.119 -  finally have "msetprod A = normalize p" ..
   1.120 +  also have "normalize e = prod_mset A"
   1.121 +    by (simp add: multiset.map_comp e_def A_def normalize_prod_mset)
   1.122 +  finally have "prod_mset A = normalize p" ..
   1.123    
   1.124    have "prime_elem p" if "p \<in># A" for p
   1.125      using that by (auto simp: A_def prime_elem_primitive_part_fract prime_elem_imp_irreducible 
   1.126                          dest!: field_poly_in_prime_factorization_imp_prime )
   1.127 -  from this and \<open>msetprod A = normalize p\<close> show ?thesis
   1.128 +  from this and \<open>prod_mset A = normalize p\<close> show ?thesis
   1.129      by (intro exI[of _ A]) blast
   1.130  qed
   1.131  
   1.132  lemma poly_prime_factorization_exists:
   1.133    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   1.134    assumes "p \<noteq> 0"
   1.135 -  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize p"
   1.136 +  shows   "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize p"
   1.137  proof -
   1.138    define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
   1.139 -  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> msetprod A = normalize (primitive_part p)"
   1.140 +  have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
   1.141      by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
   1.142    then guess A by (elim exE conjE) note A = this
   1.143 -  moreover from assms have "msetprod B = [:content p:]"
   1.144 -    by (simp add: B_def msetprod_const_poly msetprod_prime_factorization)
   1.145 +  moreover from assms have "prod_mset B = [:content p:]"
   1.146 +    by (simp add: B_def prod_mset_const_poly prod_mset_prime_factorization)
   1.147    moreover have "\<forall>p. p \<in># B \<longrightarrow> prime_elem p"
   1.148      by (auto simp: B_def intro: lift_prime_elem_poly dest: in_prime_factorization_imp_prime)
   1.149    ultimately show ?thesis by (intro exI[of _ "B + A"]) auto