Stream: Beginner Questions

Topic: Elimination rule


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

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

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

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

view this post on Zulip Gergely Buday (Mar 22 2023 at 08:08):

Thank you all


Last updated: Dec 07 2023 at 20:16 UTC