Re: [isabelle] primcorec complains about invalid map function



Hi Andreas,

> Thanks, my example now also works with wrap_free_constructors. Maybe the wrap_free_constructors declaration could be moved to Sum_Type?

Yesterday I gave it a try and failed (having "rep_datatype" and "wrap_free_constructors" in the same theory file introduces its own set of problems), but now I realized that if I put "wrap_free_constructors" before "rep_datatype" and use the "rep_compat" option, things work smoothly. Then the problem is that the entry gets overwritten, but more on this below...

> > Incidentally, looking at 062aa11e98e1 in conjunction with a87e49f4336d suggests that some Isabelle developers are like monkeys in front of typewriters.
> Unfortunately, the DUP exception is back in Isabelle/b5b64d9d1002 as the following example shows (AFP/3daf6a41c65b).
> 
> theory Scratch imports
>  "$AFP/Coinductive/Coinductive_Nat"
>  "~~/src/HOL/Probability/Probability"
> begin
> 
> *** exception DUP "Extended_Nat.enat" raised (line 374 of "General/table.ML")
> *** At command "theory"
> 
> Happy debugging,

Ah, I can already see what's going on: "Coinductive_Nat" redefines the "Ctr_Sugar" entry for "nat", whereas "Probability" doesn't. Merge then has to choose between two different entries and can't make up its mind.

So there are two problems:

1. Overwriting an entry is not harmless -- cf. the discussion above, but also after "Coinductive_Nat" all the tools that are based on the "Ctr_Sugar" entry for "nat" (and that includes "function" and some simprocs) won't know about the inductive view.

2. The "DUP" exception.

I'll start by simply reverting yesterday's change that causes the "DUP". Then I'll see how easy it is to generalize the data structure (and modify its clients) so that it can store multiple entries for a given key.

As usual, thanks for your report and patience with us mere mortals (or monkeys),

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.