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

[Andreas Lochbihler]

Hi Jasmin,

> 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.
I saw that you used the discriminator "=", but we already have functions Option.is_none 
and List.null. So far, they have been mainly used for code generation, but I have found 
them very convenient in in my codatatype usages when using the destructor style. I think 
it might be worth a try to give these discriminators official status.

> 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".
Yes, please get rid of the recursors. As you might have seen during the adaptations to my 
AFP entries, I have lemmas of the form "rec_XXX = case_XXX" such that I can prove theorems 
by unfolding a primrec definition to the recursor, then to the case combinator, and then 
use the existing split rules for case_XXX. So, for non-recursive datatypes. I'd be happy 
if recursor and case combinator are the same constant (maybe with an abbreviation rec_XXX 
= case_XXX?). This, however, also affects code generation in call-by-value languages: As 
there are case certificates for the case combinators, but not for the recursors. Hence, 
for functions defined via the recursor and without separately declared code equations, the 
code generator outputs a function definition for the recursor and CBV languages first 
evaluate all arguments to the recursor before pattern-matching on the term. This means 
that for nullary constructors, the case is evaluated even if it might not be needed. If 
there's just one case combinator (which the code generator implements as primitive case), 
this cannot happen any more.

Andreas

PS: I have not yet tried how your changes affect my primcorec definitions.