*To*: Victor Gomes <vb358 at cam.ac.uk>*Subject*: Re: [isabelle] A large mutually recursive data type*From*: Jasmin Blanchette <jasmin.blanchette at inria.fr>*Date*: Fri, 11 Mar 2016 13:45:43 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk, Dmitriy Traytel <traytel at inf.ethz.ch>*In-reply-to*: <204CD2AE-DA00-4512-AB7F-AA3D8F70C284@cam.ac.uk>*References*: <9EA07F44-212D-4E74-9085-D2C90E4BFD0C@cam.ac.uk> <7B624798-A387-44B8-817E-ABC7ABA8CC67@inf.ethz.ch> <204CD2AE-DA00-4512-AB7F-AA3D8F70C284@cam.ac.uk>

Dear Victor, > Thanks for the answer. I have also tried Isabelle2013-2 (which I believe uses the old Isabelleâs package) with no success, although I didnât wait much longer. In principle, we know how to handle such large datatypes. Mutually recursive definitions can be rephrased as nested definitions. For example, instead of datatype 'a tree_list = Nil | Cons "'a tree" "'a tree_list" and 'a tree = Node 'a "'a tree_list" one can define datatype 'a list = Nil | Cons 'a "'a list" datatype 'a tree = Node 'a "'a tree list" (We call this "nesting" because "'a tree" occurs recursively nested under "list", but this is not standard terminology.) The nested version scales much better than mutual one with modern versions of Isabelle (but much worse in old versions) -- nesting basically comes for free, whereas an n-ary mutual construction is O(n^3) or O(n^4) (Dmitriy might know). Given your specification, I see two options: 1. You could introduce nesting manually, in a more or less ad hoc fashion, inspired by the "tree_list" example above. Although this sometimes leads to satisfactory results (as in the "tree list" example above), in your case the result surely wouldn't be pretty. 2. We could internally reduce large mutual specifications to nested ones. We already have much of the machinery in place to do this (see the "Nested-to-Mutual Reduction" paragraph, starting on p. 5, in our ITP 2014 paper [*]), but some more engineering would be necessary to (1) heuristically generalize some of the types in some groups (i.e. automatizing part 1) and (2) lifting all the results across isomorphisms, so that this is completely invisible to the user (except that it scales much better). I would expect that point 2 would take us up to one week of work to get it right. It is unfortunately rather technical work. How important is this to you? What are your deadlines? And how acceptable is Option 1? Cheers, Jasmin [*] http://www.loria.fr/~jablanch/co-data-impl.pdf

**Follow-Ups**:**Re: [isabelle] A large mutually recursive data type***From:*Victor Gomes

**References**:**[isabelle] A large mutually recursive data type***From:*Victor Gomes

**Re: [isabelle] A large mutually recursive data type***From:*Dmitriy Traytel

**Re: [isabelle] A large mutually recursive data type***From:*Victor Gomes

- Previous by Date: Re: [isabelle] A large mutually recursive data type
- Next by Date: Re: [isabelle] A large mutually recursive data type
- Previous by Thread: Re: [isabelle] A large mutually recursive data type
- Next by Thread: Re: [isabelle] A large mutually recursive data type
- Cl-isabelle-users March 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list