> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
