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