*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Wed, 18 Nov 2015 10:01:35 +0100*Cc*: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <564C3C4F.9050400@in.tum.de>*References*: <564B1075.5060706@in.tum.de> <C67DA37B-EEE3-4BBD-9CEE-6AB41FF48ACE@inria.fr> <564B6249.8080603@in.tum.de> <564B6466.4070200@in.tum.de> <564C2743.7080809@inf.ethz.ch> <564C3C4F.9050400@in.tum.de>

> 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

**Follow-Ups**:**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Tobias Nipkow

**References**:**[isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Jasmin Blanchette

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Andreas Lochbihler

**Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Previous by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Thread: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Cl-isabelle-users November 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list