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 <nip...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to