*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*: Tue, 17 Nov 2015 13:45:51 +0100*Cc*: Andrei Popescu <a.popescu at mdx.ac.uk>, Dmitriy Traytel <traytel at inf.ethz.ch>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <564B1075.5060706@in.tum.de>*References*: <564B1075.5060706@in.tum.de>

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 be envisioning an ML command for generating them automatically, I suspect you will want to access the ML interfaces of the BNF package directly, and not use "bnf_note_all" (which is mostly useful for debugging and/or for sketching BNF extensions). The low-level theorems you'd need, e.g. "ctor_dtor", are stored in the 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" function constructs a "to_nat" function for a datatype (LFP) from "to_nat" functions about the types on which it depends. If you find that of any interest, I can send you the (more readable) theory files that mock 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 confusion between the actual high-level constructors (called "ctr"s in the code and some theorems) and the low-level constructors. If anybody is against this renaming, please speak out now. Jasmin

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

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

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

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

- Previous by Date: [isabelle] syntax for lifted / point-free operations
- Next by Date: Re: [isabelle] Failing afp-2015 build
- 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