*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] primcorec complains about invalid map function*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Fri, 7 Feb 2014 10:30:14 +0100*Cc*: isabelle-users Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <52F496F0.5010007@inf.ethz.ch>*References*: <52F1F458.3060905@inf.ethz.ch> <30EE3501-6736-487B-B570-8D682BAF1025@gmail.com> <52F226EC.60900@inf.ethz.ch> <62CD798F-8E1B-43E1-BB47-4EDB9460F6FB@gmail.com> <52F34B7F.2070807@inf.ethz.ch> <70BEF5F6-E63C-41A3-963A-1E89206186F1@gmail.com> <52F36866.1020309@inf.ethz.ch> <5C5AF187-5A08-4026-891A-5DFDCF9195D8@gmail.com> <52F496F0.5010007@inf.ethz.ch>

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

**Follow-Ups**:**Re: [isabelle] primcorec complains about invalid map function***From:*Johannes Hölzl

**References**:**[isabelle] primcorec complains about invalid map function***From:*Andreas Lochbihler

**Re: [isabelle] primcorec complains about invalid map function***From:*Jasmin Blanchette

**Re: [isabelle] primcorec complains about invalid map function***From:*Andreas Lochbihler

**Re: [isabelle] primcorec complains about invalid map function***From:*Jasmin Blanchette

**Re: [isabelle] primcorec complains about invalid map function***From:*Andreas Lochbihler

**Re: [isabelle] primcorec complains about invalid map function***From:*Jasmin Blanchette

**Re: [isabelle] primcorec complains about invalid map function***From:*Andreas Lochbihler

**Re: [isabelle] primcorec complains about invalid map function***From:*Jasmin Blanchette

**Re: [isabelle] primcorec complains about invalid map function***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] primcorec complains about invalid map function
- Next by Date: Re: [isabelle] primcorec complains about invalid map function
- Previous by Thread: Re: [isabelle] primcorec complains about invalid map function
- Next by Thread: Re: [isabelle] primcorec complains about invalid map function
- Cl-isabelle-users February 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list