>> Let those thoughts sink further few days. If there is no veto until Apr >> 7th, I would go ahead to turn the patches upstream. > > Well, here is my veto.
OK. Let's go one step back. As a preamble, note that I do not care much about »teminology«, but have to give some ephemeral names to things, not yet graved into stone, to be able speak about them. So lets compare our suggestions systematically. I refer to the most condensed statements available in this thread. Your suggestion has been: > a) relating two locales to each other (such as "a total order is a lattice"): > > context B begin > … > end > sublocale B < A'' > > b) Non-persistent interpretation > > context B begin > ... > interpretation A > ... > end > > makes the interpretation of A available in the block up to the closing 'end'. > The interpretation will not be persisted; results are only available > temporarily to aid establishing some results in B. Your argument for a separate top-level sublocale command has been that it adding a dependency should not happen in a non-global context. I do not follow that argument for two reasons, a) on in the frontend: > What you currently have in many places (e.g. > http://isabelle.in.tum.de/reports/Isabelle/file/757fa47af981/src/HOL/Lattices.thy) > is the pattern. > > context B begin > … > end > > sublocale B < … > > context B begin > … > end > > sublocale B < … > > context B begin > … > end > > When giving up the paradigm that sublocale dependencies may only be > introduced on the global level, you end up with sth. like > > context B begin > … > interpretation … > … > interpretation … > … > end > > which is compacter and more intuitive. b) The unification of today's »interpretation« and »sublocale« is already inherent in the existing code and needs »only« be unburried by surgery. I have transformed your argument concerning sublocale to the statement that * interpretation with permanent effect (what I have been calling subscription) and * interpretation without permanent effect should be issued by different keywords, to make the distinction clear and to disambiguate situation like context B begin … interpretation … end Note you could disambiguate that by requiring that each interpretation without permanent effect resides in an unnamed context begin … end block, but this would result in a bulky structure either, with closing ends dangling towards the end: context B begin … context begin … interpretation … … context begin … interpretation … … end … end … end So, I argue for separate keywords here. Overall, my ideas are not driven by a certain desired behaviour. It is the code »as it is« which suggests the full integration of locale interpretation with local theories, as I have shown in the consecutive series of patches opening this thread. Cheers, 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
