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

[Jasmin Blanchette]

Hi Andreas,

> I read the comment to your changeset 3def821deb70, which says that Nat.pred may show up in theorems generated by primcorec. This is fine, because the destructor view for codatatypes goes well with discriminators and selectors for datatypes. As I do not know where discriminators show up in theorems generated by datatype_new, but my guess is that they only show up in theorems that the old datatype package does not generate. Moreover, I expect that they do not show up in anyhing generated by primrec. So where would it harm to make them the official discriminators?

There's certainly no big harm in making them the official discriminators. My main fear is inconsistency: There are many theorems in Isabelle that have "xs ~= []" as a premise. If we start generating some with "null xs" or "List.null xs", we end up with an unpleasing mixture, whose only "satisfactory" resolution is to have both versions of everything (cf. the duplication of "Suc" vs "+ 1" theorems).

Hence, until there is a wider concensus about the merits of "null" and "is_none", I am reluctant to go that way (but will not stop anybody who wants to change the statu quo).

For "pred", the situation is even worse: Ideally we would have "%x. x - 1" in there. Right now I'm just hiding the theorems and constants, but they might resurface e.g. in the constructor and destructor views generated from a code view of "primcorec". My ultimate goal is to have a more or less ad hoc setup that replaces "prec" by "- 1" and then make the theorems public. Hiding the theorems is an intermediate step toward this.

Cheers,

Jasmin