Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
The BNF package internally generates such unfolding and folding constants. They are called
ctor_<typename> and dtor_<typename>. Internally, it also proves that they are inverses of
each other, but AFAIK these theorems are only made available if the attribute bnf_note_all
is set at the declaration time of the datatype.
Hope this helps,
On 17/11/15 12:33, Manuel Eberl wrote:
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?â
For this, it is very convenient to view the definition of the algebraic
datatype in terms of a (possibly recursive) sum of products. For
instance, for binary trees, I have the following "encodings":
datatype 'a bintree = Leaf 'a | Node "'a bintree" "'a bintree"
primrec encode_bintree :: "'a bintree â 'a + 'a bintree Ã 'a bintree" where
"encode_bintree (Leaf x) = Inl x"
| "encode_bintree (Node l r) = Inr (l, r)"
fun decode_bintree :: "'a + 'a bintree Ã 'a bintree â 'a bintree" where
"decode_bintree (Inl x) = Leaf x"
| "decode_bintree (Inr (l, r)) = Node l r"
Essentially, I exploit the fact that âÎ bintreeâ is a fixed point of
'ÎÎ. Î + (Î bintree)Â' and therefore âÎ bintreeâ is isomorphic to âÎ + Î
bintree Ã Î bintreeâ.
My question is now: is there an easy way to generate these encode/decode
isomorphisms automatically and prove that they are inverses of one
another? Is there perhaps a similar construction inside the internals of
the datatype package already?
This archive was generated by a fusion of
Pipermail (Mailman edition) and