msetprod based directly on Multiset.fold;
authorhaftmann
Thu Oct 11 11:56:43 2012 +0200 (2012-10-11)
changeset 49824c26665a197dc
parent 49823 1c146fa7701e
child 49825 bb5db3d1d6dd
msetprod based directly on Multiset.fold;
pretty syntax for msetprod_image
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Power.thy
     1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Oct 11 11:56:43 2012 +0200
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Oct 11 11:56:43 2012 +0200
     1.3 @@ -36,54 +36,66 @@
     1.4     "ALL i :# M. P i"? 
     1.5  *)
     1.6  
     1.7 -definition (in comm_monoid_mult) msetprod :: "'a multiset \<Rightarrow> 'a"
     1.8 +context comm_monoid_mult
     1.9 +begin
    1.10 +
    1.11 +definition msetprod :: "'a multiset \<Rightarrow> 'a"
    1.12  where
    1.13 +  "msetprod M = Multiset.fold times 1 M"
    1.14 +
    1.15 +lemma msetprod_empty [simp]:
    1.16 +  "msetprod {#} = 1"
    1.17 +  by (simp add: msetprod_def)
    1.18 +
    1.19 +lemma msetprod_singleton [simp]:
    1.20 +  "msetprod {#x#} = x"
    1.21 +proof -
    1.22 +  interpret comp_fun_commute times
    1.23 +    by (fact comp_fun_commute)
    1.24 +  show ?thesis by (simp add: msetprod_def)
    1.25 +qed
    1.26 +
    1.27 +lemma msetprod_Un [simp]:
    1.28 +  "msetprod (A + B) = msetprod A * msetprod B" 
    1.29 +proof -
    1.30 +  interpret comp_fun_commute times
    1.31 +    by (fact comp_fun_commute)
    1.32 +  show ?thesis by (induct B) (simp_all add: msetprod_def mult_ac)
    1.33 +qed
    1.34 +
    1.35 +lemma msetprod_multiplicity:
    1.36    "msetprod M = setprod (\<lambda>x. x ^ count M x) (set_of M)"
    1.37 +  by (simp add: msetprod_def setprod_def Multiset.fold_def fold_image_def funpow_times_power)
    1.38  
    1.39 -abbreviation (in comm_monoid_mult) msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
    1.40 +abbreviation msetprod_image :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b multiset \<Rightarrow> 'a"
    1.41  where
    1.42    "msetprod_image f M \<equiv> msetprod (image_mset f M)"
    1.43  
    1.44 +end
    1.45 +
    1.46  syntax
    1.47    "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
    1.48        ("(3PROD _:#_. _)" [0, 51, 10] 10)
    1.49  
    1.50 +syntax (xsymbols)
    1.51 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
    1.52 +      ("(3\<Pi>_\<in>#_. _)" [0, 51, 10] 10)
    1.53 +
    1.54 +syntax (HTML output)
    1.55 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult" 
    1.56 +      ("(3\<Pi>_\<in>#_. _)" [0, 51, 10] 10)
    1.57 +
    1.58  translations
    1.59    "PROD i :# A. b" == "CONST msetprod_image (\<lambda>i. b) A"
    1.60  
    1.61 -lemma msetprod_empty: "msetprod {#} = 1"
    1.62 -  by (simp add: msetprod_def)
    1.63 -
    1.64 -lemma msetprod_singleton: "msetprod {#x#} = x"
    1.65 -  by (simp add: msetprod_def)
    1.66 -
    1.67 -lemma msetprod_Un: "msetprod (A + B) = msetprod A * msetprod B" 
    1.68 -  apply (simp add: msetprod_def power_add)
    1.69 -  apply (subst setprod_Un2)
    1.70 -  apply auto
    1.71 -  apply (subgoal_tac 
    1.72 -      "(PROD x:set_of A - set_of B. x ^ count A x * x ^ count B x) =
    1.73 -       (PROD x:set_of A - set_of B. x ^ count A x)")
    1.74 -  apply (erule ssubst)
    1.75 -  apply (subgoal_tac 
    1.76 -      "(PROD x:set_of B - set_of A. x ^ count A x * x ^ count B x) =
    1.77 -       (PROD x:set_of B - set_of A. x ^ count B x)")
    1.78 -  apply (erule ssubst)
    1.79 -  apply (subgoal_tac "(PROD x:set_of A. x ^ count A x) = 
    1.80 -    (PROD x:set_of A - set_of B. x ^ count A x) *
    1.81 -    (PROD x:set_of A Int set_of B. x ^ count A x)")
    1.82 -  apply (erule ssubst)
    1.83 -  apply (subgoal_tac "(PROD x:set_of B. x ^ count B x) = 
    1.84 -    (PROD x:set_of B - set_of A. x ^ count B x) *
    1.85 -    (PROD x:set_of A Int set_of B. x ^ count B x)")
    1.86 -  apply (erule ssubst)
    1.87 -  apply (subst setprod_timesf)
    1.88 -  apply (force simp add: mult_ac)
    1.89 -  apply (subst setprod_Un_disjoint [symmetric])
    1.90 -  apply (auto intro: setprod_cong)
    1.91 -  apply (subst setprod_Un_disjoint [symmetric])
    1.92 -  apply (auto intro: setprod_cong)
    1.93 -  done
    1.94 +lemma (in comm_semiring_1) dvd_msetprod:
    1.95 +  assumes "x \<in># A"
    1.96 +  shows "x dvd msetprod A"
    1.97 +proof -
    1.98 +  from assms have "A = (A - {#x#}) + {#x#}" by simp
    1.99 +  then obtain B where "A = B + {#x#}" ..
   1.100 +  then show ?thesis by simp
   1.101 +qed
   1.102  
   1.103  
   1.104  subsection {* unique factorization: multiset version *}
   1.105 @@ -104,7 +116,7 @@
   1.106    } moreover {
   1.107      assume "n > 1" and "prime n"
   1.108      then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)"
   1.109 -      by (auto simp add: msetprod_def)
   1.110 +      by auto
   1.111    } moreover {
   1.112      assume "n > 1" and "~ prime n"
   1.113      with not_prime_eq_prod_nat
   1.114 @@ -132,10 +144,10 @@
   1.115    assume M: "a : set_of M"
   1.116    with assms have a: "prime a" by auto
   1.117    with M have "a ^ count M a dvd (PROD i :# M. i)"
   1.118 -    by (auto intro: dvd_setprod simp add: msetprod_def)
   1.119 +    by (auto simp add: msetprod_multiplicity intro: dvd_setprod)
   1.120    also have "... dvd (PROD i :# N. i)" by (rule assms)
   1.121    also have "... = (PROD i : (set_of N). i ^ (count N i))"
   1.122 -    by (simp add: msetprod_def)
   1.123 +    by (simp add: msetprod_multiplicity)
   1.124    also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))"
   1.125    proof (cases)
   1.126      assume "a : set_of N"
   1.127 @@ -330,7 +342,7 @@
   1.128  lemma prime_factorization_nat: "(n::nat) > 0 \<Longrightarrow> 
   1.129      n = (PROD p : prime_factors n. p^(multiplicity p n))"
   1.130    apply (frule multiset_prime_factorization)
   1.131 -  apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def)
   1.132 +  apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity)
   1.133    done
   1.134  
   1.135  lemma prime_factorization_int: 
   1.136 @@ -363,7 +375,7 @@
   1.137      apply force
   1.138      apply force
   1.139      using assms
   1.140 -    apply (simp add: Abs_multiset_inverse set_of_def msetprod_def)
   1.141 +    apply (simp add: Abs_multiset_inverse set_of_def msetprod_multiplicity)
   1.142      done
   1.143    with `f \<in> multiset` have "count (multiset_prime_factorization n) = f"
   1.144      by (simp add: Abs_multiset_inverse)
     2.1 --- a/src/HOL/Power.thy	Thu Oct 11 11:56:43 2012 +0200
     2.2 +++ b/src/HOL/Power.thy	Thu Oct 11 11:56:43 2012 +0200
     2.3 @@ -90,6 +90,19 @@
     2.4    unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right
     2.5    unfolding power_Suc power_add Let_def mult_assoc ..
     2.6  
     2.7 +lemma funpow_times_power:
     2.8 +  "(times x ^^ f x) = times (x ^ f x)"
     2.9 +proof (induct "f x" arbitrary: f)
    2.10 +  case 0 then show ?case by (simp add: fun_eq_iff)
    2.11 +next
    2.12 +  case (Suc n)
    2.13 +  def g \<equiv> "\<lambda>x. f x - 1"
    2.14 +  with Suc have "n = g x" by simp
    2.15 +  with Suc have "times x ^^ g x = times (x ^ g x)" by simp
    2.16 +  moreover from Suc g_def have "f x = g x + 1" by simp
    2.17 +  ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc)
    2.18 +qed
    2.19 +
    2.20  end
    2.21  
    2.22  context comm_monoid_mult
    2.23 @@ -727,3 +740,4 @@
    2.24    Power Arith
    2.25  
    2.26  end
    2.27 +