I wanted to give myself an intro challenge to Isabelle/HOL and prove De Morgan's law using only the rules of natural deduction (applying only rule *, erule * and assumption). However, I can't get it to work. I started out like this:
lemma "(¬P ∨ ¬Q) = (¬(P ∧ Q))"
apply (rule iffI)
apply (erule disjE)
apply (rule notI)
apply (erule notE)
apply (erule conjE)
apply assumption
apply (rule notI)
apply (erule notE)
apply (erule conjE)
apply assumption
This leaves me in the proof state
proof (prove)
goal (1 subgoal):
1. ¬ (P ∧ Q) ⟹ ¬ P ∨ ¬ Q
From there on, I can't seem to make any progress. Is there anyone who knows how to derive the second part of the proof using the natural deduction rules coded down in Isabelle/HOL? No simp, blast, fast, metis, auto, or similar junk. This must be possible, but the Isabelle syntax is so obscure and poorly documented that I find it really hard to make progress.