Re: [isabelle] simple question
On Aug 3, 2007, at 6:53 PM, lucas cavalcante wrote:
The function 'f' (above) does not work, returning the fallowing
I'd like to know what's wrong in this definition.
datatype frm = At sbf | Nt frm
f :: "frm => frm"
"f (At x) = At x"
"f (Nt x) = Nt(x)"
"f (Nt(Nt x)) = f (x)"
*** Primrec definition error:
*** illegal argument in pattern
*** "f (Nt (Nt x)) = f x"
*** At command "primrec".
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and