Re: [isabelle] even/odd with primrec



Hi Christoph,

primrec even :: "nat => bool"
     and odd :: "nat => bool" where
"even 0 = True" |
"even (Suc n) = odd n" |
"odd 0 = False" |
"odd (Suc n) = even n"
[...]

We suppose that this is due to the fact that we define a mutual
recursive primrec-function over a datatype (nat) that is not mutual
recursive. Is this true?

Yes.

Is there any not too technical explanation
why primrec cannot handle this rather simple looking function?

Simply because it wasn't designed to handle it. As there is no formal notion of "rather simple looking function", primrec uses a fixed syntactic scheme with exactly one function per mutually-recursive datatype.

For everything else use the function package, replacing the "primrec" keyword with "fun".

Alex





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.