[isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 11:46, schrieb Tobias Nipkow:
>
> On 26/05/2014 11:07, Jasmin Blanchette wrote:
>> Am 26.05.2014 um 11:02 schrieb Tobias Nipkow <nipkow at in.tum.de>:
>>
>>> The definition of list should look like before.
>> I don't see how this is an option. This would result in the following duplicate constants:
>>
>>      map_list vs. map
>>      set_list vs. set
>>      rel_list vs. forall_list2
>>      un_Cons1 vs. hd
>>      un_Cons2 vs. tl
> Duplicate constants are not a killer argument per se. But why not generate those
> constants only if the definer asks for them explicitly?
Let's distinguish between A = {hd, tl} and B = {map, set, rel}. The 
constants from B are an integral part of the package---they form 
together with the type a BNF. Thus, they will always be "generated". The 
question is whether they are exposed to the user.

The selectors (A) indeed belong in the category of syntactic sugar, and 
we have an option to not generate those constants. Here, the question is 
about the default behaviour.

>   Does any programming
> language give you all of them by default? Have you made a study of existing
> Isabelle datatypes to see how frequently people defined their own
> map/set/rel/selectors?
We did not make a global study. But let me pick a random example "'a 
rexp" from your Regular_Set AFP entry. The theory used to define both 
the set function (for atoms) and the map function (for generating marked 
regular expressions IIRC). Defining those functions are essentially 
boring bureaucracy (each taking 7 lines, not to mention the theorems one 
needs to prove about them). In the development version of the AFP, I 
changed those to be generated by the new package, saving some lines of 
code and allowing the reader to focus on more interesting constants.

The relator is in my experience slightly less user-relevant but it 
constitutes an important bridge to the Lifting and Transfer tools.

Dmitriy