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?


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".


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