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