## Stream: Beginner Questions

### Topic: Elimination rule

#### Gergely Buday (Mar 16 2023 at 10:32):

I have the following:

``````lemma p_imp_porq: assumes p shows "p ∨ q"
proof -
show ?thesis using assms by (rule disjI1[of p q])
qed

lemma qandr_imp_q: assumes "q ∧ r" shows q
proof -
show ?thesis using assms by (rule conjunct1[of q r])
qed
``````

I wonder that I cannot use erule in the second proof, despite of conjunct1 being an elimination rule. Could you explain the background here?

#### Wolfgang Jeltsch (Mar 16 2023 at 19:01):

I never figured out the details, but I think that `erule` expects the premise as part of the goal, using implication, while `rule` is fine with receiving it as a chained fact (here introduced via `using`). I think that this has to do with the fact that, according to my memories,`erule` is considered “improper” (which doesn’t prevent me from using it :sweat_smile:).

You can illustrate the different expectations of `erule` and `rule` by changing `by (rule ...)` to `by - (erule ...)` in your code. The proof method `-` just turns any chained facts into goal premises and thus makes the `erule` invocations work.

#### Zixuan Fan (Mar 16 2023 at 22:51):

If you change the `erule` to `frule`, Isabelle can figure it out and finish the proof. `frule` applies the `rule` in a forward-resolution manner. You can find a more detailed description in this manual at chapter 4.2.1.

I think some details are also available as the definition of the `erule`, `frule` etc. in the file `method.ML`.

#### Kevin Kappelmann (Mar 17 2023 at 06:40):

There's also a beginner friendly exposition here (file linked in first sentence):
https://isabelle.systems/cookbook/src/proofs/methods/

#### Gergely Buday (Mar 22 2023 at 08:08):

Thank you all

Last updated: Feb 27 2024 at 08:17 UTC