Email Gateway (Aug 22 2022 at 17:01): Email Gateway (Aug 22 2022 at 17:01):From: Mark Wassell <mpwassell@gmail.com>
Hello,
I am attempting to define programming language case statements in Nominal2
and get
exception UnequalLengths raised (line 519 of "library.ML")
A possible workaround is to define case_branch to be list like and so avoid
"case_branch list":
case_branch =
B_nil | B_cons x::x s::stmt case_branch binds x in s
but this is a little messy.
A cut down version that exhibits the problem is:
theory Nominal2Exception
imports "Nominal2.Nominal2"
begin
atom_decl x
nominal_datatype expr =
E1 x
nominal_datatype stmt =
S1 "case_branch list"
| S2 expr
and case_branch =
B1 x::x s::stmt binds x in s
end
and the full text from the output window is:
Proofs for inductive predicate(s) "rep_set_stmt_raw_case_branch_raw_1",
"rep_set_stmt_raw_case_branch_raw_2", "rep_set_stmt_raw_case_branch_raw_3"
Proving monotonicity ...
Proving the introduction rules ...
Proving the induction rule ...
Proofs for inductive predicate(s) "rec_set_stmt_raw_case_branch_raw_1",
"rec_set_stmt_raw_case_branch_raw_2", "rec_set_stmt_raw_case_branch_raw_3"
Proving monotonicity ...
Proving the introduction rules ...
Proving the elimination rules ...
Proving the simplification rules ...
exception UnequalLengths raised (line 519 of "library.ML")
Email Gateway (Aug 22 2022 at 17:01):From: Brian Huffman <huffman.brian.c@gmail.com>
Hi Mark,
I also came across the same "UnequalLengths" error for exactly the
same reason; I just wrote to Christian Urban this morning about it. I
am planning to make a project out of fixing it, and updating
nominal_datatype to be able to take advantage of all the latest
datatype package features. (Currently nominal_datatype uses the
old_datatype command internally.) I'll keep you posted on any
progress.
Email Gateway (Aug 22 2022 at 17:01):From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Hi Brian,
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? Incidentally, see also this draft:
http://matryoshka.gforge.inria.fr/pubs/bindings.pdf
Cheers,
Jasmin
Email Gateway (Aug 22 2022 at 17:02):From: "Urban, Christian" <christian.urban@kcl.ac.uk>
exception UnequalLengths raised (line 519 of "library.ML")
Yes, this is because of nested datatypes (which were not really supported when I and others implemented Nominal). It would be good to have this restriction lifted. I think this is the main obstacle in many use cases.
Christian
Email Gateway (Aug 22 2022 at 17:02):From: Brian Huffman <huffman.brian.c@gmail.com>
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.
Last updated: May 06 2024 at 20:16 UTC