*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Best practices for introducing domain specific notation*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Fri, 17 May 2019 10:55:44 +0200*In-reply-to*: <edbe3acd-4699-ed00-d527-79a6db98aa14@ut.ee>*References*: <edbe3acd-4699-ed00-d527-79a6db98aa14@ut.ee>*User-agent*: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.6.1

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 bundle no_foo_syntax begin no_notation foo ("**") end * In particular, I saw this pattern in the end of HOL/Library/Perm.thy, which I found interesting. subsection ‹Syntax› bundle no_permutation_syntax begin no_notation swap ("⟨_↔_⟩") no_notation cycle ("⟨_⟩") no_notation "apply" (infixl "⟨$⟩" 999) end bundle permutation_syntax begin notation swap ("⟨_↔_⟩") notation cycle ("⟨_⟩") notation "apply" (infixl "⟨$⟩" 999) no_notation "apply" ("(⟨$⟩)") end unbundle no_permutation_syntax 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 removed notation. > 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 your library. * 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? Best Alex

**Follow-Ups**:**Re: [isabelle] Best practices for introducing domain specific notation***From:*Lawrence Paulson

**Re: [isabelle] Best practices for introducing domain specific notation***From:*Dominique Unruh

**Re: [isabelle] Best practices for introducing domain specific notation***From:*Florian Haftmann

**References**:**[isabelle] Best practices for introducing domain specific notation***From:*Dominique Unruh

- Previous by Date: Re: [isabelle] Isabelle2019-RC2: Prover errors when using sledgehammer
- Next by Date: Re: [isabelle] Best practices for introducing domain specific notation
- Previous by Thread: [isabelle] Best practices for introducing domain specific notation
- Next by Thread: Re: [isabelle] Best practices for introducing domain specific notation
- Cl-isabelle-users May 2019 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list