theory week03A_exercise
  imports Main
begin

text \<open> exercise on slide #5:
- derive the classical contradiction rule (\<not>P =\<Rightarrow> False) =\<Rightarrow> P in Isabelle
- define nor and nand in Isabelle
- show nor x x = nand x x
-  derive safe intro and elim rules for them
-  use these in anautomated proof of nor x x = nand x x\<close>


thm ccontr

lemma "(\<not>P \<Longrightarrow> False) \<Longrightarrow> P"
 (* TODO *)
  oops

text \<open>nor and nand\<close>

definition nor  (* TODO *)

lemma norI: (* TODO *)

lemma norE: (* TODO *)

lemma
  "nor P P \<longleftrightarrow> \<not>P"
  (* TODO *)
  oops


definition 
  nand  (* TODO *)

lemma nandI: (* TODO *)

lemma nandE:  (* TODO *)

(* show nor x x = nand x x *)


end