Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

2016-08-11 Thread Florian Haftmann
See now rev. 76302202a92d

Thanks for contributing!

Cheers,
Florian

Am 08.08.2016 um 14:44 schrieb Bertram Felgenhauer:
> 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
> 
> 
> 
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> 

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de



signature.asc
Description: OpenPGP digital signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


Re: [isabelle-dev] [isabelle] Proposal: An update to Multiset theory

2016-08-08 Thread Bertram Felgenhauer
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")
-