Stream: Beginner Questions

Topic: Apply theorem to assumptions


view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Lukas Stevens (Jun 19 2020 at 15:07):

Yeah, I'd like the Pure ==> one.

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Jun 19 2020 at 15:22):

Thanks anyways!


Last updated: Sep 25 2022 at 23:25 UTC