[isabelle-dev] Notes on datatype_new list

[Makarius]

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