Re: [isabelle] Nested/Indirect Induction in Isabelle
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:
Hope this helps,
On 08/10/17 12:59, Jeremy Dawson wrote:
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 =
| 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
How do I solve this? I've poked around Google a fair bit but haven't found
This archive was generated by a fusion of
Pipermail (Mailman edition) and