theory Exercise03 imports Main begin section {* Simply-Typed Lambda Calculus *} subsection {* Higher-Order Unification *} text {* $\rhd$ Are the following pairs of $\lambda$-terms higher-order unifiable? Give a unifying substitution if one exists. \begin{itemize} \item[(a)] $?\!f \, x$ and $x$ \item[(b)] $f \, ?\!x$ and $g \, ?\!y$ \item[(c)] $?\!x \, a$ and $f \, (?\!x \, a)$ \end{itemize} *} text {* $\rhd$ What are the unifying substitutions for $\lambda x. \, ?\!n \, (\lambda y. \, y) \, x$ and $\lambda x. \, x$? (You do not need to prove your answer.) *} section {* Natural Deduction *} subsection {* Propositional Logic *} text {* \label{subsection:propositional-logic} *} text {* We will use the calculus of natural deduction to prove some lemmas of propositional logic in Isabelle. \begin{itemize} \item Only use these rules in the proofs: \quad @{text "notI:"}~@{thm notI[of A,no_vars]},\\[-12pt] \quad @{text "notE:"}~@{thm notE[of A B,no_vars]},\\[-12pt] \quad @{text "conjI:"}~@{thm conjI[of A B,no_vars]},\\[-12pt] \quad @{text "conjE:"}~@{thm conjE[of A B C,no_vars]},\\[-12pt] \quad @{text "disjI1:"}~@{thm disjI1[of A B,no_vars]},\\[-12pt] \quad @{text "disjI2:"}~@{thm disjI2[of A B,no_vars]},\\[-12pt] \quad @{text "disjE:"}~@{thm disjE[of A B C,no_vars]},\\[-12pt] \quad @{text "impI:"}~@{thm impI[of A B,no_vars]},\\[-12pt] \quad @{text "impE:"}~@{thm impE[of A B C,no_vars]},\\[-12pt] \quad @{text "mp:"}~@{thm mp[of A B,no_vars]},\\[-12pt] \quad @{text "iffI:"}~@{thm iffI[of A B,no_vars]}, \\[-12pt] \quad @{text "iffE:"}~@{thm iffE[of A B C,no_vars]}\\[-12pt] \item Only use the methods @{text "(rule"}~$r$@{text ")"}, @{text "(erule"}~$r$@{text ")"} and @{text "assumption"}, where $r$ is one of the rules given above. \end{itemize} *} text {* $\rhd$ Prove the following lemmas in Isabelle. \medskip *} lemma "((A \ B) \ C) \ A \ (B \ C)" oops lemma "(A \ A) = (A \ A)" oops lemma S: "(A \ B \ C) \ (A \ B) \ A \ C" oops lemma "(A \ (B \ C)) \ (B \ \ C) \ \ A" oops lemma "(D \ A) \ (A \ (B \ C)) \ (B \ \ C) \ \ D" oops lemma "(A \ \ B) = (B \ \ A)" oops subsection {* Knights and Knaves *} text {* \begin{quote} There is an island whose inhabitants are split into two groups: knights, who always tell the truth, and knaves, who always lie. Three of the island's inhabitants~-- $A$, $B$, and $C$~-- were talking together. $A$ said, All of us are knaves.'' Then $B$ remarked, Exactly one of us is a knight.'' \end{quote} $\rhd$ What are $A$, $B$, and $C$? *} text {* $\rhd$ Formalize the puzzle in Isabelle. Prove your solution. In addition to the rules and methods from Exercise~\ref{subsection:propositional-logic}, you may use @{text "(case_tac "}~$P$@{text ")"} (where $P$ is a Boolean expression, e.g.\ a variable) for case distinctions, and @{text "back"} to select a different unifier when applying a method. *} subsection {* Predicate Logic *} text {* We are again talking about proofs in the calculus of Natural Deduction. In addition to the theorems given in the exercise Propositional Logic'', you may now also use @{text "exI:"}~@{thm exI[no_vars]}\\ @{text "exE:"}~@{thm exE[no_vars]}\\ @{text "allI:"}~@{thm allI[no_vars]}\\ @{text "allE:"}~@{thm allE[no_vars]}\\ $\rhd$ Give a proof of the following propositions or an argument why the formula is not valid: *} lemma "(\x. \y. P x y) \ (\y. \x. P x y)" oops lemma "(\x. P x \ Q) = ((\x. P x) \ Q)" oops lemma "((\ x. P x) \ (\ x. Q x)) = (\ x. (P x \ Q x))" oops lemma "((\ x. P x) \ (\ x. Q x)) = (\ x. (P x \ Q x))" oops lemma "((\ x. P x) \ (\ x. Q x)) = (\ x. (P x \ Q x))" oops lemma "(\x. \y. P x y) \ (\y. \x. P x y)" oops lemma "(\ (\ x. P x)) = (\ x. \ P x)" oops section {* Hilbert's Choice *} text {* Only use the methods @{term rule}, @{term rule_tac}, @{term erule}, @{term erule_tac}, and @{term assumption} in this exercise. Furthermore, you may only use the same theorems as in the previous exercise, Predicate Logic'', as well as @{text "someI:"}~@{thm someI[no_vars]} $\rhd$ Use Hilbert's epsilon operator to prove the Axiom of Choice. *} lemma "\x. \y. Q x y \ \f. \x. Q x (f x)" oops section {* A Riddle: Rich Grandfather *} text {* $\rhd$ First prove the following formula, which is valid in classical predicate logic, informally with pen and paper. Use case distinctions and/or proof by contradiction. {\it If every poor man has a rich father,\\ then there is a rich man who has a rich grandfather.} *} theorem "\x. \ rich x \ rich (father x) \ \x. rich (father (father x)) \ rich x" oops text {* $\rhd$ Now prove the formula in Isabelle using a sequence of rule applications (i.e.\ only using the methods @{term rule}, @{term erule} and @{term assumption}). In addition to the theorems that were allowed in the exercise Predicate Logic'', you may now also use @{text "classical:"}~@{thm classical[no_vars]}\\ *} theorem "\x. \ rich x \ rich (father x) \ \x. rich (father (father x)) \ rich x" oops end