# HG changeset patch # User wenzelm # Date 1349982139 -7200 # Node ID be66949288a2affe9707296e79704fde763b6bd8 # Parent bb5db3d1d6dda3fb049e2cdd1786f4a2ad676ffa# Parent d15fe10593ff52c842efe4f6a0293682d58b5217 merged diff -r d15fe10593ff -r be66949288a2 NEWS --- a/NEWS Thu Oct 11 20:38:02 2012 +0200 +++ b/NEWS Thu Oct 11 21:02:19 2012 +0200 @@ -62,6 +62,16 @@ *** HOL *** +* Theory "Library/Multiset": + + - Renamed constants + fold_mset ~> Multiset.fold -- for coherence with other fold combinators + + - Renamed facts + fold_mset_commute ~> fold_mset_comm -- for coherence with fold_comm + +INCOMPATIBILITY. + * Theorem UN_o generalized to SUP_comp. INCOMPATIBILITY. * Class "comm_monoid_diff" formalises properties of bounded diff -r d15fe10593ff -r be66949288a2 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Thu Oct 11 20:38:02 2012 +0200 +++ b/src/HOL/Library/Multiset.thy Thu Oct 11 21:02:19 2012 +0200 @@ -657,146 +657,82 @@ subsection {* The fold combinator *} -text {* - The intended behaviour is - @{text "fold_mset f z {#x\<^isub>1, ..., x\<^isub>n#} = f x\<^isub>1 (\ (f x\<^isub>n z)\)"} - if @{text f} is associative-commutative. -*} - -text {* - The graph of @{text "fold_mset"}, @{text "z"}: the start element, - @{text "f"}: folding function, @{text "A"}: the multiset, @{text - "y"}: the result. -*} -inductive - fold_msetG :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b \ bool" - for f :: "'a \ 'b \ 'b" - and z :: 'b +definition fold :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - emptyI [intro]: "fold_msetG f z {#} z" -| insertI [intro]: "fold_msetG f z A y \ fold_msetG f z (A + {#x#}) (f x y)" + "fold f s M = Finite_Set.fold (\x. f x ^^ count M x) s (set_of M)" -inductive_cases empty_fold_msetGE [elim!]: "fold_msetG f z {#} x" -inductive_cases insert_fold_msetGE: "fold_msetG f z (A + {#}) y" - -definition - fold_mset :: "('a \ 'b \ 'b) \ 'b \ 'a multiset \ 'b" where - "fold_mset f z A = (THE x. fold_msetG f z A x)" - -lemma Diff1_fold_msetG: - "fold_msetG f z (A - {#x#}) y \ x \# A \ fold_msetG f z A (f x y)" -apply (frule_tac x = x in fold_msetG.insertI) -apply auto -done - -lemma fold_msetG_nonempty: "\x. fold_msetG f z A x" -apply (induct A) - apply blast -apply clarsimp -apply (drule_tac x = x in fold_msetG.insertI) -apply auto -done - -lemma fold_mset_empty[simp]: "fold_mset f z {#} = z" -unfolding fold_mset_def by blast +lemma fold_mset_empty [simp]: + "fold f s {#} = s" + by (simp add: fold_def) context comp_fun_commute begin -lemma fold_msetG_insertE_aux: - "fold_msetG f z A y \ a \# A \ \y'. y = f a y' \ fold_msetG f z (A - {#a#}) y'" -proof (induct set: fold_msetG) - case (insertI A y x) show ?case - proof (cases "x = a") - assume "x = a" with insertI show ?case by auto +lemma fold_mset_insert: + "fold f s (M + {#x#}) = f x (fold f s M)" +proof - + interpret mset: comp_fun_commute "\y. f y ^^ count M y" + by (fact comp_fun_commute_funpow) + interpret mset_union: comp_fun_commute "\y. f y ^^ count (M + {#x#}) y" + by (fact comp_fun_commute_funpow) + show ?thesis + proof (cases "x \ set_of M") + case False + then have *: "count (M + {#x#}) x = 1" by simp + from False have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s (set_of M) = + Finite_Set.fold (\y. f y ^^ count M y) s (set_of M)" + by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) + with False * show ?thesis + by (simp add: fold_def del: count_union) next - assume "x \ a" - then obtain y' where y: "y = f a y'" and y': "fold_msetG f z (A - {#a#}) y'" - using insertI by auto - have "f x y = f a (f x y')" - unfolding y by (rule fun_left_comm) - moreover have "fold_msetG f z (A + {#x#} - {#a#}) (f x y')" - using y' and `x \ a` - by (simp add: diff_union_swap [symmetric] fold_msetG.insertI) - ultimately show ?case by fast + case True + def N \ "set_of M - {x}" + from N_def True have *: "set_of M = insert x N" "x \ N" "finite N" by auto + then have "Finite_Set.fold (\y. f y ^^ count (M + {#x#}) y) s N = + Finite_Set.fold (\y. f y ^^ count M y) s N" + by (auto intro!: Finite_Set.fold_cong comp_fun_commute_funpow) + with * show ?thesis by (simp add: fold_def del: count_union) simp qed -qed simp - -lemma fold_msetG_insertE: - assumes "fold_msetG f z (A + {#x#}) v" - obtains y where "v = f x y" and "fold_msetG f z A y" -using assms by (auto dest: fold_msetG_insertE_aux [where a=x]) - -lemma fold_msetG_determ: - "fold_msetG f z A x \ fold_msetG f z A y \ y = x" -proof (induct arbitrary: y set: fold_msetG) - case (insertI A y x v) - from `fold_msetG f z (A + {#x#}) v` - obtain y' where "v = f x y'" and "fold_msetG f z A y'" - by (rule fold_msetG_insertE) - from `fold_msetG f z A y'` have "y' = y" by (rule insertI) - with `v = f x y'` show "v = f x y" by simp -qed fast - -lemma fold_mset_equality: "fold_msetG f z A y \ fold_mset f z A = y" -unfolding fold_mset_def by (blast intro: fold_msetG_determ) - -lemma fold_msetG_fold_mset: "fold_msetG f z A (fold_mset f z A)" -proof - - from fold_msetG_nonempty fold_msetG_determ - have "\!x. fold_msetG f z A x" by (rule ex_ex1I) - then show ?thesis unfolding fold_mset_def by (rule theI') qed -lemma fold_mset_insert: - "fold_mset f z (A + {#x#}) = f x (fold_mset f z A)" -by (intro fold_mset_equality fold_msetG.insertI fold_msetG_fold_mset) +corollary fold_mset_single [simp]: + "fold f s {#x#} = f x s" +proof - + have "fold f s ({#} + {#x#}) = f x s" by (simp only: fold_mset_insert) simp + then show ?thesis by simp +qed -lemma fold_mset_commute: "f x (fold_mset f z A) = fold_mset f (f x z) A" -by (induct A) (auto simp: fold_mset_insert fun_left_comm [of x]) - -lemma fold_mset_single [simp]: "fold_mset f z {#x#} = f x z" -using fold_mset_insert [of z "{#}"] by simp +lemma fold_mset_fun_comm: + "f x (fold f s M) = fold f (f x s) M" + by (induct M) (simp_all add: fold_mset_insert fun_left_comm) lemma fold_mset_union [simp]: - "fold_mset f z (A+B) = fold_mset f (fold_mset f z A) B" -proof (induct A) + "fold f s (M + N) = fold f (fold f s M) N" +proof (induct M) case empty then show ?case by simp next - case (add A x) - have "A + {#x#} + B = (A+B) + {#x#}" by (simp add: add_ac) - then have "fold_mset f z (A + {#x#} + B) = f x (fold_mset f z (A + B))" - by (simp add: fold_mset_insert) - also have "\ = fold_mset f (fold_mset f z (A + {#x#})) B" - by (simp add: fold_mset_commute[of x,symmetric] add fold_mset_insert) - finally show ?case . + case (add M x) + have "M + {#x#} + N = (M + N) + {#x#}" + by (simp add: add_ac) + with add show ?case by (simp add: fold_mset_insert fold_mset_fun_comm) qed lemma fold_mset_fusion: assumes "comp_fun_commute g" - shows "(\x y. h (g x y) = f x (h y)) \ h (fold_mset g w A) = fold_mset f (h w) A" (is "PROP ?P") + shows "(\x y. h (g x y) = f x (h y)) \ h (fold g w A) = fold f (h w) A" (is "PROP ?P") proof - interpret comp_fun_commute g by (fact assms) show "PROP ?P" by (induct A) auto qed -lemma fold_mset_rec: - assumes "a \# A" - shows "fold_mset f z A = f a (fold_mset f z (A - {#a#}))" -proof - - from assms obtain A' where "A = A' + {#a#}" - by (blast dest: multi_member_split) - then show ?thesis by simp -qed - end text {* A note on code generation: When defining some function containing a - subterm @{term"fold_mset F"}, code generation is not automatic. When + subterm @{term "fold F"}, code generation is not automatic. When interpreting locale @{text left_commutative} with @{text F}, the - would be code thms for @{const fold_mset} become thms like - @{term"fold_mset F z {#} = z"} where @{text F} is not a pattern but + would be code thms for @{const fold} become thms like + @{term "fold F z {#} = z"} where @{text F} is not a pattern but contains defined symbols, i.e.\ is not a code thm. Hence a separate constant with its own code thms needs to be introduced for @{text F}. See the image operator below. @@ -806,36 +742,46 @@ subsection {* Image *} definition image_mset :: "('a \ 'b) \ 'a multiset \ 'b multiset" where - "image_mset f = fold_mset (op + o single o f) {#}" + "image_mset f = fold (plus o single o f) {#}" -interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f -proof qed (simp add: add_ac fun_eq_iff) +lemma comp_fun_commute_mset_image: + "comp_fun_commute (plus o single o f)" +proof +qed (simp add: add_ac fun_eq_iff) lemma image_mset_empty [simp]: "image_mset f {#} = {#}" -by (simp add: image_mset_def) + by (simp add: image_mset_def) lemma image_mset_single [simp]: "image_mset f {#x#} = {#f x#}" -by (simp add: image_mset_def) - -lemma image_mset_insert: - "image_mset f (M + {#a#}) = image_mset f M + {#f a#}" -by (simp add: image_mset_def add_ac) +proof - + interpret comp_fun_commute "plus o single o f" + by (fact comp_fun_commute_mset_image) + show ?thesis by (simp add: image_mset_def) +qed lemma image_mset_union [simp]: - "image_mset f (M+N) = image_mset f M + image_mset f N" -apply (induct N) - apply simp -apply (simp add: add_assoc [symmetric] image_mset_insert) -done + "image_mset f (M + N) = image_mset f M + image_mset f N" +proof - + interpret comp_fun_commute "plus o single o f" + by (fact comp_fun_commute_mset_image) + show ?thesis by (induct N) (simp_all add: image_mset_def add_ac) +qed + +corollary image_mset_insert: + "image_mset f (M + {#a#}) = image_mset f M + {#f a#}" + by simp -lemma set_of_image_mset [simp]: "set_of (image_mset f M) = image f (set_of M)" -by (induct M) simp_all +lemma set_of_image_mset [simp]: + "set_of (image_mset f M) = image f (set_of M)" + by (induct M) simp_all -lemma size_image_mset [simp]: "size (image_mset f M) = size M" -by (induct M) simp_all +lemma size_image_mset [simp]: + "size (image_mset f M) = size M" + by (induct M) simp_all -lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \ M = {#}" -by (cases M) auto +lemma image_mset_is_empty_iff [simp]: + "image_mset f M = {#} \ M = {#}" + by (cases M) auto syntax "_comprehension1_mset" :: "'a \ 'b \ 'b multiset \ 'a multiset" @@ -989,7 +935,7 @@ lemma fold_multiset_equiv: assumes f: "\x y. x \ set xs \ y \ set xs \ f x \ f y = f y \ f x" and equiv: "multiset_of xs = multiset_of ys" - shows "fold f xs = fold f ys" + shows "List.fold f xs = List.fold f ys" using f equiv [symmetric] proof (induct xs arbitrary: ys) case Nil then show ?case by simp @@ -999,8 +945,8 @@ have "\x y. x \ set ys \ y \ set ys \ f x \ f y = f y \ f x" by (rule Cons.prems(1)) (simp_all add: *) moreover from * have "x \ set ys" by simp - ultimately have "fold f ys = fold f (remove1 x ys) \ f x" by (fact fold_remove1_split) - moreover from Cons.prems have "fold f xs = fold f (remove1 x ys)" by (auto intro: Cons.hyps) + ultimately have "List.fold f ys = List.fold f (remove1 x ys) \ f x" by (fact fold_remove1_split) + moreover from Cons.prems have "List.fold f xs = List.fold f (remove1 x ys)" by (auto intro: Cons.hyps) ultimately show ?case by simp qed @@ -1915,5 +1861,7 @@ multiset_postproc *} +hide_const (open) fold + end diff -r d15fe10593ff -r be66949288a2 src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Oct 11 20:38:02 2012 +0200 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Thu Oct 11 21:02:19 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 d15fe10593ff -r be66949288a2 src/HOL/Power.thy --- a/src/HOL/Power.thy Thu Oct 11 20:38:02 2012 +0200 +++ b/src/HOL/Power.thy Thu Oct 11 21:02:19 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 + diff -r d15fe10593ff -r be66949288a2 src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Thu Oct 11 20:38:02 2012 +0200 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Thu Oct 11 21:02:19 2012 +0200 @@ -476,7 +476,7 @@ "x \ space M1 \ g \ measurable (M1 \\<^isub>M M2) L \ (\y. g (x, y)) \ measurable M2 L" by (rule measurable_compose[OF measurable_Pair]) auto -lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst: +lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst': assumes f: "f \ borel_measurable (M1 \\<^isub>M M2)" "\x. 0 \ f x" shows "(\x. \\<^isup>+ y. f (x, y) \M2) \ borel_measurable M1" using f proof induct @@ -512,7 +512,7 @@ qed (simp_all add: M2.emeasure_pair_measure positive_integral_cmult positive_integral_add positive_integral_monotone_convergence_SUP measurable_compose_Pair1 positive_integral_positive - borel_measurable_positive_integral_fst positive_integral_mono incseq_def le_fun_def + borel_measurable_positive_integral_fst' positive_integral_mono incseq_def le_fun_def cong: positive_integral_cong) lemma (in pair_sigma_finite) positive_integral_fst_measurable: @@ -521,10 +521,21 @@ (is "?C f \ borel_measurable M1") and "(\\<^isup>+ x. (\\<^isup>+ y. f (x, y) \M2) \M1) = integral\<^isup>P (M1 \\<^isub>M M2) f" using f - borel_measurable_positive_integral_fst[of "\x. max 0 (f x)"] + borel_measurable_positive_integral_fst'[of "\x. max 0 (f x)"] positive_integral_fst[of "\x. max 0 (f x)"] unfolding positive_integral_max_0 by auto +lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst: + "(\(x, y). f x y) \ borel_measurable (M1 \\<^isub>M M2) \ (\x. \\<^isup>+ y. f x y \M2) \ borel_measurable M1" + using positive_integral_fst_measurable(1)[of "\(x, y). f x y"] by simp + +lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd: + assumes "(\(x, y). f x y) \ borel_measurable (M2 \\<^isub>M M1)" shows "(\x. \\<^isup>+ y. f x y \M1) \ borel_measurable M2" +proof - + interpret Q: pair_sigma_finite M2 M1 by default + from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp +qed + lemma (in pair_sigma_finite) positive_integral_snd_measurable: assumes f: "f \ borel_measurable (M1 \\<^isub>M M2)" shows "(\\<^isup>+ y. (\\<^isup>+ x. f (x, y) \M1) \M2) = integral\<^isup>P (M1 \\<^isub>M M2) f" diff -r d15fe10593ff -r be66949288a2 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Thu Oct 11 20:38:02 2012 +0200 +++ b/src/HOL/Probability/Information.thy Thu Oct 11 21:02:19 2012 +0200 @@ -1007,17 +1007,6 @@ "\(X ; Y | Z) \ conditional_mutual_information b (count_space (X ` space M)) (count_space (Y ` space M)) (count_space (Z ` space M)) X Y Z" -lemma (in pair_sigma_finite) borel_measurable_positive_integral_fst: - "(\(x, y). f x y) \ borel_measurable (M1 \\<^isub>M M2) \ (\x. \\<^isup>+ y. f x y \M2) \ borel_measurable M1" - using positive_integral_fst_measurable(1)[of "\(x, y). f x y"] by simp - -lemma (in pair_sigma_finite) borel_measurable_positive_integral_snd: - assumes "(\(x, y). f x y) \ borel_measurable (M2 \\<^isub>M M1)" shows "(\x. \\<^isup>+ y. f x y \M1) \ borel_measurable M2" -proof - - interpret Q: pair_sigma_finite M2 M1 by default - from Q.borel_measurable_positive_integral_fst assms show ?thesis by simp -qed - lemma (in information_space) assumes S: "sigma_finite_measure S" and T: "sigma_finite_measure T" and P: "sigma_finite_measure P" assumes Px: "distributed M S X Px"