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

On 18/11/2015 10:01, Jasmin Blanchette wrote:

On 18.11.2015, at 09:52, Manuel Eberl <eberlm at> 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."

When I read "some" I wondered what that means. Experimentally I found:

datatype t1 = A bool
==> size (A True) = 0

datatype 'a t2 = A 'a
==> size (A True) = 1

I understand why, but I am not convinced this difference in behaviour is beneficial for users of size.

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.

I could have told you that because that is one of the reasons for the old design. Experience, not only doctrine.



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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