[isabelle-dev] Notes on datatype_new list

[Tobias Nipkow]

Just to be clear on this: the ability to get all of these functions for free is
marvellous! We are now discussion only the syntactic interface to that
marvellous functionality, how much is exposed by default, and in particular in
the defn of list.

Tobias

On 26/05/2014 12:14, Dmitriy Traytel wrote:
> 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