[isabelle] Nested/Indirect Induction in Isabelle



Hello Isabelle Users,

I can't figure out how to get Isabelle to generate a sufficiently general
induction principle for the following type:

datatype tree =
Node "nat"
| Branch "tree list"

The induction principle generated here is not general enough: it applies
the "set" predicate to the list argument of Branch, but for my purposes I
also care about the order of the trees in that list (i.e., applying "set"
to the argument loses too much information, the order of elements)

I could define a mutually inductive type to capture the tree lists in the
Branch case, but this seems inelegant: I'd like to be able to use
preexisting abstractions and theorems about lists when reasoning with my
data structure.

How do I solve this? I've poked around Google a fair bit but haven't found
an answer.

Thanks,
Mario Alvarez



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