On Thu, 19 Apr 2012, Clemens Ballarin wrote:
Maybe what you want is an alternative command to 'interpretation'.
Creating definitions from definition to me is not interpreting something
in some other context by means of existing entities, but creating a new
instance of something. The interpretation command refrains from doing
so for good reasons (i.e. flexibility).
the story behind is not about syntax. It is really about the
simultaneous definitions. For a motivation, you can have a look at
the tutorial on code generation, section »Further issues«, »Locales
and interpretation«, where the pattern behind interpretation plus
definition is spelt out using the constant »funpows«.
the intension is:
def (in foo) bar where ...
--[ interpretation foo: ... ]-->
def (in -) bar where ...
rather than
def (in foo) bar where ...
--[ interpretation foo: ... ]-->
abbreviation (in -) bar where ...
I've recently been through all the locale (and local theory) code to do
some polishing, without daring to touch this sophisticated infrastructure,
especially mixins.
The issue concerning seamingly defs via abbreviations vs. actual defs via
definition above reminds me vaguely of the pending issue from our national
debts account, to make proof tools like the Simplifier aware of the
opacity of certain terms loc.c t u v; maybe the codgen issue is a
corollary of that.
Right now, I cannot really pay attention to this important thread, we
should continue it at some point after the release.
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
