Re: [isabelle] Nominal2 and exception UnequalLengths raised



On Wed, Mar 28, 2018 at 12:26 PM, Jasmin Blanchette
<jasmin.blanchette at inria.fr> wrote:
> I understand this is isabelle-users, but for the record the most recent version of Nominal2's "nominal_datatype" (since AFP/9dbda7f8b6c4, 2 Jan 2018) builds a new (BNF-style) datatype instead of an "old" datatype, and "old_datatype" has been discontinued (since Isabelle/0ee38196509e, 2 Jan 2018). But beyond that, I'm not sure we're really "taking advantage" of the latest datatype package features. What do you have in mind specifically? Nested nominal datatypes?

Specifically, I want to handle indirect recursion through types like
lists, pairs, and other BNF types. The generated function definitions
(like "permute", "fv", "alpha" etc.) should use "map" and "list_all2"
and the internal proofs should use induction rules involving "set",
rather than treating indirect recursion as mutual recursion like the
old datatype package did. The internal proofs should take advantage of
BNF-generated rules like "map_cong0", "map_ident", and "map_comp".

I'm not concerned about nested nominal datatypes, setting up
"datatype" for indirect recursion through nominal datatypes, or
anything like that.

Since there have been recent changes (post Isabelle2017) to Nominal2,
I'll base my work on the development version and I'll post any
questions I have to isabelle-dev.

- Brian




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