215 |
215 |
216 (** simplification tactics and rules **) |
216 (** simplification tactics and rules **) |
217 |
217 |
218 fun solve_all_tac solvers ss = |
218 fun solve_all_tac solvers ss = |
219 let |
219 let |
220 val (_, {subgoal_tac, ...}) = MetaSimplifier.rep_ss ss; |
220 val (_, {subgoal_tac, ...}) = MetaSimplifier.internal_ss ss; |
221 val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac); |
221 val solve_tac = subgoal_tac (MetaSimplifier.set_solvers solvers ss) THEN_ALL_NEW (K no_tac); |
222 in DEPTH_SOLVE (solve_tac 1) end; |
222 in DEPTH_SOLVE (solve_tac 1) end; |
223 |
223 |
224 (*NOTE: may instantiate unknowns that appear also in other subgoals*) |
224 (*NOTE: may instantiate unknowns that appear also in other subgoals*) |
225 fun generic_simp_tac safe mode ss = |
225 fun generic_simp_tac safe mode ss = |
226 let |
226 let |
227 val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.rep_ss ss; |
227 val (_, {loop_tacs, solvers = (unsafe_solvers, solvers), ...}) = MetaSimplifier.internal_ss ss; |
228 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
228 val loop_tac = FIRST' (map (fn (_, tac) => tac ss) (rev loop_tacs)); |
229 val solve_tac = FIRST' (map (MetaSimplifier.solver ss) |
229 val solve_tac = FIRST' (map (MetaSimplifier.solver ss) |
230 (rev (if safe then solvers else unsafe_solvers))); |
230 (rev (if safe then solvers else unsafe_solvers))); |
231 |
231 |
232 fun simp_loop_tac i = |
232 fun simp_loop_tac i = |
236 |
236 |
237 local |
237 local |
238 |
238 |
239 fun simp rew mode ss thm = |
239 fun simp rew mode ss thm = |
240 let |
240 let |
241 val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.rep_ss ss; |
241 val (_, {solvers = (unsafe_solvers, _), ...}) = MetaSimplifier.internal_ss ss; |
242 val tacf = solve_all_tac (rev unsafe_solvers); |
242 val tacf = solve_all_tac (rev unsafe_solvers); |
243 fun prover s th = Option.map #1 (Seq.pull (tacf s th)); |
243 fun prover s th = Option.map #1 (Seq.pull (tacf s th)); |
244 in rew mode prover ss thm end; |
244 in rew mode prover ss thm end; |
245 |
245 |
246 in |
246 in |