Re: [isabelle] primrec of datatype containing fset



Hi Jeremy,

________________________________

>>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?

It can, with some tricks.

But for this particular function, primrec works:

primrec count :: "val ⇒ nat" where
"count (VNat n) = 1" |
"count (VRel t) = fsum (λ((_,n), (_,m)). n + m) (fimage (map_prod (λ v. (v,count v)) (λ v. (v,count v))) t)"

If you have a genuinely primitive recursion function and primrec seems to cause you trouble, you can always use the primtive recursive combinator

rec_val :: (nat ⇒ 'a) ⇒ (((val × 'a) × val × 'a) fset ⇒ 'a) ⇒ val ⇒ 'a

explicitly, and then infer the high-level equations, e.g.:

definition count where "count = rec_val (λn. 1) (fsum (λ((_,n), (_,m)). n + m))"
lemma count_simps[simp]:
"count (VNat n) = 1"
and
"count (VRel t) = fsum (λ((_,n), (_,m)). n + m) (fimage (map_prod (λ v. (v,count v)) (λ v. (v,count v))) t)"
unfolding count_def by auto

This is essentially what the primrec package does for you automatically, but sometimes, esp. for nested recursion, the combinator version is easier to get right.

I would be curious to know what other functions you would like to define on val. These examples would help us devise the right support for ffold and friends in the finite set library.

Best,

Andrei






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


Andrei


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

> Thank you for your very thorough answer! It looks like option 1 will
suite
> 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").

Cheers
Lars

__________________________________________
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.