Re: [isabelle] primrec



On 11/09/2011 09:21 AM, Viorel Preoteasa wrote:
Hello,

I have the following definitions:

datatype Tree =
leaf1 | leaf2 | "tree" "Tree" "Tree" (infixr ".." 65)


primrec Special :: "Tree => bool" where
"Special leaf1 = True" |
"Special leaf2 = True" |
"Special (x .. y) = (case x of leaf1 => Special y | leaf2 => Special y
| (u .. v) ⇒ u = leaf1 /\ Special y /\ (Special v))"

On the definition of Special I get the error:

Extra variables on rhs: "Special"
The error(s) above occurred in definition "Special_def"

How could Special be an extra variable? Is it possible
to fix this definition?
The error message might be misleading, but this function is not primitive recursive, in the third equation, you would only be allowed to use recursive calls Special x and Special y, but not Special v.

One can probably reformulate it to fit the syntactic criteria of primrec, but it certainly easier just to use fun, as Larry suggested.


Lukas





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