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.
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
