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



I need to stress a basic fact: Flex-Flex constraints invariably involve function variables. This means that the proof involved an inference rule containing a function variable, such as imageI. It is worth attempting to identify which rule is to blame (the variable name may be a clue) and to supply a suitably instantiated instance of the rule to blast.

Larry

On 13 Dec 2013, at 12:24, Makarius <makarius at sketis.net> wrote:

> 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.