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

section {* Lambda Calculus *}

subsection {* $\alpha$-Conversion *}

text {*
  $\rhd$ Which of the following $\lambda$-terms (if any) are $\alpha$-equivalent?

  \begin{tabular}{ll}
  (a) $\lambda x \, y. \, y \, x$ & \hspace{.8cm} (e) $\lambda x. \, y \, x$ \\
  (b) $\lambda x \, y. \, x \, y$ & \hspace{.8cm} (f) $\lambda x. \, x \, y$ \\
  (c) $\lambda y \, x. \, y \, x$ & \hspace{.8cm} (g) $\lambda y. \, y \, x$ \\
  (d) $\lambda y \, x. \, x \, y$ & \hspace{.8cm} (h) $\lambda y. \, x \, y$
  \end{tabular}
*}

subsection {* $\beta$-Reduction *}

text {*
  $\rhd$ $\beta$-reduce the following $\lambda$-terms to their normal
  form.  How many derivations of the normal form exist?

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

subsection {* Church Numerals *}

text {*
  \label{subsection:church-numerals}

  Recall the encoding of natural numbers as $\lambda$-terms via \emph{Church
  numerals}:
  $$n \equiv \lambda f \, x. \, f^n x$$

  $\rhd$ Define a function $\mathrm{mult} \equiv \lambda m \, n. \, \ldots$
  as a $\lambda$-term such that $\mathrm{mult} \, m \, n$ encodes $m \cdot n$,
  i.e.\ multiplication of Church numerals.

  $\rhd$ Define a function $\mathrm{exp} \equiv \lambda m \, n. \, \ldots$
  as a $\lambda$-term such that $\mathrm{exp} \, m \, n$ encodes $m \mathop{\verb.^.} n$,
  i.e.\ exponentiation of Church numerals.
*}

subsection {* $\alpha \beta \eta$-Equivalence in Isabelle *}

text {*
  Equality in Isabelle is (usually) modulo $\alpha \beta \eta$-equivalence.
  Therefore the theorem \texttt{refl}:
  @{thm refl [no_vars]} is sufficient to prove the following lemmas:
*}

lemma alpha: "(\<lambda>x. x) = (\<lambda>y. y)"
  by (rule refl)

lemma beta: "(\<lambda>f. f x) f = f x"
  by (rule refl)

lemma eta: "(\<lambda>x. f x) = f"
  by (rule refl)

text {*
  $\rhd$ Prove these lemmas in Isabelle.  What happens wrt.\
  $\alpha \beta \eta$-equivalence?
*}

subsection {* Church Numerals in Isabelle *}

text {*
  In this exercise we will use Isabelle to perform computations with Church
  numerals.  Isabelle's \emph{simplifier}, which is invoked on a proof state by
  @{text "simp"}, performs term rewriting.  @{text "unfolding"} can be used to
  unfold definitions.

  $\rhd$ Make yourself familiar with the @{text "definition"} command
  (Section~4.1.1 of the Isabelle/Isar Reference manual).  Use it to
  define the functions @{term "add"}, @{term "mult"} and @{term "exp"} (cf.\ 
  Exercise~\ref{subsection:church-numerals}) which perform addition,
  multiplication and exponentiation, respectively, of Church numerals
  in Isabelle.
*}

(*<*)
definition
  add :: "'dummy" where "add = arbitrary"
definition
  mult :: "'dummy" where "mult = arbitrary"
definition
  exp :: "'dummy" where "exp = arbitrary"
(*>*)

text {*
  $\rhd$ Prove the following lemmas.  Which values are computed for
  @{text "?x"}?
*}

lemma "add (\<lambda>f x. f (f x)) (\<lambda>f x. f (f (f x))) = ?x"
  unfolding add_def  -- {* we can unfold the definition first \dots *}
  apply simp
  done

lemma "mult (\<lambda>f x. f (f x)) (\<lambda>f x. f (f (f x))) = ?x"
  by (simp add: mult_def)  -- {* \dots\ or give it to the simplifier directly *}

text {*
  $\rhd$ Compute $2 + 2 \cdot (3 + 1)$ in a similar fashion.
*}

text {*
  $\rhd$ Show that $2 \mathop{\verb.^.} 3 = 2 \cdot 2 \cdot 2$.
*}

(*<*)
end
(*>*)