Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.
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
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
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.
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
That detail goes back to Isabelle/93a84eb6c522 from 02-Jan-1998, where
Larry writes in the log entry "Blast_tac now squashes flex-flex pairs
immediately", but it is unclear why. Maybe Larry remembers why he was
smashing flex-flex pairs on purpose 15 years ago.
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and