[isabelle] datatype with custom admissibility proof

Dear Isabelle,

Suppose I want a datatype for finitely-branching trees. I might write something like this:

datatype 'a mytree = Lf 'a | Br "('a mytree) fset"

where fset is the type of finite sets (defined by quotienting lists up to permutations and duplications). This doesn't work, because fset is not a datatype. The usual way to handle this is to use lists instead of fsets, but then deciding the equivalence of trees is more complicated than just checking equality of terms.

Does there exist a way of making datatypes such as mytree? Is anybody working on such a thing? I feel it would be rather useful. I'm imagining an extension to the datatype package that allows the user to provide their own proof that the datatype is admissible -- rather like the way inductive definitions can be annotated with monotonicity lemmas, or the way functions can be annotated with a custom proof of termination.

Best wishes,

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