Re: [isabelle] rep_datatype and Datatype exception
On Thu, Dec 16, 2010 at 2:28 AM, Mathieu Giorgino
<mathieu.giorgino at irit.fr> wrote:
> I'm trying to use rep_datatype command, however I'm getting an exception
> "Datatype" and I'm not sure why.
> typedef 'a list2 = "UNIV:: 'a list set" ..
> definition Nil2 :: "'a list2" where "Nil2 = Abs_list2 "
> fun Cons2' :: "('a * 'a list2) \<Rightarrow> 'a list2" where
> "Cons2' (a, as) = Abs_list2 (a # Rep_list2 as)"
> rep_datatype Nil2 Cons2' (* exception Datatype raised
> (line 218 of "~~/src/HOL/Tools/Datatype/datatype_aux.ML") *)
> What does this exception mean ?
This is a bug. "Datatype" is an exception used internally in the
implementation of "rep_datatype"; users are never supposed to see it.
It appears that while "rep_datatype" supports mutual recursion, it has
problems with indirect-recursive datatypes like your "list2" type.
(Indirect recursion means that a recursive type appears as a parameter
of another datatype. In your case, type "'a list2" appears inside a
To the Isabelle developers: I was able to get a little further on this
example by modifying HOL/Tools/Datatype/datatype_data.ML like this:
val descr = map_index mk_spec cs;
val injs = Datatype_Prop.make_injs [descr] vs;
val half_distincts = map snd (Datatype_Prop.make_distincts [descr] vs);
- val ind = Datatype_Prop.make_ind [descr] vs;
+ val dt_info = get_all thy;
+ val (descrs, _) = unfold_datatypes thy descr vs dt_info descr (length cs);
+ val ind = Datatype_Prop.make_ind descrs vs;
val rules = (map o map o map) Logic.close_form [[[ind]], injs,
Now the rep_datatype command produces the right goals for me to prove,
but it raises another Datatype exception after I finish the proof.
Maybe whoever is currently maintaining the datatype package (Stefan or
Florian?) can follow up on this.
This archive was generated by a fusion of
Pipermail (Mailman edition) and