Am 26.05.2014 um 12:34 schrieb Lawrence Paulson <l...@cam.ac.uk>: > What new users see when they look at the actual definition of lists is not > that important. There are many, many situations where the actual definition > of something is much more complicated than the idealised version that one > would use for teaching.
Indeed, this is an old observation that has been repeated over and over throughout the history of computing. The definitions of most library functionality in various programming languages looks obfuscated. Take for example "stdio.h" in C. On my "user-friendly Mac", it looks like this: __BEGIN_DECLS void clearerr(FILE *); int fclose(FILE *); ... int fgetpos(FILE * __restrict, fpos_t *); char *fgets(char * __restrict, int, FILE *); #if defined(_DARWIN_UNLIMITED_STREAMS) || defined(_DARWIN_C_SOURCE) FILE *fopen(const char * __restrict, const char * __restrict) __DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_3_2, __DARWIN_EXTSN(fopen)); #else /* !_DARWIN_UNLIMITED_STREAMS && !_DARWIN_C_SOURCE */ FILE *fopen(const char * __restrict, const char * __restrict) __DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_2_0, __DARWIN_ALIAS(fopen)); #endif /* (DARWIN_UNLIMITED_STREAMS || _DARWIN_C_SOURCE) */ int fprintf(FILE * __restrict, const char * __restrict, ...) __printflike(2, 3); In Lisp, I'd like to see how they "define" nil, cons, car, cdr, and cadadaar. Even staying with Isabelle, all types defined before "'a list" and "'a option" are good examples -- products, sums, nats, unit, bools are all defined in a terrible way. Now, with jEdit allowing to jump to the definition (as opposed to the documentation), I can see that this becomes a more acute issue Yet again I would argue that the "terrific" and "truly baroque" specification of "list" is better than products, sums, nats, unit, bools. > I have almost never found destructors or discriminators to be useful. I'd be curious to understand why. Perhaps you could elaborate in a separate thread. With multiple constructor datatypes, it is true that one often ends up needing a "case" expression anyway, but there are still many situations where you need the discriminator (or a '=' or '~=' that amounts to one) in an assumption, and then it's convenient to use the selectors directly, e.g.: lemma rotate1_hd_tl: "xs \<noteq> [] \<Longrightarrow> rotate1 xs = tl xs @ [hd xs]" Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev