Hanno Becker (Apr 22 2023 at 15:28): Hanno Becker (Apr 22 2023 at 15:28):Hi! Is there a tactic/conversion in the stdlib to rotate the pure assumptions of a subgoal? (Motivation: I'd like to have an index-based version of thin_tac and want to rotate the premise-to-be-removed to the front first, and then drop it via Pure.thin_rl) The kernel has a helper for rotating subgoals themselves, but I don't see how to get from there to rotating the premises of a subgoal.
Kevin Kappelmann (Apr 22 2023 at 17:30):You are looking for rotate_tac:
ML‹
fun thin_tac i = rotate_tac i THEN' eresolve0_tac [thin_rl] THEN' rotate_tac (~i)
›
lemma "P x ⟹ Q x ⟹ C" and "⋀x. P' x ⟹ Q' x ⟹ C'"
apply -
apply (tactic ‹rotate_tac 1 1›) (*works*)
apply (tactic ‹rotate_tac 1 2›) (*works*)
apply (tactic ‹thin_tac 0 1›) (*works*)
apply (tactic ‹thin_tac 1 2›) (*works*)
oops
There’s also the rotated attribute. Not sure how relevant this is to you use case.
Hanno Becker (Apr 22 2023 at 18:22):Ah, great. Not sure how I missed that :rolling_eyes: Thank you!
Last updated: Apr 27 2024 at 16:16 UTC