(*<*)
theory Exercise
imports Main
begin
(*>*)

section {* Type Inference *}

text {*
  $\rhd$ Infer most general types for the following $\lambda$-terms.  Give the
  full typing derivations.

  \begin{itemize}
  \item[(a)] $\lambda f \, n. \, f \, n$
  \item[(b)] $\lambda f \, n. \, f \, (f \, n)$
  \item[(c)] $\lambda f \, n. \, f \, (f \, (f \, n))$
  \item[(d)] $(\lambda x. \, x) \, (\lambda x. \, x)$
  \end{itemize}
*}

text {*
  $\rhd$ Is the term $\, \lambda x. \, x \, x \,$ type correct?
  Justify your answer.
*}

section {* Natural Deduction *}

text {*
  We will use the calculus of natural deduction to prove some lemmas of
  propositional and predicate logic in Isabelle.
*}

subsection {* Propositional Logic *}

text {*
  \label{subsection:propositional-logic}
*}

text {*
  \begin{itemize}
  \item Only use these rules in the proofs:

  @{text "notI:"}~@{thm notI[no_vars]} \\
  @{text "notE:"}~@{thm notE[no_vars]} \\
  @{text "conjI:"}~@{thm conjI[no_vars]} \\
  @{text "conjE:"}~@{thm conjE[no_vars]} \\
  @{text "disjI1:"}~@{thm disjI1[no_vars]} \\
  @{text "disjI2:"}~@{thm disjI2[no_vars]} \\
  @{text "disjE:"}~@{thm disjE[no_vars]} \\
  @{text "impI:"}~@{thm impI[no_vars]} \\
  @{text "impE:"}~@{thm impE[no_vars]} \\
  @{text "mp:"}~@{thm mp[no_vars]} \\
  @{text "iffI:"}~@{thm iffI[no_vars]} \\
  @{text "iffE:"}~@{thm iffE[no_vars]}

  \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}

  $\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 "(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 {* Pierce's law *}

text {*
  Prove Pierce's law @{prop "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"}.
*}

text {*
  $\rhd$ First give a paper proof using case distinction and/or
  proof by contradiction.
*}

text {*
  $\rhd$ Now give a proof in Isabelle.  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, @{text "back"}
  to select a different unifier when applying a method, and the
  theorem @{text "classical:"}~@{thm classical[no_vars]}. 
*}


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''
  (Exercises 2), you may now also use

  \begin{quote}
  @{text "exI:"}~@{thm exI[no_vars]}\\
  @{text "exE:"}~@{thm exE[no_vars]}\\
  @{text "allI:"}~@{thm allI[no_vars]}\\
  @{text "allE:"}~@{thm allE[no_vars]}\\
  \end{quote}

  $\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 "((\<exists> x. P x) \<and> (\<exists> x. Q x)) = (\<exists> x. (P x \<and> Q x))"

(*<*)oops(*>*)

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

(*<*)oops(*>*)

text {*
  The following lemma also requires @{text "classical:"}~@{thm
  classical[no_vars]} (or an equivalent theorem) in order to be
  proved.
*}

lemma "(\<not> (\<forall> x. P x)) = (\<exists> x. \<not> P x)"

(*<*)oops(*>*)


subsection {* 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]}.
*}


(*<*)
end
(*>*)