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

[Clemens Ballarin]

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.haftmann at 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
>
>