theory a2 imports Main begin

(*
 * Question 1
 *)

lemma "(\<forall>x. \<forall>y. R x y) = (\<forall>y. \<forall>x. R x y)" 
  apply (rule iffI)
   apply (rule allI)
   apply (rule allI)
   apply (erule allE, erule allE, assumption)
  apply (rule allI)
  apply (rule allI)
  apply (erule allE, erule allE, assumption)
  done

lemma "((\<exists>x. P x) \<or> (\<exists>x. Q x)) = (\<exists>x. (P x \<or> Q x))"
  apply (rule iffI)
   apply (erule disjE)
    apply (erule exE)
    apply (rule exI, rule disjI1, assumption)
   apply (erule exE)
   apply (rule exI, rule disjI2, assumption)
  apply (erule exE)
  apply (erule disjE)
   apply (rule disjI1, rule exI, assumption)
  apply (rule disjI2, rule exI, assumption)
  done

lemma "((\<forall>x. P x) \<and> (\<forall>x. Q x)) = (\<forall>x. (P x \<and> Q x))" 
  apply (rule iffI)
   apply (erule conjE)
   apply (rule allI)
   apply (rule conjI)
    apply (erule allE, assumption)
   apply (erule allE, assumption)
  apply (rule conjI)
   apply (rule allI)
   apply (erule allE, erule conjE, assumption)
  apply (rule allI)
  apply (erule allE, erule conjE, assumption)
  done

lemma "\<not>(\<forall>x. P x) \<Longrightarrow> \<exists>x. \<not> P x"
  apply (rule classical)
  apply (erule notE)
  apply (rule allI)
  apply (case_tac "P x")
   apply assumption
  apply (erule notE)
  apply (rule exI, assumption)
  done

lemma "\<not>(\<exists>x. P x) \<Longrightarrow> \<forall>x. \<not> P x" 
  apply (rule allI)
  apply (rule notI)
  apply (erule notE)
  apply (rule exI, assumption)
  done

lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"
  apply (rule iffI)
   apply (rule impI)
   apply (erule exE)
   apply (erule allE, erule impE, assumption, assumption)
  apply (rule allI)
  apply (rule impI)
  apply (erule impE)
   apply (rule exI, assumption)
  apply assumption
  done


(*
 * Question 2 : Rich grandmother
 *
 * r(x) :: person \<Rightarrow> bool
 *     Person 'x' is rich.
 *
 * p(x) :: person \<Rightarrow> person
 *     The parent of person 'x'.
 *)

lemma "(\<forall> x. (\<not> (r x) \<longrightarrow> r (p x))) \<longrightarrow> (\<exists> x. (r x) \<and> (r (p (p x))))"
  apply (rule impI)
  apply (case_tac "\<exists> a. r a")
  (* Assume there is at least one rich person, "a". *)
   apply (erule exE)
   apply (case_tac "r (p a)")
    (* Assume that "a" has a rich mother. *)
    apply (case_tac "r (p (p a))")
     (* If "a"'s grandmother is rich, we are done. *)
     apply (rule exI, rule conjI, assumption, assumption)
    (* Otherwise, "a"'s grandmother is poor, but "a"'s mother has a rich grandmother. *)
    apply (frule_tac x="p (p a)" in spec)
    apply (erule impE)
     apply (assumption)
    apply (rule exI, rule conjI, assumption, assumption)
   (* Assume that "a" has a poor mother. In that case, "a"'s grandmother is rich. *)
   apply (frule_tac x="p a" in spec)   
    apply (erule impE)
     apply assumption
    apply (rule exI, rule conjI, assumption, assumption)
  (* Assume that nobody is rich at all. *)
  apply (erule notE)
  apply (case_tac "r b")
   apply (rule exI, assumption)
  apply (erule allE)
  apply (erule impE)
   apply assumption
  apply (rule exI)
  apply assumption
  done

(*
 * Question 4 : nand / nor
 *)

definition nand :: "bool \<Rightarrow> bool \<Rightarrow> bool"
where "nand a b \<equiv> \<not> (a \<and> b)"

definition nor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
where "nor a b \<equiv> \<not> (a \<or> b)"


(* Define my own contrapositive rule. *)
lemma contra: "\<lbrakk> \<not> x; y \<longrightarrow> x \<rbrakk> \<Longrightarrow> \<not> y"
  apply (rule notI)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

(* nand/nor manual proof *)
lemma "nor x x = nand x x"
  apply (unfold nor_def)
  apply (unfold nand_def)
  apply (rule iffI)
   apply (erule contra)
   apply (rule impI)
   apply (erule conjE)
   apply (rule disjI1)
   apply assumption
  apply (erule contra)
  apply (rule impI)
  apply (erule disjE)
   apply (rule conjI, assumption+)+
  done

(* Intro/Elim Rules *)

lemma dm1: "\<not> (A \<or> B) \<Longrightarrow> \<not>A \<and> \<not>B"
  apply (rule conjI)
   apply (rule classical)
   apply (erule notE)
   apply (rule disjI1)
   apply (erule notnotD)
  apply (rule classical)
  apply (erule notE)
  apply (rule disjI2)
  apply (erule notnotD)
  done

lemma dm2: "\<not> (A \<and> B) \<Longrightarrow> (\<not>A \<or> \<not>B)"
  apply (rule classical)
  apply (erule notE)
  apply (rule conjI)
   apply (rule classical)
   apply (erule notE)
   apply (erule disjI1)
  apply (rule classical)
  apply (erule notE)
  apply (erule disjI2)
  done

lemma norI [intro!]:
  "\<lbrakk>\<not> A; \<not> B\<rbrakk> \<Longrightarrow> nor A B"
  apply (unfold nor_def)
  apply (rule notI)
  apply (erule disjE)
  apply (erule (1) notE)
  apply (erule (1) notE)
  done

lemma norE [elim!]:
  assumes n: "nor A B" 
  assumes r: "\<lbrakk> \<not>A; \<not>B \<rbrakk> \<Longrightarrow> R"
  shows "R"
  apply (insert n) 
  apply (unfold nor_def)
  apply (drule dm1)
  apply (erule conjE)
  apply (erule (1) r)
  done

lemma nandI [intro!]:
  assumes ab: "\<lbrakk> A; B \<rbrakk> \<Longrightarrow> False"
  shows "nand A B"
  apply (unfold nand_def)
  apply (rule notI)
  apply (erule conjE)
  apply (erule (1) ab)
  done

lemma nandE [elim!]:
  assumes n: "nand A B" 
  assumes A: "\<not>A \<Longrightarrow> R"
  assumes B: "\<not>B \<Longrightarrow> R"
  shows "R"
  apply (insert n) 
  apply (unfold nand_def)
  apply (drule dm2)
  apply (erule disjE)
   apply (erule A)
  apply (erule B)
  done

(* Automation: *)
lemma "nor x x = nand x x"
  by(blast)

end