src/HOL/TPTP/TPTP_Parser_Example.thy
 author paulson 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
```