Re: [isabelle] Some comments on CONST/\<^const> mechanism in 2008



On Fri, 20 Feb 2009, Dr. Brendan Patrick Mahony wrote:

> Sorry to be slow to the party, but the significance of the way the 
> definition/notation mechanism now works has only just started to sink 
> in.

What you have discovered here is called "authentic syntax" in internal 
jargon.  It merely means that things work as expected, i.e. the syntax is 
really attached to certain entities in a robust fashion.

Right now, the dividing line for unrobust legacy syntax and authentic 
syntax is mostly the "local theory" interface.  Thus newer commands like 
'definition' and 'notation' already benefit on it, as well as 'inductive', 
'function' etc.  As we move on to make old packages fit for the local 
theory concept, syntax will also improve, although this is only a small 
thing compared to the full power of local theories.  (Both of these 
renovations coincide mostly by accident, though.)

Anyway, upgrading to authentic syntax is not completely trivial due to old 
syntax translations, which usually expect syntactic const names in the 
(fragile) unqualified form.  Right now you can already use the 
@{const_syntax foo} antiquotation in ML, or "CONST foo" in translation 
rules, to make things fit for the future.


> Is there anyway include a const declared in the old way, say because it 
> is being defined by extension rather than intension?

You can try it like this:

  abbreviation "foo == old_foo"  (mixfix)

which will produce an authentic const "foo", corresponding to some other 
term, which happens to be based on non-authentic syntax (or no syntax at 
all).


> Are type names included or planned for inclusion is a similar scheme?

In the end, yes.  It will probably happen in the next round, when we 
provide typedecl/typedef interfaces for local theories (this is a bit 
tricky, because local theories do not really support type constructors).


	Makarius





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