Re: [isabelle] Nested/Indirect Induction in Isabelle



Hi Mario,

I agree with Andrei that structural induction on rose trees should not depend on the order of the subtrees in the list, as you only have one inductive property. With the old datatype package, nested datatype recursion was mapped to mutual recursion (as shown by Jeremy below) where you could specify *two* inductive predicates (one for trees and one for lists of trees) for the induction. If this is what you want, you can have the datatype package generate the appropriate rule:

datatype_compat tree

thm compat_tree_tree_list.induct

Hope this helps,
Andreas

On 08/10/17 12:59, Jeremy Dawson wrote:
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

Cheers,

Jeremy

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.

Thanks,
Mario Alvarez






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