## Stream: Beginner Questions

### Topic: Apply theorem to assumptions

#### 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: Aug 13 2022 at 05:18 UTC