theory s1 imports Main begin text \ Question 1 \ text \ Let \' = \, [x::Tx, y::Ty, z::'a] and Tx = 'a \ 'b \ 'c, Ty = 'd \ 'b, \1 \2 --------------------------------------------------------App \' \ x z (y (f z)) :: 'c ------------------------------------------------------- Abs \, [x::Tx, y::Ty] \ \z. x z (y (f z)) :: 'a \ 'c ------------------------------------------------------- Abs \, [x::Tx] \ \y z. x z (y (f z)) :: Ty \ 'a \ 'c ------------------------------------------------------- Abs \ \ \x y z. x z (y (f z)) :: ('a \ 'b \ 'c) \ ('d \ 'b) \ 'a \ 'c where \1 is the following subtree: ---------------Var ------------Var \' \ x :: Tx \' \ z :: 'a -------------------------------------App \' \ x z :: 'b \ 'c and \2 is the following subtree: [*] --------------------Var --------------Var \' \ f :: 'a \ 'd \' \ z :: 'a -------------Var -----------------------------------------App \' \ y :: Ty \' \ f z :: 'd ----------------------------------------------------App \' \ y (f z) :: 'b [*]: assuming \(f) = 'a \ 'd Therefore the term \x y z. x z (y (f z)) is type correct with type ('a \ 'b \ 'c) \ ('d \ 'b) \ 'a \ 'c in contexts where f has type 'a \ 'd. This is also a most general type for this term. \ context notes [[show_types]] begin term "\x y z. x z (y (f z))" end text \ Question 2 (a) \ text \ add 2 x = (\m n. \f x. m f (n f x)) (\f x. f (f x)) x \\ ----------------------------------------- (\n. \f x. (\f x. f (f x)) f (n f x)) x \\ --------------------------------------- \f y. (\f x. f (f x)) f (x f y) \\ ----------------- \f y. (\x. f (f x)) (x f y) \\ --------------------- \f y. f (f (x f y)) add x 2 = (\m n. \f x. m f (n f x)) x (\f x. f (f x)) \\ --------------------------- (\n. \f y. x f (n f y)) (\f x. f (f x)) \\ --------------------------------------- \f y. x f ((\f x. f (f x)) f y) \\ ----------------- \f y. x f ((\x. f (f x)) y) \\ ----------------- \f y. x f (f (f y)) \ text \ Question 2 (b) \ text \ The two normal forms for @{text "add 2 x"} and @{text "add x 2"} are not equal. This means that @{text "add 2 x"} is not \ convertible into @{text "add x 2"} for all x. For instance, for @{text "x = \f x. f"}, @{text "add 2 x"} reduces to @{text "\f x. f (f f)"}, and @{text "add x 2"} reduces to @{text "\f x. f"}. If x is of the form @{text "\f x. f^n x"}, i.e. is a Church Numeral, both terms will \-reduce to terms of the form @{text "\f x. f^(n+2) x"}, and therefore @{text "add 2 x"} and @{text "add x 2"} are equivalent under \ conversion for such x. \ text \ Question 3 \ lemma prop_a: "(\B \ A) = (A \ B)" apply (rule iffI) apply (cases B) apply (rule disjI2, assumption) apply (erule (1) impE) apply (rule disjI1, assumption) apply (rule impI) apply (erule disjE) apply assumption apply (erule (1) notE) done lemma prop_b: "(A \ B \ C) = (B \ A \ C)" apply (rule iffI) apply (rule impI) apply (rule impI) apply (erule (1) impE) apply (erule (2) impE) apply (rule impI) apply (rule impI) apply (erule (1) impE) apply (erule (2) impE) done lemma prop_c: "(P \ Q) = (\Q \ \P)" apply (rule iffI) apply (rule impI) apply (rule notI) apply (erule (1) impE) apply (erule (1) notE) apply (rule impI) apply (rule ccontr) apply (erule (1) impE) apply (erule (1) notE) done lemma prop_d: "((A \ B) \ C) = (A \ C \ C \ B)" apply (rule iffI) apply (erule conjE) apply (erule disjE) apply (rule disjI1) apply (rule conjI, assumption, assumption) apply (rule disjI2) apply (rule conjI, assumption, assumption) apply (rule conjI) apply (erule disjE) apply (erule conjE) apply (rule disjI1, assumption) apply (erule conjE) apply (rule disjI2, assumption) apply (erule disjE) apply (erule conjE, assumption) apply (erule conjE, assumption) done lemma prop_e: "((P \ (((Q \ R) \ Q) \ Q)) \ P) \ P" apply (rule impI) apply (rule classical) apply (erule impE) apply (rule impI) apply (erule (1) notE) apply (erule (1) notE) done lemma prop_f: "\ \ P \ P" apply (rule classical) apply (erule notE) apply assumption done lemma prop_g: "(\A \ (B \ C)) = (A \ B \ \A \ C)" apply (rule iffI) apply (rule impI) apply (erule conjE) apply (rule conjI, assumption) apply (erule disjE) apply (erule (1) notE) apply (erule (2) impE) apply (rule conjI) apply (rule notI) apply (erule impE) apply (rule disjI1, assumption) apply (erule conjE) apply (erule (1) notE) apply (rule impI) apply (erule impE) apply (rule disjI2, assumption) apply (erule conjE) apply (assumption) done text \ Question 4 \ lemma hol_a: "((\x. P x) \ (\x. Q x)) = (\x. Q x \ P x)" apply (rule iffI) apply (erule conjE) apply (rule allI) apply (rule conjI) apply (erule_tac P=Q in allE, assumption) apply (erule_tac P=P in allE, assumption) apply (rule conjI) apply (rule allI) apply (erule allE) apply (erule (1) conjE) apply (rule allI) apply (erule allE) apply (erule (1) conjE) done lemma hol_b: "(\x. P x \ Q) \ (\x. P x) \ Q" apply (rule impI) apply (erule exE) apply (erule allE, erule (1) impE) apply assumption done lemma hol_c: "(\ (\ x. P x)) = (\ x. \ P x)" apply (rule iffI) apply (rule classical) apply (erule notE) apply (rule allI) apply (rule classical) apply (erule notE) apply (rule exI) apply assumption apply (erule exE) apply (rule notI) apply (erule allE) apply (erule notE) apply assumption done lemma hol_d: "(\a. P a a) \ \(\a b. P b a \ \P a b)" apply (rule impI) apply (rule notI) apply (erule allE) apply (erule allE) apply (erule allE) apply (erule (1) impE) apply (erule (1) notE) done lemma hol_e: "(\P x. P x) = False" apply (rule iffI) apply (erule_tac x="\x. False" in allE) apply (erule (1) allE) apply (erule FalseE) done lemma hol_f: "\P h. (\x. \P x \ P (h x)) \ (\x. P x \ P (h (h x)))" apply (rule allI) apply (rule allI) apply (rule impI) apply (case_tac "\x. P x") apply (erule exE) apply (case_tac "P (h x)") apply (case_tac "P (h (h x))") apply (rule exI, erule (1) conjI) apply (erule allE) apply (erule (1) impE) apply (rule exI, erule (1) conjI) apply (erule allE) apply (erule (1) impE) apply (rule exI, erule (1) conjI) apply (erule notE) apply (case_tac "P x") apply (rule exI, assumption) apply (erule allE) apply (erule (1) impE) apply (rule exI, assumption) done end