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

section {* Lambda Calculus *}

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"}
  which perform addition,
  multiplication and exponentiation, respectively, of Church numerals
  in Isabelle.
*}

definition
  add :: "_" where "add m n = (\<lambda>f x. n f (m f x))"
definition
  mult :: "_" where "mult m n = (\<lambda>f x. n (m f) x)"
definition
  exp :: "_" where "exp m n = (\<lambda>f x. n m f x)"

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

lemma five: "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 (rule refl)
  done

text {*
  The value @{thm_style rhs five} is computed for @{text "?x"}.
*}

lemma six: "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 {*
  The value @{thm_style rhs six} is computed for @{text "?x"}.
*}

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

lemma ten: "add (\<lambda>f x. f (f x))
           (mult (\<lambda>f x. f (f x))
                 (add (\<lambda>f x. f (f (f x)))
                      (\<lambda>f x. f x))) = ?x"
  by (simp add: add_def mult_def)

text {*
  The value @{thm_style rhs ten} is computed for $2 + 2 \cdot (3 + 1)$.
*}

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

lemma "exp (\<lambda>f x. f (f x)) (\<lambda>f x. f (f (f x))) =
       mult (\<lambda>f x. f (f x)) (mult (\<lambda>f x. f (f x))(\<lambda>f x. f (f x)))"
  by (simp add: mult_def exp_def)

(*<*)
end
(*>*)