Jan van Brügge (Nov 03 2023 at 11:31): Jan van Brügge (Nov 03 2023 at 11:31):Hi, I am trying to find a way to get from a goal that looks like this:
(⋀a. P a ⟹ Q a) ⟹ (⋀a. P2 a ⟹ Q2 a) ⟹ P2 x ⟹ Y ⟹ W
to a state where the assumption and the higher order assumption have been resolved, so like this:
(⋀a. P a ⟹ Q a) ⟹ (⋀a. P2 a ⟹ Q2 a) ⟹ Q2 x ⟹ Y ⟹ W
ideally without having to know that it needs the second higher order assumption, but if that is not easily possible that's ok as well.
I know I can use subgoal premises, but I have other assumptions that I want to use with erule so that make my life a lot harder. If W = Q2 x then I could just use assumption, however that does not apply in my case
And just to make it clear, I need it as apply script, not as isar proof. This is supposed to be automated with ML later
Lukas Stevens (Nov 03 2023 at 12:05):I suspect that there is no way around some variant of Subgoal.FOCUS
Last updated: Apr 27 2024 at 16:16 UTC