Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



On Wed, 11 Dec 2013, Makarius wrote:

Anyway, after heating my office with more CPU power (running Isabelle + AFP + IsaFoR a few times), I have the impression that there is nothing to see on this thread, and we can just move on. This means we can probably remove the extra clean-up step from blast in coming Isabelle versions.

Further explanations when the current build has terminated ...

There were various delays, failures, non-termination, but mostly due to other reasons. We have again a situation where AFP feels very "heavy" (even on 8 cores), and the many repository clones and branches sometimes cause confusion what needs to be tested.


Anyway, according to the current situation in Isabelle2013-2, there are merely these few spots where flexflex-pairs occur and blast smashes them:

(line 99 of "~~/src/HOL/Cardinals/Wellorder_Embedding.thy")
(line 406 of "~~/src/HOL/Library/Ramsey.thy")
(line 408 of "~~/src/HOL/Library/Ramsey.thy")
(line 318 of "$AFP/thys/Markov_Models/ex/PCTL.thy")
(line 376 of "$AFP/thys/Stuttering_Equivalence/PLTL.thy")
(line 534 of "$AFP/thys/Stuttering_Equivalence/PLTL.thy")

All of these are harmless. Doing nothing about flexflex pairs within blast means they are smashed a bit later at the end of the proof, as usual.

I've recently seen other proof tools like "fast" introducing left-over flexflex pairs, but the only problem was some divergence in the enclosing goal infrastructure, where they were treated non-uniformly by accident.


So it looks like the global flexflex context of a goal state (the "tpairs") is best left alone by regular proof tools. They just accumulate monotonically like maxidx, and final results are somehow standardized by the system infrastructure.

Thus tools that do require pending fleflex constraints to work, will have better chances.

We should try that, but of course observations might change again in the coming months before the next release.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.