*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 18 Nov 2015 10:32:42 +0100*In-reply-to*: <9E245509-0BC3-4A1D-A2AE-0D5999744F36@inria.fr>*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> <9E245509-0BC3-4A1D-A2AE-0D5999744F36@inria.fr>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

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

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

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

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.

Tobias

Jasmin

**Attachment:
smime.p7s**

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

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

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

- 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