Re: [isabelle] primrec of datatype containing fset

Thanks Andrei!


On Jul 9, 2017, at 8:16 AM, Andrei Popescu <A.Popescu at<mailto:A.Popescu at>> wrote:

Dear Larry,

>> These days, users should regard "primrec" as an internal feature necessary for bootstrapping the system but for implementers only.

While this is true in most cases, in complex situations involving nested recursion "primrec" can provide the most elegant solution. For example, compare the "function"-based definition with the following correct primrec definition:

primrec count' :: "val â nat" where
"count' (VNat n) = 1" |
"count' (VRel t) = fsum (Î((_,v), (_,u)). v + u) (fimage (map_prod (Î v. (v,count' v)) (Î v. (v,count' v))) t)"

(This is now correct since all subtrees are counted as separate entities, taking advantage of full primitive recursion as opposed to mere iteration.)

With a proper setting for congruences and such, this can be handled by "function" as well, but this is tricky and quite laborious -- as the current thread shows.



Larry Paulson

> On 9 Jul 2017, at 11:15, Lars Hupel <hupel at<mailto:hupel at>> wrote:
> this is a restriction of "primrec". What you're writing is not in fact a
> primitive recursive specification. There are two ways around that:
> 1) Rewrite it as primitive recursive
> 2) Use the "fun"/"function" command

Jeremy G. Siek    <jsiek at<mailto:jsiek at>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington

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