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?


Andrei

________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Mario Alvarez <mmalvare at eng.ucsd.edu>
Sent: 08 October 2017 06:57:43
To: cl-isabelle-users at lists.cam.ac.uk
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.

Thanks,
Mario Alvarez



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