Email Gateway (Aug 18 2022 at 10:42): Email Gateway (Aug 18 2022 at 10:42):From: lucas cavalcante <thesupervisar@gmail.com>
Hello all,
The function 'f' (above) does not work, returning the fallowing message.
I'd like to know what's wrong in this definition.
typedecl sbf
datatype frm = At sbf | Nt frm
consts
f :: "frm => frm"
primrec
"f (At x) = At x"
"f (Nt x) = Nt(x)"
"f (Nt(Nt x)) = f (x)"
*** Primrec definition error:
*** illegal argument in pattern
*** in
*** "f (Nt (Nt x)) = f x"
*** At command "primrec".
Thank you,
Lucas Cavalcante
Email Gateway (Aug 18 2022 at 10:44):From: Alexander Krauss <krauss@in.tum.de>
Primrec does not support nested patterns ("Nt (Nt x)"). Rewrite your
definition or use recdef. Also note that the third pattern is an
instance of the second one, so (if you think of f as a functional
program like in ML), the third equation will never be used...
Alex
Email Gateway (Aug 18 2022 at 10:45):From: George Karabotsos <g_karab@cs.concordia.ca>
Hi Lucas,
I am not sure what you are trying to do but I think you have to rethink
the definition of your datatype.
I took the liberty to modify it a bit and here is an alternative definition:
datatype frm = At sbf | Nt frm | Nts frm;
consts
f :: "frm => frm"
primrec
"f (At x) = At x"
"f (Nt x) = Nt x"
"f (Nts x) = f x"
I hope it helps.
George
lucas cavalcante wrote:
Email Gateway (Aug 18 2022 at 10:46):From: John Ridgway <john@jacelridge.com>
There are several issues here. The first is that f(Nt(Nt x)) is
illegal. According to the book "Isabelle's Logics: HOL" available on
the Isabelle site:
"reduction rules specify one or more equations of the form:
f x1 ... xm (C y1...yk) z1...zn = r
such that C is a constructor of the datatype, r contains only the
free variables on the left-hand
side, and all the recursive calls in r are of the from f ...
yi ... for some i." (page 44 in my copy at
least).
f (Nt (Nt x)) does not match this form since the inner use of "(Nt
x)" is not a variable. The rule is that you can only "peel off" one
level of constructor at a time.
The second issue is that your third clause would never get invoked,
since the second would cover it anyway.
Peace
Last updated: May 03 2024 at 04:19 UTC