Email Gateway (Aug 22 2022 at 09:03): Email Gateway (Aug 22 2022 at 09:03):From: "K. Nienhuis" <kn307@cam.ac.uk>
Hi,
In the attached example, blast fails when given an elim of the form "P
/\ Q /\ R" but succeeds when given the same rule with parenthesis "(P /\
Q) /\ R". What is the explanation for that behaviour?
Thanks,
Kyndylan
BracketsAndBlast.pdf
BracketsAndBlast.thy
Email Gateway (Aug 22 2022 at 09:03):From: Larry Paulson <lp15@cam.ac.uk>
This is quite a strange example, indeed they should all work. But it’s worth pointing out that the result you express using “obtains” should be free of conjunctions:
obtains “bar" “True" "∀x. True"
In this case, it does work correctly.
Larry Paulson
Email Gateway (Aug 22 2022 at 09:04):From: Makarius <makarius@sketis.net>
Note that "blast" is a variant of the so-called Classical Reasoner, which
is explained in the "isar-ref" manual section 9. In particular, section
9.4.6 on single-step tactics helps to develop a sense how these tools
normally work, e.g. via "apply step" you similate a crude trace mode.
That should eventually provide clues about "fast" and "best", and might
help to bridges over to "blast" and "auto", although these tools have
their own specialities.
Makarius
Last updated: Apr 24 2024 at 01:07 UTC