Re: [isabelle] primrec of datatype containing fset



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.

Best,

Andrei


Larry Paulson


> On 9 Jul 2017, at 11:15, Lars Hupel <hupel at in.tum.de> 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





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