Re: [isabelle] Nested/Indirect Induction in Isabelle
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 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 =
| 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