Re: [isabelle] HOLCF



On Fri, 29 Jun 2012, Brian Huffman wrote:

On Wed, Jun 27, 2012 at 7:36 AM, Christian Sternagel
------------------------------------------------------------------
Domain Package:

* syntax annotations are allowed for constructors but do not work if given
separately with "notation", e.g.,

 domain 'a list = Nil | Cons (lazy 'a) (lazy "'a list") (infixr ":" 65)
works, but
 notation Cons (infixr ":" 65)
doesn't (due to being a continuous function)

Yes, you would need to define this syntax using an abbreviation, like
you do below for your fixrec functions.

Way back when we used to define functions with separate "consts",
"syntax", and "defs" commands, HOLCF used to provide a replacement
"syntax" command that knew about the continuous function type.

Unfortunately things are less consistent now, when each command is
responsible for handling its own syntax declarations.

Sorry, this does not make any sense. Things are *more* consistent now, because the full responsibility is to the packages, which fulfill that easily by handing over to standard Isabelle operations to introduce terms with mixfix syntax and specifications in the standard way. So it all works out uniformly in the post-Isabelle2005 era.

In contrast, the old scheme where 'consts' where separate had several conceptual problems. The one that might still be remembered is the "unify consts" problem: since an earlier 'consts' declaration would already be polymorphic, a subsequent 'defs' (or derived form) would often get an unexpected type, or different types for different equations. Historically, this has led to some packages trying to "repair" type-inference in different ways. So old 'primrec', 'recdef', 'inductive' could give the user different versions of type-inference.


As already observed, abbreviations handle alternative syntax views better, but users need to write them down themselves.

Some packages like 'inductive_set' allow the user to include such abbreviations simultaneously into the specification -- they are recognized by the Pure == form. Thus old idioms like pretending that "(x, y) : R" is actually a judgement "x -R-> y" could be supported with reasonable add-on functionality to that particular package. This is not exceedingly elegant, but better than the old scheme based on 'translations', which does not quite fit into the local theory specification concept.


	Makarius


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.