Email Gateway (May 17 2021 at 13:26): Email Gateway (May 17 2021 at 13:26):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear primrec experts,
In the attached theory for Isabelle2021, I'm trying to define a simple primitively
recursive function over a datatype. However, primrec complains about "extra variables on
rhs" in the underlying foundational definition. It looks to me as if primrec does not
correctly construct the lambda abstraction for the second argument to the recursor. My
current workaround is to use fun instead, but it would be nice to get the support for
transfer rules from primrec.
Best,
Andreas
Scratch.thy
Email Gateway (May 17 2021 at 19:51):From: Mikhail Mandrykin <mandrykin@ispras.ru>
Andreas Lochbihler писал 2021-05-17 16:26:
My current workaround is to use fun instead, but it
would be nice to get the support for transfer rules from primrec.
I'm not at all a primrec expert, but I was able to get the resulting
equations from primrec rather than fun by
using another work-around:
‹
datatype 'a dt
= C1 | C2 'a "'a dt list" "'a dt"
primrec f :: "'a ⇒ 'a dt list ⇒ 'a dt ⇒ 'a dt list ⇒ 'a dt" where
f1: "f n y C1 y' = C2 n (y @ y') C1"
| f2[unfolded Let_def]: "f n y (C2 n' y' co) y'' = (let r = λ x y. f x y
co in C2 n y (r n' y' y''))"
thm f1 f2
›
Regards, Mikhail
Email Gateway (May 18 2021 at 04:50):From: Andreas Lochbihler <mail@andreas-lochbihler.de>
Dear Mikhail,
Thanks for finding a workaround. This highlights that there is indeed some problem in the
primrec implementation.
Best,
Andreas
Email Gateway (Jul 14 2021 at 08:06):From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear primrec user,
Thank you for your report. I have now solved the issue in primrec so that your example should work in the next Isabelle release. I'm glad you have a workaround in the meantime.
Cheers,
Jasmin
Last updated: Jan 04 2025 at 20:18 UTC