Defining functions in Isabelle [isa-001O]

The fun command can be used to define functions in Isabelle. Unlike definitions, functions can be defined by multiple pattern-matching equations, they may be recursive, and their equations are automatically added to the simpset.

ExampleFibonacci as a fun

fun fib :: "nat ⇒ nat" where "fib 0 = 0" | "fib (Suc 0) = Suc 0" | "fib (Suc (Suc n)) = fib n + fib (Suc n)" print_theorems

The print_theorems command allows us to see all of the lemmas generated by this command.

Problem.

  • December 3, 2025

Isabelle functions must provably terminate. The problem with non-terminating functions can be illustrated by a definition like:

fun bad :: "nat ⇒ bool" where "bad x = ¬ (bad x)"

If such a non-terminating definition were allowed, this would render our logic inconsistent (as bad x is equal to its own negation). Therefore, Isabelle requires that all functions be accompanied by a proof of termination.

The fun command attempts to prove termination automatically. If it does not succeed, it will give an error message and fail to define the function. Manual proofs of termination can be supplied if the function command is used instead, but the function command is beyond the scope of this course.

In cases where the recursion and pattern matching follows exactly the structure of the datatype in one argument, primrec can be used instead of fun, which is a bit more efficient:

ExampleFactorial as a primrec [isa-001R]

primrec factorial :: "nat ⇒ nat" where "factorial 0 = Suc 0" | "factorial (Suc n) = Suc n * factorial n" print_theorems

Context

    Lecture. Definitions, Datatypes, Induction, Functions [isa-001B]

    Related

      Proof Method. simp [isa-001H]

      Isabelle definitions [isa-001G]