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 \<or> B) \<or> C) \<longrightarrow> A \<or> (B \<or> C)"  oops

lemma "(A \<or> A) = (A \<and> A)" oops

lemma S: "(A \<longrightarrow> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> B) \<longrightarrow> A \<longrightarrow> C" oops

lemma "(A \<longrightarrow> (B \<and> C)) \<longrightarrow> (B \<longrightarrow> \<not> C) \<longrightarrow> \<not> A" oops

lemma "(D \<longrightarrow> A) \<longrightarrow> (A \<longrightarrow> (B \<and> C)) \<longrightarrow> (B \<longrightarrow> \<not> C) \<longrightarrow> \<not> D" oops

lemma "(A \<longrightarrow> \<not> B) = (B \<longrightarrow> \<not> 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 "(\<exists>x. \<forall>y. P x y) \<longrightarrow> (\<forall>y. \<exists>x. P x y)"  oops

lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> Q)"  oops

lemma "((\<forall> x. P x) \<and> (\<forall> x. Q x)) = (\<forall> x. (P x \<and> Q x))"  oops

lemma "((\<forall> x. P x) \<or> (\<forall> x. Q x)) = (\<forall> x. (P x \<or> Q x))"  oops

lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"  oops

lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>y. \<forall>x. P x y)"  oops

lemma "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> 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 "\<forall>x. \<exists>y. Q x y \<Longrightarrow> \<exists>f. \<forall>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
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow>
  \<exists>x. rich (father (father x)) \<and> 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
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow>
  \<exists>x. rich (father (father x)) \<and> rich x"
  oops


end