Re: [isabelle] Nested/Indirect Induction in Isabelle

Hi Mario,

What is the induction principle you get, and what is the one you want?

The reason I ask is because, using the old datatype package, I get

> set show_types ;
val it = true : bool
> tree.induct ;
val it =
   "[| !!nat::nat. (?P1.0::tree => bool) (Node nat);
         !!list::tree list.
            (?P2.0::tree list => bool) list ==> ?P1.0 (Branch list);
         ?P2.0 [];
         !!(tree::tree) list::tree list.
            [| ?P1.0 tree; ?P2.0 list |] ==> ?P2.0 (tree # list) |]
      ==> ?P1.0 (?tree::tree) & ?P2.0 (?list::tree list)" : Thm.thm

which doesn't use the "set" predicate at all



On 08/10/17 16:57, Mario Alvarez wrote:
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.

Mario Alvarez

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