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

section {* Type Inference *}

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

text {*
  No.  The only applicable typing rule is that for abstraction:
  $$\frac{\Gamma[x \mapsto \tau_1] \vdash x \, x :: \tau_2}
    {\Gamma \vdash \lambda x. \, x \, x :: \tau_1 \Rightarrow \tau_2}.$$
  Next, the only applicable typing rule is that for application:
  $$\frac{\Gamma[x \mapsto \tau_1] \vdash x :: \sigma \Rightarrow \tau_2 \qquad \Gamma[x \mapsto \tau_1] \vdash x :: \sigma}
    {\Gamma[x \mapsto \tau_1] \vdash x \, x :: \tau_2}.$$
  Next, the only applicable typing rule (on both sides) is that for variables.
  This rule is only applicable on both sides however if $\Gamma[x \mapsto
  \tau_1](x) = \sigma \Rightarrow \tau_2$ \emph{and} $\Gamma[x \mapsto
  \tau_1](x) = \sigma$, i.e.\ $\sigma \, = \, \sigma \Rightarrow \tau_2$ for
  some types $\sigma$ and $\tau_2$, which is clearly not possible.
*}

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)"
  apply (rule impI)
  apply (erule disjE)
   apply (erule disjE)
    apply (rule disjI1)
    apply assumption
   apply (rule disjI2)
   apply (rule disjI1)
   apply assumption
  apply (rule disjI2)
  apply (rule disjI2)
  apply assumption
  done

lemma "(A \<or> A) = (A \<and> A)"
  apply (rule iffI)
   apply (erule disjE)
    apply (rule conjI)
     apply assumption
    apply assumption
   apply (rule conjI)
    apply assumption
   apply assumption
  apply (erule conjE)
  apply (rule disjI1)
  apply assumption
  done

lemma "(D \<longrightarrow> A) \<longrightarrow> (A \<longrightarrow> (B \<and> C)) \<longrightarrow> (B \<longrightarrow> \<not> C) \<longrightarrow> \<not> D"
  apply (rule impI)+  (* multiple applications until methods fails *)
  apply (rule notI)
  apply (erule impE)
   apply assumption
  apply (erule impE)
   apply assumption
  apply (erule conjE)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done

lemma "(A \<longrightarrow> \<not> B) = (B \<longrightarrow> \<not> A)"
  apply (rule iffI)
   apply (rule impI)
   apply (rule notI)
   apply (erule impE)
    apply assumption
   apply (erule notE)
   apply assumption
  apply (rule impI)
  apply (rule notI)
  apply (erule impE)
   apply assumption
  apply (erule notE)
  apply assumption
  done


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 {*
  A proof by case distinction works as follows.  Suppose @{term A}.
  Then the proposition holds, because this is the consequent of the
  the outermost implication.

  Otherwise, if we suppose @{term B} the proposition evaluates to
  true, and likewise if we suppose @{term "\<not>B"}.
*}

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

lemma Pierce: "((A \<longrightarrow> B) \<longrightarrow> A) \<longrightarrow> A"
  apply (case_tac "A")
   apply (rule impI)
   apply assumption
  -- {* case @{term "\<not>A"} *}
  apply (case_tac "B")
   apply (rule impI)
   apply (erule impE)
    apply (rule impI)
    apply assumption
   apply assumption
  -- {* case @{text "\<not>A; \<not>B"} *}
  apply (rule impI)
  apply (erule impE)
   apply (rule impI)
   apply (erule notE)
   apply assumption
  apply assumption
  done
  

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)"
  apply (rule impI)
  apply (rule allI)
  apply (erule exE)
  apply (rule exI)
  apply (erule allE)
  apply assumption
  done

lemma "(\<forall>x. P x \<longrightarrow> Q) = ((\<exists>x. P x) \<longrightarrow> 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

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

text {*
  A possible counterexample is: @{text "P = even"}, @{text "Q = odd"},
  interpreted over the natural numbers.
*}


lemma "((\<exists> x. P x) \<or> (\<exists> x. Q x)) = (\<exists> x. (P x \<or> Q x))"
  apply (rule iffI)
   apply (erule disjE)
    apply (erule exE)
    apply (rule exI)
    apply (rule disjI1)
    apply assumption
   apply (erule exE)
   apply (rule exI)
   apply (rule disjI2)
   apply assumption
  apply (erule exE)
  apply (erule disjE)
   apply (rule disjI1)
   apply (rule exI)
   apply assumption
  apply (rule disjI2)
  apply (rule exI)
  apply assumption
  done

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)"
  apply (rule iffI)
   apply (rule classical)
   apply (erule notE)
   apply (rule allI)
   apply (rule classical)
   apply (erule notE)
   apply (rule exI)
   apply assumption
  apply (erule exE)
  apply (rule notI)
  apply (erule allE)
  apply (erule notE)
  apply assumption
  done


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 {*
\begin{tabbing}
{\bf Proof} \\
(1)\ \= We first show: @{term "\<exists>x. rich x"}. \\
Proof by contradiction. \\
    \> {\bf Assume} \=  @{term "\<not> (\<exists>x. rich x)"}. \\
    \>               \> Then @{term "\<forall>x. \<not> rich x"}. \\
    \>               \> We consider an arbitrary @{term "y"} with
                          @{term "\<not> rich y"}. \\
    \>               \> Then @{term "rich (father y)"}. \\
(2) \> Now we show the theorem. \\
Proof by cases. \\
    \> {\bf Case 1:} \> @{term "rich (father (father x))"}. \\
    \>               \> The rich man who has a rich grandfather is @{term x}.  We are done. \\ 
    \> {\bf Case 2:} \> @{term "\<not> rich (father (father x))"}. \\  
    \>               \> Then @{term "rich (father (father (father x)))"}. \\
    \>               \> Also @{term "rich (father x)"}, \\
    \>               \> because otherwise @{term "rich (father (father x))"}. \\
    \>               \> The rich man who has a rich grandfather is @{term "father x"}. \\
{\bf qed} \\
\end{tabbing}
*}

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


text {* Since we are not allowed to use lemmas, (1) will show up as
  two copies of the same proof script in the proof. *}

theorem
  "\<forall>x. \<not> rich x \<longrightarrow> rich (father x) \<Longrightarrow>
  \<exists>x. rich (father (father x)) \<and> rich x"
  apply (rule classical)
  apply (rule exI)
  apply (rule conjI)

 -- {* Show @{term "rich (father (father x2))"} *}
    apply (rule classical)
 -- {* Assume @{term "\<not> rich (father (father x2))"}, case 2 *}
    apply (rule allE) apply assumption
    -- {* use @{text rule} rather then @{text erule} in order not to
      delete the assumption, it is needed a second time *}
    apply (erule impE) apply assumption
 -- {* Now we have @{term "rich (father (father (father x2)))"} *}
    apply (erule notE)
 -- {* Show @{term "\<exists>x. rich (father (father x)) \<and> rich x"} *}
    apply (rule exI)
    apply (rule conjI) apply assumption
 -- {* Show @{term "rich (father x2)"} *}
    apply (rule classical)
    apply (erule allE)
    apply (erule notE)
    apply (erule impE) apply assumption
    apply assumption

 -- {* Show @{term "rich x2"} *}
  apply (rule classical)
 -- {* Assume @{term "\<not> rich x2"}, case 1 *}
  apply (rule allE) apply assumption
  apply (erule impE) apply assumption
 -- {* Now we have @{term "rich (father x2)"} *}
  apply (erule notE)
 -- {* Show @{term "\<exists>x. rich (father (father x)) \<and> rich x"} *}
  apply (rule exI)
  apply (rule conjI) apply assumption
 -- {* Show @{term "rich x41"} *}
  apply (rule classical)
  apply (erule allE)
  apply (erule notE)
  apply (erule impE) apply assumption
  apply assumption
  done

(*<*)
end
(*>*)