Re: [isabelle] Exporting Proof Terms to Text File

On Mon, 5 Nov 2012, Gransden, Thomas wrote:

I'm looking for some guidance to complete a task that I would like to do.

In my theory file, I have the following code:

ML {*
val thm = @{thm "a1"};
val prf = Proofterm.proof_of (Proofterm.strip_thm (Thm.proof_body_of thm));

ML {*
Pretty.writeln (Proof_Syntax.pretty_proof @{context} prf'');

which gives me a proof term, as required. I would like to export the proof terms for each lemma in my theory file into a text file, so that I can do some analysis on the proof steps used in each proof.

These are actually two independent things: writing stuff to a file and analysing what the prover did internally. Isabelle/ML is a quite able language to do analysis of symbolic datastructures, so if you stay within that environment you don't have to read or write files. File-system operations introduce statefulness that make it hard to work reliably in a multi-version multi-threaded environment like Isabelle --- unless you force it into sequential TTY mode and spoil the game.

If you still do need to externalize and export material from Isabelle/ML, the current way to do it (in Isabelle2012) is via the XML data encoding, and prefereably the YXML transfer syntax (then you don't have to struggle with XML parsers on the other side). See $ISABELLE_HOME/src/Pure/PIDE/ with xml.ML and yxml.ML in particular. There are also Scala versions of the same. Example applications are $ISABELLE_HOME/src/Pure/term_xml.ML for the main logical datatypes of Isabelle.

This is all perfectly normal Isabelle/ML user space.

Moreover, see where the same approach is made independent of Isabelle/ML, to work in plain SML or OCaml.

I still hope that more people will pick up this simple and efficient approach to externalize ML datastructures, without the full burden of XML getting in the way.

When doing the sort/typ/term application myself, I also tried the same for the proof datatype, and eliminate the old Pure/Tools/xml_syntax.ML in the course. Unfortunately, I failed to apply the proof reconstruction functions in the way they were documented 10 years ago, and did not spend further time to investigate the current situation.

So ultimately, it is probably a matter to motivate Stefan Berghofer to brush up his proof term interfaces to work with current Isabelle and the XML/YXML data representation smoothly.


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