[isabelle-dev] Notes on datatype_new list

[Tobias Nipkow]

I can only agree with what Makarius has observed but would go one step further:
the new definition of list is truly baroque and unsuitable for beginners, but
beginners are bound to look at it. Sometimes languages have to reduce complexity
to cater for novices. The three types bool, nat and list should be defined in
the plain standard manner.

Tobias

On 23/05/2014 23:39, Makarius wrote:
> The following is relevant to the BNF guys, with continously growing team
> strength (according to Isabelle/aa7f051ba6ab).
> 
> Today we've had a tutorial with mostly fresh users, which is always useful to
> see remaining snags.  There were also 2-3 experienced Coq users, who have the
> usual problems of a different kind: being stuck to Emacs or using strange Window
> managers like Xmonad.
> 
> 
> Examples for beginners usually use the list datatype, and the Prover IDE makes
> it easy to find its definition.  Many users started looking in the HOL theories
> routinely, to get an idea how things are defined and how proofs are done with
> them.  Navigation makes the sources more accessible and raises the demands for
> their quality.  (I have ocasionally cleaned up typical hyperlink target
> positions in Pure, to make them look more obvious, if users happen to enter there.)
> 
> 
> For the new high-end BNF version of 'a list there were a few funny effects.
> 
> (1) Its definition looks terrific:
> 
> datatype_new (set: 'a) list (map: map rel: list_all2) =
>     =: Nil (defaults tl: "[]")  ("[]")
>   | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
> 
> It means it can no longer serve as example template for your own datatype
> definitions.  Note that I have already put the independent Seq.thy example in a
> prominent place some years ago, to decouple basic examples from the particularly
> difficult List.thy.
> 
> (2) Some users somehow used the "hd" and "tl" selector specifications above as
> suggestion to define primitive recursive functions, e.g. like this:
> 
> primref foo where
>   "foo [] = ..."
> | "foo (Cons hd tl) = ..."
> 
> Of course this fails, since these are constants, not variables.  It results in
> type-inference errors that beginners find hard to understand, and the Prover IDE
> has no position information about type errors yet.
> 
> (3) A genuine name space problem: "list" is concealed, and thus cannot be
> completed in semantic completion.
> 
> Looking briefly through the sources, I merely found some odd workarounds in
> BNF_Util.typedef -- it is usually worth investing the time to sort out the fine
> points that lead to such complications and eliminate them:
> (*TODO: is this really different from Typedef.add_typedef_global?*)
> 
> 
>     Makarius
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev