theory Solution02 imports Main begin section {* Exercise 1 *} text {* In this exercise, we will prove some lemmas of propositional and predicate logic with the aid of a calculus of natural deduction. For the proofs, you may only use the lemmas @{thm notI}, @{thm notE}, @{thm conjI}, @{thm conjE}, @{thm disjI1}, @{thm disjI2}, @{thm disjE}, @{thm impI}, @{thm impE}, @{thm mp}, @{thm iffI}, @{thm iffE}, @{thm classical}, @{thm allI}, @{thm allE}, @{thm exI}, @{thm exE} and the proof methods rule(_tac), erule(_tac) and assumption. rule(_tac) is used with introduction rules (the name often ends in "I"), while erule(_tac) is used for elimination rules (usually ending in an "E"). The _tac variants can be used when an unknown in the rule needs to be instantiated manually. For example, apply (rule_tac x=a in exI) instantiates the unknown ?x in @{thm exI} with @{term a}. @{term a} can be an arbitrary term. In particular, a can refer to meta-bound variables in the goal. *} lemma I: "A \ A" apply (rule impI) apply assumption done lemma "A \ B \ B \ A" apply (rule impI) apply (erule conjE) apply (rule conjI) apply assumption apply assumption done lemma "(A \ B) \ (A \ B)" apply (rule impI) apply (erule conjE) apply (rule disjI1) apply assumption done lemma "(A \ B) \ (B \ C) \ A \ C" apply (rule impI) apply (rule impI) apply (rule impI) apply (erule impE) apply assumption apply (erule impE) apply assumption apply assumption done lemma "(\x. \y. P x y) \ (\y. \x. P x y)" apply (rule impI) apply (rule allI) apply (erule exE) apply (rule_tac x=x in exI) apply (erule_tac x=y in allE) apply assumption done lemma "(\x. P x \ Q) = ((\x. P x) \ Q)" apply (rule iffI) apply (rule impI) apply (erule exE) apply (erule allE) apply (erule impE) apply assumption apply assumption apply (rule allI) apply (rule impI) apply (erule impE) apply (rule exI) apply assumption apply assumption done section {* Exercise 2 *} text {* For introductory purposes, we define our own list datatype with functions to append and reverse lists. *} datatype 'a mylist = Mynil ("<>") | Mycons 'a "'a mylist" (infixr "##" 65) text {* Define functions @{term myapp} and @{term myrev} to append and reverse @{typ "'a mylist"}s. *} fun myapp :: "'a mylist \ 'a mylist \ 'a mylist" (infixr "@@" 65) where "<> @@ ys = ys" | "(x ## xs) @@ ys = x ## xs @@ ys" fun myrev :: "'a mylist \ 'a mylist" where "myrev <> = <>" | "myrev (x ## xs) = myrev xs @@ x ## <>" text {* Prove that @{term "myapp xs ys"} is the empty list, if and only iff both @{term xs} and @{term ys} are empty *} lemma myapp_Nil_eq_iff: "myapp xs ys = <> \ xs = <> \ ys = <>" apply (cases xs) apply auto done text {* Prove that @{term myapp} distributes over @{term myrev}. You might need to prove additional lemmas. *} lemma myapp_Nil_r: "xs @@ <> = xs" apply (induct xs) apply auto done lemma myapp_assoc: "(xs @@ ys) @@ zs = xs @@ ys @@ zs" apply (induct xs) apply auto done lemma myrev_app: "myrev (xs @@ ys) = myrev ys @@ myrev xs" apply (induct xs) apply auto apply (auto simp: myapp_Nil_r myapp_assoc) done section {* Exercise 3 *} text {* Syntax for sets: The empty set is denoted by @{term "{}"}, membership by @{term "a \ A"} or @{term "a : A"} and union by @{term "A \ B"}. Inserting a single element is denoted by @{term "insert a A"}. *} fun myset :: "'a mylist \ 'a set" where "myset <> = {}" | "myset (x ## xs) = insert x (myset xs)" fun mynth :: "'a mylist \ nat \ 'a" where "mynth (x ## xs) 0 = x" | "mynth (x ## xs) (Suc n) = mynth xs n" fun mylen :: "'a mylist \ nat" where "mylen <> = 0" | "mylen (x ## xs) = Suc (mylen xs)" lemma mynth_in_set: "n < mylen xs \ mynth xs n \ myset xs" apply (induction xs arbitrary: n) apply auto apply (case_tac n) apply auto done end