Re: [isabelle] HOL-Proofs



On Thu, 13 Jun 2013, Stefan Berghofer wrote:

On 06/13/2013 09:17 AM, Christian Sternagel wrote:
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?

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 :-(

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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.