src/HOL/TPTP/TPTP_Parser_Example.thy
author paulson <lp15@cam.ac.uk>
Tue Apr 25 16:39:54 2017 +0100 (2017-04-25)
changeset 65578 e4997c181cce
parent 63167 0909deb8059b
permissions -rw-r--r--
New material from PNT proof, as well as more default [simp] declarations. Also removed duplicate theorems about geometric series
     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 begin
    10 
    11 ML_file "sledgehammer_tactics.ML"
    12 
    13 import_tptp "$TPTP/Problems/LCL/LCL414+1.p"
    14 
    15 ML \<open>
    16 val an_fmlas =
    17   TPTP_Interpret.get_manifests @{theory}
    18   |> hd (*FIXME use named lookup*)
    19   |> #2 (*get problem contents*)
    20   |> #3 (*get formulas*)
    21 \<close>
    22 
    23 (*Display nicely.*)
    24 ML \<open>
    25 List.app (fn (n, role, fmla, _) =>
    26   Pretty.writeln
    27     (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
    28       TPTP_Syntax.role_to_string role  ^ "): "), Syntax.pretty_term @{context} fmla])
    29   ) (rev an_fmlas)
    30 \<close>
    31 
    32 ML \<open>
    33 (*Extract the (name, term) pairs of formulas having roles belonging to a
    34  user-supplied set*)
    35 fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
    36  (string * term) list =
    37    let
    38      fun role_predicate (_, role, _, _) =
    39        fold (fn r1 => fn b => role = r1 orelse b) roles false
    40    in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
    41 \<close>
    42 
    43 ML \<open>
    44 (*Use a given tactic on a goal*)
    45 fun prove_conjectures tactic ctxt an_fmlas =
    46   let
    47     val assumptions =
    48       extract_terms
    49        [TPTP_Syntax.Role_Definition, TPTP_Syntax.Role_Axiom]
    50        an_fmlas
    51       |> map snd
    52     val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
    53     fun driver (n, goal) =
    54       (n, Goal.prove ctxt [] assumptions goal (fn _ => tactic ctxt))
    55   in map driver goals end
    56 
    57 val auto_prove = prove_conjectures auto_tac
    58 val sh_prove = prove_conjectures (fn ctxt =>
    59   Sledgehammer_Tactics.sledgehammer_with_metis_tac ctxt []
    60   (*FIXME use relevance_override*)
    61   {add = [], del = [], only = false} 1)
    62 \<close>
    63 
    64 ML \<open>
    65 @{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
    66 \<close>
    67 
    68 sledgehammer_params [provers = z3, debug]
    69 ML \<open>
    70 @{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
    71 \<close>
    72 
    73 end