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
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
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
frule etc. in the file
There's also a beginner friendly exposition here (file linked in first sentence):
Thank you all
Last updated: Dec 07 2023 at 20:16 UTC