Re: [isabelle] Nested/Indirect Induction in Isabelle

Hi Mario,

It does not make sense to factor in the order in the induction hypothesis, since the induction hypothesis involves all components at the same time (as given by the "set" operator). What is the proof principle you have in mind?


From: cl-isabelle-users-bounces at <cl-isabelle-users-bounces at> on behalf of Mario Alvarez <mmalvare at>
Sent: 08 October 2017 06:57:43
To: cl-isabelle-users at
Subject: [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.

Mario Alvarez

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