[isabelle] Nominal2 and exception UnequalLengths raised



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")



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