[isabelle] Exporting Proof Terms to Text File



Hello all,

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.

Firstly, is there any existing functionality to do this task? Something that will take each lemma in the theory file, and perform the above commands on them.

If not, I realise that there might be a few alternatives, such as writing my own function in ML, modifying existing Isabelle functionality, or modifying Proof General, in which case I realise the Isabelle dev mailing list might be a better place to post.

If anybody has any thoughts on this problem, I would be interested to hear them.

All the best,

Tom




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