Email Gateway (Aug 18 2022 at 15:08): Email Gateway (Aug 18 2022 at 15:08):From: Christoph Feller <c_feller@informatik.uni-kl.de>
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
Email Gateway (Aug 18 2022 at 15:08):From: Alexander Krauss <krauss@in.tum.de>
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
Email Gateway (Aug 18 2022 at 15:08):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Also note that the original specification of things does not matter as
long as you can derive the desired properties. In that case you could
e.g. define
definition even :: "nat => bool" where
"even n <-> n mod 2 = 0"
definition odd :: "nat => bool" where
odd n <-> n mod 2 = 1"
and derive the recursive rules:
lemma [simp]:
"even 0 = True"
"even (Suc n) = odd n"
"odd 0 = False"
"odd (Suc n) = even n"
<proof>
Also note that even/odd is already present in the HOL theory Parity;
just import theory Complex_Main to use it.
Hope this helps,
Florian
signature.asc
Last updated: Apr 20 2024 at 08:16 UTC