[isabelle-dev] Interpretation [was HOL/ex/Set_Algebras]

[Makarius]

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