Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] HOL-Proofs


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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: Mar 29 2024 at 12:28 UTC