[isabelle-dev] Notes on datatype_new list

[Thomas Sewell]

I have no particular stake in this issue, but I would think there was an 
option (c) which is to do the *opposite* of what Jasmin said about 
bringing the additional constant names etc as close as possible to 
wherever they "fit":

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

with
   set: set
   rel: list_all2
   map: map
   selectors: hd tl (default "[]")
     for "Cons hd tl"
   discriminator: "op = []"

Or something like that, excuse my made-up syntax. That clarifies what 
the datatype really is and where the associated constants came from 
(well, a little bit) without having to introduce any "funny" syntax to 
fit all the relevant options into a single bit of syntax. It also keeps 
all the data in a single command, so the package can do everything with 
the canonical names at once.

That's just my ten cents worth. As I said, I have no particular interest 
in this.

Cheers,
     Thomas.

On 26/05/14 19:56, Dmitriy Traytel wrote:
> 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
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev 
>