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

2012-04-19 Thread 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.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

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

2012-04-19 Thread 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___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev