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

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

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

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: Sep 25 2021 at 09:17 UTC