[isabelle] "Unfolding" the sum-of-products encoding of datatypes



Hallo,

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?


Cheers,

Manuel






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.