Re: [isabelle] simple question



On Aug 3, 2007, at 6:53 PM, lucas cavalcante wrote:

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

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
- John






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.