98 Logic.list_implies (assms |> map snd, concl) |
98 Logic.list_implies (assms |> map snd, concl) |
99 |> subst_free subst |
99 |> subst_free subst |
100 |> Skip_Proof.make_thm thy |
100 |> Skip_Proof.make_thm thy |
101 end |
101 end |
102 |
102 |
103 fun tac_of_method ctxt (local_facts, global_facts) meth = |
|
104 Method.insert_tac local_facts THEN' |
|
105 (case meth of |
|
106 Metis_Method (type_enc_opt, lam_trans_opt) => |
|
107 Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc] |
|
108 (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts |
|
109 | SMT_Method => SMT_Solver.smt_tac ctxt global_facts |
|
110 | Meson_Method => Meson.meson_tac ctxt global_facts |
|
111 | _ => |
|
112 Method.insert_tac global_facts THEN' |
|
113 (case meth of |
|
114 Simp_Method => Simplifier.asm_full_simp_tac ctxt |
|
115 | Simp_Size_Method => |
|
116 Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt) |
|
117 | Auto_Method => K (Clasimp.auto_tac ctxt) |
|
118 | Fastforce_Method => Clasimp.fast_force_tac ctxt |
|
119 | Force_Method => Clasimp.force_tac ctxt |
|
120 | Arith_Method => Arith_Data.arith_tac ctxt |
|
121 | Blast_Method => blast_tac ctxt |
|
122 | Algebra_Method => Groebner.algebra_tac [] [] ctxt)) |
|
123 |
|
124 (* main function for preplaying Isar steps; may throw exceptions *) |
103 (* main function for preplaying Isar steps; may throw exceptions *) |
125 fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) = |
104 fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) = |
126 let |
105 let |
127 val goal = |
106 val goal = |
128 (case xs of |
107 (case xs of |
147 resolve_fact_names ctxt fact_names |
126 resolve_fact_names ctxt fact_names |
148 |>> append (map (thm_of_proof ctxt) subproofs) |
127 |>> append (map (thm_of_proof ctxt) subproofs) |
149 |
128 |
150 fun prove () = |
129 fun prove () = |
151 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
130 Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} => |
152 HEADGOAL (tac_of_method ctxt facts meth)) |
131 HEADGOAL (tac_of_proof_method ctxt facts meth)) |
153 handle ERROR msg => error ("Preplay error: " ^ msg) |
132 handle ERROR msg => error ("Preplay error: " ^ msg) |
154 |
133 |
155 val play_outcome = take_time timeout prove () |
134 val play_outcome = take_time timeout prove () |
156 in |
135 in |
157 (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |
136 (if Config.get ctxt trace then preplay_trace ctxt facts goal play_outcome else (); |