<div dir="ltr">Hello Isabelle developers,<div><br></div><div>I've noticed that Isabelle's logic for `case` statements and `fun` definitions automatically defaults to returning `undefined` for unspecified inputs:</div><div><br></div><div>```isabelle</div><div>fun f :: "'a option \<Rightarrow> nat" where "f x = (case x of Some _ \<Rightarrow> 1)"<br>lemma "f None = undefined" by simp<br><br>fun f' :: "'a option \<Rightarrow> nat" where "f' (Some _) = 1"<br>lemma "f' None = undefined" by (meson f'.elims option.distinct(1))<br></div><div>```</div><div><br></div><div>However, the same does not hold for `primrec` definitions:</div><div><br></div><div>```isabelle</div><div>primrec (nonexhaustive) f'' :: "'a option \<Rightarrow> nat" where "f'' (Some _) = 0"<br>lemma "f'' None = undefined" oops<br></div><div>```</div><div><br></div><div>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.</div><div><br></div><div>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.</div><div><br></div><div>Elliot</div></div>