# HG changeset patch # User haftmann # Date 1364378105 -3600 # Node ID 757fa47af9814c1c3f72ae59063429fce9c1afc9 # Parent 604d73671fa73ef0a9e8269bc4b198dd4f51baf0 centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively diff -r 604d73671fa7 -r 757fa47af981 src/HOL/BNF/More_BNFs.thy --- a/src/HOL/BNF/More_BNFs.thy Tue Mar 26 22:09:39 2013 +0100 +++ b/src/HOL/BNF/More_BNFs.thy Wed Mar 27 10:55:05 2013 +0100 @@ -532,34 +532,6 @@ (* Multisets *) -(* The cardinal of a mutiset: this, and the following basic lemmas about it, -should eventually go into Multiset.thy *) -definition "mcard M \ setsum (count M) {a. count M a > 0}" - -lemma mcard_emp[simp]: "mcard {#} = 0" -unfolding mcard_def by auto - -lemma mcard_emp_iff[simp]: "mcard M = 0 \ M = {#}" -unfolding mcard_def apply safe - apply simp_all - by (metis multi_count_eq zero_multiset.rep_eq) - -lemma mcard_singl[simp]: "mcard {#a#} = Suc 0" -unfolding mcard_def by auto - -lemma mcard_Plus[simp]: "mcard (M + N) = mcard M + mcard N" -proof - - have "setsum (count M) {a. 0 < count M a + count N a} = - setsum (count M) {a. a \# M}" - apply (rule setsum_mono_zero_cong_right) by auto - moreover - have "setsum (count N) {a. 0 < count M a + count N a} = - setsum (count N) {a. a \# N}" - apply (rule setsum_mono_zero_cong_right) by auto - ultimately show ?thesis - unfolding mcard_def count_union [THEN ext] by (simp add: setsum.distrib) -qed - lemma setsum_gt_0_iff: fixes f :: "'a \ nat" assumes "finite A" shows "setsum f A > 0 \ (\ a \ A. f a > 0)" @@ -1246,7 +1218,7 @@ using multiset_rel_Zero multiset_rel_Plus by auto lemma mcard_multiset_map[simp]: "mcard (multiset_map f M) = mcard M" -proof- +proof - def A \ "\ b. {a. f a = b \ a \# M}" let ?B = "{b. 0 < setsum (count M) (A b)}" have "{b. \a. f a = b \ a \# M} \ f ` {a. a \# M}" by auto @@ -1273,7 +1245,7 @@ also have "?J = {a. a \# M}" unfolding AB unfolding A_def by auto finally have "setsum (\ x. setsum (count M) (A x)) ?B = setsum (count M) {a. a \# M}" . - thus ?thesis unfolding A_def mcard_def multiset_map_def by (simp add: mmap_def) + then show ?thesis by (simp add: A_def mcard_unfold_setsum multiset_map_def set_of_def mmap_def) qed lemma multiset_rel_mcard: diff -r 604d73671fa7 -r 757fa47af981 src/HOL/Library/Multiset.thy --- a/src/HOL/Library/Multiset.thy Tue Mar 26 22:09:39 2013 +0100 +++ b/src/HOL/Library/Multiset.thy Wed Mar 27 10:55:05 2013 +0100 @@ -702,7 +702,7 @@ then show ?thesis by simp qed -lemma fold_mset_fun_comm: +lemma fold_mset_fun_left_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) @@ -714,7 +714,7 @@ 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) + with add show ?case by (simp add: fold_mset_insert fold_mset_fun_left_comm) qed lemma fold_mset_fusion: @@ -821,9 +821,7 @@ declare image_mset.identity [simp] -subsection {* Alternative representations *} - -subsubsection {* Lists *} +subsection {* Further conversions *} primrec multiset_of :: "'a list \ 'a multiset" where "multiset_of [] = {#}" | @@ -950,6 +948,257 @@ ultimately show ?case by simp qed +lemma multiset_of_insort [simp]: + "multiset_of (insort x xs) = multiset_of xs + {#x#}" + by (induct xs) (simp_all add: ac_simps) + +definition multiset_of_set :: "'a set \ 'a multiset" +where + "multiset_of_set = folding.F (\x M. {#x#} + M) {#}" + +interpretation multiset_of_set!: folding "\x M. {#x#} + M" "{#}" +where + "folding.F (\x M. {#x#} + M) {#} = multiset_of_set" +proof - + interpret comp_fun_commute "\x M. {#x#} + M" by default (simp add: fun_eq_iff ac_simps) + show "folding (\x M. {#x#} + M)" by default (fact comp_fun_commute) + from multiset_of_set_def show "folding.F (\x M. {#x#} + M) {#} = multiset_of_set" .. +qed + +context linorder +begin + +definition sorted_list_of_multiset :: "'a multiset \ 'a list" +where + "sorted_list_of_multiset M = fold insort [] M" + +lemma sorted_list_of_multiset_empty [simp]: + "sorted_list_of_multiset {#} = []" + by (simp add: sorted_list_of_multiset_def) + +lemma sorted_list_of_multiset_singleton [simp]: + "sorted_list_of_multiset {#x#} = [x]" +proof - + interpret comp_fun_commute insort by (fact comp_fun_commute_insort) + show ?thesis by (simp add: sorted_list_of_multiset_def) +qed + +lemma sorted_list_of_multiset_insert [simp]: + "sorted_list_of_multiset (M + {#x#}) = List.insort x (sorted_list_of_multiset M)" +proof - + interpret comp_fun_commute insort by (fact comp_fun_commute_insort) + show ?thesis by (simp add: sorted_list_of_multiset_def) +qed + +end + +lemma multiset_of_sorted_list_of_multiset [simp]: + "multiset_of (sorted_list_of_multiset M) = M" + by (induct M) simp_all + +lemma sorted_list_of_multiset_multiset_of [simp]: + "sorted_list_of_multiset (multiset_of xs) = sort xs" + by (induct xs) simp_all + +lemma finite_set_of_multiset_of_set: + assumes "finite A" + shows "set_of (multiset_of_set A) = A" + using assms by (induct A) simp_all + +lemma infinite_set_of_multiset_of_set: + assumes "\ finite A" + shows "set_of (multiset_of_set A) = {}" + using assms by simp + +lemma set_sorted_list_of_multiset [simp]: + "set (sorted_list_of_multiset M) = set_of M" + by (induct M) (simp_all add: set_insort) + +lemma sorted_list_of_multiset_of_set [simp]: + "sorted_list_of_multiset (multiset_of_set A) = sorted_list_of_set A" + by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps) + + +subsection {* Big operators *} + +no_notation times (infixl "*" 70) +no_notation Groups.one ("1") + +locale comm_monoid_mset = comm_monoid +begin + +definition F :: "'a multiset \ 'a" +where + eq_fold: "F M = Multiset.fold f 1 M" + +lemma empty [simp]: + "F {#} = 1" + by (simp add: eq_fold) + +lemma singleton [simp]: + "F {#x#} = x" +proof - + interpret comp_fun_commute + by default (simp add: fun_eq_iff left_commute) + show ?thesis by (simp add: eq_fold) +qed + +lemma union [simp]: + "F (M + N) = F M * F N" +proof - + interpret comp_fun_commute f + by default (simp add: fun_eq_iff left_commute) + show ?thesis by (induct N) (simp_all add: left_commute eq_fold) +qed + +end + +notation times (infixl "*" 70) +notation Groups.one ("1") + +definition (in comm_monoid_add) msetsum :: "'a multiset \ 'a" +where + "msetsum = comm_monoid_mset.F plus 0" + +definition (in comm_monoid_mult) msetprod :: "'a multiset \ 'a" +where + "msetprod = comm_monoid_mset.F times 1" + +sublocale comm_monoid_add < msetsum!: comm_monoid_mset plus 0 +where + "comm_monoid_mset.F plus 0 = msetsum" +proof - + show "comm_monoid_mset plus 0" .. + from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" .. +qed + +context comm_monoid_add +begin + +lemma setsum_unfold_msetsum: + "setsum f A = msetsum (image_mset f (multiset_of_set A))" + by (cases "finite A") (induct A rule: finite_induct, simp_all) + +abbreviation msetsum_image :: "('b \ 'a) \ 'b multiset \ 'a" +where + "msetsum_image f M \ msetsum (image_mset f M)" + +end + +syntax + "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" + ("(3SUM _:#_. _)" [0, 51, 10] 10) + +syntax (xsymbols) + "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" + ("(3\_:#_. _)" [0, 51, 10] 10) + +syntax (HTML output) + "_msetsum_image" :: "pttrn \ 'b set \ 'a \ 'a::comm_monoid_add" + ("(3\_\#_. _)" [0, 51, 10] 10) + +translations + "SUM i :# A. b" == "CONST msetsum_image (\i. b) A" + +sublocale comm_monoid_mult < msetprod!: comm_monoid_mset times 1 +where + "comm_monoid_mset.F times 1 = msetprod" +proof - + show "comm_monoid_mset times 1" .. + from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" .. +qed + +context comm_monoid_mult +begin + +lemma msetprod_empty: + "msetprod {#} = 1" + by (fact msetprod.empty) + +lemma msetprod_singleton: + "msetprod {#x#} = x" + by (fact msetprod.singleton) + +lemma msetprod_Un: + "msetprod (A + B) = msetprod A * msetprod B" + by (fact msetprod.union) + +lemma setprod_unfold_msetprod: + "setprod f A = msetprod (image_mset f (multiset_of_set A))" + by (cases "finite A") (induct A rule: finite_induct, simp_all) + +lemma msetprod_multiplicity: + "msetprod M = setprod (\x. x ^ count M x) (set_of M)" + by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) + +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 (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 {* Cardinality *} + +definition mcard :: "'a multiset \ nat" +where + "mcard = msetsum \ image_mset (\_. 1)" + +lemma mcard_empty [simp]: + "mcard {#} = 0" + by (simp add: mcard_def) + +lemma mcard_singleton [simp]: + "mcard {#a#} = Suc 0" + by (simp add: mcard_def) + +lemma mcard_plus [simp]: + "mcard (M + N) = mcard M + mcard N" + by (simp add: mcard_def) + +lemma mcard_empty_iff [simp]: + "mcard M = 0 \ M = {#}" + by (induct M) simp_all + +lemma mcard_unfold_setsum: + "mcard M = setsum (count M) (set_of M)" +proof (induct M) + case empty then show ?case by simp +next + case (add M x) then show ?case + by (cases "x \ set_of M") + (simp_all del: mem_set_of_iff add: setsum.distrib setsum.delta' insert_absorb, simp) +qed + + +subsection {* Alternative representations *} + +subsubsection {* Lists *} + context linorder begin diff -r 604d73671fa7 -r 757fa47af981 src/HOL/List.thy --- a/src/HOL/List.thy Tue Mar 26 22:09:39 2013 +0100 +++ b/src/HOL/List.thy Wed Mar 27 10:55:05 2013 +0100 @@ -4338,6 +4338,10 @@ context linorder begin +lemma set_insort_key: + "set (insort_key f x xs) = insert x (set xs)" + by (induct xs) auto + lemma length_insort [simp]: "length (insort_key f x xs) = Suc (length xs)" by (induct xs) simp_all diff -r 604d73671fa7 -r 757fa47af981 src/HOL/Number_Theory/UniqueFactorization.thy --- a/src/HOL/Number_Theory/UniqueFactorization.thy Tue Mar 26 22:09:39 2013 +0100 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy Wed Mar 27 10:55:05 2013 +0100 @@ -36,102 +36,6 @@ "ALL i :# M. P i"? *) -no_notation times (infixl "*" 70) -no_notation Groups.one ("1") - -locale comm_monoid_mset = comm_monoid -begin - -definition F :: "'a multiset \ 'a" -where - eq_fold: "F M = Multiset.fold f 1 M" - -lemma empty [simp]: - "F {#} = 1" - by (simp add: eq_fold) - -lemma singleton [simp]: - "F {#x#} = x" -proof - - interpret comp_fun_commute - by default (simp add: fun_eq_iff left_commute) - show ?thesis by (simp add: eq_fold) -qed - -lemma union [simp]: - "F (M + N) = F M * F N" -proof - - interpret comp_fun_commute f - by default (simp add: fun_eq_iff left_commute) - show ?thesis by (induct N) (simp_all add: left_commute eq_fold) -qed - -end - -notation times (infixl "*" 70) -notation Groups.one ("1") - -definition (in comm_monoid_mult) msetprod :: "'a multiset \ 'a" -where - "msetprod = comm_monoid_mset.F times 1" - -sublocale comm_monoid_mult < msetprod!: comm_monoid_mset times 1 -where - "comm_monoid_mset.F times 1 = msetprod" -proof - - show "comm_monoid_mset times 1" .. - from msetprod_def show "comm_monoid_mset.F times 1 = msetprod" by rule -qed - -context comm_monoid_mult -begin - -lemma msetprod_empty: - "msetprod {#} = 1" - by (fact msetprod.empty) - -lemma msetprod_singleton: - "msetprod {#x#} = x" - by (fact msetprod.singleton) - -lemma msetprod_Un: - "msetprod (A + B) = msetprod A * msetprod B" - by (fact msetprod.union) - -lemma msetprod_multiplicity: - "msetprod M = setprod (\x. x ^ count M x) (set_of M)" - by (simp add: Multiset.fold_def setprod.eq_fold msetprod.eq_fold funpow_times_power comp_def) - -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 (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 *}