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?

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.

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`

.

There's also a beginner friendly exposition here (file linked in first sentence):

https://isabelle.systems/cookbook/src/proofs/methods/

Thank you all

Last updated: Nov 11 2024 at 04:22 UTC