Hi Florian,
I understood that much. What I was hoping for was an answer on a more
technical level. The definition + interpretation pattern seem a
useful thing to have. But it sounds like, if you change the main
interpretation command like this, you will break it for intended use
cases (or at least clutter up user's theories with definitions they
might not want to have).
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).
Clemens
Quoting Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de>:
Hi Clemens,
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«.
This looks to me like a special case, but maybe one that is encountered
frequently when generating code. What do you intend to do? Provide a
special version of interpretation for code generation?
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 ...
with --[ ... ]--> being the interpretation morphism. The interpretation +
defines pattern was something which could be accomplished rather simple,
so I decided to make an experimental start with this in December 2010.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
