Re: [isabelle] HOLCF
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: Re: [isabelle] HOLCF
- From: Makarius <makarius at sketis.net>
- Date: Thu, 5 Jul 2012 17:59:34 +0200 (CEST)
- Cc: Christian Sternagel <c-sterna at jaist.ac.jp>, Brian Huffman <huffman at in.tum.de>
- In-reply-to: <CAAMXsiYCztT=PCbSTRVEUXWGS-uGJrMUjOkdjj40XDFsjH5eDA@mail.gmail.com>
- References: <4FEA9BC8.firstname.lastname@example.org> <CAAMXsiYCztT=PCbSTRVEUXWGS-uGJrMUjOkdjj40XDFsjH5eDA@mail.gmail.com>
- User-agent: Alpine 2.00 (LNX 1167 2008-08-23)
On Fri, 29 Jun 2012, Brian Huffman wrote:
On Wed, Jun 27, 2012 at 7:36 AM, Christian Sternagel
* 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)
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and