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
