theory a1 imports Main begin section "Q1: Types (12 marks)" (* provide your answers here or in an separate PDF file *) section "Q2: @text \-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: "(\B \ A) = (A \ B)" oops lemma prop_b: "(A \ B \ C) = (B \ A \ C)" oops lemma prop_c: "(P \ Q) = (\Q \ \P)" oops lemma prop_d: "((A \ B) \ C) = (A \ C \ C \ B)" oops lemma prop_e: "((P \ (((Q \ R) \ Q) \ Q)) \ P) \ P" oops lemma prop_f: "\ \ P \ P" oops lemma prop_g: "(\A \ (B \ C)) = (A \ B \ \A \ 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: "((\x. P x) \ (\x. Q x)) = (\x. Q x \ P x)" oops lemma hol_b: "(\x. P x \ Q) \ (\x. P x) \ Q" oops lemma hol_c: "(\ (\ x. P x)) = (\ x. \ P x)" oops lemma hol_d: "(\a. P a a) \ \(\a b. P b a \ \P a b)" oops lemma hol_e: "(\P x. P x) = False" oops lemma hol_f: "\P h. (\x. \P x \ P (h x)) \ (\x. P x \ P (h (h x)))" oops end