Re: [isabelle] primrec of datatype containing fset
On Jul 9, 2017, at 8:16 AM, Andrei Popescu <A.Popescu at mdx.ac.uk<mailto:A.Popescu at mdx.ac.uk>> wrote:
>> 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.
> 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>>
School of Informatics and Computing
Indiana University Bloomington
This archive was generated by a fusion of
Pipermail (Mailman edition) and