[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

Hi again!

> On our running gag list with have at least these related issues:
> 
>   * codgeneration as sketched above
> 
>   * behaviour of the Simplifier on seemingly atomic "constants" c (due
>     to abbreviations) that are actually of the form "loc.c x y z"
> 
>   * stability and expectedness of abbreviations, as they are printed
> 
>   * the Haftmann/Wenzel educated guess here
>    
> http://isabelle.in.tum.de/repos/isabelle/file/38af9102ee75/src/Pure/Isar/named_target.ML#l56
> 
>     which can be traced back here:
>     http://isabelle.in.tum.de/repos/isabelle/rev/9dd61cb753ae
>     (Fall/Winter 2007 was the time where we desparately tried to recover
>     from the 2006/2007 gap in the Isabelle release chain).
> 
> Is there any nice, sane, simple approach to all that?

A prerequisite to tackle any of these would be that the current context
could be queried for a mapping from names to terms
  f ~> t
expressing for each entry that term »t« morally corresponds to a
symbol/definition »f« in the current context.  Then different tools
could use this information to react appropriately, e.g. the simplifier
could provide additional cong rules etc.

For code generation, there remains the problem that
a) an explicit constant is still needed and must be declared appropriately
b) a transformation of code theorems *before* they enter the bookkepping
is required in order fold the appropriate constant into the theorem.
The current infrastructure has only a preprocessor applied *after* the
internal bookkeeping (for reasons I will explain in a separate, long
promised mail), so this would add further complexity here.

Conclusion:

I still argue that in the short run it is better to have a special
»interpretation*« on top of the existing »interpretation« (which is not
supposed to be changed!).  The prototype of this »interpretation*« is
interpretation_with_defs.ML, and I deem that it would be better to
generalize the interpretation interface in expression.ML a little and
get rid of the almost-clones in interpretation_with_defs.ML.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 259 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20121004/270efc2d/attachment-0001.asc>