author | blanchet |
Fri, 18 Nov 2011 11:47:12 +0100 | |
changeset 45567 | 8e3891309a8e |
parent 45559 | 22d6fb988306 |
child 45568 | 211a6e6cbc04 |
permissions | -rw-r--r-- |
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset
|
1 |
(* Title: HOL/Tools/Metis/metis_tactic.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 |
|
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset
|
10 |
signature METIS_TACTIC = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
sig |
39979
b13515940b53
added "trace_meson" configuration option, replacing old-fashioned reference
blanchet
parents:
39978
diff
changeset
|
12 |
val trace : bool Config.T |
40665
1a65f0c74827
added "verbose" option to Metis to shut up its warnings if necessary
blanchet
parents:
40262
diff
changeset
|
13 |
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
|
14 |
val new_skolemizer : bool Config.T |
44934 | 15 |
val type_has_top_sort : typ -> bool |
45514 | 16 |
val metis_tac : |
17 |
string list -> string -> Proof.context -> thm list -> int -> tactic |
|
45521 | 18 |
val metis_lam_transs : string list |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
19 |
val parse_metis_options : (string list option * string option) parser |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
20 |
val setup : theory -> theory |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
end |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
|
44651
5d6a11e166cf
renamed "Metis_Tactics" to "Metis_Tactic", now that there is only one Metis tactic ("metisFT" is legacy)
blanchet
parents:
44634
diff
changeset
|
23 |
structure Metis_Tactic : METIS_TACTIC = |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
24 |
struct |
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
25 |
|
43085
0a2f5b86bdd7
first step in sharing more code between ATP and Metis translation
blanchet
parents:
43050
diff
changeset
|
26 |
open ATP_Translate |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
27 |
open ATP_Reconstruct |
39494
bf7dd4902321
rename "Metis_Clauses" to "Metis_Translate" for consistency with "Sledgehammer_Translate"
blanchet
parents:
39450
diff
changeset
|
28 |
open Metis_Translate |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
29 |
open Metis_Reconstruct |
35826 | 30 |
|
43089 | 31 |
val new_skolemizer = |
32 |
Attrib.setup_config_bool @{binding metis_new_skolemizer} (K false) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
33 |
|
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
34 |
(* Designed to work also with monomorphic instances of polymorphic theorems. *) |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
35 |
fun have_common_thm ths1 ths2 = |
43301
8d7fc4a5b502
removed needless function that duplicated standard functionality, with a little unnecessary twist
blanchet
parents:
43299
diff
changeset
|
36 |
exists (member (Term.aconv_untyped o pairself prop_of) ths1) |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
37 |
(map Meson.make_meta_clause ths2) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
38 |
|
32956 | 39 |
(*Determining which axiom clauses are actually used*) |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
40 |
fun used_axioms axioms (th, Metis_Proof.Axiom _) = SOME (lookth axioms th) |
43128 | 41 |
| used_axioms _ _ = NONE |
24855 | 42 |
|
43129 | 43 |
(* Lightweight predicate type information comes in two flavors, "t = t'" and |
44 |
"t => t'", where "t" and "t'" are the same term modulo type tags. |
|
45 |
In Isabelle, type tags are stripped away, so we are left with "t = t" or |
|
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
46 |
"t => t". Type tag idempotence is also handled this way. *) |
45508 | 47 |
fun reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth = |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
48 |
let val thy = Proof_Context.theory_of ctxt in |
45508 | 49 |
case hol_clause_from_metis ctxt type_enc sym_tab concealed mth of |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
50 |
Const (@{const_name HOL.eq}, _) $ _ $ t => |
44408
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
51 |
let |
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
52 |
val ct = cterm_of thy t |
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
53 |
val cT = ctyp_of_term ct |
30ea62ab4f16
made reconstruction of type tag equalities "\?x = \?x" reliable
blanchet
parents:
44402
diff
changeset
|
54 |
in refl |> Drule.instantiate' [SOME cT] [SOME ct] end |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
55 |
| Const (@{const_name disj}, _) $ t1 $ t2 => |
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
56 |
(if can HOLogic.dest_not t1 then t2 else t1) |
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
57 |
|> HOLogic.mk_Trueprop |> cterm_of thy |> Thm.trivial |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
58 |
| _ => raise Fail "expected reflexive or trivial clause" |
43136
cf5cda219058
handle lightweight tags sym theorems gracefully in the presence of TVars with interesting type classes
blanchet
parents:
43135
diff
changeset
|
59 |
end |
43129 | 60 |
|> Meson.make_meta_clause |
61 |
||
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
62 |
fun lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth = |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
63 |
let |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
64 |
val thy = Proof_Context.theory_of ctxt |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
65 |
val tac = rewrite_goals_tac @{thms lambda_def_raw} THEN rtac refl 1 |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
66 |
val t = hol_clause_from_metis ctxt type_enc sym_tab concealed mth |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
67 |
val ct = cterm_of thy (HOLogic.mk_Trueprop t) |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
68 |
in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
69 |
|
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
70 |
fun introduce_lambda_wrappers_in_theorem ctxt th = |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
71 |
if Meson_Clausify.is_quasi_lambda_free (prop_of th) then |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
72 |
th |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
73 |
else |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
74 |
let |
45558
0939c38b1fc9
eta-contract to avoid needless "lambda" wrappers
blanchet
parents:
45521
diff
changeset
|
75 |
val th = th |> Drule.eta_contraction_rule |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
76 |
fun conv wrap ctxt ct = |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
77 |
if Meson_Clausify.is_quasi_lambda_free (term_of ct) then |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
78 |
Thm.reflexive ct |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
79 |
else case term_of ct of |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
80 |
Abs _ => |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
81 |
Conv.abs_conv (conv false o snd) ctxt ct |
45567
8e3891309a8e
avoid that var names get changed by resolution in Metis lambda-lifting
blanchet
parents:
45559
diff
changeset
|
82 |
|> wrap |
8e3891309a8e
avoid that var names get changed by resolution in Metis lambda-lifting
blanchet
parents:
45559
diff
changeset
|
83 |
? (fn th => Meson.first_order_resolve th @{thm Metis.eq_lambdaI}) |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
84 |
| _ => Conv.comb_conv (conv true ctxt) ct |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
85 |
val eqth = conv true ctxt (cprop_of th) |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
86 |
in Thm.equal_elim eqth th end |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
87 |
|
44588 | 88 |
val clause_params = |
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
89 |
{ordering = Metis_KnuthBendixOrder.default, |
44492
a330c0608da8
avoid using ":" for anything but systematic type tag annotations, because Hurd's Metis gives it that special semantics
blanchet
parents:
44411
diff
changeset
|
90 |
orderLiterals = Metis_Clause.UnsignedLiteralOrder, |
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
91 |
orderTerms = true} |
44588 | 92 |
val active_params = |
93 |
{clause = clause_params, |
|
39450
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
94 |
prefactor = #prefactor Metis_Active.default, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
95 |
postfactor = #postfactor Metis_Active.default} |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
96 |
val waiting_params = |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
97 |
{symbolsWeight = 1.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
98 |
variablesWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
99 |
literalsWeight = 0.0, |
7e9879fbb7c5
supply the Metis parameter defaults as argument, instead of patching the Metis sources;
blanchet
parents:
39419
diff
changeset
|
100 |
models = []} |
44588 | 101 |
val resolution_params = {active = active_params, waiting = waiting_params} |
37573 | 102 |
|
37516
c81c86bfc18a
have "metis" method and "metis_tac" fall back on "metisFT" upon failure, following a suggestion by Larry
blanchet
parents:
37509
diff
changeset
|
103 |
(* Main function to start Metis proof and reconstruction *) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
104 |
fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 = |
42361 | 105 |
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
|
106 |
val new_skolemizer = |
39950 | 107 |
Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy) |
35826 | 108 |
val th_cls_pairs = |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
109 |
map2 (fn j => fn th => |
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
110 |
(Thm.get_name_hint th, |
45508 | 111 |
Meson_Clausify.cnf_axiom ctxt new_skolemizer |
45514 | 112 |
(lam_trans = combinatorsN) j th)) |
39894
35ae5cf8c96a
encode number of skolem assumptions in them, for more efficient retrieval later
blanchet
parents:
39892
diff
changeset
|
113 |
(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
|
114 |
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
|
115 |
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
|
116 |
val _ = trace_msg ctxt (fn () => "FOL_SOLVE: CONJECTURE CLAUSES") |
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
117 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) cls |
44411
e3629929b171
change Metis's default settings if type information axioms are generated
blanchet
parents:
44408
diff
changeset
|
118 |
val _ = trace_msg ctxt (fn () => "type_enc = " ^ type_enc) |
44634
2ac4ff398bc3
make "sound" sound and "unsound" more sound, based on evaluation
blanchet
parents:
44588
diff
changeset
|
119 |
val type_enc = type_enc_from_string Sound type_enc |
45559 | 120 |
val (sym_tab, axioms0, concealed) = |
45514 | 121 |
prepare_metis_problem ctxt type_enc lam_trans cls ths |
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
122 |
fun get_isa_thm mth Isa_Reflexive_or_Trivial = |
45508 | 123 |
reflexive_or_trivial_from_metis ctxt type_enc sym_tab concealed mth |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
124 |
| get_isa_thm mth Isa_Lambda_Lifted = |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
125 |
lambda_lifted_from_metis ctxt type_enc sym_tab concealed mth |
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
126 |
| get_isa_thm _ (Isa_Raw ith) = |
45514 | 127 |
ith |> lam_trans = lam_liftingN |
45511
9b0f8ca4388e
continued implementation of lambda-lifting in Metis
blanchet
parents:
45508
diff
changeset
|
128 |
? introduce_lambda_wrappers_in_theorem ctxt |
45559 | 129 |
val axioms = axioms0 |> map (fn (mth, ith) => (mth, get_isa_thm mth ith)) |
130 |
val _ = trace_msg ctxt (fn () => "ISABELLE CLAUSES") |
|
131 |
val _ = app (fn (_, ith) => trace_msg ctxt (fn () => Display.string_of_thm ctxt ith)) axioms |
|
132 |
val _ = trace_msg ctxt (fn () => "METIS CLAUSES") |
|
133 |
val _ = app (fn (mth, _) => trace_msg ctxt (fn () => Metis_Thm.toString mth)) axioms |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
134 |
val _ = trace_msg ctxt (fn () => "START METIS PROVE PROCESS") |
32956 | 135 |
in |
43159
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
136 |
case filter (fn t => prop_of t aconv @{prop False}) cls of |
29b55f292e0b
added support for helpers in new Metis, so far only for polymorphic type encodings
blanchet
parents:
43136
diff
changeset
|
137 |
false_th :: _ => [false_th RS @{thm FalseE}] |
32956 | 138 |
| [] => |
44588 | 139 |
case Metis_Resolution.new resolution_params |
45559 | 140 |
{axioms = axioms |> map fst, conjecture = []} |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
141 |
|> Metis_Resolution.loop of |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
142 |
Metis_Resolution.Contradiction mth => |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
143 |
let val _ = trace_msg ctxt (fn () => "METIS RECONSTRUCTION START: " ^ |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
144 |
Metis_Thm.toString mth) |
32956 | 145 |
val ctxt' = fold Variable.declare_constraints (map prop_of cls) ctxt |
146 |
(*add constraints arising from converting goal to clause form*) |
|
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
147 |
val proof = Metis_Proof.proof mth |
43094 | 148 |
val result = |
43212 | 149 |
axioms |
45508 | 150 |
|> fold (replay_one_inference ctxt' type_enc concealed sym_tab) proof |
45559 | 151 |
val used = |
152 |
proof |> map_filter (used_axioms axioms0) |
|
153 |
|> map_filter (fn Isa_Raw ith => SOME ith | _ => NONE) |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
154 |
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
|
155 |
val _ = app (fn th => trace_msg ctxt (fn () => Display.string_of_thm ctxt th)) used |
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
156 |
val names = th_cls_pairs |> map fst |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
157 |
val used_names = |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
158 |
th_cls_pairs |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
159 |
|> map_filter (fn (name, (_, cls)) => |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
160 |
if have_common_thm used cls then SOME name |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
161 |
else NONE) |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
162 |
val unused_names = names |> subtract (op =) used_names |
32956 | 163 |
in |
39497
fa16349939b7
complete refactoring of Metis along the lines of Sledgehammer
blanchet
parents:
39494
diff
changeset
|
164 |
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
|
165 |
verbose_warning ctxt "The assumptions are inconsistent" |
36383 | 166 |
else |
167 |
(); |
|
43134
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
168 |
if not (null unused_names) then |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
169 |
"Unused theorems: " ^ commas_quote unused_names |
0c82e00ba63e
make sure no warnings are given for polymorphic facts where we use a monomorphic instance
blanchet
parents:
43133
diff
changeset
|
170 |
|> verbose_warning ctxt |
36230
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
171 |
else |
43d10a494c91
added warning about inconsistent context to Metis;
blanchet
parents:
36170
diff
changeset
|
172 |
(); |
32956 | 173 |
case result of |
174 |
(_,ith)::_ => |
|
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
175 |
(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
|
176 |
[discharge_skolem_premises ctxt dischargers ith]) |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
177 |
| _ => (trace_msg ctxt (fn () => "Metis: No result"); []) |
32956 | 178 |
end |
39419
c9accfd621a5
"Metis." -> "Metis_" to reflect change in "metis.ML"
blanchet
parents:
39376
diff
changeset
|
179 |
| Metis_Resolution.Satisfiable _ => |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
180 |
(trace_msg ctxt (fn () => "Metis: No first-order proof with the lemmas supplied"); |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
181 |
if null fallback_type_encs then |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
182 |
() |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
183 |
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
|
184 |
raise METIS ("FOL_SOLVE", |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
185 |
"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
|
186 |
[]) |
42733
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset
|
187 |
end |
01ef1c3d9cfd
more robust exception handling in Metis (also works if there are several subgoals)
blanchet
parents:
42650
diff
changeset
|
188 |
handle METIS (loc, msg) => |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
189 |
case fallback_type_encs of |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
190 |
[] => error ("Failed to replay Metis proof in Isabelle." ^ |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
191 |
(if Config.get ctxt verbose then "\n" ^ loc ^ ": " ^ msg |
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
192 |
else "")) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
193 |
| first_fallback :: _ => |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
194 |
(verbose_warning ctxt |
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
195 |
("Falling back on " ^ |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
196 |
quote (metis_call first_fallback lam_trans) ^ "..."); |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
197 |
FOL_SOLVE fallback_type_encs lam_trans ctxt cls ths0) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
198 |
|
45508 | 199 |
fun neg_clausify ctxt combinators = |
38028 | 200 |
single |
43964
9338aa218f09
thread proper context through, to make sure that "using [[meson_max_clauses = 200]]" is not ignored when clausifying the conjecture
blanchet
parents:
43963
diff
changeset
|
201 |
#> Meson.make_clauses_unsorted ctxt |
45508 | 202 |
#> combinators ? map Meson_Clausify.introduce_combinators_in_theorem |
38028 | 203 |
#> Meson.finish_cnf |
204 |
||
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
|
205 |
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
|
206 |
(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
|
207 |
(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
|
208 |
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
|
209 |
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
|
210 |
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
|
211 |
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
|
212 |
|
38652
e063be321438
perform eta-expansion of quantifier bodies in Sledgehammer translation when needed + transform elim rules later;
blanchet
parents:
38632
diff
changeset
|
213 |
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
|
214 |
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
|
215 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
216 |
fun generic_metis_tac type_encs lam_trans ctxt ths i st0 = |
37926
e6ff246c0cdb
renamings + only need second component of name pool to reconstruct proofs
blanchet
parents:
37925
diff
changeset
|
217 |
let |
39978
11bfb7e7cc86
added "trace_metis" configuration option, replacing old-fashioned references
blanchet
parents:
39964
diff
changeset
|
218 |
val _ = trace_msg ctxt (fn () => |
43194 | 219 |
"Metis called with theorems\n" ^ |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
220 |
cat_lines (map (Display.string_of_thm ctxt) ths)) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
221 |
val type_encs = type_encs |> maps unalias_type_enc |
45508 | 222 |
fun tac clause = |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
223 |
resolve_tac (FOL_SOLVE type_encs lam_trans ctxt clause ths) 1 |
32956 | 224 |
in |
37626
1146291fe718
move blacklisting completely out of the clausifier;
blanchet
parents:
37625
diff
changeset
|
225 |
if exists_type type_has_top_sort (prop_of st0) then |
43299
f78d5f0818a0
be a bit more liberal with respect to the universal sort -- it sometimes help
blanchet
parents:
43298
diff
changeset
|
226 |
verbose_warning ctxt "Proof state contains the universal sort {}" |
35568
8fbbfc39508f
renamed type_has_empty_sort to type_has_topsort -- {} is the full universal sort;
wenzelm
parents:
34087
diff
changeset
|
227 |
else |
43299
f78d5f0818a0
be a bit more liberal with respect to the universal sort -- it sometimes help
blanchet
parents:
43298
diff
changeset
|
228 |
(); |
45508 | 229 |
Meson.MESON (preskolem_tac ctxt) |
45514 | 230 |
(maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0 |
32956 | 231 |
end |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
232 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
233 |
fun metis_tac [] = generic_metis_tac partial_type_encs |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
234 |
| metis_tac type_encs = generic_metis_tac type_encs |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
235 |
|
38632
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
236 |
(* Whenever "X" has schematic type variables, we treat "using X by metis" as |
43100 | 237 |
"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
|
238 |
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
|
239 |
(in the rare and subtle case where a proof relied on extensionality not being |
38994 | 240 |
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
|
241 |
val has_tvar = |
9cde57cdd0e3
treat "using X by metis" (more or less) the same as "by (metis X)"
blanchet
parents:
38614
diff
changeset
|
242 |
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
|
243 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
244 |
fun method default_type_encs ((override_type_encs, lam_trans), ths) ctxt facts = |
43100 | 245 |
let |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
246 |
val _ = |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
247 |
if default_type_encs = full_type_encs then |
44052 | 248 |
legacy_feature "Old \"metisFT\" method -- use \"metis (full_types)\" instead" |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
249 |
else |
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
250 |
() |
43100 | 251 |
val (schem_facts, nonschem_facts) = List.partition has_tvar facts |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
252 |
val type_encs = override_type_encs |> the_default default_type_encs |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
253 |
val lam_trans = lam_trans |> the_default metis_default_lam_trans |
43100 | 254 |
in |
43099 | 255 |
HEADGOAL (Method.insert_tac nonschem_facts THEN' |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
256 |
CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt |
45514 | 257 |
(schem_facts @ ths)) |
43099 | 258 |
end |
43100 | 259 |
|
45521 | 260 |
val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN] |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
261 |
|
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
262 |
fun consider_opt s = |
45521 | 263 |
if member (op =) metis_lam_transs s then apsnd (K (SOME s)) |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
264 |
else apfst (K (SOME [s])) |
45514 | 265 |
|
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
266 |
val parse_metis_options = |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
267 |
Scan.optional |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
268 |
(Args.parens (Parse.short_ident |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
269 |
-- Scan.option (Parse.$$$ "," |-- Parse.short_ident)) |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
270 |
>> (fn (s, s') => |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
271 |
(NONE, NONE) |> consider_opt s |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
272 |
|> (case s' of SOME s' => consider_opt s' | _ => I))) |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
273 |
(NONE, NONE) |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
274 |
|
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
275 |
fun setup_method (binding, type_encs) = |
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
276 |
Scan.lift parse_metis_options -- Attrib.thms >> (METHOD oo method type_encs) |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
277 |
|> Method.setup binding |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
278 |
|
32956 | 279 |
val setup = |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
280 |
[((@{binding metis}, partial_type_encs), |
43228
2ed2f092e990
obsoleted "metisFT", and added "no_types" version of Metis as fallback to Sledgehammer after noticing how useful it can be
blanchet
parents:
43212
diff
changeset
|
281 |
"Metis for FOL and HOL problems"), |
45519
cd6e78cb6ee8
make metis reconstruction handling more flexible
blanchet
parents:
45514
diff
changeset
|
282 |
((@{binding metisFT}, full_type_encs), |
43212 | 283 |
"Metis for FOL/HOL problems with fully-typed translation")] |
43034
18259246abb5
try both "metis" and (on failure) "metisFT" in replay
blanchet
parents:
42847
diff
changeset
|
284 |
|> fold (uncurry setup_method) |
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
285 |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
286 |
end; |