Lukas Stevens (Jul 27 2021 at 14:13): Lukas Stevens (Jul 27 2021 at 14:13):How can I delete the i-th premise of a subgoal? No worries, this is for a tactic and not an apply-style proof :sweat_smile:
Simon Roßkopf (Jul 27 2021 at 21:36):I do not know of anything built in. There is Tactic.filter_prems_tac, which you could modify to also take the position of the premise into account.
A three minute hack, to show what I mean:
fun filter_prems_pos_tac ctxt pred =
let
fun Then NONE tac = SOME tac
| Then (SOME tac) tac' = SOME (tac THEN' tac');
fun thins H (tac, n, i) =
if pred H i then (tac, n + 1, i + 1)
else (Then tac (rotate_tac n THEN' eresolve_tac ctxt [thin_rl]), 0, i + 1);
in
SUBGOAL (fn (goal, i) =>
let val Hs = Logic.strip_assums_hyp goal in
(case fold thins Hs (NONE, 0, 0) of
(NONE, _, _) => no_tac
(* filter_prems_tac seems to reorder prems without this rotate_tac *)
| (SOME tac, n, _) => (tac THEN' rotate_tac n) i)
end)
end;
Last updated: Apr 23 2024 at 20:15 UTC