Re: [isabelle-dev] Analysis not building
Florian Haftmann wrote: > > HOL-Analysis can’t be built (reproducibly) with the latest version > > (76f2d492627e). It simply dies, no error message. > > I cannot reproduce this. Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis with Isabelle-24bbc4e30e5b and manual init-component for Poly/ML and both HOL-Analysis and IsaFoR with Isabelle-2018 and the same manual init-component. Maybe this is somehow specific to OS/X, which I believe Larry uses? That said, polyml-1b2dcf8f5202 seems to work just as well, for me. In other news, the problem with the sharing pass appears to be resolved and the IsaFoR images with x86_64_32 are now all about 60% the size of the x86_64 ones. Nice! Cheers, Bertram Numbers: ML_PLATFORM="x86_64_32-linux" ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6" ISABELLE_BUILD_OPTIONS="threads=10 parallel_proofs=2" polyml-test-1b2dcf8f5202 polyml-test-b68438d33c69 Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished HOL (0:02:23 elapsed time, 0:08:49 cpu time, factor 3.68) Finished HOL (0:02:26 elapsed time, 0:08:58 cpu time, factor 3.69) Finished HOL-Lib (0:05:12 elapsed time, 0:32:06 cpu time, factor 6.17) Finished HOL-Lib (0:04:58 elapsed time, 0:31:08 cpu time, factor 6.25) Finished HOL-AFP (0:05:40 elapsed time, 0:32:52 cpu time, factor 5.79) Finished HOL-AFP (0:05:38 elapsed time, 0:32:51 cpu time, factor 5.82) Finished IsaFoR_1 (0:05:10 elapsed time, 0:27:31 cpu time, factor 5.32) Finished IsaFoR_1 (0:05:11 elapsed time, 0:27:39 cpu time, factor 5.33) Finished IsaFoR_2 (0:05:26 elapsed time, 0:25:37 cpu time, factor 4.71) Finished IsaFoR_2 (0:05:27 elapsed time, 0:25:37 cpu time, factor 4.69) Finished IsaFoR_3 (0:06:38 elapsed time, 0:39:22 cpu time, factor 5.92) Finished IsaFoR_3 (0:06:36 elapsed time, 0:39:24 cpu time, factor 5.96) Finished IsaFoR_4 (0:08:26 elapsed time, 0:26:28 cpu time, factor 3.14) Finished IsaFoR_4 (0:08:37 elapsed time, 0:26:55 cpu time, factor 3.12) Finished Code (0:08:03 elapsed time, 0:08:11 cpu time, factor 1.02) Finished Code (0:08:02 elapsed time, 0:08:11 cpu time, factor 1.02) 19271289 Pure (0.69 x 28081037 (x86_64 heap image size)) 19269857 Pure (0.69) 250024211 HOL (0.61 x 410972244) 250129275 HOL (0.61) 307851090 HOL-Lib (0.59 x 525949867) 307921910 HOL-Lib (0.59) 537798522 HOL-AFP (0.59 x 913422879) 537694918 HOL-AFP (0.59) 428162386 IsaFoR_1 (0.59 x 724672759) 427425094 IsaFoR_1 (0.59) 367783763 IsaFoR_2 (0.59 x 623083120) 367626511 IsaFoR_2 (0.59) 419599023 IsaFoR_3 (0.59 x 712211696) 419246195 IsaFoR_3 (0.59) 284804855 IsaFoR_4 (0.59 x 480209352) 284701607 IsaFoR_4 (0.59) ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
Makarius wrote: > There was indeed something odd with sharing: David Matthews has changed > that in polyml-1b2dcf8f5202 (see Isabelle/bb0a354f6b46). I may give it another try later... > > Hardware: > > i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD > > > > Common build flags: > > ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2" > > > > Configurations: > > polyml 5.7.1x86_64ML_OPTIONS="--maxheap 24G -H 500 > > --gcthreads 6" > > polyml-a444f281ccec x86_64ML_OPTIONS="--maxheap 24G -H 500 > > --gcthreads 6" > > For this hardware I recommend threads=6. In the sessions beyond HOL, I see a speedup from threads=12. The timings are basically the same with threads=10, but I have not checked the full range of possibilities. I've made sure that the machine is mostly idle; things will be much different if several processes start competing for the ressources. Configurations: threads=6 threads=10 threads=12 Times: Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.12) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished HOL (0:02:21 elapsed time, 0:07:47 cpu time, factor 3.30) Finished HOL (0:02:25 elapsed time, 0:08:56 cpu time, factor 3.68) Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84) Finished HOL-Lib (0:05:47 elapsed time, 0:25:18 cpu time, factor 4.37) Finished HOL-Lib (0:05:12 elapsed time, 0:32:29 cpu time, factor 6.24) Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88) Finished HOL-AFP (0:06:33 elapsed time, 0:27:55 cpu time, factor 4.26) Finished HOL-AFP (0:05:51 elapsed time, 0:34:10 cpu time, factor 5.83) Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28) Finished IsaFoR_1 (0:05:11 elapsed time, 0:22:30 cpu time, factor 4.34) Finished IsaFoR_1 (0:05:04 elapsed time, 0:27:15 cpu time, factor 5.38) Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59) Finished IsaFoR_2 (0:05:57 elapsed time, 0:21:49 cpu time, factor 3.66) Finished IsaFoR_2 (0:05:43 elapsed time, 0:26:24 cpu time, factor 4.61) Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87) Finished IsaFoR_3 (0:07:13 elapsed time, 0:31:05 cpu time, factor 4.30) Finished IsaFoR_3 (0:06:51 elapsed time, 0:40:15 cpu time, factor 5.87) Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45) Finished IsaFoR_4 (0:08:37 elapsed time, 0:24:58 cpu time, factor 2.90) Finished IsaFoR_4 (0:08:48 elapsed time, 0:27:08 cpu time, factor 3.08) Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17) Finished Code (0:08:04 elapsed time, 0:08:12 cpu time, factor 1.02) Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02) Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02) > Moreover note that --gcthreads is automatically provided, if ML_OPTIONS > does not say anything else. I intended to experiment with smaller numbers but have not yet done so. On another, similar machine, --gcthreads=2 was just as fast as 6. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
Bertram Felgenhauer wrote: > Makarius wrote: > > So this is the right time for further testing of applications: > > Isabelle2018 should work as well, but I have not done any testing beyond > > "isabelle build -g main" -- Isabelle development only moves forward in > > one direction on a single branch. > > I have tried this with Isabelle2018 and IsaFoR; I've encountered no > problems and there's a nice speedup (estimated 1.25 times faster). > Heap images are 40% smaller, which is a welcome change as well. I have gathered some more data (below). There are some curiosities: - Code export (that's the only thing that the 'Code' session does, besides theory merges) seems to be slower with polyml-a444f281ccec compared to polyml 5.7.1, even when sticking to the x86_64 platform. - A similar slowdown seems to affect the IsaFoR_3 session, but I don't know what's special about that one. - While most heap images are about 40% smaller with x86_64_32, this is not always the case; some heap images ended up being even larger in this experiment. Could there be a problem with the sharing pass on x86_64_32? Cheers, Bertram Hardware: i7-6850K CPU @ 3.60GHz (6 cores x 2 hyperthreads) / 32GB RAM / SSD Software: GNU/Linux Isabelle2018 afp-2018 @ 400c722462b3 IsaFoR @ acb9096ce08a Common build flags: ISABELLE_BUILD_OPTIONS="threads=12 parallel_proofs=2" Configurations: polyml 5.7.1x86_64ML_OPTIONS="--maxheap 24G -H 500 --gcthreads 6" polyml-a444f281ccec x86_64ML_OPTIONS="--maxheap 24G -H 500 --gcthreads 6" polyml-0a6ebca445fc x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6" polyml-a444f281ccec x86_64_32 ML_OPTIONS="--maxheap 16G -H 500 --gcthreads 6" Timings: Finished Pure (0:00:11 elapsed time, 0:00:14 cpu time, factor 1.20) Finished Pure (0:00:15 elapsed time, 0:00:17 cpu time, factor 1.18) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.14) Finished Pure (0:00:13 elapsed time, 0:00:15 cpu time, factor 1.13) Finished HOL (0:02:46 elapsed time, 0:10:50 cpu time, factor 3.91) Finished HOL (0:02:41 elapsed time, 0:10:05 cpu time, factor 3.75) Finished HOL (0:02:32 elapsed time, 0:09:46 cpu time, factor 3.84) Finished HOL (0:02:28 elapsed time, 0:09:20 cpu time, factor 3.78) Finished HOL-Lib (0:05:00 elapsed time, 0:35:54 cpu time, factor 7.18) Finished HOL-Lib (0:05:19 elapsed time, 0:36:41 cpu time, factor 6.88) Finished HOL-Lib (0:05:10 elapsed time, 0:35:32 cpu time, factor 6.88) Finished HOL-Lib (0:04:57 elapsed time, 0:34:16 cpu time, factor 6.91) Finished HOL-AFP (0:05:59 elapsed time, 0:37:39 cpu time, factor 6.28) Finished HOL-AFP (0:06:15 elapsed time, 0:38:31 cpu time, factor 6.15) Finished HOL-AFP (0:05:41 elapsed time, 0:35:44 cpu time, factor 6.28) Finished HOL-AFP (0:05:33 elapsed time, 0:35:01 cpu time, factor 6.30) Finished IsaFoR_1 (0:05:46 elapsed time, 0:31:43 cpu time, factor 5.49) Finished IsaFoR_1 (0:05:42 elapsed time, 0:31:06 cpu time, factor 5.46) Finished IsaFoR_1 (0:05:21 elapsed time, 0:29:58 cpu time, factor 5.59) Finished IsaFoR_1 (0:05:17 elapsed time, 0:29:15 cpu time, factor 5.54) Finished IsaFoR_2 (0:06:07 elapsed time, 0:29:37 cpu time, factor 4.84) Finished IsaFoR_2 (0:06:04 elapsed time, 0:29:15 cpu time, factor 4.82) Finished IsaFoR_2 (0:05:40 elapsed time, 0:27:39 cpu time, factor 4.87) Finished IsaFoR_2 (0:05:59 elapsed time, 0:28:14 cpu time, factor 4.72) Finished IsaFoR_3 (0:07:30 elapsed time, 0:47:56 cpu time, factor 6.38) Finished IsaFoR_3 (0:09:58 elapsed time, 0:55:27 cpu time, factor 5.56) ? Finished IsaFoR_3 (0:06:45 elapsed time, 0:43:32 cpu time, factor 6.45) Finished IsaFoR_3 (0:06:49 elapsed time, 0:43:20 cpu time, factor 6.35) Finished IsaFoR_4 (0:09:40 elapsed time, 0:30:25 cpu time, factor 3.15) Finished IsaFoR_4 (0:09:14 elapsed time, 0:29:16 cpu time, factor 3.17) Finished IsaFoR_4 (0:08:47 elapsed time, 0:27:52 cpu time, factor 3.17) Finished IsaFoR_4 (0:08:52 elapsed time, 0:27:57 cpu time, factor 3.15) Finished Code (0:05:30 elapsed time, 0:05:42 cpu time, factor 1.03) Finished Code (0:08:34 elapsed time, 0:08:46 cpu time, factor 1.02) ? Finished Code (0:07:59 elapsed time, 0:08:08 cpu time, factor 1.02) Finished Code (0:08:00 elapsed time, 0:08:08 cpu time, factor 1.02) total 00:48:29 total 00:54:02 total 00:48:08 total 00:48:08 Heap image sizes (factor): 28081037 Pure (1.00) 25131549 Pure (0.89) 19271077 Pure (0.68) 19270685 Pure (0.68) 410972244 HOL (1.00) 403934084 HOL (0.98) 249583659 HOL (0.61) 249808871 HOL (0.61) 525949867 HOL-Lib (1.00) 526132427 HOL-Lib (1.00) 308088218 HOL-Lib (0.59) 307456194 HOL-Lib (0.58) 913422879 HOL-AFP (1.00) 915450415 HOL-AFP (1.00) 537947934 HOL-AFP (0.59) 538445922 HOL-AFP (0.59) 724
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
Makarius wrote: > On 22/01/2019 12:31, Bertram Felgenhauer wrote: > > Makarius wrote: > >> So this is the right time for further testing of applications: > >> Isabelle2018 should work as well, but I have not done any testing beyond > >> "isabelle build -g main" -- Isabelle development only moves forward in > >> one direction on a single branch. > > > > I have tried this with Isabelle2018 and IsaFoR; I've encountered no > > problems and there's a nice speedup (estimated 1.25 times faster). > > Heap images are 40% smaller, which is a welcome change as well. > > Is that compared to x86_64 (full 64-bit) or x86 (old 32-bit)? This is compared to x86_64. Sorry, I should have mentioned this, but to my mind it was implied because IsaFoR is notorious for running out of memory with the x86 version of PolyML. > I am asking this, because I have noted a speedup of building heap > images: x86_64_32 compared to x86, and was wondering about the reasons > for it. (For x86_64 everything is just more bulky, of course, including > heaps.) As far as I can see, one difference between x86 and x86_64_32 is that PolyML keeps heap objects aligned to 8 byte boundaries for the latter. This may impact performance. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Poly/ML x86_64_32 available for testing
Makarius wrote: > So this is the right time for further testing of applications: > Isabelle2018 should work as well, but I have not done any testing beyond > "isabelle build -g main" -- Isabelle development only moves forward in > one direction on a single branch. I have tried this with Isabelle2018 and IsaFoR; I've encountered no problems and there's a nice speedup (estimated 1.25 times faster). Heap images are 40% smaller, which is a welcome change as well. Thanks a lot, David and Makarius! Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
Makarius wrote: > On 08/11/2018 14:59, Bertram Felgenhauer wrote: > >> > >> I've misunderstood the problem. You intend to invoke old-style > >> $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > >> Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. > > > > This may be premature, but I foresee that now that `isabelle ghc` > > and `isabelle ghci` exist, we will have scripts that use them. > > There is indeed some confusion here. > > My reluctance to execute $ISABELLE_GHC inside lib/Tools/ghc is explained > by the odd recursive setup: in the stack situation, $ISABELLE_GHC points > to lib/Tools/ghc, and some mistake in the configuration could lead to > infinite recursion of sub-processes (potential bombing of the OS). > > It is probably better to leave the meaning of ISABELLE_GHC (and > ISABELLE_OCAML, ISABELLE_OCAMLC) unchanged, and remove the "isabelle > ghc" tool entry points: these auxiliary scripts should go into > $ISABELLE_HOME/lib/scripts where they cannot be mistaken as regular > Isabelle tools. Sounds good to me. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
Makarius wrote: > On 08/11/2018 11:30, Bertram Felgenhauer wrote: > > Makarius wrote: > >> Nonetheless, it is still possible to use "isabelle ghc" without stack: > >> you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the > >> Isabelle settings mechanism to override ISABELLE_GHC with the > >> stack-based tools. > > > > After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about > > a missing GHC setup, since there's no fallback on a custom > > $ISABELLE_GHC. I've added such a fallback in the attached patch, > > does that look reasonable? > > I've misunderstood the problem. You intend to invoke old-style > $ISABELLE_GHC via the new-style "isabelle ghc" interface, but within > Isabelle/ML sessions the standard way is still $ISABELLE_GHC in both cases. This may be premature, but I foresee that now that `isabelle ghc` and `isabelle ghci` exist, we will have scripts that use them. > So just the usual question: What are remaining uses of this? Why not > uninstall the "system ghc" and only use stack? I don't think that the desire of using an existing ghc installation is unusual. I'm not sure how common maintaining a ghc installation without stack is these days, but ghc + cabal-install are still quite sufficient for Haskell development. I don't care much about disk space, but I do resent stack's propensity for downloading huge tarballs without even prompting; my bandwidth is often limited. So I try hard to avoid that particular tool. > My impression is that up-to-date Haskell projects are all using stack by > default. My desire is to be able to override the default, not to change it. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
Makarius wrote: > Nonetheless, it is still possible to use "isabelle ghc" without stack: > you need to purge the $ISABELLE_STACK_ROOT directory, to prevent the > Isabelle settings mechanism to override ISABELLE_GHC with the > stack-based tools. After purging $ISABELLE_STACK_ROOT, `isabelle ghc` complains about a missing GHC setup, since there's no fallback on a custom $ISABELLE_GHC. I've added such a fallback in the attached patch, does that look reasonable? Cheers, Bertram diff -r 0a9688695a1b lib/Tools/ghc --- a/lib/Tools/ghc Thu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghc Thu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghc -- "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" "$@" else echo "Cannot execute ghc: missing Isabelle GHC setup" >&2 exit 127 diff -r 0a9688695a1b lib/Tools/ghci --- a/lib/Tools/ghciThu Nov 08 09:11:52 2018 +0100 +++ b/lib/Tools/ghciThu Nov 08 11:25:55 2018 +0100 @@ -6,6 +6,8 @@ if [ -d "$ISABELLE_STACK_ROOT" -a -n "$ISABELLE_GHC" ]; then isabelle_stack ghci "$@" +elif [ -n "$ISABELLE_GHC" ]; then + "$ISABELLE_GHC" --interactive "$@" else echo "Cannot execute ghci: missing Isabelle GHC setup" >&2 exit 127 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS: support for GHC
Makarius wrote: > *** System *** > > * Support for Glasgow Haskell Compiler via command-line tools "isabelle > ghc_setup", "isabelle ghci", "isabelle ghc", "isabelle ghc_stack". > Existing settings variable ISABELLE_GHC is maintained dynamically > according the state of ISABELLE_STACK_ROOT and ISABELLE_STACK_RESOLVER. > > > This refers to Isabelle/1722cc56d22e. Is there a way to use a system ghc with `isabelle ghc` and `isabelle ghci`? I want to avoid the 145MB download and extra installation of ghc if possible. Note in particular that setting ISABELLE_GHC now has a peculiar effect on `isabelle ghc`. Without the environment variable, the command complains: Cannot execute ghc: missing Isabelle GHC setup However, if ISABELLE_GHC is set in $ISABELLE_HOME/etc/settings, then the same command starts downloading ghc via stack... > isabelle ghc Preparing to install GHC (tinfo6) to an isolated location. This will not interfere with any system-level installation. Preparing to download ghc-tinfo6-8.4.4 ...^C Given the size of the download I find this unsatisfactory (145 MB is still big for mobile plans.) Cheers, Bertram ___ 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
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
Re: [isabelle-dev] Multiset insert
Tobias Nipkow wrote:
>
> I am all in favour of a variation of "add" - it corresponds nicely to "+".
> Of course not "add" by itself, that is too generic. How about
>
> definition add_mset :: "'a ⇒ 'a multiset ⇒ 'a multiset" ("add#") where
> "add# x M = {#x#} + M"
I like "add#".
Will the introduction of add# mean that the induction principle for
multisets will be changed as well? If so, do you have a migration path
for proofs based on the current induction principle? (Currently there
are two cases, {#} and M + {#x#}; note that the singleton multiset
appears on the right, and given that Isabelle's simplifier is not very
good at handling AC symbols, changing the order has to potential to
break a lot of proofs).
Cheers,
Bertram
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] code abbreviation for mapping over a fixed range
Hi Florian, > > This email refers to the following commit: > > > > http://isabelle.in.tum.de/repos/isabelle/rev/7d1127ac2251 > > > > code abbreviation for mapping over a fixed range > > > > Is there a specific reason for this code equation: > > > > "map_range f (Suc n) = map_range f n @ [f n]" > > > > It seems rather inefficient. Anyway, what's the purpose of "map_range". > > the idea of map_range is to avoid building a list first and then mapping it. Please don't forget about this. The new definition actually causes *more* allocation than the original one, except for very short lists, because every call of @ copies its first argument. Note that the code equation for [_..<_] is lemma upt_rec[code]: "[i..https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] AFP devel not reachable
David Cock wrote: > Apparently they had a storage system issue, and obviously didn't have a > tested recovery plan. There's some more information here: http://sourceforge.net/blog/sourceforge-infrastructure-and-service-restoration/ In short, they are working on it, and interestingly, they are holding restoration of SCM services off until last... > At this point, the sooner everybody moves off of > Sourceforge, the better. It'd also be nice to have a mirror of the repository, regardless of where it's hosted. Cheers, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Broken component: jdk7u40
Lars Hupel wrote: > I was trying to update to the repository version today, but: > > $ bin/isabelle components -a > ### Missing Isabelle component: "/home/lars/.isabelle/contrib/jdk-7u40" > Getting "http://isabelle.in.tum.de/components/jdk-7u40.tar.gz"; > Unpacking "/home/lars/.isabelle/contrib/jdk-7u40.tar.gz" > tar: Skipping to next header > tar: A lone zero block at 840553 > tar: Exiting with failure status due to previous errors This happens here, too. I have two copies of the jdk-7u40.tar.gz file, one three days old, with sha1sum dd24d63afd6d17b29ec9cb2b2464d4ff2e02de2c and one downloaded today with sha1sum 246651f97aacf79b9833ff8988bb1f5e7263037b The latter file produces the error from above when unpacked. Re-downloading doesn't help; the file checksum stays the same. The two files are almost identical; they have the same size, and just a few bytes differ in the 8kb block starting at offset 185348096. Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
[isabelle-dev] Tweak Haskell output for future Haskell compatibility.
Dear Isabelle developers, the Haskell code generator of Isabelle currently emits contexts for data and newtype generates, e.g. (from CeTA): newtype (Linorder a) => Rbt a b = Rbt (Rbta a b); The sole effect of such contexts is that the programmer must provide a (Linorder a) context wherever Rbt a b is used, which is fairly uselss. In the next version of the Haskell language definition (whenever that will be), this feature will be removed. http://www.haskell.org/pipermail/haskell-prime/2011-January/003335.html http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts Ghc currently requires a flag (-XDatatypeContexts) to compile code using datatype contexts. In the latest release (7.4.1), this option emits a warning: Warning: -XDatatypeContexts is deprecated: It was widely considered a misfeature, and has been removed from the Haskell language. I propose, therefore, to omit these contexts in code generated by Isabelle. This can safely wait until after the release, of course. (patch attached) Best regards, Bertram # HG changeset patch # User felgenhauer # Date 1336397766 -7200 # Node ID 1a976d546b94ca265a26f6d916a7f54979c0c547 # Parent 29212a4bb866adc5f8f94a85602acb8dbcd65f81 do not generate contexts for datatype declarations in generated Haskell code (see http://hackage.haskell.org/trac/haskell-prime/wiki/NoDatatypeContexts) diff -r 29212a4bb866 -r 1a976d546b94 src/Tools/Code/code_haskell.ML --- a/src/Tools/Code/code_haskell.ML Fri May 04 17:12:37 2012 +0200 +++ b/src/Tools/Code/code_haskell.ML Mon May 07 15:36:06 2012 +0200 @@ -57,7 +57,7 @@ | SOME (_, print) => print (print_typ tyvars) fxy tys) | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; fun print_typdecl tyvars (vs, tycoexpr) = - Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); + print_tyco_expr tyvars NOBR tycoexpr; fun print_typscheme tyvars (vs, ty) = Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty); fun print_term tyvars some_thm vars fxy (IConst c) = ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Isabelle_11-Sep-2011
Dear Makarius and René, > >However, testing Isabelle_20-Sep-2011 with Emacs 23.3, there seems to be a > >problem for Mac OS Lion users: > >Many special characters like ==> \in, => are not displayed correctly which > >makes working inconvenient. Under > > > >http://cl-informatik.uibk.ac.at/~thiemann/emacs.html I believe I know this bug. It's an emacs problem, and should be fixed in emacs 23.4 once it becomes available. That said I don't know of any elisp code other than ProofGeneral that tickles this bug. As far as Isabell/PG are concerned, it's not a new problem -- it also affects Isabelle2011. See http://debbugs.gnu.org/cgi/bugreport.cgi?bug=8703 (Note that I encountered this problem with Linux -- I hope that the MacOS version uses the same code, but I have not tested this theory.) Best regards, Bertram ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
