10 |
10 |
11 val atps: string Unsynchronized.ref |
11 val atps: string Unsynchronized.ref |
12 val timeout: int Unsynchronized.ref |
12 val timeout: int Unsynchronized.ref |
13 val full_types: bool Unsynchronized.ref |
13 val full_types: bool Unsynchronized.ref |
14 val default_params : theory -> (string * string) list -> params |
14 val default_params : theory -> (string * string) list -> params |
|
15 val setup: theory -> theory |
15 end; |
16 end; |
16 |
17 |
17 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
18 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR = |
18 struct |
19 struct |
19 |
20 |
20 open Sledgehammer_Util |
21 open Sledgehammer_Util |
|
22 open Sledgehammer_Fact_Preprocessor |
21 open ATP_Manager |
23 open ATP_Manager |
22 open ATP_Systems |
24 open ATP_Systems |
23 open Sledgehammer_Fact_Minimizer |
25 open Sledgehammer_Fact_Minimizer |
24 |
26 |
25 structure K = OuterKeyword and P = OuterParse |
27 structure K = OuterKeyword and P = OuterParse |
|
28 |
|
29 (** Proof method used in Isar proofs **) |
|
30 |
|
31 val neg_clausify_setup = |
|
32 Method.setup @{binding neg_clausify} |
|
33 (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac)) |
|
34 "conversion of goal to negated conjecture clauses" |
|
35 |
|
36 val parse_clausify_attribute = |
|
37 Scan.lift OuterParse.nat |
|
38 >> (fn i => Thm.rule_attribute (fn context => fn th => |
|
39 let val thy = Context.theory_of context in |
|
40 Meson.make_meta_clause (nth (cnf_axiom thy th) i) |
|
41 end)) |
|
42 |
|
43 (** Attribute for converting a theorem into clauses **) |
|
44 |
|
45 val clausify_setup = |
|
46 Attrib.setup @{binding clausify} parse_clausify_attribute |
|
47 "conversion of theorem to clauses" |
|
48 |
|
49 (** Sledgehammer commands **) |
26 |
50 |
27 fun add_to_relevance_override ns : relevance_override = |
51 fun add_to_relevance_override ns : relevance_override = |
28 {add = ns, del = [], only = false} |
52 {add = ns, del = [], only = false} |
29 fun del_from_relevance_override ns : relevance_override = |
53 fun del_from_relevance_override ns : relevance_override = |
30 {add = [], del = ns, only = false} |
54 {add = [], del = ns, only = false} |
321 val parse_sledgehammer_params_command = |
345 val parse_sledgehammer_params_command = |
322 parse_params #>> sledgehammer_params_trans |
346 parse_params #>> sledgehammer_params_trans |
323 |
347 |
324 val _ = |
348 val _ = |
325 OuterSyntax.improper_command sledgehammerN |
349 OuterSyntax.improper_command sledgehammerN |
326 "search for first-order proof using automatic theorem provers" K.diag |
350 "search for first-order proof using automatic theorem provers" K.diag |
327 parse_sledgehammer_command |
351 parse_sledgehammer_command |
328 val _ = |
352 val _ = |
329 OuterSyntax.command sledgehammer_paramsN |
353 OuterSyntax.command sledgehammer_paramsN |
330 "set and display the default parameters for Sledgehammer" K.thy_decl |
354 "set and display the default parameters for Sledgehammer" K.thy_decl |
331 parse_sledgehammer_params_command |
355 parse_sledgehammer_params_command |
|
356 |
|
357 val setup = |
|
358 neg_clausify_setup |
|
359 #> clausify_setup |
332 |
360 |
333 end; |
361 end; |