theory Hilbert imports Main
begin

(* Axioms *)

lemma A1: "P \<longrightarrow> (Q \<longrightarrow> P)" by simp
lemma A2: "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R))" by simp
lemma A3: "(\<not>P \<longrightarrow> \<not>Q) \<longrightarrow> (Q \<longrightarrow> 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 "\<not>\<not>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 \<longrightarrow> (a \<longrightarrow> a)"
...
done


lemma Exercise_2_b:
"(\<not>a \<longrightarrow> \<not>a)"
...
done

lemma Exercise_2_c:
"\<not>\<not>a \<Longrightarrow> a"
...
done

end