Search code examples
lambdaisabellelambda-calculushol

Recursion in a lambda expression

Is it possible to write a recursive lambda expression in Isabelle/HOL? If so, how?

For example (a silly one):

fun thing :: "nat ⇒ nat" where
  "thing x = (λx. if x=0 then x else …) x"

so instead of … I'd like to write the λ function applied to x-1.

How would I do this? Thanks in advance.

Solution

  • There is only one case where such things are necessary: when defining a function in a proof. I have done so, but this is far from beginner friendly, because you have to derive the simp rules by hand.

    The solution is to mimic what fun is doing internally and expressing your definition in terms of rec_nat:

    fun thing :: "nat ⇒ nat" where
  "thing x = rec_nat 0 (λ_ x. if x=0 then x else (x-1)) x"

(*simp rules*)
lemma thing_simps[simp]:
  ‹thing 0 = 0›
  ‹thing (Suc n) = thing n - Suc 0›
  unfolding thing_def
  by simp_all

    I cannot recommend doing that unless it is unavoidable...