Re: [isabelle] primrec of datatype containing fset

Hi Andrei,

Good catch!

But now I’m a bit unsatisfied… the function version of count required a fair bit of work and
looks like it’s rather specific, so I may have to repeat this amount of work for every
other recursive function on datatype val.

I wonder if the termination argument involving fsum could be adapted to ffold?


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

Hi Jeremy and Lars,

Special care is needed when recursing through permutative structures like sets and multisets. For example, the primrec version discussed here is _not_ equal to the 'fun' version of 'count', since it recursively collapses the numbers coming from subtrees that happen to have the same count. The 'fun' version is the correct one.

All the best,


From: cl-isabelle-users-bounces at<mailto:cl-isabelle-users-bounces at> <cl-isabelle-users-bounces at<mailto:cl-isabelle-users-bounces at>> on behalf of Lars Hupel <hupel at<mailto:hupel at>>
Sent: 09 July 2017 11:28
To: Siek, Jeremy
Cc: cl-isabelle-users at<mailto:cl-isabelle-users at>
Subject: Re: [isabelle] primrec of datatype containing fset

> Thank you for your very thorough answer! It looks like option 1 will
> my needs.

On second thought, I realised that your use of "ffold" is merely to
compute the sum of some things in a set. Luckily, we can make "function"
cope with that. See attachment for a possible solution (also a version with
"primrec" that doesn't use "ffold").


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.