author desharna Sat, 27 Nov 2021 10:16:46 +0100 changeset 75251 74ac414618e2 parent 75250 3e55e47a37e7 child 75252 aa51e974b688
added lemmas multp_implies_one_step, one_step_implies_multp, and subset_implies_multp
```--- a/src/HOL/Library/Multiset.thy	Sat Nov 27 10:05:59 2021 +0100
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 27 10:16:46 2021 +0100
@@ -2986,6 +2986,9 @@
qed
qed

+lemmas multp_implies_one_step =
+  mult_implies_one_step[of "{(x, y). r x y}" for r, folded multp_def transp_trans, simplified]
+
lemma one_step_implies_mult:
assumes
"J \<noteq> {#}" and
@@ -3018,6 +3021,9 @@
qed
qed

+lemmas one_step_implies_multp =
+  one_step_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def, simplified]
+
lemma subset_implies_mult:
assumes sub: "A \<subset># B"
shows "(A, B) \<in> mult r"
@@ -3030,6 +3036,8 @@
by (rule one_step_implies_mult[of "B - A" "{#}" _ A, unfolded ApBmA, simplified])
qed

+lemmas subset_implies_multp = subset_implies_mult[of _ _ "{(x, y). r x y}" for r, folded multp_def]
+

subsection \<open>The multiset extension is cancellative for multiset union\<close>
```