# HG changeset patch
# User sultana
# Date 1392825422 0
# Node ID 25d7b485df816bdc639076ab2942826140ea1739
# Parent  928b9f6771652b978d80b42bea89cd6357071e6c
added a function that carries out all the reconstruction steps, for improved usability;
added documentation;

diff -r 928b9f677165 -r 25d7b485df81 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -3,6 +3,42 @@
 
 Proof reconstruction for Leo-II.
 
+USAGE:
+* Simple call the "reconstruct_leo2" function.
+* For more advanced use, you could use the component functions used in
+  "reconstruct_leo2" -- see TPTP_Proof_Reconstruction_Test.thy for
+  examples of this.
+
+This file contains definitions describing how to interpret LEO-II's
+calculus in Isabelle/HOL, as well as more general proof-handling
+functions. The definitions in this file serve to build an intermediate
+proof script which is then evaluated into a tactic -- both these steps
+are independent of LEO-II, and are defined in the TPTP_Reconstruct SML
+module.
+
+CONFIG:
+The following attributes are mainly useful for debugging:
+  tptp_unexceptional_reconstruction |
+  unexceptional_reconstruction      |-- when these are true, a low-level exception
+                                        is allowed to float to the top (instead of
+                                        triggering a higher-level exception, or
+                                        simply indicating that the reconstruction failed).
+  tptp_max_term_size                --- fail of a term exceeds this size. "0" is taken
+                                        to mean infinity.
+  tptp_informative_failure          |
+  informative_failure               |-- produce more output during reconstruction.
+  tptp_trace_reconstruction         |
+
+There are also two attributes, independent of the code here, that
+influence the success of reconstruction: blast_depth_limit and
+unify_search_bound. These are documented in their respective modules,
+but in summary, if unify_search_bound is increased then we can
+handle larger terms (at the cost of performance), since the unification
+engine takes longer to give up the search; blast_depth_limit is
+a limit on proof search performed by Blast. Blast is used for
+the limited proof search that needs to be done to interpret
+instances of LEO-II's inference rules.
+
 TODO:
   use RemoveRedundantQuantifications instead of the ad hoc use of
    remove_redundant_quantification_in_lit and remove_redundant_quantification
@@ -2189,7 +2225,11 @@
   end
 *}
 
+
+section "Importing proofs and reconstructing theorems"
+
 ML {*
+(*Preprocessing carried out on a LEO-II proof.*)
 fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy =
   let
     val ctxt = Proof_Context.init_global thy
@@ -2220,4 +2260,28 @@
   end
 *}
 
+ML {*
+(*Imports and reconstructs a LEO-II proof.*)
+fun reconstruct_leo2 path thy =
+  let
+    val prob_file = Path.base path
+    val dir = Path.dir path
+    val thy' = TPTP_Reconstruct.import_thm true [dir, prob_file] path leo2_on_load thy
+    val ctxt =
+      Context.Theory thy'
+      |> Context.proof_of
+    val prob_name =
+      Path.implode prob_file
+      |> TPTP_Problem_Name.parse_problem_name
+    val theorem =
+      TPTP_Reconstruct.reconstruct ctxt
+       (TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference)
+       prob_name
+  in
+    (*NOTE we could return the theorem value alone, since
+       users could get the thy value from the thm value.*)
+    (thy', theorem)
+  end
+*}
+
 end
\ No newline at end of file
diff -r 928b9f677165 -r 25d7b485df81 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Feb 19 15:57:02 2014 +0000
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Wed Feb 19 15:57:02 2014 +0000
@@ -6,12 +6,30 @@
 NOTE
   - Makes use of the PolyML structure.
   - looks for THF proofs in the path indicated by $THF_PROOFS
+  - these proofs are generated using LEO-II with the following
+    configuration choices: -po 1 -nux -nuc --expand_extuni
+    You can simply filter LEO-II's output using the filter_proof
+    script which is distributed with LEO-II.
 *)
 
 theory TPTP_Proof_Reconstruction_Test
 imports TPTP_Test TPTP_Proof_Reconstruction
 begin
 
+section "Main function"
+text "This function wraps all the reconstruction-related functions. Simply
+ point it at a THF proof produced by LEO-II (using the configuration described
+ above), and it will try to reconstruct it into an Isabelle/HOL theorem.
+ It also returns the theory (into which the axioms and definitions used in the
+ proof have been imported), but note that you can get the theory value from
+ the theorem value."
+
+ML {*
+  reconstruct_leo2 (Path.explode "$THF_PROOFS/NUM667^1.p.out") @{theory}
+*}
+
+section "Prep for testing the component functions"
+
 declare [[
   tptp_trace_reconstruction = false,
   tptp_test_all = false,