theory a1
imports Main
begin

section "Q1: Types (12 marks)"

(* provide your answers here or in an separate PDF file *)


section "Q2: @text \<lambda>-Calculus (18 marks)"

(* provide your answers here or in an separate PDF file *)


section "Q3: Propositional Logic (36 marks)"

(*
  You must use only these proof methods:
   - rule, erule, assumption, cases

  You must use only there proof rules:
   - impI, impE, conjI, conjE, disjI1, disjI2, disjE, notI, notE
     iffI, iffE, iffD1, iffD1, iffD2, ccontr, classical, FalseE,
     TrueI, conjunct1, conjunct2, mp
*)

lemma prop_a:
  "(\<not>B \<longrightarrow> A) = (A \<or> B)"
  oops

lemma prop_b:
  "(A \<longrightarrow> B \<longrightarrow> C) = (B \<longrightarrow> A \<longrightarrow> C)"
  oops

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

lemma prop_d:
  "((A \<or> B) \<and> C) = (A \<and> C \<or> C \<and> B)"
  oops

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

lemma prop_f:
  "\<not> \<not> P \<Longrightarrow> P"
  oops

lemma prop_g:
  "(\<not>A \<and> (B \<longrightarrow> C)) = (A \<or> B \<longrightarrow> \<not>A \<and> C)"
  oops


section "Q4: Higher-Order Logic (34 marks)"

(*
You must only these proof methods:
  - rule, erule, assumption, frule, drule,
    rule_tac, erule_tac, frule_tac, drule_tac, rename_tac, case_tac
You must use only these proof rules:
  -  impI, impE, conjI, conjE, disjI1, disjI2, disjE, notI, notE,
     iffI, iffE, iffD1, iffD2, ccontr, classical, FalseE, TrueI,
     allI, allE, exI, and exE
*)

lemma hol_a:
  "((\<forall>x. P x) \<and> (\<forall>x. Q x)) = (\<forall>x. Q x \<and> P x)"
  oops

lemma hol_b:
  "(\<forall>x. P x \<longrightarrow> Q) \<Longrightarrow> (\<exists>x. P x) \<longrightarrow> Q"
  oops

lemma hol_c:
  "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> P x)"
  oops

lemma hol_d:
  "(\<forall>a. P a a) \<longrightarrow> \<not>(\<forall>a b. P b a \<longrightarrow> \<not>P a b)"
  oops

lemma hol_e:
  "(\<forall>P x. P x) = False"
  oops

lemma hol_f:
  "\<forall>P h. (\<forall>x. \<not>P x \<longrightarrow> P (h x)) \<longrightarrow> (\<exists>x. P x \<and> P (h (h x)))"
  oops

end