Re: [isabelle] primrec of datatype containing fset



Dear Lars,

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

Thank you!
Jeremy

> On Jul 9, 2017, at 6:15 AM, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Dear Jeremy,
> 
>> Iâd like to write recursive functions over the following datatype:
>> 
>> datatype val = VNat nat | VRel "(val à val) fset"
>> 
>> As a simple example,
>> 
>> primrec count :: "val â nat" where
>>  "count (VNat n) = 1" |
>>  "count (VRel t) = (ffold (Î (v1,v2). Î r. count v1 + count v2 + r) 0
> t)"
>> 
>> But this getâs rejected with the âInvalid map functionâ error.
> 
> 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
> 
> Here is option 1:
> 
> primrec count :: "val â nat" where
> "count (VNat n) = 1" |
> "count (VRel t) = (ffold (Î (v1,v2). Î r. v1 + v2 + r) 0 (map_prod count
> count |`| t))"
> 
> Observe that the recursive calls of "count" must only occur within
> suitable "map functions" of the involved type constructors. In your case,
> the recursion of "val" is nested through a pair and an "fset". Hence, the
> use of "|`|" (map for "fset") and "map_prod" (map for "prod").
> 
> Option 2:
> 
> fun count :: "val â nat" where
> "count (VNat n) = 1" |
> "count (VRel t) = (ffold (Î (v1,v2). Î r. count v1 + count v2 + r) 0 t)"
> 
> The problem here is showing termination. The function package tries to
> automatically derive a termination relation, which fails here.
> 
> It can be specified manually as follows:
> 
> function (sequential) count :: "val â nat" where
> "count (VNat n) = 1" |
> "count (VRel t) = (ffold (Î (v1,v2). Î r. count v1 + count v2 + r) 0 t)"
>  by pat_completeness auto
> 
> termination
>  apply (relation "measure size")
>  <proof>
> 
> But as far as I can tell, the resulting goal is not actually provable. The
> reason is that the function package has no idea how recursive calls nested
> in "ffold" work. There are ways to explain to the function package how this
> works, but I'm not sure if it's possible in this concrete case. One would
> need a lemma like this:
> 
> lemma ffold_cong[fundef_cong]:
>  assumes "âx y. x |â| S â f x y = g x y" "x = y" "S = T"
>  shows "ffold f x S = ffold g y T"
> sorry
> 
> Using this lemma, we can successfully prove termination, but I'm not sure
> whether it actually holds.
> 
> In summary, I think you're left with either rewriting your function to be
> primitive recursive, or avoid "non-deterministic" functions like "ffold".
> 
> Cheers
> Lars


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