header {* Automated Reasoning, Exercise Sheet 2 *}

theory ex2
imports Main

begin

text {* Prove the following lemmas in Isabelle *}

lemma one: "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R))"
oops

lemma two: "\<not>\<not>P \<longrightarrow> P"
oops

lemma three: "(P \<longrightarrow> Q \<and> R) \<longrightarrow> ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))"
oops

lemma four: "(\<not>P \<longrightarrow> Q) \<longrightarrow> (\<not>Q \<longrightarrow> P)"
oops

lemma five: "P \<or> \<not>P"
oops

text {* To fully understand the proofs you have constructed, try
drawing out the proof trees that correspond to the proof steps
accepted by Isabelle. *}

end