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'
> 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
> 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":
> http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg04268.html
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
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