Email Gateway (Aug 18 2022 at 10:38): Email Gateway (Aug 18 2022 at 10:38):From: Revantha Ramanayake <revantha@rsise.anu.edu.au>
Hi.
Is the subset relation defined in the obvious way for multisets? I.e.
how do I write
N is a sub-multiset of M.
I know that I can define: N is a sub-multiset of M as (ALL b. count N b
<= count M b)
but then I will have to prove a host of properties for the sub-multiset
relation.
I was wondering if the relation is already defined somewhere?
Thanks,
Revantha.
Email Gateway (Aug 18 2022 at 10:40):From: Lawrence Paulson <lp15@cam.ac.uk>
Multiset.thy defines the relation mset_le as you describe.
It also overloads <= with the much stronger multiset ordering, which
is described in a classic paper:
Nachum Dershowitz, Zohar Manna: Proving Termination with Multiset
Orderings. Commun. ACM 22(8): 465-476 (1979)
Larry
Email Gateway (Aug 18 2022 at 10:40):From: Peter Lammich <peter.lammich@uni-muenster.de>
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
mset_le_def, auto iff add: multiset_eq_conv_count_eq)
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
mset_le_add_left by (auto simp add: union_commute)
lemmas mset_le_add = mset_le_add_left mset_le_add_right
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
Last updated: May 03 2024 at 08:18 UTC