[isabelle-dev] [isabelle] primcorec complains about invalid map function

[Jasmin Blanchette]

Hi Andreas,

(I'm moving the thread to "isabelle-dev".)

Am 07.02.2014 um 09:18 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

> On 06/02/14 17:15, Jasmin Blanchette wrote:
>> Ah, that one was easy to fix (a87e49f4336d).
> Thanks, my example now also works with wrap_free_constructors. Maybe the wrap_free_constructors declaration could be moved to Sum_Type?

I have just pushed a series of changes whereby "sum", "prod", "bool", "unit", and "nat" are first registered with "wrap_free_constructors", before they are passed to "rep_datatype". The selectors "proj{l,r}" (renamed from "Sum_Type.Proj{l,r}"), "fst", and "snd" (and a completely hidden "Nat.pred") are generated by the command.

In addition, "option" and "list" are now defined using "datatype_new" and registered as old-style datatypes using "datatype_new_command". I have yet to do some clean up with the set and map functions and the relators, though.

Some time ago, we decided at a weekly meeting to use postfix for generated constant names by default -- e.g. "map_tree", "case_tree", "rec_tree", etc. This puts the important part first. Indeed, one can think of the type as a subscript ($\mathit{map}_{\mathit{tree}}$). Tobias was a strong proponent of the scheme, and I had found myself using it for mutually recursive functions before (cf. our ITP submission). To ease the transition, I have now changed the old package to generate such names as well for "case" and "rec".

Due to the peculiar, temporary setup I adopted, the recursors for "sum", "prod", "bool", "unit", and "nat" are prefixed by "old." (e.g. "old.rec_sum"). For the first four of the five, my goal is to do away with the recursors entirely, since they coincide with the case combinators -- and also to do this for types generated by "datatype_new".

When porting existing theories, the main issues were the occasional "xxx_{rec,case}" and the references to generated variable names in "apply" scripts. I also discovered the hard way how Stefan's code extraction from proof terms works and what kinds of assumption it makes (i.e., that the derivations of certain theorems are named and that the exhaust rule's variables are called "P" and "y").

In a nutshell: (1) It should now be easier to use "case" expressions with "primcorec"; (2) we are one step further in the transition from the old to the new datatype package.

Cheers,

Jasmin