Gergely Buday (Mar 16 2023 at 10:32): 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: Apr 19 2024 at 08:19 UTC