theory a1
imports Main
begin


section "Q1: \<lambda>-Calculus"

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




section "Q2: Types"

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




section "Q3: Propositional Logic"

(*
You must use only these proof methods:
  - rule, erule, assumption, cases, 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, conjunct1, conjunct2, mp
*)


lemma prop_a: "A \<longrightarrow> \<not>\<not>A"
  (* TODO *)
  oops


lemma prop_b: "\<not>\<not>\<not> A \<longrightarrow> \<not>A"
  (* TODO *)
  oops


lemma prop_c: "\<not>\<not> A \<longrightarrow> A"
  (* TODO *)
  oops


lemma prop_d:  "\<not>(A \<and> B) \<longrightarrow> \<not> A \<or> \<not> B"
  (* TODO *)
  oops


lemma prop_e:  "(A \<longrightarrow> B) \<longrightarrow> (\<not> A \<or> B)"
  (* TODO *)
  oops


lemma prop_f:  "\<not>A\<and>\<not>B \<longleftrightarrow> \<not>(A\<or>B)"
  (* TODO *)
  oops


lemma prop_g: "(A \<longrightarrow> B) \<longrightarrow> (((B \<longrightarrow> C) \<longrightarrow> A) \<longrightarrow> B)"
  (* TODO *)
  oops



section "Q4: Higer-Order Logic"

(*
You must use 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, conjunct1, conjunct2, mp;
   - allI, allE, exI, and exE
*)


lemma hol_a: "(\<exists>x. P x \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P x) \<longrightarrow> Q"
  (* TODO *)
  oops


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


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

lemma hol_d: "(\<forall>x. P x \<and> Q x) \<longrightarrow> (\<forall>x. P x) \<and> (\<forall>x. Q x)"
  (* TODO *)
  oops


lemma hol_e: "(\<exists>x. P x \<or> Q x) \<longrightarrow> (\<exists>x. P x) \<or> (\<exists>x. Q x)"
  (* TODO *)
  oops


lemma hol_f: "(\<forall>x y. A y \<or> B x) \<longrightarrow> (\<forall>x. B x) \<or> (\<forall>y. A y)" 
  (* TODO *)
  oops


end