Email Gateway (Aug 19 2022 at 11:16): Email Gateway (Aug 19 2022 at 11:16):From: Christian Sternagel <c.sternagel@gmail.com>
Dear all,
when browsing ~~/src/HOL/Proofs/Extraction/Higman_Extraction.thy using
isabelle jedit -l HOL-Proofs Higman_Extraction.thy
I get the error
name_of_thm: bad proof of theorem
...
in line 14. What am I missing?
cheers
chris
Email Gateway (Aug 19 2022 at 11:16):From: Stefan Berghofer <berghofe@in.tum.de>
Hi Christian,
looks like you have not switched on proof terms for the current session. You could
try to temporarily add something like
ML {* proofs := 2 *}
at the beginning of Higman.thy. In ProofGeneral, proof terms can be switched on for
the current session using the Settings menu, but I have no idea how this can be done
in JEdit :-(
Greetings,
Stefan
Email Gateway (Aug 19 2022 at 11:19):From: Makarius <makarius@sketis.net>
Experimenting a bit with proof terms recently, I've come across the same
pitfall, and there are a few more of them.
Conceptually it is wrong to ask the user to switch the prover interface
into a certain "mode" when processing certain theories -- that should be
specified within the theories themselves instead (in a stateless manner).
There are historical reasons, why there is still this global "proofs"
reference variable even until today in Isabelle2013. It is a fine point
to be reconsidered eventually, maybe for the next release.
Anyway, do you have some concrete applications of proof terms in mind
right now? It would be nice to get a critical mass of enthusiasm to
revitalize this important aspect of Isabelle.
Makarius
Email Gateway (Aug 19 2022 at 11:53):From: Ramana Kumar <rk436@cam.ac.uk>
One application I have in mind is generating OpenTheory packages from
Isabelle/HOL theories.
Email Gateway (Aug 19 2022 at 11:54):From: Makarius <makarius@sketis.net>
I've done a few refinements together with Stefan already, so it will be in
the next release (October / November 2013).
If you want to get involved in further testing right now, you are welcome
to come over to the isabelle-dev mailing list, based on an adhoc version
of Isabelle according to README_REPOSITORY from some repository snapshot.
(I cannot resist to point out that compiling an unofficial Isabelle
snapshot is easier than an official version of HOL4, or even Coq :-)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC