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

On 10/12/13 05:36, Makarius wrote:
> On Mon, 9 Dec 2013, Lawrence Paulson wrote:
>> If you get these constraints in a proof, even if it currently works, it
>> might be a good idea to look for a different proof (by explicitly
>> instantiating a variable that is currently left uninstantiated) to get
>> rid of them yourself.
> It is definitely a good idea to avoid relying on such boundary
> situations, like pending flex-flex pairs, back tracking after 'apply'
> etc.
> Anyway, the reason why blast works slightly differently in
> Isabelle2013-2 (and the obsolete Isabelle2013-1) is this detail from
> the NEWS:
>    * SELECT_GOAL now retains the syntactic context of the overall goal
>    state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
>    situations.
> The change to SELECT_GOAL (210bca64b894) ensures that the goal context
> is preserved more rigorously, with add-on information like maxidxs,
> flex-flex pairs etc.  That was the very purpose of the change, in
> order to prevent other oddities from the following mailing list
> threads about "SELECT_GOAL and schematic variables":
> at

Ah, that helps explains why this suddenly came up when I couldn't see
any relevant changes to "blast" itself in the Isabelle2013/Isabele2013-1

> Note that in these threads there was never any talk about "bugs" nor
> "fixes" -- the notoriously meaningless words. The NEWS entry correctly
> anticipates some "potential INCOMPATIBILITY", although I did not know
> about this particular case when writing that piece of text.

When I use the word "bug", I tend to mean a behaviour of a computer
program that is unexpected, unintended and undesirable. There is
certainly subjectivity in whether particular behaviours are unexpected,
unintended and/or undesirable, but that doesn't make the word "bug"

> It is funny that blast smashes flex-flex pairs in the first place, and
> thus affects the overall goal state, not just the subgoal where it is
> applied.

Indeed it is funny. I would even go so far as to say it is unexpected,
unintended and undesirable.

> Trying without, i.e. removing the following line
> shows that there is no change in the success of the immediately reachable
> universe of Isabelle + AFP examples.
> Maybe there is a different impact on top-secret proofs that are
> locked-up in some cellar like the Lost Ark in some Indiana Jones
> movie, but who knows?

Thanks for the suggestion.

I will make the change and see how it affects all the top-secret proofs
available in the dark cellars around here and report back.



The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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