# Re: [isabelle] sub-multiset relation for theory Multiset in the standard distribution

```I use the following additional lemmas when working with mset_le:

subsubsection {* Pointwise ordering *}
interpretation mset_le: partial_order["\<lambda>x y. (x\<le>#y)"] by
(auto intro: partial_order.intro mset_le_refl mset_le_antisym mset_le_trans)

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

lemma mset_le_add_left: "a\<le>#b \<Longrightarrow> a\<le>#b+c" using
mset_le_mono_add[of a b "{#}" c, simplified] .
lemma mset_le_add_right: "a\<le>#b \<Longrightarrow> a\<le>#c+b" using

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_subtract_left: "A+B \<le># V+W \<Longrightarrow> B
\<le># V+W-A" by (auto dest: mset_le_subtract[of "A+B" "V+W" "A"])
lemma mset_le_subtract_right: "A+B \<le># V+W \<Longrightarrow> A
\<le># V+W-B" by (auto dest: mset_le_subtract[of "A+B" "V+W" "B"])

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)

maybe that helps

-- Peter

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.