It would be nice if "interpretation" were enhanced with "defines", in which case people could make use of it w/o having to learn about and load "permanent_interpretation" (whose future is still under discussion).
Tobias On 29/10/2015 11:31, Florian Haftmann wrote:
Hi Clemens et al., let me put things in a broader perspective. I think we have two views on the whole machinery: * The algebraic view with locales, sublocale statements and (somehow global) interpretation statements. This view is important because it essentially describes the implementation of the whole thing. * The »local everything« view, where you have certain targets which allow certain operations, most notably »notes«, »defines«, and something which might internally be called »subscribes«, a permanent connection to existing locales covered by a locale expression. Internally, this falls back to existing mechanism, particularly »sublocale« for subscriptions into locales. But note that this is only the typical sandwich principle of target implementations, similiarly to definitions in locales which are essentially global definitions plus an abbreviation, which appears in theory text as plain »definition« nonetheless! (Also note that »subclass« is something special between type classes only, it is not a generic »local everything« construct.) We may well come to the conclusion that both views are legitimate to be present in user space, i.e. as isar keywords; although this is not very common in Isabelle, it may be attributed to the complexity of the machinery itself. However I forsee two possible future extensions where both notions are in conflict an a decision has to be made. Starting point: there has been the decision that »interpretation« in confined contexts (locales, classes, nested contexts, …) denotes epheremal interpretation. This fits nicely with »interpret« in proofs. But a) Also a theory is a confined context »theory … begin … end«; although we are technically far off from that, in future it might be possible to issue interpretation epheremal inside a particular theory only, and in the current setting this would just be »interpretation«, demanding an alternative keyword for subscriptions into theories. b) Similarly, also interpretation in a »context … begin … end« block might include a subscription into the surrounding target, leaving additional premises in the results of subscription. As a possible example, think of conditionally complete lattices which subscribe to a existing complete lattice locale under the premise of an additional predicate. Again, if the surrounding target is a theory, how would the keyword look like, as »interpretation« is already needed for epheremal interpretation? So, if we want to maintain both views in the long run consistenly, we must 1) either find an alternative keyword for interpretation/subscription into theories 2) or find an alternative keyword for epheremal interpretation. In the light of this, some minor remarks:Your 'permanent_interpretation' lets users make some definitions followed by, depending on the context, an interpretation or a sublocale declaration.Note that it is just a restriction of the current implementation that permanent_interpretation requires either a theory or a locale/class target; each target is able to provide its own implementation for that, and currently only these to do so.It also blurs the distinction between 'interpretation' and 'sublocale' by calling the latter 'permanent_interpretation' when in a locale context, but not at the level of theories, but instead calling the former 'permanent_interpretation' at the level of theories.This »blurring« is inherent in the »local everything« approach. »definition« in locale targets is essentially an abbreviation, but called that nonetheless.It should be kept in mind that in the current design the 'interpretation' commands are effective for the lifetime of their context: in theories they are therefore permanentIt is not clear whether the »lifetime« of theories should exceed the final »end« or not.Certainly, your work has partly been inspired by the feeling that the current locale commands only provide the bare basics for manipulating locales. For example, basing an interpretation or sublocale declaration on definitions is certainly something that could be done in a fancier manner.According to my feelings, the whole locale machinery is an excellent and powerful part of the systems. The addition of mixin definitions as special case of mixin rewrites do not touch the foundations (locale.ML / expression.ML) at all – there is no restriction to achieve the same result withotuh them.The situation is perhaps a bit similar to that of 'axclass' several years ago, where your work on type classes has improved the user experience dramatically. If you would like to bring locales forward, you might consider developing ideas along those lines. The required definitions and proofs for an interpretation could for example be collected in a dedicated context in a step-by-step manner similar to that of class instantiation. Your work also seems to be inspired by the desire to gradually rename 'sublocale' to 'interpretation', which I find surprising, because, compared to classes, 'sublocale' is the direct analogue of 'subclass' and 'interpretation' is the direct analogue of 'instantiation'.Clemens On 13 October, 2015 15:13 CEST, Florian Haftmann <florian.haftm...@informatik.tu-muenchen.de> wrote:Recently in private discussion there was the question what the supposed future of permanent_interpretation is supposed to be. It looks as follows: Step 1) * Put »permanent_interpretation« into Pure directly.Step 2) * Careful revisiting of the documentation to emphasize the presence of permanent_interpretation. * »permanent_interpretation« as leading construct in the distribution and the AFP as far as appropriate Step 3) * Discontinue theory-global »interpretation«, which then is just a degenerated form of »permanent_interpretation«. * Discontinue locale-level »sublocale«, which then is just a degenerated form of »permanent_interpretation«. There will definitely be one release to breath between step 2 and step 3. 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_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev