Re: [isabelle] Best practices for introducing domain specific notation
Hi Dominique, hi all,
This thread hasn't got much attention so far, but I think it touches an
issue that is worth discussing. I also want to learn more about this.
Am 06.05.2019 um 14:50 schrieb Dominique Unruh:
> 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).
I think locales were built mostly with the logical applications in mind.
I would consider their use for just syntax/extra-logical matters an
abuse, although that has been common...
> * 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 looked around a bit to see what others do with bundles today. Here are
some things I found:
* Sometimes there are "negative" syntax bundles in the style of
no_notation foo ("**")
* In particular, I saw this pattern in the end of HOL/Library/Perm.thy,
which I found interesting.
no_notation swap ("⟨_↔_⟩")
no_notation cycle ("⟨_⟩")
no_notation "apply" (infixl "⟨$⟩" 999)
notation swap ("⟨_↔_⟩")
notation cycle ("⟨_⟩")
notation "apply" (infixl "⟨$⟩" 999)
no_notation "apply" ("(⟨$⟩)")
This effectively gives users an "on/off" switch, although it is not
particularly pretty when the respective (no_)notation declarations are
stacked onto each other. A similar thing is done in the end of
HOL/Decision_Procs/Approximation.thy and in several places in the AFP.
* HOL/Main.thy also removes quite a bit of common syntax at the end, and
declares a bundle cardinal_syntax which contains some of the previously
> 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.
Given the observations above, I think in current Isabelle the best
practice for library developers would be:
* Provide a canonical entry point for users of your library.
* At the end of that entry point, remove any syntax that is specific to
* Declare a foo_syntax bundle that users can use to activate the syntax,
and possibly also a no_foo_syntax bundle.
> (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.
I think not everything was designed for being reused, and this is
probably ok, since AFP contains both libraries and applications. But
when something is used as a library, it should avoid syntax pollution.
Another interesting question is: What concepts should future-Isabelle
provide to make this more natural? I find the above pattern quite
verbose and somewhat unintuitive. Would extensible bundles help?
This archive was generated by a fusion of
Pipermail (Mailman edition) and