theory tut1
imports Main

begin

(* Exercise 4 *)

lemma "(R \<longrightarrow> P) \<longrightarrow> (((\<not>R \<or> P) \<longrightarrow> (Q \<longrightarrow> S)) \<longrightarrow> (Q \<longrightarrow> S))"
apply (rule impI)
apply (rule impI)
apply (rule impI)
apply (cut_tac P="R" in excluded_middle)
apply (erule_tac P="\<not> R \<or> P" in impE)
apply (erule disjE)
apply (erule disjI1)
apply (erule impE)
apply assumption
apply (erule disjI2)
apply (erule_tac P=Q in impE)
apply assumption
apply assumption
done

(* Alternative proof, without the cut rule but with ccontr, which is an alternative to 
   exluded_middle  *)

lemma "(R \<longrightarrow> P) \<longrightarrow> (((\<not>R \<or> P) \<longrightarrow> (Q \<longrightarrow> S)) \<longrightarrow> (Q \<longrightarrow> S))"
apply (rule impI)
apply (rule impI)
apply (rule impI)
apply (rule ccontr)
apply (erule impE)
apply (rule ccontr)
apply (erule impE)
apply (rule disjI1)
apply assumption
apply (erule impE)
apply assumption
apply (rule notE)
apply assumption
apply assumption
apply (erule impE)
apply (rule disjI2)
apply assumption
apply (erule impE)
apply assumption
apply (erule notE)
apply assumption
done

(* Exercise 5 *)

lemma one: "(P \<longrightarrow> (Q \<longrightarrow> R)) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R))"
apply (rule impI)
apply (rule impI)
apply (rule impI)
apply (erule impE)
apply assumption
apply (erule impE)
apply assumption
apply (erule impE)
by assumption+

lemma two: "\<not>\<not>P \<longrightarrow> P"
apply (rule impI)
apply (rule ccontr)
apply (rule notE)
apply assumption
apply assumption
done

lemma three: "(P \<longrightarrow> Q \<and> R) \<longrightarrow> ((P \<longrightarrow> Q) \<and> (P \<longrightarrow> R))"
apply (rule impI)
apply (rule conjI)
apply (rule impI)
apply (rule conjunct1)
apply (rule mp)
apply assumption
apply assumption
apply (rule impI)
apply (rule conjunct2)
apply (rule mp)
apply assumption
apply assumption
done

thm ccontr
thm classical


lemma four: "(\<not>P \<longrightarrow> Q) \<longrightarrow> (\<not>Q \<longrightarrow> P)"
apply (rule impI)
apply (rule impI)
apply (rule ccontr)
apply (rule notE)
apply assumption
apply (rule mp)
apply assumption
apply assumption
done

lemma five: "P \<or> \<not>P"
apply (rule disjE)
apply (rule excluded_middle)
apply (rule disjI2)
apply assumption
apply (rule disjI1)
apply assumption
done

end