theory Hilbert imports Main begin (* Axioms *) lemma A1: "P \ (Q \ P)" by simp lemma A2: "(P \ (Q \ R)) \ ((P \ Q) \ (P \ R))" by simp lemma A3: "(\P \ \Q) \ (Q \ P)" by blast (* Proof Schema A pen & paper proof can be translated into an Isabelle proof using the following schema: Instantiating an axiom is done with a proof command like this: apply (insert A3 [of a "\\a"]) Applying the MP rule of the calculus to derive a new fact is done like this: apply (frule(1) mp [of _ a]) where the instantiations of the schema variables is used to show Isabelle which facts to combine. Finally, once the last element in the sequence is the theorem to be proven, we apply assumption once to close the proof. *) lemma Exercise_2_a: "b \ (a \ a)" ... done lemma Exercise_2_b: "(\a \ \a)" ... done lemma Exercise_2_c: "\\a \ a" ... done end