[isabelle-dev] Locale interpretation with mixins

[Florian Haftmann]

> The term "foundation" was actually introduced formally in one of the
> local theory target reforms by yourself, e.g. see
> http://isabelle.in.tum.de/repos/isabelle/file/38af9102ee75/src/Pure/Isar/generic_target.ML#l292

Indeed.  However, when stating »The idea has always been to rely as
closely as possible on the foundation without doing more extralogical
things than necessary.«, the term »foundation« is used in the broader
sense of »background theory«.

> 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?

OK, lets tackle the matter from that perspective.

One unifying approach (which is *not* simple) would be to extend the
concept of locales to cover definitions explicitly.

Currently we have

  def (in l)
    is realised by
  foundation-def + abbrev

which after interpretation (phi) leads to

  phi(abbrev)

What I always had in mind was that locales should keep book about
definitions explicitly., i.e.

  def (in l)
    is realised by
  locale-def
    is realised by
  foundation-def + abbrev

which after interpretation (phi) leads to

  phi(locale-def)

in the sense of the underlying target.  In particular, an interpretation
into another locale l' would result in

  def (in l')
    is realised by
  foundation-def + abbrev

An interpretation into the background theory would result in

  def (in -)

which is already foundational!

But a consequent exploration of this approach with explicit def
bookkeepings would, I guess, exhibit a lot of difficult questions (e.g.
some kind of sharing constraints for defs).  Moreover, it would not
overcome problems with the simplifier inside locales etc.

> So when the code generator sees an interpreted function application
> "loc.c t1 t2 t3 x y z" it should somehow do the right thing, in taking
> it as "(loc.c t1 t2 t3) x y z", and considering the inner part as
> "atomic entity" (and instance of c defined earlier in the abstract
> context).

I will elaborate on this in a separate mail, since here some non-trivial
things in the code generator architecture come together.

> Some months ago I mentally experimented with a notion of explicit
> "boundaries" for locale contexts and somehow follow the structure of
> interpretations.  This could help here, although in the first and second
> round of testing the hypothesis against the real system, I got deflected.
> It might also turn out to be too complicated as a concept.

I cannot grasp the concept of »boundaries«.  But maybe that's a
different story.

	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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20120922/647687c1/attachment.sig>