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

[Jasmin Blanchette]

Hi Andreas,

> 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.

I worked from the principle that "is_none" and "List.null" are internal constructs and used "=" to avoid generating more theorems about internal things. Can you confirm that the convenience you found in your codatatype usage also applies to datatypes? If there is a concensus about making them more public, we can remove the "=" trick.

(For the rest of the mailing list: "=" is a special notation in the (co)datatype specification that indicates that for a nullary constructor "C", the discriminator should be "%x. x = C" rather than "is_C". Thus, some theorems about destructors are currently generated with "xs = []" and "x = None" as premises instead of "null xs" and "is_none x". Andreas found, and reported privately, that this use of constructors to encode destructors can weaken "auto" and "simp" by giving rise to goals that mix constructors and destructors in bad ways.)

> Yes, please get rid of the recursors.

OK, thanks for the arguments (esp. the one about code generation call-by-value, which I hadn't thought of). I'll look into this.

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

There's no hurry, really. I am almost certain you will run into new issues of some sort of another, and I need to catch up with my backlog. ;)

Cheers,

Jasmin