Default case for non-exhaustive primrec definitions?

[Elliot Bobrow]

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/20250720/7c829f41/attachment.htm>