src/HOL/Library/Multiset.thy
changeset 67051 e7e54a0b9197
parent 66938 c78ff0aeba4c
child 67332 cb96edae56ef
     1.1 --- a/src/HOL/Library/Multiset.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Library/Multiset.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -2155,6 +2155,42 @@
     1.4    "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
     1.5    by (induct n) simp_all
     1.6  
     1.7 +lemma replicate_mset_msubseteq_iff:
     1.8 +  "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
     1.9 +  by (cases m)
    1.10 +    (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
    1.11 +
    1.12 +lemma msubseteq_replicate_msetE:
    1.13 +  assumes "A \<subseteq># replicate_mset n a"
    1.14 +  obtains m where "m \<le> n" and "A = replicate_mset m a"
    1.15 +proof (cases "n = 0")
    1.16 +  case True
    1.17 +  with assms that show thesis
    1.18 +    by simp
    1.19 +next
    1.20 +  case False
    1.21 +  from assms have "set_mset A \<subseteq> set_mset (replicate_mset n a)"
    1.22 +    by (rule set_mset_mono)
    1.23 +  with False have "set_mset A \<subseteq> {a}"
    1.24 +    by simp
    1.25 +  then have "\<exists>m. A = replicate_mset m a"
    1.26 +  proof (induction A)
    1.27 +    case empty
    1.28 +    then show ?case
    1.29 +      by simp
    1.30 +  next
    1.31 +    case (add b A)
    1.32 +    then obtain m where "A = replicate_mset m a"
    1.33 +      by auto
    1.34 +    with add.prems show ?case
    1.35 +      by (auto intro: exI [of _ "Suc m"])
    1.36 +  qed
    1.37 +  then obtain m where A: "A = replicate_mset m a" ..
    1.38 +  with assms have "m \<le> n"
    1.39 +    by (auto simp add: replicate_mset_msubseteq_iff)
    1.40 +  then show thesis using A ..
    1.41 +qed
    1.42 +
    1.43  
    1.44  subsection \<open>Big operators\<close>
    1.45