# HG changeset patch # User haftmann # Date 1349949403 -7200 # Node ID c26665a197dcf6986558fb1b610d0a2188e186cf # Parent 1c146fa7701ecb704e493496622529cd0d9a98dd msetprod based directly on Multiset.fold; pretty syntax for msetprod_image diff -r 1c146fa7701e -r c26665a197dc src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Oct 11 11:56:43 2012 +0200 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Oct 11 11:56:43 2012 +0200 @@ -36,54 +36,66 @@ "ALL i :# M. P i"? *) -definition (in comm_monoid_mult) msetprod :: "'a multiset \ 'a" +context comm_monoid_mult +begin + +definition msetprod :: "'a multiset \ 'a" where + "msetprod M = Multiset.fold times 1 M" + +lemma msetprod_empty [simp]: + "msetprod {#} = 1" + by (simp add: msetprod_def) + +lemma msetprod_singleton [simp]: + "msetprod {#x#} = x" +proof - + interpret comp_fun_commute times + by (fact comp_fun_commute) + show ?thesis by (simp add: msetprod_def) +qed + +lemma msetprod_Un [simp]: + "msetprod (A + B) = msetprod A * msetprod B" +proof - + interpret comp_fun_commute times + by (fact comp_fun_commute) + show ?thesis by (induct B) (simp_all add: msetprod_def mult_ac) +qed + +lemma msetprod_multiplicity: "msetprod M = setprod (\x. x ^ count M x) (set_of M)" + by (simp add: msetprod_def setprod_def Multiset.fold_def fold_image_def funpow_times_power) -abbreviation (in comm_monoid_mult) msetprod_image :: "('b \ 'a) \ 'b multiset \ 'a" +abbreviation msetprod_image :: "('b \ 'a) \ 'b multiset \ 'a" where "msetprod_image f M \ msetprod (image_mset f M)" +end + syntax "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" ("(3PROD _:#_. _)" [0, 51, 10] 10) +syntax (xsymbols) + "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" + ("(3\_\#_. _)" [0, 51, 10] 10) + +syntax (HTML output) + "_msetprod_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_mult" + ("(3\_\#_. _)" [0, 51, 10] 10) + translations "PROD i :# A. b" == "CONST msetprod_image (\i. b) A" -lemma msetprod_empty: "msetprod {#} = 1" - by (simp add: msetprod_def) - -lemma msetprod_singleton: "msetprod {#x#} = x" - by (simp add: msetprod_def) - -lemma msetprod_Un: "msetprod (A + B) = msetprod A * msetprod B" - apply (simp add: msetprod_def power_add) - apply (subst setprod_Un2) - apply auto - apply (subgoal_tac - "(PROD x:set_of A - set_of B. x ^ count A x * x ^ count B x) = - (PROD x:set_of A - set_of B. x ^ count A x)") - apply (erule ssubst) - apply (subgoal_tac - "(PROD x:set_of B - set_of A. x ^ count A x * x ^ count B x) = - (PROD x:set_of B - set_of A. x ^ count B x)") - apply (erule ssubst) - apply (subgoal_tac "(PROD x:set_of A. x ^ count A x) = - (PROD x:set_of A - set_of B. x ^ count A x) * - (PROD x:set_of A Int set_of B. x ^ count A x)") - apply (erule ssubst) - apply (subgoal_tac "(PROD x:set_of B. x ^ count B x) = - (PROD x:set_of B - set_of A. x ^ count B x) * - (PROD x:set_of A Int set_of B. x ^ count B x)") - apply (erule ssubst) - apply (subst setprod_timesf) - apply (force simp add: mult_ac) - apply (subst setprod_Un_disjoint [symmetric]) - apply (auto intro: setprod_cong) - apply (subst setprod_Un_disjoint [symmetric]) - apply (auto intro: setprod_cong) - done +lemma (in comm_semiring_1) dvd_msetprod: + assumes "x \# A" + shows "x dvd msetprod A" +proof - + from assms have "A = (A - {#x#}) + {#x#}" by simp + then obtain B where "A = B + {#x#}" .. + then show ?thesis by simp +qed subsection {* unique factorization: multiset version *} @@ -104,7 +116,7 @@ } moreover { assume "n > 1" and "prime n" then have "(ALL p : set_of {# n #}. prime p) & n = (PROD i :# {# n #}. i)" - by (auto simp add: msetprod_def) + by auto } moreover { assume "n > 1" and "~ prime n" with not_prime_eq_prod_nat @@ -132,10 +144,10 @@ assume M: "a : set_of M" with assms have a: "prime a" by auto with M have "a ^ count M a dvd (PROD i :# M. i)" - by (auto intro: dvd_setprod simp add: msetprod_def) + by (auto simp add: msetprod_multiplicity intro: dvd_setprod) also have "... dvd (PROD i :# N. i)" by (rule assms) also have "... = (PROD i : (set_of N). i ^ (count N i))" - by (simp add: msetprod_def) + by (simp add: msetprod_multiplicity) also have "... = a^(count N a) * (PROD i : (set_of N - {a}). i ^ (count N i))" proof (cases) assume "a : set_of N" @@ -330,7 +342,7 @@ lemma prime_factorization_nat: "(n::nat) > 0 \ n = (PROD p : prime_factors n. p^(multiplicity p n))" apply (frule multiset_prime_factorization) - apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_def) + apply (simp add: prime_factors_nat_def multiplicity_nat_def msetprod_multiplicity) done lemma prime_factorization_int: @@ -363,7 +375,7 @@ apply force apply force using assms - apply (simp add: Abs_multiset_inverse set_of_def msetprod_def) + apply (simp add: Abs_multiset_inverse set_of_def msetprod_multiplicity) done with `f \ multiset` have "count (multiset_prime_factorization n) = f" by (simp add: Abs_multiset_inverse) diff -r 1c146fa7701e -r c26665a197dc src/HOL/Power.thy --- a/src/HOL/Power.thy Thu Oct 11 11:56:43 2012 +0200 +++ b/src/HOL/Power.thy Thu Oct 11 11:56:43 2012 +0200 @@ -90,6 +90,19 @@ unfolding numeral_Bit1 One_nat_def add_Suc_right add_0_right unfolding power_Suc power_add Let_def mult_assoc .. +lemma funpow_times_power: + "(times x ^^ f x) = times (x ^ f x)" +proof (induct "f x" arbitrary: f) + case 0 then show ?case by (simp add: fun_eq_iff) +next + case (Suc n) + def g \ "\x. f x - 1" + with Suc have "n = g x" by simp + with Suc have "times x ^^ g x = times (x ^ g x)" by simp + moreover from Suc g_def have "f x = g x + 1" by simp + ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult_assoc) +qed + end context comm_monoid_mult @@ -727,3 +740,4 @@ Power Arith end +