How can I apply a theorem to the assumptions? Specifically, I want to convert the assumptions to a single conjunction.
You mean you want to apply a rule like
A1 /\ ... /\ An ==> B and you know the
No, I have the goal
A ==> B ==> C ==> D and I want to get the goal
A /\ B /\ C ==> D.
If that's a Pure
==> (as opposed to a HOL
-->) then I'm not sure this is easily doable...
Yeah, I'd like the Pure
I seem to recall the last time I asked something like this the answer was that such direct manipulation of meta-implications breaks some Isar paradigm...
But I'm a rebel, so: try
simp only: atomize_conjL.
BEGINNER WARNING THIS IS BAD PRACTICE, there's most likely a better way to prove the concrete statement you want.
I am not afraid since it is only a preprocessing for a tactic and I am using SUBGOAL.Focus :D
Excellent! :D But if you're already using Subgoal.FOCUS then why is this in beginner questions :p
Ah, I think I had a lapse of thought. Instead of doing this step, I can just convert the thms that I get from SUBGOAL.Focus to a single thm that is the conjunction of those thms.
Last updated: Aug 13 2022 at 05:18 UTC