src/HOL/TPTP/TPTP_Parser_Example.thy
author sultana
Mon Apr 23 12:23:23 2012 +0100 (2012-04-23)
changeset 47687 bfbd2d0bb348
parent 47558 55b42f9af99d
child 47790 2e1636e45770
permissions -rw-r--r--
moved function for testing problem-name parsing;
list of TPTP test files not immediately evaluated;
     1 (*  Title:      HOL/TPTP/TPTP_Parser_Example.thy
     2     Author:     Nik Sultana, Cambridge University Computer Laboratory
     3 
     4 Example of importing a TPTP problem and trying to prove it in Isabelle/HOL.
     5 *)
     6 
     7 theory TPTP_Parser_Example
     8 imports TPTP_Parser TPTP_Interpret
     9 uses "~~/src/HOL/ex/sledgehammer_tactics.ML"
    10 begin
    11 
    12 import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
    13 
    14 ML {*
    15 val an_fmlas =
    16   TPTP_Interpret.get_manifests @{theory}
    17   |> hd (*FIXME use named lookup*)
    18   |> #2 (*get problem contents*)
    19   |> #3 (*get formulas*)
    20 *}
    21 
    22 (*Display nicely.*)
    23 ML {*
    24 List.app (fn (n, role, fmla, _) =>
    25   Pretty.writeln
    26     (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
    27       TPTP_Syntax.role_to_string role  ^ "): "), Syntax.pretty_term @{context} fmla])
    28   ) (rev an_fmlas)
    29 *}
    30 
    31 ML {*
    32 (*Extract the (name, term) pairs of formulas having roles belonging to a
    33  user-supplied set*)
    34 fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
    35  (string * term) list =
    36    let
    37      fun role_predicate (_, role, _, _) =
    38        fold (fn r1 => fn b => role = r1 orelse b) roles false
    39    in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
    40 *}
    41 
    42 ML {*
    43 (*Use a given tactic on a goal*)
    44 fun prove_conjectures tactic ctxt an_fmlas =
    45   let
    46     val assumptions =
    47       extract_terms
    48        [TPTP_Syntax.Role_Definition (*FIXME include axioms, etc here*)]
    49        an_fmlas
    50       |> map snd
    51     val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
    52     fun driver (n, goal) =
    53       (n, Goal.prove ctxt [] assumptions goal (fn _ => tactic ctxt))
    54   in map driver goals end
    55 
    56 val auto_prove = prove_conjectures auto_tac
    57 val sh_prove = prove_conjectures (fn ctxt =>
    58   Sledgehammer_Tactics.sledgehammer_with_metis_tac ctxt []
    59   (*FIXME use relevance_override*)
    60   {add = [], del = [], only = false} 1)
    61 *}
    62 
    63 ML "auto_prove @{context} an_fmlas"
    64 
    65 sledgehammer_params [provers = z3_tptp leo2, debug]
    66 ML "sh_prove @{context} an_fmlas"
    67 
    68 end