Re: [isabelle] Nested/Indirect Induction in Isabelle



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



________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Jeremy Dawson <Jeremy.Dawson at anu.edu.au>
Sent: 08 October 2017 11:59
To: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] Nested/Indirect Induction in Isabelle

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

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 =
> 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
>

Attachment: New_to_Old.thy
Description: New_to_Old.thy



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