Lukas Stevens (Jun 19 2020 at 14:40): Lukas Stevens (Jun 19 2020 at 14:40):How can I apply a theorem to the assumptions? Specifically, I want to convert the assumptions to a single conjunction.
Josh Chen (Jun 19 2020 at 15:00):You mean you want to apply a rule like A1 /\ ... /\ An ==> B and you know the Ai separately?
Lukas Stevens (Jun 19 2020 at 15:02):No, I have the goal A ==> B ==> C ==> D and I want to get the goal A /\ B /\ C ==> D.
Josh Chen (Jun 19 2020 at 15:06):If that's a Pure ==> (as opposed to a HOL -->) then I'm not sure this is easily doable...
Lukas Stevens (Jun 19 2020 at 15:07):Yeah, I'd like the Pure ==> one.
Josh Chen (Jun 19 2020 at 15:13):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...
Josh Chen (Jun 19 2020 at 15:13):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.
Lukas Stevens (Jun 19 2020 at 15:16):I am not afraid since it is only a preprocessing for a tactic and I am using SUBGOAL.Focus :D
Josh Chen (Jun 19 2020 at 15:16):Excellent! :D But if you're already using Subgoal.FOCUS then why is this in beginner questions :p
Lukas Stevens (Jun 19 2020 at 15:22):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.
Lukas Stevens (Jun 19 2020 at 15:22):Thanks anyways!
Last updated: Apr 26 2024 at 01:06 UTC