Email Gateway (Aug 18 2022 at 13:40): Email Gateway (Aug 18 2022 at 13:40):From: Bart Kastermans <Bart.Kastermans@Colorado.EDU>
I am looking for pointers on how to extract information
about proofs from Isabelle.
Say I have some simple proof such as:
lemma
assumes "A" and "C"
shows "B --> (A --> C)"
proof
assume "B"
from A show "(A --> C)" using C ..
qed;
I would like to
1) extract the proof term,
2) find out which rules .. used to prove the lemma.
Thanks for the help.
Best,
Bart
Email Gateway (Aug 18 2022 at 13:41):From: Stefan Berghofer <berghofe@in.tum.de>
Bart Kastermans wrote:
Hi Bart,
you can use the prf and full_prf commands to inspect proof terms:
lemma test:
assumes "A" and "C"
shows "B --> (A --> C)"
proof
assume "B"
show "(A --> C)" using C .. full_prf
qed
full_prf test
The commands can either be used inside a proof, e.g. after the ..
proof method, in which case they just print the proof term corresponding
to the current proof state, or on the theory level. In the latter
case, the commands expect the name of a theorem as an argument,
whose proof term should be printed. In contrast to the full_prf
command, the prf command shows the "compact" version of the proof,
where some (reconstructable) arguments of the inference rules have been
omitted. In order for these commands to work properly, you have to switch
on proof terms for your current session by selecting
Isabelle -> Settings -> Full Proofs in ProofGeneral. Moreover,
your HOL image must have been compiled with support for proof terms
switched on, which can be achieved by adding
HOL_USEDIR_OPTIONS="-p 2"
to your .isabelle/etc/settings file.
Greetings,
Stefan
Email Gateway (Aug 18 2022 at 13:41):From: Makarius <makarius@sketis.net>
BTW, this is already the default for the precompiled image from the
Isabelle download site. There is normally no need to reconfigure and
compile yourself.
Makarius
Last updated: May 03 2024 at 12:27 UTC