Email Gateway (Aug 22 2022 at 16:12): Email Gateway (Aug 22 2022 at 16:12):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
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
Email Gateway (Aug 22 2022 at 16:12):From: Jeremy Dawson <Jeremy.Dawson@anu.edu.au>
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
Email Gateway (Aug 22 2022 at 16:13):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
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
Email Gateway (Aug 22 2022 at 16:13):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Jeremy (and Mario),
The old-style principle can be inferred by composing tree induction with list induction. (Theory also attached. The proof can be condensed into a one-liner, but I wish to show its structure more clearly.)
datatype tree = Node "nat" | Branch "tree list"
lemma old_tree_induct:
assumes N: "(⋀nat. P1 (Node nat))"
and B: "⋀list. P2 list ⟹ P1 (Branch list)"
and Nl: "P2 []" and Cs: "⋀tree list. P1 tree ⟹ P2 list ⟹ P2 (tree # list)"
shows "P1 tree ∧ P2 list"
proof-
{fix tree
have "P1 tree ∧ (∀ list. tree = Branch list ⟶ P2 list)"
proof (induction)
case (Node) thus ?case using N by auto
next
case (Branch list)
thus ?case apply(induct list) using B Nl Cs by auto blast+
qed
}
thus ?thesis by auto
qed
The reason why we prefer "set"-based induction for nested datatypes in the new datatype package is because this follows the type structure modularly, without breaking the abstraction layer. This happens for both induction and recursion: Whenever a datatype T is defined by nesting a (polymorphic) type L, the induction/recursion principle for T appeals to the set/map operator for L, without delving into the constructors of L. Incidentally, without this modularity principle we would not have been able to nest inductive types into coinductive types or vice versa.
Andrei
New_to_Old.thy
Email Gateway (Aug 22 2022 at 16:13):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 16:13):From: Mario Alvarez <mmalvare@eng.ucsd.edu>
Thank you all for your feedback. I think the old style inductor for my tree
datatype is just what I want. Thanks especially for the code segment
showing how to do it.
Best,
Mario
Last updated: Apr 25 2024 at 16:19 UTC