src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 55597 25d7b485df81
parent 55596 928b9f677165
child 56220 4c43a2881b25
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Feb 19 15:57:02 2014 +0000
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Feb 19 15:57:02 2014 +0000
     1.3 @@ -3,6 +3,42 @@
     1.4  
     1.5  Proof reconstruction for Leo-II.
     1.6  
     1.7 +USAGE:
     1.8 +* Simple call the "reconstruct_leo2" function.
     1.9 +* For more advanced use, you could use the component functions used in
    1.10 +  "reconstruct_leo2" -- see TPTP_Proof_Reconstruction_Test.thy for
    1.11 +  examples of this.
    1.12 +
    1.13 +This file contains definitions describing how to interpret LEO-II's
    1.14 +calculus in Isabelle/HOL, as well as more general proof-handling
    1.15 +functions. The definitions in this file serve to build an intermediate
    1.16 +proof script which is then evaluated into a tactic -- both these steps
    1.17 +are independent of LEO-II, and are defined in the TPTP_Reconstruct SML
    1.18 +module.
    1.19 +
    1.20 +CONFIG:
    1.21 +The following attributes are mainly useful for debugging:
    1.22 +  tptp_unexceptional_reconstruction |
    1.23 +  unexceptional_reconstruction      |-- when these are true, a low-level exception
    1.24 +                                        is allowed to float to the top (instead of
    1.25 +                                        triggering a higher-level exception, or
    1.26 +                                        simply indicating that the reconstruction failed).
    1.27 +  tptp_max_term_size                --- fail of a term exceeds this size. "0" is taken
    1.28 +                                        to mean infinity.
    1.29 +  tptp_informative_failure          |
    1.30 +  informative_failure               |-- produce more output during reconstruction.
    1.31 +  tptp_trace_reconstruction         |
    1.32 +
    1.33 +There are also two attributes, independent of the code here, that
    1.34 +influence the success of reconstruction: blast_depth_limit and
    1.35 +unify_search_bound. These are documented in their respective modules,
    1.36 +but in summary, if unify_search_bound is increased then we can
    1.37 +handle larger terms (at the cost of performance), since the unification
    1.38 +engine takes longer to give up the search; blast_depth_limit is
    1.39 +a limit on proof search performed by Blast. Blast is used for
    1.40 +the limited proof search that needs to be done to interpret
    1.41 +instances of LEO-II's inference rules.
    1.42 +
    1.43  TODO:
    1.44    use RemoveRedundantQuantifications instead of the ad hoc use of
    1.45     remove_redundant_quantification_in_lit and remove_redundant_quantification
    1.46 @@ -2189,7 +2225,11 @@
    1.47    end
    1.48  *}
    1.49  
    1.50 +
    1.51 +section "Importing proofs and reconstructing theorems"
    1.52 +
    1.53  ML {*
    1.54 +(*Preprocessing carried out on a LEO-II proof.*)
    1.55  fun leo2_on_load (pannot : TPTP_Reconstruct.proof_annotation) thy =
    1.56    let
    1.57      val ctxt = Proof_Context.init_global thy
    1.58 @@ -2220,4 +2260,28 @@
    1.59    end
    1.60  *}
    1.61  
    1.62 +ML {*
    1.63 +(*Imports and reconstructs a LEO-II proof.*)
    1.64 +fun reconstruct_leo2 path thy =
    1.65 +  let
    1.66 +    val prob_file = Path.base path
    1.67 +    val dir = Path.dir path
    1.68 +    val thy' = TPTP_Reconstruct.import_thm true [dir, prob_file] path leo2_on_load thy
    1.69 +    val ctxt =
    1.70 +      Context.Theory thy'
    1.71 +      |> Context.proof_of
    1.72 +    val prob_name =
    1.73 +      Path.implode prob_file
    1.74 +      |> TPTP_Problem_Name.parse_problem_name
    1.75 +    val theorem =
    1.76 +      TPTP_Reconstruct.reconstruct ctxt
    1.77 +       (TPTP_Reconstruct.naive_reconstruct_tac ctxt interpret_leo2_inference)
    1.78 +       prob_name
    1.79 +  in
    1.80 +    (*NOTE we could return the theorem value alone, since
    1.81 +       users could get the thy value from the thm value.*)
    1.82 +    (thy', theorem)
    1.83 +  end
    1.84 +*}
    1.85 +
    1.86  end
    1.87 \ No newline at end of file