[isabelle] Best practices for introducing domain specific notation



Hi,

one thing that has always been bugging me is the pollution of Isabelle syntax with domain specific notation.

For example, if I develop a theory involving inner products, I may want to introduce the notation "a · b" to make my theorems readable.

But that means that everyone who uses my theory will suddenly have my notation "·" in their namespace. Possibly conflicting with syntax from other theories.

Of course, there are mechanisms for local syntax. For example, locals and bundles. But I am not sure what the best practices are for using them.

 * With locales, I have the following problems: I cannot separate the
   notation from the logical context. For example, sometimes my
   definition will not be in any natural way part of a locale. For
   example, if I introduce a datatype and an operation on it (say,
   lists, and · for concatenation) then I would not know where to put
   the notation. Also, as far as I understand, with locales, there is
   no way to use the notation (like "including" with bundles) locally
   without actually using the whole logical context of the locale (in
   particular, if I want to use some notation from a locale in the
   statement of a lemma by using "(in name)", that lemma will then
   automatically be in the name space of the locale).
 * Bundles seem to have more flexibility. I can put a number of syntax
   elements together and include them as needed. Unfortunately, it
   seems that bundles are not extensible. For example, assume a theory
   that introduces a number of concepts throughout the theory (or even
   several theories). E.g., inner product, norm, closure of sets,
   Minkowski product, etc. If I want to use bundles, I have the
   following choices:
     o I introduce all the definitions at the beginning of the theory
       (and thus break the logical structure of the presentation) and
       make a bundle with syntax at the beginning.
     o I introduce all the definitions where they fit logically, and
       introduce syntax only at the very end (as one bundle). Then I
       cannot use the notation within the theories.
     o I introduce a new bundle each time I introduce new syntax (and
       end up with a lot of bundles that I can later combine into one
       bundle). That avoids the above problems, but it means that I
       pollute the name space with a lot of temporary bundle names.

What is the best approach here?

I feel that a clear guideline for such situations might be useful not just for me, but could also make the AFP more reuse-friendly. (Currently, I get all the notation introduced by an author when I import an AFP theory, even if I only want to use one theorem of theirs for a technical lemma.) I'd even go so far to say that I think on the long run it would be a good idea to require the absence of syntax pollution as part of the requirements for AFP submissions.

Best wishes,
Dominique.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.