*To*: "Gransden, Thomas" <tg75 at student.le.ac.uk>*Subject*: Re: [isabelle] Exporting Proof Terms to Text File*From*: Tjark Weber <webertj at in.tum.de>*Date*: Tue, 06 Nov 2012 13:11:13 +0100*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <C090B02D9A593C4FB10E6E465AB703C401D5B0C1@DBXPRD0610MB360.eurprd06.prod.outlook.com>*References*: <C090B02D9A593C4FB10E6E465AB703C401D5B0C1@DBXPRD0610MB360.eurprd06.prod.outlook.com>

On Mon, 2012-11-05 at 16:56 +0000, Gransden, Thomas wrote: > [...] 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. 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

(* Title: Pure/General/persistent.ML ID: $Id$ Author: Tjark Weber, (c) 2007 A tactical which stores proof terms on disk and attempts to retrieve them later if the same theorem is to be proved again. *) local (* A simple hash function (from Robert Sedgewick's "Algorithms in C" book). Do NOT use for cryptographic purposes. *) val hash : Word32.word list -> Word32.word = let fun hash' a h [] = h | hash' a h (n::ns) = hash' (a * (Word32.fromInt 378551)) (h * a + n) ns in hash' (Word32.fromInt 63689) (Word32.fromInt 0) end (* maps a theorem to a string of the form "xxxxxxxx.prf" *) fun hash_thm st = st |> Thm.rep_thm |> (fn {shyps, hyps, tpairs, prop, ...} => ML_Syntax.print_list I (ML_Syntax.print_list ML_Syntax.print_sort shyps :: ML_Syntax.print_list ML_Syntax.print_term hyps :: ML_Syntax.print_list (ML_Syntax.print_pair ML_Syntax.print_term ML_Syntax.print_term) tpairs :: [ML_Syntax.print_term prop])) |> explode |> map (Word32.fromInt o ord) |> hash |> Word32.toString |> (fn s => let val size = String.size s in if size < 8 then Library.prefix (Library.replicate_string (8 - size) "0") s else s end) |> Library.suffix ".prf" (* exports a theorem's proof term to disk *) fun export path st = let val thy = Thm.theory_of_thm st in tracing ("Exporting proof to file " ^ Path.implode path); st |> Thm.proof_of |> Proofterm.rewrite_proof_notypes ([], []) |> Reconstruct.reconstruct_proof thy (Thm.prop_of st) |> Reconstruct.expand_proof thy [("", NONE)] |> XMLSyntax.xml_of_proof |> XML.string_of_tree |> File.write path end (* imports a proof term from disk *) fun import path thy = let val st = File.read path |> XML.tree_of_string |> XMLSyntax.proof_of_xml |> ProofChecker.thm_of_proof thy in tracing ("Proof read from file " ^ Path.implode path); SOME st end handle IO.Io _ => NONE | ERROR msg => (warning ("File " ^ Path.implode path ^ ": " ^ msg); NONE) in fun PERSISTENT tacf st = let val path = Path.basic (hash_thm st) in case import path (Thm.theory_of_thm st) of SOME st' => Seq.single st' | NONE => (case SINGLE tacf st of SOME st' => (if !proofs = 2 andalso (Thm.prop_of st') aconv (Thm.concl_of st) then export path st' else (); Seq.single st') | NONE => Seq.empty) end end; (*local*)

**References**:**[isabelle] Exporting Proof Terms to Text File***From:*Gransden, Thomas

- Previous by Date: Re: [isabelle] Isabelle operator precedence
- Next by Date: [isabelle] ACL2 2013 - Call For Papers
- Previous by Thread: [isabelle] Exporting Proof Terms to Text File
- Next by Thread: Re: [isabelle] Exporting Proof Terms to Text File
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list