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

[Andreas Lochbihler]

Hi Jasmin,

On 13/02/14 13:47, Jasmin Blanchette wrote:
> Hi Andreas,
>
> Am 13.02.2014 um 13:34 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:
>
>> In summary, I do not want to replace "_ = None" and "_ = []" with null and is_none, I'd just like to make null and is_none somewhat official. I am not sure when these discriminators can show up in practice, but I thought that only primcorec needs them. So from my point of view, it seems sensible to make them the official discriminators.
>
> Now I'm confused. If we do what you just proposed, the discriminators end up appearing in some of the generated theorems -- and you observed yourself that "the destructor view is not at all convenient for datatypes, because most functions pattern match on the constructors. Therefore, it is better the have the constructors explicit." For a datatype, being an "official" discriminator basically amounts to "appearing in generated theorems". Or did I misunderstood something?
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?

Andreas