Hi all,
I found a solution to lemma (A ∨ ¬A)
in the Isabelle/Isar Reference Manual by Wenzel (2021), Section 2.3.4 "Classical logic". Very similar to my original question, so I adapted it to solve my problem:
lemma "¬¬ (A ∨ ¬A)"
proof (rule notI)
assume n1: "¬ (A ∨ ¬A)"
have "¬ A"
proof (rule notI)
assume A
then have "A ∨ ¬A" by (rule disjI1)
with n1 show False by (rule notE)
qed
then have "A ∨ ¬A" by (rule disjI2)
with n1 show False by (rule notE)
qed
On hindsight, my problem is not knowing that I can prove an intermediate result, i.e. having a proof block following a have statement. It's eye-opening and I find it quite elegant to be able to do so. (Thank you to Isabelle/Isar designer!)
Hope that you find this useful! :wink:
Jia Hong Lee has marked this topic as resolved.
Last updated: Jul 15 2022 at 23:21 UTC