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
