--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Thu Jan 30 21:56:25 2014 +0100
@@ -34,9 +34,10 @@
val trace = Attrib.setup_config_bool @{binding sledgehammer_preplay_trace} (K false)
-fun preplay_trace ctxt assms concl result =
+fun preplay_trace ctxt assmsp concl result =
let
val ctxt = ctxt |> Config.put show_markup true
+ val assms = op @ assmsp
val time = "[" ^ string_of_play_outcome result ^ "]" |> Pretty.str
val nr_of_assms = length assms
val assms = assms
@@ -64,8 +65,7 @@
fun resolve_fact_names ctxt names =
(names
|>> map string_of_label
- |> op @
- |> maps (thms_of_name ctxt))
+ |> pairself (maps (thms_of_name ctxt)))
handle ERROR msg => error ("preplay error: " ^ msg)
fun thm_of_proof ctxt (Proof (fixed_frees, assms, steps)) =
@@ -86,15 +86,15 @@
|> Skip_Proof.make_thm thy
end
-fun tac_of_method meth type_enc lam_trans ctxt facts =
+fun tac_of_method meth type_enc lam_trans ctxt (local_facts, global_facts) =
+ Method.insert_tac local_facts THEN'
(case meth of
- Metis_Method_with_Args => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts
- | Meson_Method => Meson.meson_tac ctxt facts
+ Meson_Method => Meson.meson_tac ctxt global_facts
+ | Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt global_facts
| _ =>
- Method.insert_tac facts THEN'
+ Method.insert_tac global_facts THEN'
(case meth of
- Metis_Method => Metis_Tactic.metis_tac [type_enc] lam_trans ctxt []
- | Simp_Method => Simplifier.asm_full_simp_tac ctxt
+ Simp_Method => Simplifier.asm_full_simp_tac ctxt
| Simp_Size_Method =>
Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
| Auto_Method => K (Clasimp.auto_tac ctxt)
@@ -128,7 +128,10 @@
Logic.all thesis (Logic.mk_implies (inner_prop, thesis_prop))
end)
- val facts = map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
+ val facts =
+ resolve_fact_names ctxt fact_names
+ |>> append (map (thm_of_proof ctxt) subproofs)
+
val ctxt' = ctxt |> silence_reconstructors debug
fun prove () =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML Thu Jan 30 21:56:25 2014 +0100
@@ -165,12 +165,19 @@
| Meson_Method => "meson"
| _ => raise Fail "Sledgehammer_Print: by_method")
- fun using_facts [] [] = ""
- | using_facts ls ss = "using " ^ space_implode " " (map string_of_label ls @ ss) ^ " "
+ fun with_facts none _ [] [] = none
+ | with_facts _ some ls ss = some (space_implode " " (map string_of_label ls @ ss))
+
+ val using_facts = with_facts "" (enclose "using " " ")
- fun of_metis ls ss = reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 (ls, ss)
-
- fun of_method ls ss Metis_Method_with_Args = of_metis ls ss
+ (* Local facts are always passed via "using", which affects "meson" and "metis". This is
+ arguably stylistically superior, because it emphasises the structure of the proof. It is also
+ more robust w.r.t. preplay: Preplay is performed before chaining of local facts with "hence"
+ and "thus" is introduced. See also "tac_of_method" in "Sledgehammer_Preplay". *)
+ fun of_method ls ss Metis_Method =
+ using_facts ls [] ^ reconstructor_command (Metis (type_enc, lam_trans)) 1 1 [] 0 ([], ss)
+ | of_method ls ss Meson_Method =
+ using_facts ls [] ^ with_facts "by meson" (enclose "by (meson " ")") [] ss
| of_method ls ss meth = using_facts ls ss ^ by_method meth
fun of_byline ind (ls, ss) meth =
@@ -245,7 +252,7 @@
(* One-step Metis proofs are pointless; better use the one-liner directly. *)
(case proof of
Proof ([], [], []) => "" (* degenerate case: the conjecture is "True" with Z3 *)
- | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method_with_Args :: _) :: _))]) => ""
+ | Proof ([], [], [Prove (_, [], _, _, [], (_, (Metis_Method :: _) :: _))]) => ""
| _ =>
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^
of_indent 0 ^ "proof -\n" ^ of_proof 1 ctxt proof ^
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Thu Jan 30 21:56:25 2014 +0100
@@ -20,8 +20,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
and proof_method =
- Metis_Method_with_Args | Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method |
- Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method
val no_label : label
val no_facts : facts
@@ -69,8 +69,8 @@
Prove of isar_qualifier list * (string * typ) list * label * term * isar_proof list *
(facts * proof_method list list)
and proof_method =
- Metis_Method_with_Args | Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method |
- Fastforce_Method | Force_Method | Arith_Method | Blast_Method | Meson_Method
+ Metis_Method | Simp_Method | Simp_Size_Method | Auto_Method | Fastforce_Method | Force_Method |
+ Arith_Method | Blast_Method | Meson_Method
val no_label = ("", ~1)
val no_facts = ([],[])
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 30 21:02:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Thu Jan 30 21:56:25 2014 +0100
@@ -194,14 +194,14 @@
val arith_methodss =
[[Arith_Method, Simp_Method, Auto_Method, Fastforce_Method, Blast_Method, Force_Method,
- Metis_Method_with_Args], [Meson_Method]]
+ Metis_Method], [Meson_Method]]
val datatype_methodss = [[Simp_Size_Method, Simp_Method]]
val metislike_methodss =
- [[Metis_Method_with_Args, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
+ [[Metis_Method, Simp_Method, Auto_Method, Arith_Method, Blast_Method, Fastforce_Method,
Force_Method], [Meson_Method]]
val rewrite_methodss =
- [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method_with_Args], [Meson_Method]]
-val skolem_methodss = [[Metis_Method_with_Args, Blast_Method], [Metis_Method], [Meson_Method]]
+ [[Auto_Method, Simp_Method, Fastforce_Method, Force_Method, Metis_Method], [Meson_Method]]
+val skolem_methodss = [[Metis_Method, Blast_Method], [Meson_Method]]
fun isar_proof_text ctxt debug isar_proofs isar_params
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) =