--- a/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Mon Feb 01 19:57:58 2016 +0100
@@ -17,7 +17,7 @@
thm list * thm Seq.seq
val metis_tac : string list -> string -> Proof.context -> thm list -> int -> tactic
val metis_method : (string list option * string option) * thm list -> Proof.context -> thm list ->
- thm -> thm Seq.seq
+ tactic
val metis_lam_transs : string list
val parse_metis_options : (string list option * string option) parser
end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Feb 01 19:57:58 2016 +0100
@@ -63,11 +63,6 @@
fun is_metis_method (Metis_Method _) = true
| is_metis_method _ = false
-fun add_chained [] t = t
- | add_chained chained ((t as Const (@{const_name Pure.all}, _)) $ Abs (s, T, u)) =
- t $ Abs (s, T, add_chained chained u)
- | add_chained chained t = Logic.list_implies (chained, t)
-
fun play_one_line_proof minimize timeout used_facts0 state i (preferred_meth, methss) =
let val used_facts = filter_out (fn (_, (sc, _)) => sc = Chained) used_facts0 in
if timeout = Time.zeroTime then
@@ -79,7 +74,6 @@
val fact_names = map fst used_facts
val {facts = chained, goal, ...} = Proof.goal state
val goal_t = Logic.get_goal (Thm.prop_of goal) i
- |> add_chained (map (Thm.prop_of o forall_intr_vars) chained)
fun try_methss [] [] = (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime))
| try_methss ress [] =
@@ -92,7 +86,7 @@
fun mk_step fact_names meths =
Prove ([], [], ("", 0), goal_t, [], ([], fact_names), meths, "")
in
- (case preplay_isar_step ctxt timeout [] (mk_step fact_names meths) of
+ (case preplay_isar_step ctxt chained timeout [] (mk_step fact_names meths) of
(res as (meth, Played time)) :: _ =>
(* if a fact is needed by an ATP, it will be needed by "metis" *)
if not minimize orelse is_metis_method meth then
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML Mon Feb 01 19:57:58 2016 +0100
@@ -173,7 +173,7 @@
(* check if the modified step can be preplayed fast enough *)
val timeout = adjust_merge_timeout preplay_timeout (Time.+ (time, reference_time l'))
in
- (case preplay_isar_step ctxt timeout hopeless step'' of
+ (case preplay_isar_step ctxt [] timeout hopeless step'' of
meths_outcomes as (_, Played time'') :: _ =>
(* "l'" successfully eliminated *)
(decrement_step_count ();
@@ -218,7 +218,8 @@
val total_time = Library.foldl Time.+ (reference_time l, times0)
val timeout = adjust_merge_timeout preplay_timeout
(Time.fromReal (Time.toReal total_time / Real.fromInt n))
- val meths_outcomess = @{map 2} (preplay_isar_step ctxt timeout) hopelesses succs'
+ val meths_outcomess =
+ @{map 2} (preplay_isar_step ctxt [] timeout) hopelesses succs'
in
(case try (map (fn (_, Played time) :: _ => time)) meths_outcomess of
NONE => steps
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML Mon Feb 01 19:57:58 2016 +0100
@@ -45,7 +45,7 @@
fun minimize_half _ min_facts [] time = (min_facts, time)
| minimize_half mk_step min_facts (fact :: facts) time =
- (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
+ (case preplay_isar_step_for_method ctxt [] (Time.+ (time, slack)) meth
(mk_step (min_facts @ facts)) of
Played time' => minimize_half mk_step min_facts facts time'
| _ => minimize_half mk_step (fact :: min_facts) facts time)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML Mon Feb 01 19:57:58 2016 +0100
@@ -19,10 +19,10 @@
val peek_at_outcome : play_outcome Lazy.lazy -> play_outcome
val enrich_context_with_local_facts : isar_proof -> Proof.context -> Proof.context
- val preplay_isar_step_for_method : Proof.context -> Time.time -> proof_method -> isar_step ->
- play_outcome
- val preplay_isar_step : Proof.context -> Time.time -> proof_method list -> isar_step ->
- (proof_method * play_outcome) list
+ val preplay_isar_step_for_method : Proof.context -> thm list -> Time.time -> proof_method ->
+ isar_step -> play_outcome
+ val preplay_isar_step : Proof.context -> thm list -> Time.time -> proof_method list ->
+ isar_step -> (proof_method * play_outcome) list
val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
isar_preplay_data Unsynchronized.ref -> isar_step -> (proof_method * play_outcome) list -> unit
val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
@@ -126,7 +126,8 @@
end
(* may throw exceptions *)
-fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, facts, _, _)) =
+fun raw_preplay_step_for_method ctxt chained timeout meth
+ (Prove (_, xs, _, t, subproofs, facts, _, _)) =
let
val goal =
(case xs of
@@ -150,6 +151,7 @@
val assmsp =
resolve_fact_names ctxt facts
|>> append (map (thm_of_proof ctxt) subproofs)
+ |>> append chained
fun prove () =
Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
@@ -162,14 +164,14 @@
play_outcome
end
-fun preplay_isar_step_for_method ctxt timeout meth =
- try (raw_preplay_step_for_method ctxt timeout meth) #> the_default Play_Failed
+fun preplay_isar_step_for_method ctxt chained timeout meth =
+ try (raw_preplay_step_for_method ctxt chained timeout meth) #> the_default Play_Failed
val min_preplay_timeout = seconds 0.002
-fun preplay_isar_step ctxt timeout0 hopeless step =
+fun preplay_isar_step ctxt chained timeout0 hopeless step =
let
- fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt timeout meth step)
+ fun preplay timeout meth = (meth, preplay_isar_step_for_method ctxt chained timeout meth step)
fun get_time (_, Played time) = SOME time
| get_time _ = NONE
@@ -194,7 +196,7 @@
(step as Prove (_, _, l, _, _, _, meths, _)) meths_outcomes0 =
let
fun lazy_preplay meth =
- Lazy.lazy (fn () => preplay_isar_step_for_method ctxt timeout meth step)
+ Lazy.lazy (fn () => preplay_isar_step_for_method ctxt [] timeout meth step)
val meths_outcomes = meths_outcomes0
|> map (apsnd Lazy.value)
|> fold (fn meth => AList.default (op =) (meth, lazy_preplay meth)) meths
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 01 23:52:06 2016 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML Mon Feb 01 19:57:58 2016 +0100
@@ -114,7 +114,6 @@
end
fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
- Method.insert_tac ctxt local_facts THEN'
(case meth of
Metis_Method (type_enc_opt, lam_trans_opt) =>
let
@@ -122,26 +121,29 @@
|> Config.put Metis_Tactic.verbose false
|> Config.put Metis_Tactic.trace false
in
- Metis_Tactic.metis_tac [type_enc_opt |> the_default (hd partial_type_encs)]
- (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
+ SELECT_GOAL (Metis_Tactic.metis_method ((Option.map single type_enc_opt, lam_trans_opt),
+ global_facts) ctxt local_facts)
end
- | Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
- | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
- | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
- | Simp_Size_Method =>
- Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
+ | SMT_Method => SMT_Solver.smt_tac ctxt (local_facts @ global_facts)
| _ =>
- Method.insert_tac ctxt global_facts THEN'
+ Method.insert_tac ctxt local_facts THEN'
(case meth of
- SATx_Method => SAT.satx_tac ctxt
- | Blast_Method => blast_tac ctxt
- | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
- | Fastforce_Method => Clasimp.fast_force_tac ctxt
- | Force_Method => Clasimp.force_tac ctxt
- | Moura_Method => moura_tac ctxt
- | Linarith_Method => Lin_Arith.tac ctxt
- | Presburger_Method => Cooper.tac true [] [] ctxt
- | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
+ Meson_Method => Meson_Tactic.meson_general_tac ctxt global_facts
+ | Simp_Method => Simplifier.asm_full_simp_tac (ctxt addsimps global_facts)
+ | Simp_Size_Method =>
+ Simplifier.asm_full_simp_tac (ctxt addsimps (@{thm size_ne_size_imp_ne} :: global_facts))
+ | _ =>
+ Method.insert_tac ctxt global_facts THEN'
+ (case meth of
+ SATx_Method => SAT.satx_tac ctxt
+ | Blast_Method => blast_tac ctxt
+ | Auto_Method => SELECT_GOAL (Clasimp.auto_tac ctxt)
+ | Fastforce_Method => Clasimp.fast_force_tac ctxt
+ | Force_Method => Clasimp.force_tac ctxt
+ | Moura_Method => moura_tac ctxt
+ | Linarith_Method => Lin_Arith.tac ctxt
+ | Presburger_Method => Cooper.tac true [] [] ctxt
+ | Algebra_Method => Groebner.algebra_tac [] [] ctxt)))
fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
| string_of_play_outcome (Play_Timed_Out time) =