Default case for non-exhaustive primrec definitions?

[Dmitriy Traytel]

Hi Elliot,

For your simplified example the property actually holds:

primrec (nonexhaustive) f'' :: "'a option \<Rightarrow> nat" where "f'' (Some _) = 0"
lemma "f'' None = undefined"
  unfolding f''_def by simp

This is not exported to the user on purpose, but still available.

With nth it is more subtle because of the extra argument. Primrec choses to let the unspecified value depend on the additional parameter (therefore "[] ! 42 = [] ! 43” will not be provable as “[] ! 42 = undefined 42” and “[] ! 43 = undefined 43” unless the element type is a singleton).

lemma "nth [] n = undefined n"
  unfolding nth_def by simp

The “fun” command indeed makes a different choice (which would make "[] ! 42 = [] ! 43” and "[] ! 42 = undefined" true, if nth was defined using fun).

I think it depends on the application which choice is good or bad (the latter gives you “accidental" equalities such as "[] ! 42 = [] ! 43” or “hd [] = [] ! 43” which may raise some questions about your model but might eliminate some side conditions from lemmas). If you don’t like a particular choice you can always wrap the function in question to correct it.

Best wishes,
Dmitriy

On 20 Jul 2025, at 18.45, Elliot Bobrow <ebobrow at g.hmc.edu> wrote:

Hello Isabelle developers,

I've noticed that Isabelle's logic for `case` statements and `fun` definitions automatically defaults to returning `undefined` for unspecified inputs:

```isabelle
fun f :: "'a option \<Rightarrow> nat" where "f x = (case x of Some _ \<Rightarrow> 1)"
lemma "f None = undefined" by simp

fun f' :: "'a option \<Rightarrow> nat" where "f' (Some _) = 1"
lemma "f' None = undefined" by (meson f'.elims option.distinct(1))
```

However, the same does not hold for `primrec` definitions:

```isabelle
primrec (nonexhaustive) f'' :: "'a option \<Rightarrow> nat" where "f'' (Some _) = 0"
lemma "f'' None = undefined" oops
```

Is there a reason for this? It seems it would be good to be consistent here, and the functions would still be primitive recursive. Having `undefined` as a default case seems like a good idea for the sake of clarity and explicitness.

This has come up in a research project (collaborators CC'd) which involves proving a number of functions primitive recursive according to a user-defined predicate. We are doing this by constructing equivalent functions out of known primitive recursive functions and proving them equivalent on all inputs. However, it is impossible to do this for e.g. `nth` because an equivalent function must always return `[] ! n` for out-of-bounds inputs. This is a function of n and we do not know it to be primitive recursive, so we're stuck. If instead we had that `[] ! n` evaluates to undefined, the problem becomes trivial by returning the constant `undefined` on out-of-bounds inputs, which we know to be primitive recursive because it is a constant. This might not be the only instance where the current behavior makes it more difficult/impossible to reason about equality.

Elliot

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20250811/4e1f9f8a/attachment.htm>