*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Tue, 17 Nov 2015 18:31:18 +0100*In-reply-to*: <564B6249.8080603@in.tum.de>*References*: <564B1075.5060706@in.tum.de> <C67DA37B-EEE3-4BBD-9CEE-6AB41FF48ACE@inria.fr> <564B6249.8080603@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.3.0

size_foo sz x = setsum sz (set_foo x)

On 17/11/15 18:22, Manuel Eberl wrote:

Thanks, that already looks like pretty much exactly what I want.Another problem is that I need a kind of parameterised âsizeâfunction, which simply adds together the size of all the containedobjects while ignoring the structure of the datatype itself.Essentially, for a datatype âÎ fooâ with a single type parameter, thebehaviour should be something likeOr, in other words: I would something that works like datatype'sbuiltin size_foo, but without counting the structure of the datatypeitself. (e.g. I would the size of â[0,0,0]â to be 0, not 3)How would I best go about doing something like this generically fordatatypes with arbitrarily many type parameters? This is not a veryurgent question; the above construction with set_foo works fine forone parameter and one parameter is all I currently need, but it wouldbe nice to know.Cheers, Manuel On 17/11/15 13:45, Jasmin Blanchette wrote:Hi Manuel,I have been playing around with some analytic combinatorics lately, asking questions like âHow many values are there of a given datatype with a certain size?âAndreas gave you the most important pointer. Since you seem to beenvisioning an ML command for generating them automatically, Isuspect you will want to access the ML interfaces of the BNF packagedirectly, and not use "bnf_note_all" (which is mostly useful fordebugging and/or for sketching BNF extensions).The low-level theorems you'd need, e.g. "ctor_dtor", are stored inthe BNF (co)datatype database:ML {* BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name bintree} |> the |> #fp_res |> #ctor_dtors |> hd *}You might find the code in "~~/src/HOL/Library/bnf_lfp_countable.ML"a useful source of inspiration. The "mk_encode_funs" functionconstructs a "to_nat" function for a datatype (LFP) from "to_nat"functions about the types on which it depends. If you find that ofany interest, I can send you the (more readable) theory files thatmock up the construction performed at the ML level.Incidentally, I'm tempted to rename "ctor" to "in" and "dtor" to"out", in keeping with some of the literature, to avoid any confusionbetween the actual high-level constructors (called "ctr"s in the codeand some theorems) and the low-level constructors. If anybody isagainst this renaming, please speak out now.Jasmin

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

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

- Previous by Date: Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
- Next by Date: [isabelle] Proving termination of a recursive function
- 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