Email Gateway (Aug 19 2022 at 09:17): Email Gateway (Aug 19 2022 at 09:17):From: "Gransden, Thomas" <tg75@student.le.ac.uk>
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
Email Gateway (Aug 19 2022 at 09:18):From: Tjark Weber <webertj@in.tum.de>
Around 2007 I wrote a tactical that exported proof terms in XML format,
based on functionality by Stefan Berghofer. I am attaching my code
(which never made it into the Isabelle repository and most likely no
longer works with Isabelle2012, but may still serve as a starting point
for your own investigations). For explanations, see Section 5.5 of
http://user.it.uu.se/~tjawe125/publications/weber08satbased.pdf
Best regards,
Tjark
persistent.ML
Email Gateway (Aug 19 2022 at 09:21):From: Makarius <makarius@sketis.net>
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 https://bitbucket.org/makarius/yxml 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.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC