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