[isabelle-dev] unhelpful low-level error message from primrec

[Alexander Krauss]

Hi Brian,

> I just noticed this error message from primrec if you write a
> specification that is not primitive recursive. Here is a simplified
> example:
>
> primrec foo :: "nat =>  nat" where
>    "foo 0 = 1" | "foo (Suc n) = foo 0"
>
> *** Extra variables on rhs: "foo"
> *** The error(s) above occurred in definition "foo_def":
> ***   "foo \<equiv>  \<lambda>a. nat_rec 1 (\<lambda>n na. foo 0) a"
> *** At command "primrec"
>
> Apparently, the primrec package gets as far as trying to register the
> non-recursive definition; then the definition command fails, and the
> error is not caught by primrec.

This is a regular source of confusion for newbies, and I want to see 
this improved for a long time. IIRC, the problem is that the primrec 
schema is not so easy to check (in the presence of mutual/nested types 
etc.), and thus the package simply defers that check to the lower level 
layers. Catching the low-level error and assuming that it is due to a 
violation of the primrec schema is not really a good alternative, since 
more serious confusion will arise in cases where that assumption does 
not hold...

If anybody wants to investigate this in detail, and work out what the 
missing check should look like, I'll be happy to look at patches...

Alex