Re: [isabelle] Exporting Proof Terms to Text File



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*)


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