Re: [isabelle] primrec

Dear Viorel,

your specification of Special is not primitively recursive, because the last line calls special on the right child v of the left child x, but primitive recursion only allows to call Special on the immediate children x and y. Admittedly, the error message could be better.

There are two ways to solve this:

a) Since your function is not primitvely recursive, use the more general function package. This way, you can also transform the ugly case expression into multiple pattern matches. Moreover, fun generates custom rules for induction and case analysis.

b) Transform your definition into primitive recursion. I think the following is equivalent to your definition:

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


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"

Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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