[isabelle] even/odd with primrec



Hallo,

we tried to define the functions even and odd like this:

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"

and got the error

 inconsistent functions for datatype "nat"

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?

Thanks,
Christoph Feller





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