A short note about Joachim Breitner’s post on the totality of Isabelle functions which says:

For example, no Isabelle command allows you define a function bogus :: () ⇒ nat with the equation bogus () = Suc (bogus ()), because this equation does not have a solution.

In fact, the following is completely legitimate:

function bogus :: "unit ⇒ nat" where "bogus () = Suc (bogus ())"
  by pat_completeness auto

function lets you define a function and defer the termination proof until later. Until termination is proved, all the generated facts about the function have an extra precondition involving a predicate bogus_dom that restricts the fact to elements of the domain of the function:

Scratch.bogus.psimps: bogus_dom () ⟹ bogus () = Suc (bogus ())
Scratch.bogus.pinduct: bogus_dom ?a0.0 ⟹ (bogus_dom () ⟹ ?P () ⟹ ?P ()) ⟹ ?P ?a0.0
Scratch.bogus.pelims: bogus ?x = ?y ⟹ bogus_dom ?x ⟹ (?x = () ⟹ ?y = Suc (bogus ()) ⟹ bogus_dom () ⟹ ?P) ⟹ ?P

This allows you to work with the partial definition of the function in a somewhat natural way. It’s a bit of a pain, but it is less painful than completely forbidding the partial definition. At some point you can try and turn these facts into the following total facts using a termination proof:

Scratch.bogus.simps: bogus () = Suc (bogus ())
Scratch.bogus.elims: bogus ?x = ?y ⟹ (?x = () ⟹ ?y = Suc (bogus ()) ⟹ ?P) ⟹ ?P

The termination proof of course is impossible here:

termination bogus proof (intro allI)

> proof (prove)
> goal (1 subgoal):
>  1. ⋀x. bogus_dom x

In other words we must show that every element is in the domain of the function, which is false. Perhaps interestingly it’s false more because bogus () is defined in terms of itself, rather than because there is no value n :: nat satisfying n = Suc n: the termination proof provides a local introduction lemma:

local.termination: wf ?R ⟹ ((), ()) ∈ ?R ⟹ All bogus_dom

This tells us that in order to show termination we need to find a wellfounded relation that relates each equation in the function’s definition to the values on which it depends, and any relation that includes ((), ()) is clearly not wellfounded.

Technically, bogus is indeed a total function of type unit ⇒ nat, but until we know anything about its domain its values are completely arbitrary. This means that theorems like

lemma "bogus () ≥ 0" by auto

are true, simply because that’s true of any natural number, and bogus () is some natural number, even if we don’t know which one. In some contexts, the difference is important, but as a working user of Isabelle the difference doesn’t matter too much.