[isabelle] "Unfolding" the sum-of-products encoding of datatypes
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