Re: [isabelle] primrec



Thank you all for the quick answers.
I will use "fun". I was afraid that using fun
would require providing the well founded
relation which ensures termination.

However it seems that in this case Isabelle
figures it out automatically.

Viorel


On 11/09/2011 10:39 AM, Lukas Bulwahn wrote:
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.