Florian Haftmann wrote:
> Hi Bertram,
>
> > How shall we proceed? As I hinted at earlier I do not have (nor want, at
> > this point) push access, but I can prepare a patch or clone of the repo,
> > if that helps, or just provide a plain theory file that works with the
> > development version of Isabelle.
>
> a repo URL or a patch is indeed the best thing to proceed: there is not
> »the« development version but an ongoing agile development.
Okay, I have exported a series of two patches against 1e7c5bbea36d,
the first adding monotonicity lemmata and the second for cancellation
and `multp`, `multeq`. See the attached file.
Cheers,
Bertram
# HG changeset patch
# User Bertram Felgenhauer
# Date 1470657709 -7200
# Mon Aug 08 14:01:49 2016 +0200
# Node ID 852c841c2ecde57bd9d0695edbad5b392ab418b5
# Parent 1e7c5bbea36dd2dd56705630f8e456de91b9788a
add monotonicity propertyies of `mult1` and `mult`
diff -r 1e7c5bbea36d -r 852c841c2ecd src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Sun Aug 07 12:10:49 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Aug 08 14:01:49 2016 +0200
@@ -2214,6 +2214,14 @@
obtains a M0 K where "M = M0 + {#a#}" "N = M0 + K" "\b. b \# K \ (b, a) \ r"
using assms unfolding mult1_def by blast
+lemma mono_mult1:
+ assumes "r \ r'" shows "mult1 r \ mult1 r'"
+unfolding mult1_def using assms by blast
+
+lemma mono_mult:
+ assumes "r \ r'" shows "mult r \ mult r'"
+unfolding mult_def using mono_mult1[OF assms] trancl_mono by blast
+
lemma not_less_empty [iff]: "(M, {#}) \ mult1 r"
by (simp add: mult1_def)
# HG changeset patch
# User Bertram Felgenhauer
# Date 1470657822 -7200
# Mon Aug 08 14:03:42 2016 +0200
# Node ID 842352253b462144ba8a26e45080f53a1cefe2d8
# Parent 852c841c2ecde57bd9d0695edbad5b392ab418b5
prove monotonicity of `mult1` and `mult`
diff -r 852c841c2ecd -r 842352253b46 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy Mon Aug 08 14:01:49 2016 +0200
+++ b/src/HOL/Library/Multiset.thy Mon Aug 08 14:03:42 2016 +0200
@@ -2404,115 +2404,103 @@
\ (I + K, I + J) \ mult r"
using one_step_implies_mult_aux by blast
-subsection \A quasi-executable characterization\
-
-text \
- The decreasing parts \A\ and \B\ of multisets in a multiset-comparison
- \(I + B, I + A) \ mult r\, can always be made disjoint.
-\
-lemma decreasing_parts_disj:
- assumes "irrefl r" and "trans r"
-and "A \ {#}" and *: "\b\#B. \a\#A. (b, a) \ r"
- defines "Z \ A #\ B"
- defines "X \ A - Z"
- defines "Y \ B - Z"
- shows "X \ {#} \ X #\ Y = {#} \
-A = X + Z \ B = Y + Z \ (\y\#Y. \x\#X. (y, x) \ r)"
+
+subsection \The multiset extension is cancellative for multiset union\
+
+lemma mult_cancel:
+ assumes "trans s" and "irrefl s"
+ shows "(X + Z, Y + Z) \ mult s \ (X, Y) \ mult s" (is "?L \ ?R")
+proof
+ assume ?L thus ?R
+ proof (induct Z)
+case (add Z z)
+obtain X' Y' Z' where *: "X + Z + {#z#} = Z' + X'" "Y + Z + {#z#} = Z' + Y'" "Y' \ {#}"
+ "\x \ set_mset X'. \y \ set_mset Y'. (x, y) \ s"
+ using mult_implies_one_step[OF `trans s` add(2)] unfolding add.assoc by blast
+consider Z2 where "Z' = Z2 + {#z#}" | X2 Y2 where "X' = X2 + {#z#}" "Y' = Y2 + {#z#}"
+ using *(1,2) by (metis mset_add union_iff union_single_eq_member)
+thus ?case
+proof (cases)
+ case 1 thus ?thesis using * one_step_implies_mult[of Y' X' s Z2]
+by (auto simp: add.commute[of _ "{#_#}"] add.assoc intro: add(1))
+next
+ case 2 then obtain y where "y \ set_mset Y2" "(z, y) \ s" using *(4) `irrefl s`
+by (auto simp: irrefl_def)
+ moreover from this transD[OF `trans s` _ this(2)]
+ have "x' \ set_mset X2 \ \y \ set_mset Y2. (x', y) \ s" for x'
+using 2 *(4)[rule_format, of x'] by auto
+ ultimately show ?thesis using * one_step_implies_mult[of Y2 X2 s Z'] 2
+by (force simp: add.commute[of "{#_#}"] add.assoc[symmetric] intro: add(1))
+qed
+ qed auto
+next
+ assume ?R then obtain I J K
+where "Y = I + J" "X = I + K" "J \ {#}" "\k \ set_mset K. \j \ set_mset J. (k, j) \ s"
+using mult_implies_one_step[OF `trans s`] by blast
+ thus ?L using one_step_implies_mult[of J K s "I + Z"] by (auto simp: ac_simps)
+qed
+
+lemma mult_cancel_max:
+ assumes "trans s" and "irrefl s"
+ shows "(X, Y) \ mult s \ (X - X #\ Y, Y - X #\ Y) \ mult s" (is "?L \ ?R")
proof -
- define D
-where "D = set_mset A \ set_mset B"
- let ?r = "r \ D \ D"
- have "irrefl ?r" and "trans ?r" and "finite ?r"
-using \irrefl r\ and \trans r\ by (auto simp: D_def irrefl_def trans_Restr)
- note wf_converse_induct = wf_induct [OF wf_converse [OF this]]
- { fix b assume "b \# B"
-then have "\x. x \# X \ (b, x) \ r"
-proof (induction rule: wf_converse_induct)
- case (1 b)
- then obtain a where "b \# B" and "a \# A" and "(b, a) \ r"
-using * by blast
- then show ?case
- proof (cases "a \# X")
-case False
-then have "a \# B" using \a \# A\
-
