[isabelle] Best practices for introducing domain specific notation
- To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Best practices for introducing domain specific notation
- From: Dominique Unruh <unruh at ut.ee>
- Date: Mon, 6 May 2019 15:50:08 +0300
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1
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
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and