Re: [isabelle] A large mutually recursive data type
> 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
'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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and