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
sultana@47366
     1
(*  Title:      HOL/TPTP/TPTP_Parser_Example.thy
sultana@47366
     2
    Author:     Nik Sultana, Cambridge University Computer Laboratory
sultana@47366
     3
sultana@47366
     4
Example of importing a TPTP problem and trying to prove it in Isabelle/HOL.
sultana@47366
     5
*)
sultana@47366
     6
sultana@47366
     7
theory TPTP_Parser_Example
sultana@47518
     8
imports TPTP_Parser TPTP_Interpret
sultana@47366
     9
begin
sultana@47366
    10
wenzelm@48891
    11
ML_file "sledgehammer_tactics.ML"
wenzelm@48891
    12
sultana@53393
    13
import_tptp "$TPTP/Problems/LCL/LCL414+1.p"
sultana@47366
    14
wenzelm@63167
    15
ML \<open>
sultana@47366
    16
val an_fmlas =
sultana@47366
    17
  TPTP_Interpret.get_manifests @{theory}
sultana@47366
    18
  |> hd (*FIXME use named lookup*)
sultana@47366
    19
  |> #2 (*get problem contents*)
sultana@47366
    20
  |> #3 (*get formulas*)
wenzelm@63167
    21
\<close>
sultana@47366
    22
sultana@47366
    23
(*Display nicely.*)
wenzelm@63167
    24
ML \<open>
sultana@47548
    25
List.app (fn (n, role, fmla, _) =>
sultana@47366
    26
  Pretty.writeln
sultana@47366
    27
    (Pretty.block [Pretty.str ("\"" ^ n ^ "\"" ^ "(" ^
sultana@47366
    28
      TPTP_Syntax.role_to_string role  ^ "): "), Syntax.pretty_term @{context} fmla])
sultana@47366
    29
  ) (rev an_fmlas)
wenzelm@63167
    30
\<close>
sultana@47366
    31
wenzelm@63167
    32
ML \<open>
sultana@47366
    33
(*Extract the (name, term) pairs of formulas having roles belonging to a
sultana@47366
    34
 user-supplied set*)
sultana@47366
    35
fun extract_terms roles : TPTP_Interpret.tptp_formula_meaning list ->
sultana@47366
    36
 (string * term) list =
sultana@47366
    37
   let
sultana@47548
    38
     fun role_predicate (_, role, _, _) =
sultana@47366
    39
       fold (fn r1 => fn b => role = r1 orelse b) roles false
sultana@47548
    40
   in filter role_predicate #> map (fn (n, _, t, _) => (n, t)) end
wenzelm@63167
    41
\<close>
sultana@47366
    42
wenzelm@63167
    43
ML \<open>
sultana@47366
    44
(*Use a given tactic on a goal*)
sultana@47366
    45
fun prove_conjectures tactic ctxt an_fmlas =
sultana@47366
    46
  let
sultana@47366
    47
    val assumptions =
sultana@47366
    48
      extract_terms
sultana@53393
    49
       [TPTP_Syntax.Role_Definition, TPTP_Syntax.Role_Axiom]
sultana@47366
    50
       an_fmlas
sultana@47366
    51
      |> map snd
sultana@47366
    52
    val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
sultana@47366
    53
    fun driver (n, goal) =
sultana@47366
    54
      (n, Goal.prove ctxt [] assumptions goal (fn _ => tactic ctxt))
sultana@47366
    55
  in map driver goals end
sultana@47366
    56
sultana@47366
    57
val auto_prove = prove_conjectures auto_tac
sultana@47366
    58
val sh_prove = prove_conjectures (fn ctxt =>
sultana@47366
    59
  Sledgehammer_Tactics.sledgehammer_with_metis_tac ctxt []
sultana@47366
    60
  (*FIXME use relevance_override*)
sultana@47366
    61
  {add = [], del = [], only = false} 1)
wenzelm@63167
    62
\<close>
sultana@47366
    63
wenzelm@63167
    64
ML \<open>
sultana@53393
    65
@{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
wenzelm@63167
    66
\<close>
sultana@47366
    67
boehmes@55049
    68
sledgehammer_params [provers = z3, debug]
wenzelm@63167
    69
ML \<open>
sultana@53393
    70
@{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
wenzelm@63167
    71
\<close>
sultana@47366
    72
boehmes@55049
    73
end