Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



> On 18.11.2015, at 09:52, Manuel Eberl <eberlm at in.tum.de> wrote:
> 
>> So if you just want the sum over the elements, how about using 
>> list_size f xs - size xs?
> 
> That's a great idea. It may not be the most elegant solution, but it
> sounds pretty foolproof.

Incidentally, for the record, this would have led to off-by-one bugs with the old datatype package. From "datatypes.pdf":

"The size function has a slightly different definition. The new function returns 1 instead of 0 for some nonrecursive constructors. This departure from the old behavior made it possible to implement size in terms of the generic function t.size_t."

In other words, the old package defined "size" and "size_list" (or rather, back then, "list_size") independently of each other, with some anomalies. IIRC, a constructor like "C 'a" used to count as 0 for "size" (instead of 1 now) and as "1 + f a" (where a is C's argument of type 'a) for "size_list". I thought this was crazy, but experience has shown that the old definition often gave better automation in termination proofs, as the IsaFoR developers discovered when porting their theories to the new package.

Jasmin





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