Jan van Brügge (Jan 22 2022 at 14:05): Jan van Brügge (Jan 22 2022 at 14:05):I ended up using SUBPROOF anyways, because it is easier to branch on the goal and then I can just use Local_Defs.unfold0
Subgoal.FOCUS (fn {context, prems = [p1, p2], ...} =>
if HOLogic.dest_Trueprop (Thm.prop_of p2) = @{term False} then
rtac ctxt @{thm FalseE} 1 THEN
rtac ctxt p2 1
else
resolve_tac ctxt F_wit_thms 1 THEN
rtac ctxt (unfold context [p2] p1) 1
) ctxt)
Jan van Brügge has marked this topic as resolved.
Lukas Stevens (Jan 22 2022 at 14:44):Just keep in mind that Subgoal.FOCUS is quite expensive in general
Dmitriy Traytel (Jan 22 2022 at 17:16):There is also hypsubst_tac that would work here if T does not depend on x.
Jan van Brügge (Jan 23 2022 at 10:00):Ah, yes that is the tactic that I originally wanted. Now without Subgoal.FOCUS:
(
K (unfold_thms_tac ctxt @{thms False_implies_equals}) THEN'
rtac ctxt @{thm TrueI}
) ORELSE' (EVERY' [
hyp_subst_tac ctxt,
dresolve_tac ctxt F_wit_thms,
assume_tac ctxt
])
Is there an unfold_thms_tac but restricted to only one subgoal?
Dmitriy Traytel (Jan 24 2022 at 07:59):SELECT_GOAL can be used to restrict a tactic to a subgoal
Last updated: Jul 15 2022 at 23:21 UTC