[isabelle-dev] Notes on datatype_new list

[Andrei Popescu]

>> datatype_new (set: 'a) list (map: map rel: list_all2) =
>>    =: Nil (defaults tl: "[]")  ("[]")
>>  | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)


>> Can you explain the squiggle =: above?  I did not find it in the manual
>> nor in the sources so far.  It seems to be special to main HOL datatypes.

> what it does is indicate for Nil that a discriminator (of type "'a list => bool") 
> should not be provided, but instead equality with Nil should be used.  
> This option seems to only be available for nullary constructors.  

A couple more notes on this: 


The places before the constructor names,  like the one before Nil where "=:" 

currently stands, can be used to give any discriminator name, as in 


datatype_new (set: 'a) list (map: map rel: list_all2) =
    myDiscriminatorForNil: Nil (defaults tl: "[]")  ("[]")
  | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)

which yields myDiscriminatorForNil :: "'a list => bool" together with the relevant facts.  

The default is to generate a discriminator with name built from the constructor, here is_Nil. 

Note however that for lists a discriminator is_Cons is *not* generated unless the user explicitly 

requires one, since the datatype has only two constructors and it is more convenient to use the negation 

of is_Nil instead of is_Cons.  However, if the datatype has more than two constructors, as in 

datatype_new (set: 'a) listBlah (map: map rel: list_all2) =
    Nil (defaults tl: "[]")  ("[]")
  | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
  | Blah

then discriminators are produced for all of them: is_Nil, is_Cons, and is_Blah.

Jasmin has polished these to the extreme.  

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2013-2/doc/datatypes.pdf


Andrei