[isabelle-dev] Notes on datatype_new list

[Dmitriy Traytel]

Am 26.05.2014 11:07, schrieb Jasmin Blanchette:
> 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
Here are some compromise options that lighten the presentation, but 
still reusing the conveniences provided by the package (which are not 
only the constants, but also many theorems about the constants):

(a)

datatype_new 'a list =
Nil (defaults un_Cons2: "[]") ("[]")
| Cons 'a "'a list" (infixr "#" 65)

abbreviation "map ≡ map_list"
abbreviation "set ≡ set_list"
abbreviation "list_all2 ≡ rel_list"
abbreviation "hd ≡ un_Cons1"
abbreviation "tl ≡ un_Cons2"

(b)

datatype_new 'a list =
Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)

abbreviation "map ≡ map_list"
abbreviation "set ≡ set_list"
abbreviation "list_all2 ≡ rel_list"

Option (a) is closest to the original definition---the only difference 
is in the annotation defining the default value of "tl Nil". However, 
not using the selector requires us to use the automatically generated 
name un_Cons2, which makes this option too obscure.

My favourite (next to the current definition from the repository) is 
option (b)---giving name to the selectors makes the "defaults" 
annotation easy to parse. And even major functional programming 
languages support similar selector annotations (e.g. via record syntax 
for data in Haskell).

For both options we probably would change the package to generate the 
discriminator "%x. x = Nil" by default for nullary constructors.

Dmitriy