src/HOL/Library/Multiset.thy
changeset 60804 080a979a985b
parent 60752 b48830b670a1
child 61031 162bd20dae23
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Jul 27 22:08:46 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jul 27 22:44:02 2015 +0200
     1.3 @@ -1140,6 +1140,36 @@
     1.4  by (cases "finite A") (induct A rule: finite_induct, simp_all add: ac_simps)
     1.5  
     1.6  
     1.7 +subsection \<open>Replicate operation\<close>
     1.8 +
     1.9 +definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
    1.10 +  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
    1.11 +
    1.12 +lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
    1.13 +  unfolding replicate_mset_def by simp
    1.14 +
    1.15 +lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
    1.16 +  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
    1.17 +
    1.18 +lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
    1.19 +  unfolding replicate_mset_def by (induct n) simp_all
    1.20 +
    1.21 +lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
    1.22 +  unfolding replicate_mset_def by (induct n) simp_all
    1.23 +
    1.24 +lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
    1.25 +  by (auto split: if_splits)
    1.26 +
    1.27 +lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
    1.28 +  by (induct n, simp_all)
    1.29 +
    1.30 +lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
    1.31 +  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
    1.32 +
    1.33 +lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
    1.34 +  by (induct D) simp_all
    1.35 +
    1.36 +
    1.37  subsection \<open>Big operators\<close>
    1.38  
    1.39  no_notation times (infixl "*" 70)
    1.40 @@ -1195,6 +1225,10 @@
    1.41    from msetsum_def show "comm_monoid_mset.F plus 0 = msetsum" ..
    1.42  qed
    1.43  
    1.44 +lemma (in semiring_1) msetsum_replicate_mset [simp]:
    1.45 +  "msetsum (replicate_mset n a) = of_nat n * a"
    1.46 +  by (induct n) (simp_all add: algebra_simps)
    1.47 +
    1.48  lemma setsum_unfold_msetsum:
    1.49    "setsum f A = msetsum (image_mset f (mset_set A))"
    1.50    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    1.51 @@ -1267,6 +1301,10 @@
    1.52    "msetprod (A + B) = msetprod A * msetprod B"
    1.53    by (fact msetprod.union)
    1.54  
    1.55 +lemma msetprod_replicate_mset [simp]:
    1.56 +  "msetprod (replicate_mset n a) = a ^ n"
    1.57 +  by (induct n) (simp_all add: ac_simps)
    1.58 +
    1.59  lemma setprod_unfold_msetprod:
    1.60    "setprod f A = msetprod (image_mset f (mset_set A))"
    1.61    by (cases "finite A") (induct A rule: finite_induct, simp_all)
    1.62 @@ -1302,37 +1340,6 @@
    1.63  qed
    1.64  
    1.65  
    1.66 -subsection \<open>Replicate operation\<close>
    1.67 -
    1.68 -definition replicate_mset :: "nat \<Rightarrow> 'a \<Rightarrow> 'a multiset" where
    1.69 -  "replicate_mset n x = ((op + {#x#}) ^^ n) {#}"
    1.70 -
    1.71 -lemma replicate_mset_0[simp]: "replicate_mset 0 x = {#}"
    1.72 -  unfolding replicate_mset_def by simp
    1.73 -
    1.74 -lemma replicate_mset_Suc[simp]: "replicate_mset (Suc n) x = replicate_mset n x + {#x#}"
    1.75 -  unfolding replicate_mset_def by (induct n) (auto intro: add.commute)
    1.76 -
    1.77 -lemma in_replicate_mset[simp]: "x \<in># replicate_mset n y \<longleftrightarrow> n > 0 \<and> x = y"
    1.78 -  unfolding replicate_mset_def by (induct n) simp_all
    1.79 -
    1.80 -lemma count_replicate_mset[simp]: "count (replicate_mset n x) y = (if y = x then n else 0)"
    1.81 -  unfolding replicate_mset_def by (induct n) simp_all
    1.82 -
    1.83 -lemma set_mset_replicate_mset_subset[simp]: "set_mset (replicate_mset n x) = (if n = 0 then {} else {x})"
    1.84 -  by (auto split: if_splits)
    1.85 -
    1.86 -lemma size_replicate_mset[simp]: "size (replicate_mset n M) = n"
    1.87 -  by (induct n, simp_all)
    1.88 -
    1.89 -lemma count_le_replicate_mset_le: "n \<le> count M x \<longleftrightarrow> replicate_mset n x \<le># M"
    1.90 -  by (auto simp add: assms mset_less_eqI) (metis count_replicate_mset subseteq_mset_def)
    1.91 -
    1.92 -
    1.93 -lemma filter_eq_replicate_mset: "{#y \<in># D. y = x#} = replicate_mset (count D x) x"
    1.94 -  by (induct D) simp_all
    1.95 -
    1.96 -
    1.97  subsection \<open>Alternative representations\<close>
    1.98  
    1.99  subsubsection \<open>Lists\<close>