author | blanchet |
Wed, 01 Jun 2011 10:29:43 +0200 | |
changeset 43129 | 4301f1c123d6 |
parent 43128 | a19826080596 |
child 43133 | eb8ec21c9a48 |
permissions | -rw-r--r-- |
39958 | 1 |
(* Title: HOL/Tools/Metis/metis_tactics.ML |
38027 | 2 |
Author: Kong W. Susanto, Cambridge University Computer Laboratory |
3 |
Author: Lawrence C. Paulson, Cambridge University Computer Laboratory |
|
4 |
Author: Jasmin Blanchette, TU Muenchen |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
5 |
Copyright Cambridge University 2007 |
23447 | 6 |
|
29266 | 7 |
HOL setup for the Metis prover. |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
*) |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
|
35826 | 10 |
signature METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
sig |
43102 | 12 |
type type_sys = ATP_Translate.type_sys |
43100 | 13 |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
14 |
val metisN : string |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
15 |
val metisF_N : string |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
16 |
val metisFT_N : string |
43089 | 17 |
val metisX_N : string |
39979
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39978
diff
changeset
|
18 |
val trace : bool Config.T |
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset
|
19 |
val verbose : bool Config.T |
39891
8e12f1956fcd
"meson_new_skolemizer" -> "metis_new_skolemizer" option (since Meson doesn't support the new skolemizer (yet))
blanchet
parents:
39890
diff
changeset
|
20 |
val new_skolemizer : bool Config.T |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
21 |
val metis_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
22 |
val metisF_tac : Proof.context -> thm list -> int -> tactic |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
23 |
val metisFT_tac : Proof.context -> thm list -> int -> tactic |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
24 |
val metisHO_tac : Proof.context -> thm list -> int -> tactic |
43102 | 25 |
val metisX_tac : Proof.context -> type_sys option -> thm list -> int -> tactic |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
26 |
val setup : theory -> theory |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
27 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
28 |
|
35826 | 29 |
structure Metis_Tactics : METIS_TACTICS = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
30 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43050
diff
changeset
|
32 |
open ATP_Translate |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39450
diff
changeset
|
33 |
open Metis_Translate |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
34 |
open Metis_Reconstruct |
35826 | 35 |
|
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
36 |
fun method_binding_for_mode HO = @{binding metis} |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
37 |
| method_binding_for_mode FO = @{binding metisF} |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
38 |
| method_binding_for_mode FT = @{binding metisFT} |
43103 | 39 |
| method_binding_for_mode MX = @{binding metisX} |
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
40 |
|
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
41 |
val metisN = Binding.qualified_name_of (method_binding_for_mode HO) |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
42 |
val metisF_N = Binding.qualified_name_of (method_binding_for_mode FO) |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
43 |
val metisFT_N = Binding.qualified_name_of (method_binding_for_mode FT) |
43103 | 44 |
val metisX_N = Binding.qualified_name_of (method_binding_for_mode MX) |
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
45 |
|
43089 | 46 |
val new_skolemizer = |
47 |
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
48 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
49 |
fun is_false t = t aconv (HOLogic.mk_Trueprop HOLogic.false_const); |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
50 |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
51 |
fun have_common_thm ths1 ths2 = |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
52 |
exists (member Thm.eq_thm ths1) (map Meson.make_meta_clause ths2) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
53 |
|
32956 | 54 |
(*Determining which axiom clauses are actually used*) |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
55 |
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
43128 | 56 |
| used_axioms _ _ = NONE |
24855 | 57 |
|
43129 | 58 |
fun cterm_from_metis ctxt sym_tab tm = |
59 |
let val thy = Proof_Context.theory_of ctxt in |
|
60 |
tm |> hol_term_from_metis MX sym_tab ctxt |
|
61 |
|> Syntax.check_term |
|
62 |
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt) |
|
63 |
|> cterm_of thy |
|
64 |
end |
|
65 |
||
66 |
(* Lightweight predicate type information comes in two flavors, "t = t'" and |
|
67 |
"t => t'", where "t" and "t'" are the same term modulo type tags. |
|
68 |
In Isabelle, type tags are stripped away, so we are left with "t = t" or |
|
69 |
"t => t". *) |
|
70 |
fun lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth = |
|
71 |
(case Metis_LiteralSet.toList (Metis_Thm.clause mth) of |
|
72 |
[(true, (_, [_, tm]))] => |
|
73 |
tm |> cterm_from_metis ctxt sym_tab |> Thm.reflexive |
|
74 |
RS @{thm meta_eq_to_obj_eq} |
|
75 |
| [_, (_, tm)] => |
|
76 |
tm |> Metis_Term.Fn |> cterm_from_metis ctxt sym_tab |> Thm.assume |
|
77 |
| _ => raise Fail "unexpected tags sym clause") |
|
78 |
|> Meson.make_meta_clause |
|
79 |
||
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
80 |
val clause_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
81 |
{ordering = Metis_KnuthBendixOrder.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
82 |
orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
83 |
orderTerms = true} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
84 |
val active_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
85 |
{clause = clause_params, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
86 |
prefactor = #prefactor Metis_Active.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
87 |
postfactor = #postfactor Metis_Active.default} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
88 |
val waiting_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
89 |
{symbolsWeight = 1.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
90 |
variablesWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
91 |
literalsWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
92 |
models = []} |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
93 |
val resolution_params = {active = active_params, waiting = waiting_params} |
37573 | 94 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
95 |
(* Main function to start Metis proof and reconstruction *) |
43100 | 96 |
fun FOL_SOLVE type_sys (mode :: fallback_modes) ctxt cls ths0 = |
42361 | 97 |
let val thy = Proof_Context.theory_of ctxt |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset
|
98 |
val new_skolemizer = |
39950 | 99 |
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) |
35826 | 100 |
val th_cls_pairs = |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
101 |
map2 (fn j => fn th => |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
102 |
(Thm.get_name_hint th, |
39901
75d792edf634
make "cnf_axiom" work (after a fashion) in the absence of the axiom of choice
blanchet
parents:
39899
diff
changeset
|
103 |
Meson_Clausify.cnf_axiom ctxt new_skolemizer j th)) |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
104 |
(0 upto length ths0 - 1) ths0 |
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
105 |
val ths = maps (snd o snd) th_cls_pairs |
39938
0a2091f86eb4
fixed two bugs in new skolemizer: instantiations now take types into consideration, and rotate_tac is given the proper offset
blanchet
parents:
39937
diff
changeset
|
106 |
val dischargers = map (fst o snd) th_cls_pairs |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
107 |
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
108 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
109 |
val _ = trace_msg ctxt (fn () => "THEOREM CLAUSES") |
43092
93ec303e1917
more work on new metis that exploits the powerful new type encodings
blanchet
parents:
43091
diff
changeset
|
110 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) ths |
43094 | 111 |
val (mode, sym_tab, {axioms, old_skolems, ...}) = |
43100 | 112 |
prepare_metis_problem ctxt mode type_sys cls ths |
43129 | 113 |
val axioms = |
114 |
axioms |> map |
|
115 |
(fn (mth, SOME th) => (mth, th) |
|
116 |
| (mth, NONE) => |
|
117 |
(mth, lightweight_tags_sym_theorem_from_metis ctxt sym_tab mth)) |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
118 |
val _ = trace_msg ctxt (fn () => "CLAUSES GIVEN TO METIS") |
32956 | 119 |
val thms = map #1 axioms |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
120 |
val _ = app (fn th => trace_msg ctxt (fn () => Metis_Thm.toString th)) thms |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
121 |
val _ = trace_msg ctxt (fn () => "mode = " ^ string_of_mode mode) |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
122 |
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
32956 | 123 |
in |
33317 | 124 |
case filter (is_false o prop_of) cls of |
32956 | 125 |
false_th::_ => [false_th RS @{thm FalseE}] |
126 |
| [] => |
|
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
127 |
case Metis_Resolution.new resolution_params {axioms = thms, conjecture = []} |
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
128 |
|> Metis_Resolution.loop of |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
129 |
Metis_Resolution.Contradiction mth => |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
130 |
let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
131 |
Metis_Thm.toString mth) |
32956 | 132 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
133 |
(*add constraints arising from converting goal to clause form*) |
|
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
134 |
val proof = Metis_Proof.proof mth |
43094 | 135 |
val result = |
136 |
fold (replay_one_inference ctxt' mode old_skolems sym_tab) |
|
137 |
proof axioms |
|
32956 | 138 |
and used = map_filter (used_axioms axioms) proof |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
139 |
val _ = trace_msg ctxt (fn () => "METIS COMPLETED...clauses actually used:") |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
140 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
141 |
val unused = th_cls_pairs |> map_filter (fn (name, (_, cls)) => |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
142 |
if have_common_thm used cls then NONE else SOME name) |
32956 | 143 |
in |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
144 |
if not (null cls) andalso not (have_common_thm used cls) then |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
145 |
verbose_warning ctxt "The assumptions are inconsistent" |
36383 | 146 |
else |
147 |
(); |
|
148 |
if not (null unused) then |
|
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
149 |
verbose_warning ctxt ("Unused theorems: " ^ commas_quote unused) |
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
150 |
else |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
151 |
(); |
32956 | 152 |
case result of |
153 |
(_,ith)::_ => |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
154 |
(trace_msg ctxt (fn () => "Success: " ^ Display.string_of_thm ctxt ith); |
39887
74939e2afb95
second step in introducing the new Skolemizer -- notably, added procedure for discharging Skolem assumptions
blanchet
parents:
39886
diff
changeset
|
155 |
[discharge_skolem_premises ctxt dischargers ith]) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
156 |
| _ => (trace_msg ctxt (fn () => "Metis: No result"); []) |
32956 | 157 |
end |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
158 |
| Metis_Resolution.Satisfiable _ => |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
159 |
(trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
160 |
if null fallback_modes then |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
161 |
() |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
162 |
else |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
163 |
raise METIS ("FOL_SOLVE", |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
164 |
"No first-order proof with the lemmas supplied"); |
38097
5e4ad2df09f3
revert exception throwing in FOL_SOLVE, since they're not caught anyway
blanchet
parents:
38028
diff
changeset
|
165 |
[]) |
42733
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset
|
166 |
end |
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset
|
167 |
handle METIS (loc, msg) => |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
168 |
case fallback_modes of |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
169 |
[] => error ("Failed to replay Metis proof in Isabelle." ^ |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
170 |
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
171 |
else "")) |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
172 |
| mode :: _ => |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
173 |
(verbose_warning ctxt |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
174 |
("Falling back on " ^ |
43050
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
175 |
quote (Binding.qualified_name_of |
59284a13abc4
support "metis" and "metisFT" as provers in the architecture, so they can be used for minimizing
blanchet
parents:
43034
diff
changeset
|
176 |
(method_binding_for_mode mode)) ^ "..."); |
43100 | 177 |
FOL_SOLVE type_sys fallback_modes ctxt cls ths0) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
178 |
|
42847 | 179 |
val neg_clausify = |
38028 | 180 |
single |
181 |
#> Meson.make_clauses_unsorted |
|
39890 | 182 |
#> map Meson_Clausify.introduce_combinators_in_theorem |
38028 | 183 |
#> Meson.finish_cnf |
184 |
||
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
185 |
fun preskolem_tac ctxt st0 = |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
186 |
(if exists (Meson.has_too_many_clauses ctxt) |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
187 |
(Logic.prems_of_goal (prop_of st0) 1) then |
42336
d63d43e85879
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents:
40665
diff
changeset
|
188 |
Simplifier.full_simp_tac (Meson_Clausify.ss_only @{thms not_all not_ex}) 1 |
d63d43e85879
improve definitional CNF on goal by moving "not" past the quantifiers
blanchet
parents:
40665
diff
changeset
|
189 |
THEN cnf.cnfx_rewrite_tac ctxt 1 |
39269
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
190 |
else |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
191 |
all_tac) st0 |
c2795d8a2461
use definitional CNF for the goal if at least one of the premisses would lead to too many clauses in Meson
blanchet
parents:
39267
diff
changeset
|
192 |
|
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
193 |
val type_has_top_sort = |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
194 |
exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false) |
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
195 |
|
43100 | 196 |
fun generic_metis_tac modes type_sys ctxt ths i st0 = |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
197 |
let |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
198 |
val _ = trace_msg ctxt (fn () => |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
199 |
"Metis called with theorems " ^ |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
200 |
cat_lines (map (Display.string_of_thm ctxt) ths)) |
43100 | 201 |
fun tac clause = resolve_tac (FOL_SOLVE type_sys modes ctxt clause ths) 1 |
32956 | 202 |
in |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset
|
203 |
if exists_type type_has_top_sort (prop_of st0) then |
42650
552eae49f97d
reintroduce this idea of running "metisFT" after a failed "metis" -- I took it out in e85ce10cef1a because I couldn't think of a reasonable use case, but now that ATPs use sound encodings and include dangerous facts (e.g. True_or_False) it makes more sense than ever to run "metisFT" after "metis"
blanchet
parents:
42616
diff
changeset
|
204 |
(verbose_warning ctxt "Proof state contains the universal sort {}"; |
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset
|
205 |
Seq.empty) |
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset
|
206 |
else |
43100 | 207 |
Meson.MESON (preskolem_tac ctxt) (maps neg_clausify) tac ctxt i st0 |
32956 | 208 |
end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
209 |
|
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
210 |
val metis_modes = [HO, FT] |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
211 |
val metisF_modes = [FO, FT] |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
212 |
val metisFT_modes = [FT] |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
213 |
val metisHO_modes = [HO] |
43103 | 214 |
val metisX_modes = [MX] |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
215 |
|
43100 | 216 |
val metis_tac = generic_metis_tac metis_modes NONE |
217 |
val metisF_tac = generic_metis_tac metisF_modes NONE |
|
218 |
val metisFT_tac = generic_metis_tac metisFT_modes NONE |
|
219 |
val metisHO_tac = generic_metis_tac metisHO_modes NONE |
|
220 |
fun metisX_tac ctxt type_sys = generic_metis_tac metisX_modes type_sys ctxt |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
221 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
222 |
(* Whenever "X" has schematic type variables, we treat "using X by metis" as |
43100 | 223 |
"by (metis X)" to prevent "Subgoal.FOCUS" from freezing the type variables. |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
224 |
We don't do it for nonschematic facts "X" because this breaks a few proofs |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
225 |
(in the rare and subtle case where a proof relied on extensionality not being |
38994 | 226 |
applied) and brings few benefits. *) |
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
227 |
val has_tvar = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
228 |
exists_type (exists_subtype (fn TVar _ => true | _ => false)) o prop_of |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
229 |
|
43100 | 230 |
fun method modes (type_sys, ths) ctxt facts = |
231 |
let |
|
232 |
val (schem_facts, nonschem_facts) = List.partition has_tvar facts |
|
233 |
val type_sys = type_sys |> Option.map type_sys_from_string |
|
234 |
in |
|
43099 | 235 |
HEADGOAL (Method.insert_tac nonschem_facts THEN' |
43100 | 236 |
CHANGED_PROP |
237 |
o generic_metis_tac modes type_sys ctxt (schem_facts @ ths)) |
|
43099 | 238 |
end |
43100 | 239 |
|
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
240 |
fun setup_method (modes as mode :: _) = |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
241 |
Method.setup (method_binding_for_mode mode) |
43103 | 242 |
((if mode = MX then |
43100 | 243 |
Scan.lift (Scan.option (Args.parens Parse.short_ident)) |
244 |
else |
|
245 |
Scan.succeed NONE) |
|
246 |
-- Attrib.thms >> (METHOD oo method modes)) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
247 |
|
32956 | 248 |
val setup = |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
249 |
[(metis_modes, "Metis for FOL and HOL problems"), |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
250 |
(metisF_modes, "Metis for FOL problems"), |
43089 | 251 |
(metisFT_modes, "Metis for FOL/HOL problems with fully-typed translation"), |
252 |
(metisX_modes, "Metis for FOL and HOL problems (experimental)")] |
|
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
253 |
|> fold (uncurry setup_method) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
254 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
255 |
end; |