Re: [isabelle] primrec of datatype containing fset



Thanks Andrei!

Cheers,
Jeremy

On Jul 9, 2017, at 8:16 AM, Andrei Popescu <A.Popescu at mdx.ac.uk<mailto:A.Popescu at mdx.ac.uk>> 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.

Best,

Andrei


Larry Paulson


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

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/





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