# Re: [isabelle] Notation issues trying to make Multiset more convenient

```Viktor Kuncak wrote:
> I was wondering whether it also makes sense to extend set
> comprehensions with function image {# f x| x:M. P x #} in analogy with
> set comprehensions.  The multiset image preserves multiplicities by
> adding up the number of occurrences of each element that maps to a
> given one.  That is, I think we would like to have the following
> theorem hold (and perhaps this can be a definition):
>
> count {# f x| x:M. P x #} a = size {# y:M. f y = a & P y #}
>
> Actually, it seems more sensible for me to write :# within set
> comprehension whenever we refer to multisets, so that we can have both
>
> {# f x| x : S. P x #}     when S is a set, and
> {# f x| x :# M. P x #}     when M is a multiset.
>
> Am I mistaken that this is currently not in the library?
>
>   Viktor
>
>
You're right, this stuff is currently not in the library.

I've done similar stuff last month. Unfortunately, it depends on some
unsorted collection of (partially superfluous) helper lemmas. I'll try
to remove this dependence if I have some time.
I'm using the syntax f`#M for the image of M under f (in analogy to f`S
for sets)
I do not use such a clean definition, but define the graph of the
image-function by an inductive_set definition, exploiting that multisets
are always finite:

inductive_set
mset_map_Set :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a multiset
\<times> 'b multiset) set"
for f:: "'a \<Rightarrow> 'b"
where
mset_map_Set_empty: "({#},{#})\<in>mset_map_Set f"
(A+{#a#},B+{#f a#})\<in>mset_map_Set f"

I nevertheless attached my theory, perhaps it helps.

btw.

--
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380

```
```theory Multiset_fun_img
imports Main dep_lemmas
begin

subsubsection {* Image under function *}

inductive_set
mset_map_Set :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a multiset \<times> 'b multiset) set"
for f:: "'a \<Rightarrow> 'b"
where
mset_map_Set_empty: "({#},{#})\<in>mset_map_Set f"
| mset_map_Set_add: "(A,B)\<in>mset_map_Set f \<Longrightarrow> (A+{#a#},B+{#f a#})\<in>mset_map_Set f"

lemma mset_map_Set_empty_simps[simp]: "(({#},B)\<in>mset_map_Set f) = (B={#})" "((A,{#})\<in>mset_map_Set f) = (A={#})"
by (auto elim: mset_map_Set.cases intro: mset_map_Set_empty)

lemma mset_map_Set_single_left[simp]: "(({#a#},B)\<in>mset_map_Set f) = (B={#f a#})" by (auto elim: mset_map_Set.cases intro: mset_map_Set_add[of "{#}" "{#}", simplified])
lemma mset_map_Set_single_rightE[cases set, case_names orig]: "\<lbrakk>(A,{#b#})\<in>mset_map_Set f; !!a. \<lbrakk>A={#a#}; b=f a\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by (auto elim: mset_map_Set.cases)

lemma mset_map_Set_sizes: "(A,B)\<in>mset_map_Set f \<Longrightarrow> size A = size B" by (induct rule: mset_map_Set.induct) auto

text {* Intuitively, this lemma allows one to choose a single image element corresponding to an original element *}
lemma mset_map_Set_choose[cases set, case_names choice]: assumes A: "(A+{#a#},B)\<in>mset_map_Set f" "!!B'. \<lbrakk>B=B'+{#f a#}; (A,B')\<in>mset_map_Set f\<rbrakk> \<Longrightarrow> P" shows "P"
proof -
{ fix n
have "\<lbrakk>size B=n; (A+{#a#},B)\<in>mset_map_Set f; !!B'. \<lbrakk>B=B'+{#f a#}; (A,B')\<in>mset_map_Set f\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" proof (induct n arbitrary: A a B P)

(*have "!!A a B P. \<lbrakk>size B=n; (A+{#a#},B)\<in>mset_map_Set f; !!B'. \<lbrakk>B=B'+{#f a#}; (A,B')\<in>mset_map_Set f\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" proof (induct n)*)
case 0 thus ?case by simp
next
case (Suc n') from Suc.prems(2) show ?case proof (cases rule: mset_map_Set.cases)
case mset_map_Set_empty hence False by simp thus ?thesis ..
next
hence "A+{#a#}=A'+{#a'#}" by simp
thus ?thesis proof (cases rule: mset_single_cases2')
case loc with mset_map_Set_add Suc.prems(3) show ?thesis by auto
next
case (env A'')
from Suc.prems(1) mset_map_Set_add(2) have SIZE: "size B' = n'" by auto
from mset_map_Set_add env have MM: "(A'' + {#a#}, B') \<in> mset_map_Set f" by simp
from Suc.hyps[OF SIZE MM] obtain B'' where B'': "B'=B''+{#f a#}" "(A'',B'')\<in>mset_map_Set f" by blast
from mset_map_Set.mset_map_Set_add[OF B''(2)] env(2) have "(A, B'' + {#f a'#}) \<in> mset_map_Set f" by simp
moreover from B''(1) mset_map_Set_add have "B=B'' + {#f a'#} + {#f a#}" by (simp add: union_ac)
ultimately show ?thesis using Suc.prems(3) by blast
qed
qed
qed
} with A show P by blast
qed

lemma mset_map_Set_unique: "!!B B'. \<lbrakk>(A,B)\<in>mset_map_Set f; (A,B')\<in>mset_map_Set f\<rbrakk> \<Longrightarrow> B=B'" by (induct A) (auto elim!: mset_map_Set_choose)
lemma mset_map_Set_surjective: "\<lbrakk> !!B. (A,B)\<in>mset_map_Set f \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (induct A) (auto intro: mset_map_Set_add)

constdefs
mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" (infixr "`#" 90)
"f `# A == (THE B. (A,B)\<in>mset_map_Set f)"

text {* Locale to define functions from surjective, unique relations *}
locale su_rel_fun =
fixes F and f
assumes unique: "\<lbrakk>(A,B)\<in>F; (A,B')\<in>F\<rbrakk> \<Longrightarrow> B=B'"
assumes surjective: "\<lbrakk>!!B. (A,B)\<in>F \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
assumes f_def: "f A == THE B. (A,B)\<in>F"

lemma (in su_rel_fun) repr1: "(A,f A)\<in>F" proof (unfold f_def)
obtain B where "(A,B)\<in>F" by (rule surjective)
with theI[where P="\<lambda>B. (A,B)\<in>F", OF this] show "(A, THE x. (A, x) \<in> F) \<in> F" by (blast intro: unique)
qed

lemma (in su_rel_fun) repr2: "(A,B)\<in>F \<Longrightarrow> B=f A" using repr1 by (blast intro: unique)

lemma (in su_rel_fun) repr: "(f A = B) = ((A,B)\<in>F)" using repr1 repr2 by (blast)

interpretation mset_map: su_rel_fun["mset_map_Set f" "op `# f"]
apply (rule su_rel_fun.intro)
apply (erule mset_map_Set_unique, assumption)
apply (erule mset_map_Set_surjective)
apply (rule mset_map_def)
done

text {* Transfer the defining equations *}
lemma mset_map_empty[simp]: "f `# {#} = {#}"
apply (subst mset_map.repr)
apply (rule mset_map_Set_empty)
done

lemma mset_map_add[simp]: "f `# (A+{#a#}) = f `# A + {#f a#}" "f `# ({#a#}+A) = {#f a#} + f `# A"

text {* Transfer some other lemmas *}
lemma mset_map_single_rightE[consumes 1, case_names orig]: "\<lbrakk>f `# P = {#y#}; !!x. \<lbrakk> P={#x#}; f x = y \<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
by (auto simp add: mset_map.repr elim: mset_map_Set_single_rightE)

text {* And show some further equations *}
lemma mset_map_single[simp]: "f `# {#a#} = {#f a#}" using mset_map_add(1)[where A="{#}", simplified] .

lemma mset_map_union: "!!B. f `# (A+B) = f `# A + f `# B" by (induct A) (auto simp add: union_ac)

lemma mset_map_size: "size A = size (f `# A)" by (induct A) auto

lemma mset_map_empty_eq[simp]: "(f `# P = {#}) = (P={#})" using mset_map_size[of P f] by auto

lemma mset_map_le: "!!B. A \<le># B \<Longrightarrow> f `# A \<le># f `# B" proof (induct A)
case empty thus ?case by simp
next
hence "A\<le>#B-{#x#}" and SM: "{#x#}\<le>#B" using mset_le_subtract_right by (fastsimp+)
with "add.hyps" have "f `# A \<le># f `# (B-{#x#})" by blast
hence "f `# (A+{#x#}) \<le># f `# (B-{#x#}) + {#f x#}" by auto
also have "\<dots> = f `# (B-{#x#}+{#x#})" by simp
also with SM have "\<dots> = f `# B" by simp
finally show ?case .
qed

lemma mset_map_set_of: "set_of (f `# A) = f ` set_of A" by (induct A) auto

lemma mset_map_split_orig: "!!M1 M2. \<lbrakk>f `# P = M1+M2; !!P1 P2. \<lbrakk>P=P1+P2; f `# P1 = M1; f `# P2 = M2\<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q"
apply (induct P)
apply fastsimp
apply (fastsimp elim!: mset_un_single_un_cases simp add: union_ac) (* TODO: This proof need's quite long. Try to write a faster one. *)
done

lemma mset_map_id: "\<lbrakk>!!x. f (g x) = x\<rbrakk> \<Longrightarrow> f `# g `# X = X" by (induct X) auto

text {* The following is a very specialized lemma. Intuitively, it splits the original multiset by a splitting of some pointwise supermultiset of its image.

Application:
This lemma came in handy when proving the correctness of a constraint system that collects at most k sized submultisets of the sets of spawned threads.
*}
lemma mset_map_split_orig_le: assumes A: "f `# P \<le># M1+M2" and EX: "!!P1 P2. \<lbrakk>P=P1+P2; f `# P1 \<le># M1; f `# P2 \<le># M2\<rbrakk> \<Longrightarrow> Q" shows "Q"
using A EX by (auto elim: mset_le_distrib mset_map_split_orig)

end
```
```theory dep_lemmas
imports Main Multiset
begin

subsection {* Multisets *}

(*
The following is a syntax extension for multisets. Unfortunately, it depends on a change in the Library/Multiset.thy, so it is commented out here, until it will be incorporated
into Library/Multiset.thy by its maintainers.

The required change in Library/Multiset.thy is removing the syntax for single:
- single :: "'a => 'a multiset"    ("{#_#}")
+ single :: "'a => 'a multiset"

+ syntax
+ "@multiset" :: "args \<Rightarrow> 'a multiset" ("{#(_)#}")

+ translations
+   "{#x, xs#}" == "{#x#} + {#xs#}"
+   "{# x #}" == "single x"

This translates "{# \<dots> #}" into a sum of singletons, that is parenthesized to the right. ?? Can we also achieve left-parenthesizing ??

*)

(* Let's try what happens if declaring AC-rules for multiset union as simp-rules *)
(*declare union_ac[simp] -- don't do it !*)

subsubsection {* Case distinction *}
text {* Install a (new) default case-distinction lemma for multisets, that distinguishes between empty multiset and multiset that is the union of of some multisetset and a singleton multiset.
This is the same case distinction as done by the @{thm [source] multiset_induct} rule that is installed as default induction rule for multisets by Multiset.thy. *}
lemma mset_cases[case_names empty add, cases type: multiset]: "\<lbrakk> M={#} \<Longrightarrow> P; !!x M'. M=M'+{#x#} \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply (induct M)
apply auto
done

lemma multiset_induct'[case_names empty add]: "\<lbrakk>P {#}; \<And>M x. P M \<Longrightarrow> P ({#x#}+M)\<rbrakk> \<Longrightarrow> P M" by (induct rule: multiset_induct) (auto simp add: union_commute)

lemma mset_cases'[case_names empty add]: "\<lbrakk> M={#} \<Longrightarrow> P; !!x M'. M={#x#}+M' \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"
apply (induct M rule: multiset_induct')
apply auto
done

subsubsection {* Count *}
lemma count_ne_remove: "\<lbrakk> x ~= t\<rbrakk> \<Longrightarrow> count S x = count (S-{#t#}) x" by (auto)
lemma mset_empty_count[simp]: "(\<forall>p. count M p = 0) = (M={#})" by (auto simp add: multiset_eq_conv_count_eq)

subsubsection {* Union, difference and intersection *}

(* TODO: Check whether this proof can be done simpler *)
lemma mset_union_diff_comm: "t :# S \<Longrightarrow> T + (S - {#t#}) = (T + S) - {#t#}" proof -
assume "t :# S"
hence "count S t = count (S-{#t#}) t + 1" by auto
hence "count (S+T) t = count (S-{#t#}+T) t + 1" by auto
hence "count (S+T-{#t#}) t = count (S-{#t#}+T) t" by (simp)
moreover have "ALL x. x~=t \<longrightarrow> count (S+T-{#t#}) x = count (S-{#t#}+T) x" by auto
qed

lemma mset_diff_union_cancel[simp]: "t :# S \<Longrightarrow> (S - {#t#}) + {#t#} = S" by (auto simp add: mset_union_diff_comm union_ac)

lemma mset_diff_diff_left: "A-B-C = A-((B::'a multiset)+C)" proof -
have "ALL e . count (A-B-C) e = count (A-(B+C)) e" by auto
thus ?thesis by (simp add: multiset_eq_conv_count_eq)
qed

lemma mset_diff_commute: "A-B-C = A-C-(B::'a multiset)" proof -
have "A-B-C = A-(B+C)" by (simp add: mset_diff_diff_left)
also have "\<dots> = A-(C+B)" by (simp add: union_commute)
thus ?thesis by (simp add: mset_diff_diff_left)
qed

(* Todo: This should be more simply to prove, should'nt it ??*)
lemma mset_diff_same_empty[simp]: "(S::'a multiset) - S = {#}"
proof -
have "ALL e . count (S-S) e = 0" by auto
hence "ALL e . ~ (e : set_of (S-S))" by auto
hence "set_of (S-S) = {}" by blast
thus ?thesis by (auto)
qed

lemma mset_right_cancel_union: "\<lbrakk>a :# A+B; ~(a :# B)\<rbrakk> \<Longrightarrow> a:#A" by (simp)
lemma mset_left_cancel_union: "\<lbrakk>a :# A+B; ~(a :# A)\<rbrakk> \<Longrightarrow> a:#B" by (simp)

lemmas mset_cancel_union = mset_right_cancel_union mset_left_cancel_union;

lemma mset_right_cancel_elem: "\<lbrakk>a :# A+{#b#}; a~=b\<rbrakk> \<Longrightarrow> a:#A"
apply(subgoal_tac "~(a :# {#b#})")
apply(auto)
done

lemma mset_left_cancel_elem: "\<lbrakk>a :# {#b#}+A; a~=b\<rbrakk> \<Longrightarrow> a:#A"
apply(subgoal_tac "~(a :# {#b#})")
apply(auto)
done

lemmas mset_cancel_elem = mset_right_cancel_elem mset_left_cancel_elem;

lemma mset_diff_cancel1elem[simp]: "~(a :# B) \<Longrightarrow> {#a#}-B = {#a#}" proof -
assume A: "~(a :# B)"
hence "count ({#a#}-B) a = count ({#a#}) a" by auto
moreover have "ALL e . e~=a \<longrightarrow> count ({#a#}-B) e = count ({#a#}) e" by auto
ultimately show ?thesis by (auto simp add: multiset_eq_conv_count_eq)
qed

lemma diff_union_inverse[simp]: "A + B - B = (A::'a multiset)" by (auto iff add: multiset_eq_conv_count_eq)

lemma diff_union_inverse2[simp]: "B + A - B = (A::'a multiset)" by (auto iff add: multiset_eq_conv_count_eq)

lemma union_diff_assoc_se: "t :# B \<Longrightarrow> (A+B)-{#t#} = A + (B-{#t#})" by (auto iff add: multiset_eq_conv_count_eq)
(*lemma union_diff_assoc_se2: "t :# A \<Longrightarrow> (A+B)-{#t#} = (A-{#t#}) + B" by (auto iff add: multiset_eq_conv_count_eq)
lemmas union_diff_assoc_se = union_diff_assoc_se1 union_diff_assoc_se2*)

lemma union_diff_assoc: "C-B={#} \<Longrightarrow> (A+B)-C = A + (B-C)" by (simp add: multiset_eq_conv_count_eq)

lemma mset_union_1_elem1[simp]: "({#a#} = M+{#b#}) = (a=b & M={#})" proof
assume A: "{#a#} = M+{#b#}"
from A have "size {#a#} = size (M+{#b#})" by simp
hence "1 = 1 + size M" by auto
hence "M={#}" by auto
moreover with A have "a=b" by auto
ultimately show "a=b & M={#}" by auto
next
assume "a = b \<and> M = {#}"
thus "{#a#} = M+{#b#}" by auto
qed

lemma mset_union_1_elem2[simp]: "({#a#} = {#b#}+M) = (a=b & M={#})" using mset_union_1_elem1 by (simp add: union_ac)

lemma mset_union_1_elem3[simp]: "(M+{#b#}={#a#}) = (b=a & M={#})" by (auto simp add: eq_sym_conv)
lemma mset_union_1_elem4[simp]: "({#b#}+M={#a#}) = (b=a & M={#})" using mset_union_1_elem3 by (simp add: union_ac)

lemma mset_inter_1elem1[simp]: assumes A: "~(a :# B)" shows "{#a#} #\<inter> B = {#}" proof (unfold multiset_inter_def)
from A have "{#a#} - B = {#a#}" by simp
thus "{#a#} - ({#a#} - B) = {#}" by simp
qed

lemma mset_inter_1elem2[simp]: "~(a :# B) \<Longrightarrow> B #\<inter> {#a#} = {#}" proof -
assume "~(a :# B)"
hence "{#a#} #\<inter> B = {#}" by simp
thus ?thesis by (simp add: multiset_inter_commute)
qed

lemmas mset_inter_1elem = mset_inter_1elem1 mset_inter_1elem2

lemmas mset_neutral_cancel1 = union_left_cancel[where N="{#}", simplified] union_right_cancel[where N="{#}", simplified]
declare mset_neutral_cancel1[simp]

lemma mset_neutral_cancel2[simp]: "(c=n+c) = (n={#})" "(c=c+n) = (n={#})"
apply (subgoal_tac "c+n=c", simp_all)+
done

(* TODO: The proof seems too complicated, there should be an easier one ! *)
lemma mset_union_2_elem: "{#a#}+{#b#} = M + {#c#} \<Longrightarrow> {#a#}=M & b=c | a=c & {#b#}=M"
proof -
assume A: "{#a#}+{#b#} = M + {#c#}"
hence "{#a#}+{#b#}-{#b#} = M + {#c#} - {#b#}" by auto
hence AEQ: "{#a#} = M + {#c#} - {#b#}" by (auto simp add: union_assoc)
{ assume "c=b"
with AEQ have "{#a#} = M" by auto
} moreover {
from A have "{#b#}+{#a#} = M + {#c#}" by (auto simp add: union_commute)
moreover assume "a=c"
ultimately have "{#b#} = M" by auto
} moreover {
assume NEQ: "c~=b & a~=c"
from A have "{#a#}+{#b#}-{#c#} = M + {#c#}-{#c#}" by auto
hence "{#a#}+{#b#}-{#c#} = M" by (auto simp add: union_assoc)
with NEQ have "{#a#}-{#c#}+{#b#} = M" by (subgoal_tac "~ (c :# {#b#})", auto simp add: mset_inter_1elem multiset_union_diff_commute)
with NEQ have "{#a#}+{#b#} = M" by (subgoal_tac "~(a :# {#c#})", auto simp add: mset_diff_cancel1elem)
hence S1: "size M = 2" by auto
moreover from A have "size ({#a#}+{#b#}) = size (M + {#c#})" by auto
hence "size M = 1" by auto
ultimately have "False" by simp
}
ultimately show ?thesis by blast
qed

lemma mset_diff_union_s_inverse[simp]: "s :# S \<Longrightarrow> {#s#} + (S - {# s #}) = S" proof -
assume "s :# S"
hence "S = S - {#s#} + {#s#}" by (auto simp add: mset_union_diff_comm)
thus ?thesis by (auto simp add: union_ac)
qed

lemma mset_un_iff: "(a :# A + B) = (a :# A | a :# B)" by (simp)
lemma mset_un_cases[cases set, case_names left right]: "\<lbrakk>a :# A + B; a:#A \<Longrightarrow> P; a:#B \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by (auto)

lemma mset_unplusm_dist_cases[cases set, case_names left right]:
assumes A: "{#s#}+A = B+C"
assumes L: "\<lbrakk>B={#s#}+(B-{#s#}); A=(B-{#s#})+C\<rbrakk> \<Longrightarrow> P"
assumes R: "\<lbrakk>C={#s#}+(C-{#s#}); A=B+(C-{#s#})\<rbrakk> \<Longrightarrow> P"
shows P
proof -
from A[symmetric] have "s :# B+C" by simp
thus ?thesis proof (cases rule: mset_un_cases)
case left hence 1: "B={#s#}+(B-{#s#})" by simp
with A have "{#s#}+A = {#s#}+((B-{#s#})+C)" by (simp add: union_ac)
hence 2: "A = (B-{#s#})+C" by (simp)
from L[OF 1 2] show ?thesis .
next
case right hence 1: "C={#s#}+(C-{#s#})" by simp
with A have "{#s#}+A = {#s#}+(B+(C-{#s#}))" by (simp add: union_ac)
hence 2: "A = B+(C-{#s#})" by (simp)
from R[OF 1 2] show ?thesis .
qed
qed

lemma mset_unplusm_dist_cases2[cases set, case_names left right]:
assumes A: "B+C = {#s#}+A"
assumes L: "\<lbrakk>B={#s#}+(B-{#s#}); A=(B-{#s#})+C\<rbrakk> \<Longrightarrow> P"
assumes R: "\<lbrakk>C={#s#}+(C-{#s#}); A=B+(C-{#s#})\<rbrakk> \<Longrightarrow> P"
shows P
using mset_unplusm_dist_cases[OF A[symmetric]] L R by blast

lemma mset_single_cases[cases set, case_names loc env]:
assumes A: "{#s#}+c = {#r'#}+c'"
assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "\<lbrakk>c'={#s#}+(c'-{#s#}); c={#r'#}+(c-{#r'#}); c-{#r'#} = c'-{#s#} \<rbrakk> \<Longrightarrow> P"
shows "P"
proof -
{ assume CASE: "s=r'"
with A have "c=c'" by simp
with CASE CASES have ?thesis by auto
} moreover {
assume CASE: "s\<noteq>r'"
have "s:#{#s#}+c" by simp
with A have "s:#{#r'#}+c'" by simp
with CASE have "s:#c'" by (auto elim!: mset_un_cases split: split_if_asm)
from mset_diff_union_s_inverse[OF this, symmetric] have 1: "c' = {#s#} + (c' - {#s#})" .
with A have "{#s#}+c = {#s#}+({#r'#}+(c' - {#s#}))" by (auto simp add: union_ac)
hence 2: "c={#r'#}+(c' - {#s#})" by (auto)
hence 3: "c-{#r'#} = (c' - {#s#})" by auto
from 1 2 3 CASES have ?thesis by auto
} ultimately show ?thesis by blast
qed

lemma mset_single_cases'[cases set, case_names loc env]:
assumes A: "{#s#}+c = {#r'#}+c'"
assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "!!cc. \<lbrakk>c'={#s#}+cc; c={#r'#}+cc; c'-{#s#}=cc; c-{#r'#}=cc\<rbrakk> \<Longrightarrow> P"
shows "P"
using A  CASES by (auto elim!: mset_single_cases)

lemma mset_single_cases2[cases set, case_names loc env]:
assumes A: "c+{#s#} = c'+{#r'#}"
assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "\<lbrakk>c'=(c'-{#s#})+{#s#}; c=(c-{#r'#})+{#r'#}; c-{#r'#} = c'-{#s#} \<rbrakk> \<Longrightarrow> P"
shows "P"
proof -
from A have "{#s#}+c = {#r'#}+c'" by (simp add: union_ac)
thus ?thesis proof (cases rule: mset_single_cases)
case loc with CASES show ?thesis by simp
next
case env with CASES show ?thesis by (simp add: union_ac)
qed
qed

lemma mset_single_cases2'[cases set, case_names loc env]:
assumes A: "c+{#s#} = c'+{#r'#}"
assumes CASES: "\<lbrakk>s=r'; c=c'\<rbrakk> \<Longrightarrow> P" "!!cc. \<lbrakk>c'=cc+{#s#}; c=cc+{#r'#}; c'-{#s#}=cc; c-{#r'#}=cc\<rbrakk> \<Longrightarrow> P"
shows "P"
using A  CASES by (auto elim!: mset_single_cases2)

lemma mset_un_single_un_cases[consumes 1, case_names left right]: assumes A: "A+{#a#} = B+C" and CASES: "\<lbrakk>a:#B; A=(B-{#a#})+C\<rbrakk> \<Longrightarrow> P" "\<lbrakk>a:#C; A=B+(C-{#a#})\<rbrakk> \<Longrightarrow> P" shows "P"
proof -
have "a:#A+{#a#}" by simp
with A have "a:#B+C" by auto
thus ?thesis proof (cases rule: mset_un_cases)
case left hence "B=B-{#a#}+{#a#}" by auto
with A have "A+{#a#} = (B-{#a#})+C+{#a#}" by (auto simp add: union_ac)
hence "A=(B-{#a#})+C" by simp
with CASES(1)[OF left] show ?thesis by blast
next
case right hence "C=C-{#a#}+{#a#}" by auto
with A have "A+{#a#} = B+(C-{#a#})+{#a#}" by (auto simp add: union_ac)
hence "A=B+(C-{#a#})" by simp
with CASES(2)[OF right] show ?thesis by blast
qed
qed

(* TODO: Can this proof be done more automatically ? *)
lemma mset_distrib[consumes 1, case_names dist]: assumes A: "(A::'a multiset)+B = M+N" "!!Am An Bm Bn. \<lbrakk>A=Am+An; B=Bm+Bn; M=Am+Bm; N=An+Bn\<rbrakk> \<Longrightarrow> P" shows "P"
proof -
{
fix X
have "!!A B M N P. \<lbrakk> (X::'a multiset)=A+B; A+B = M+N; !!Am An Bm Bn. \<lbrakk>A=Am+An; B=Bm+Bn; M=Am+Bm; N=An+Bn\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
proof (induct X)
case empty thus ?case by simp
next
case (add X x A B M N)
from add(2,3) have MN: "X+{#x#} = M+N" by simp
from add(2) show ?case proof (cases rule: mset_un_single_un_cases)
case left from MN show ?thesis proof (cases rule: mset_un_single_un_cases[case_names left' right'])
case left' with left have "X=A-{#x#}+B" "A-{#x#}+B = M-{#x#}+N" by simp_all
from "add.hyps"[OF this] obtain Am An Bm Bn where "A - {#x#} = Am + An" "B = Bm + Bn" "M - {#x#} = Am + Bm" "N = An + Bn" .
hence "A - {#x#} + {#x#} = Am+{#x#} + An" "B = Bm + Bn" "M - {#x#}+{#x#} = Am+{#x#} + Bm" "N = An + Bn" by (simp_all add: union_ac)
with left(1) left'(1) show ?thesis using "add.prems"(3) by auto
next
case right' with left have "X=A-{#x#}+B" "A-{#x#}+B = M+(N-{#x#})" by simp_all
from "add.hyps"[OF this] obtain Am An Bm Bn where "A - {#x#} = Am + An" "B = Bm + Bn" "M = Am + Bm" "N-{#x#} = An + Bn" .
hence "A - {#x#} + {#x#} = Am + (An+{#x#})" "B = Bm + Bn" "M = Am + Bm" "N - {#x#}+{#x#} = (An+{#x#}) + Bn" by (simp_all add: union_ac)
with left(1) right'(1) show ?thesis using "add.prems"(3) by auto
qed
next
case right from MN show ?thesis proof (cases rule: mset_un_single_un_cases[case_names left' right'])
case left' with right have "X=A+(B-{#x#})" "A+(B-{#x#}) = M-{#x#}+N" by simp_all
from "add.hyps"[OF this] obtain Am An Bm Bn where "A = Am + An" "B-{#x#} = Bm + Bn" "M - {#x#} = Am + Bm" "N = An + Bn" .
hence "A = Am + An" "B-{#x#}+{#x#} = Bm+{#x#} + Bn" "M - {#x#}+{#x#} = Am + (Bm+{#x#})" "N = An + Bn" by (simp_all add: union_ac)
with right(1) left'(1) show ?thesis using "add.prems"(3) by auto
next
case right' with right have "X=A+(B-{#x#})" "A+(B-{#x#}) = M+(N-{#x#})" by simp_all
from "add.hyps"[OF this] obtain Am An Bm Bn where "A = Am + An" "B-{#x#} = Bm + Bn" "M = Am + Bm" "N-{#x#} = An + Bn" .
hence "A = Am + An" "B-{#x#}+{#x#} = Bm + (Bn+{#x#})" "M = Am + Bm" "N - {#x#}+{#x#} = An + (Bn+{#x#})" by (simp_all add: union_ac)
with right(1) right'(1) show ?thesis using "add.prems"(3) by auto
qed
qed
qed
} with A show ?thesis by blast
qed

subsubsection {* Singleton multisets *}
lemma mset_singletonI[intro!]: "a :# {#a#}" by auto

lemma mset_singletonD[dest!]: "b :# {#a#} \<Longrightarrow> b=a"
apply(cases "a=b")
apply(auto)
done

lemma mset_size_le1_cases[case_names empty singleton,consumes 1]: "\<lbrakk> size M \<le> Suc 0; M={#} \<Longrightarrow> P; !!m. M={#m#} \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (cases M) auto

lemma diff_union_single_conv2: "a :# J \<Longrightarrow> J + I - {#a#} = (J - {#a#}) + I" using diff_union_single_conv[of J a I] by (simp add: union_ac)

lemmas diff_union_single_convs = diff_union_single_conv diff_union_single_conv2

lemma mset_contains_eq: "(m:#M) = ({#m#}+(M-{#m#})=M)" proof (auto)
assume "{#m#} + (M - {#m#}) = M"
moreover have "m :# {#m#} + (M - {#m#})" by simp
ultimately show "m:#M" by simp
qed

subsubsection {* Pointwise ordering *}

declare mset_le_trans[trans] (* Why is this not done in Multiset.thy or order-class ? *)

lemma mset_empty_minimal[simp, intro!]: "{#} \<le># c" by (unfold mset_le_def, auto)
lemma mset_empty_least[simp]: "c \<le># {#} = (c={#})" by (unfold mset_le_def, auto)
lemma mset_empty_leastI[intro!]: "c={#} \<Longrightarrow> c \<le># {#}" by (simp only: mset_empty_least)

lemma mset_le_incr_right1: "a\<le>#b \<Longrightarrow> a\<le>#b+c" using mset_le_mono_add[of a b "{#}" c, simplified] .
lemma mset_le_incr_right2: "a\<le>#b \<Longrightarrow> a\<le>#c+b" using mset_le_incr_right1 by (auto simp add: union_commute)
lemmas mset_le_incr_right = mset_le_incr_right1 mset_le_incr_right2

lemma mset_le_decr_left1: "a+c\<le>#b \<Longrightarrow> a\<le>#b" using mset_le_incr_right1 mset_le_mono_add_right_cancel by blast
lemma mset_le_decr_left2: "c+a\<le>#b \<Longrightarrow> a\<le>#b" using mset_le_decr_left1 by (auto simp add: union_ac)
lemmas mset_le_decr_left = mset_le_decr_left1 mset_le_decr_left2

lemma mset_le_single_conv[simp]: "({#e#}\<le>#M) = (e:#M)" by (unfold mset_le_def) auto

lemma mset_le_trans_elem: "\<lbrakk>e :# c; c \<le># c'\<rbrakk> \<Longrightarrow> e :# c'" using mset_le_trans[of "{#e#}" c c', simplified] by assumption

lemma mset_le_subtract: "A\<le>#B \<Longrightarrow> A-C \<le># B-C"
apply (unfold mset_le_def)
apply auto
apply (subgoal_tac "count A a \<le> count B a")
apply arith
apply simp
done

lemma mset_le_union: "A+B \<le># C \<Longrightarrow> A\<le>#C \<and> B\<le>#C" by (auto dest: mset_le_decr_left)

lemma mset_le_subtract_left: "A+B \<le># X \<Longrightarrow> B \<le># X-A \<and> A\<le>#X" by (auto dest: mset_le_subtract[of "A+B" "X" "A"] mset_le_union)
lemma mset_le_subtract_right: "A+B \<le># X \<Longrightarrow> A \<le># X-B \<and> B\<le>#X" by (auto dest: mset_le_subtract[of "A+B" "X" "B"] mset_le_union)

lemma mset_le_addE: "\<lbrakk> xs \<le># ys; !!zs. ys=xs+zs \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" using mset_le_exists_conv by blast

lemma mset_2dist2_cases:
assumes A: "{#a#}+{#b#} \<le># A+B"
assumes CASES: "{#a#}+{#b#} \<le># A \<Longrightarrow> P" "{#a#}+{#b#} \<le># B \<Longrightarrow> P" "\<lbrakk>a :# A; b :# B\<rbrakk> \<Longrightarrow> P" "\<lbrakk>a :# B; b :# A\<rbrakk> \<Longrightarrow> P"
shows "P"
proof -
{ assume C: "a :# A" "b :# A-{#a#}"
with mset_le_mono_add[of "{#a#}" "{#a#}" "{#b#}" "A-{#a#}"] have "{#a#}+{#b#} \<le># A" by auto
} moreover {
assume C: "a :# A" "\<not> (b :# A-{#a#})"
with A have "b:#B" by (unfold mset_le_def) (auto split: split_if_asm)
} moreover {
assume C: "\<not> (a :# A)" "b :# B-{#a#}"
with A have "a :# B" by (unfold mset_le_def) (auto split: split_if_asm)
with C mset_le_mono_add[of "{#a#}" "{#a#}" "{#b#}" "B-{#a#}"] have "{#a#}+{#b#} \<le># B" by auto
} moreover {
assume C: "\<not> (a :# A)" "\<not> (b :# B-{#a#})"
with A have "a:#B \<and> b:#A" by (unfold mset_le_def) (auto split: split_if_asm)
} ultimately show P using CASES by blast
qed

lemma mset_union_subset: "A+B \<le># C \<Longrightarrow> A\<le>#C \<and> B\<le># C"
apply (unfold mset_le_def)
apply auto
apply (subgoal_tac "count A a + count B a \<le> count C a", arith, simp)+
done

lemma mset_union_subset_s: "{#a#}+B \<le># C \<Longrightarrow> a :# C \<and> B \<le># C" by (auto dest: mset_union_subset)

lemma mset_le_eq_refl: "a=b \<Longrightarrow> a\<le>#b" by simp

lemma mset_singleton_eq[simplified,simp]: "a :# {#b#} = (a=b)" by auto -- {* The simplification is here due to the lemma @{thm [source] "Multiset.count_single"}, that will be applied first deleting any application potential for this rule*}
lemma mset_le_single_single[simp]: "({#a#} \<le># {#b#}) = (a=b)" by auto

lemma mset_le_single_conv1[simp]: "(M+{#a#} \<le># {#b#}) = (M={#} \<and> a=b)"
proof (auto)
assume A: "M+{#a#} \<le># {#b#}" thus "a=b" by (auto dest: mset_le_decr_left2)
with A mset_le_mono_add_right_cancel[of M "{#a#}" "{#}", simplified] show "M={#}" by blast
qed

lemma mset_le_single_conv2[simp]: "({#a#}+M \<le># {#b#}) = (M={#} \<and> a=b)" by (simp add: union_ac)

lemma mset_le_single_cases[consumes 1, case_names empty singleton]: "\<lbrakk>M\<le>#{#a#}; M={#} \<Longrightarrow> P; M={#a#} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" by (induct M) auto

lemma mset_le_distrib[consumes 1, case_names dist]: "\<lbrakk>X\<le>#A+B; !!Xa Xb. \<lbrakk>X=Xa+Xb; Xa\<le>#A; Xb\<le>#B\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P"