--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 12:02:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Mon Dec 16 12:26:18 2013 +0100
@@ -230,9 +230,9 @@
fun chain_qs_lfs NONE lfs = ([], lfs)
| chain_qs_lfs (SOME l0) lfs =
if member (op =) lfs l0 then ([Then], lfs |> remove (op =) l0) else ([], lfs)
- fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), method))) =
+ fun chain_step lbl (Prove (qs, xs, l, t, subproofs, ((lfs, gfs), meths))) =
let val (qs', lfs) = chain_qs_lfs lbl lfs in
- Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), method))
+ Prove (qs' @ qs, xs, l, t, chain_proofs subproofs, ((lfs, gfs), meths))
end
| chain_step _ step = step
and chain_steps _ [] = []
@@ -248,6 +248,15 @@
bool * bool * string * string * Time.time option * real * bool * (term, string) atp_step list *
thm
+val arith_methods =
+ [Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
+ Metis_Method]
+val metislike_methods =
+ [Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+ Force_Method, Meson_Method]
+val rewrite_methods = [Simp_Method, Auto_Method, Fastforce_Method, Force_Method, Metis_Method]
+val skolem_methods = [Metis_Method, Meson_Method]
+
fun isar_proof_text ctxt isar_proofs
(debug, verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress, isar_try0,
atp_proof, goal)
@@ -287,12 +296,12 @@
map_filter (get_role (curry (op =) Lemma)) atp_proof
|> map (fn ((l, t), rule) =>
let
- val (skos, meth) =
- if is_skolemize_rule rule then (skolems_of t, Metis_Method)
- else if is_arith_rule rule then ([], Arith_Method)
- else ([], Auto_Method)
+ val (skos, meths) =
+ if is_skolemize_rule rule then (skolems_of t, skolem_methods)
+ else if is_arith_rule rule then ([], arith_methods)
+ else ([], rewrite_methods)
in
- Prove ([], skos, l, t, [], (([], []), meth))
+ Prove ([], skos, l, t, [], (([], []), meths))
end)
val bot = atp_proof |> List.last |> #1
@@ -340,7 +349,7 @@
accum
|> (if tainted = [] then
cons (Prove (if outer then [Show] else [], [], no_label, concl_t, [],
- ((the_list predecessor, []), Metis_Method)))
+ ((the_list predecessor, []), metislike_methods)))
else
I)
|> rev
@@ -355,15 +364,15 @@
fun do_rest l step = isar_steps outer (SOME l) (step :: accum) infs
val deps = fold add_fact_of_dependencies gamma no_facts
- val meth = if is_arith_rule rule then Arith_Method else Metis_Method
- val by = (deps, meth)
+ val meths = if is_arith_rule rule then arith_methods else metislike_methods
+ val by = (deps, meths)
in
if is_clause_tainted c then
(case gamma of
[g] =>
if skolem andalso is_clause_tainted g then
let val subproof = Proof (skolems_of (prop_of_clause g), [], rev accum) in
- isar_steps outer (SOME l) [prove [subproof] (no_facts, Metis_Method)] []
+ isar_steps outer (SOME l) [prove [subproof] (no_facts, skolem_methods)] []
end
else
do_rest l (prove [] by)
@@ -381,7 +390,7 @@
val step =
Prove (maybe_show outer c [], [], l, t,
map isar_case (filter_out (null o snd) cases),
- ((the_list predecessor, []), Metis_Method))
+ ((the_list predecessor, []), metislike_methods))
in
isar_steps outer (SOME l) (step :: accum) infs
end