Search code examples
isabelle

Can I use negated versions of arbitrary symbols in Isabelle?


Isabelle allows you to use symbols that are negated versions of certain other symbols. Examples are and . Is there a mechanism for getting negated versions of arbitrary symbols, like the \not macro in LaTeX?


Solution

  • Your question has two parts: whether arbitrary negated symbols can be used, and whether such symbols can be input with a convenient macro. Let's start with the first part:

    The Isabelle FAQ explains that JEdit converts mathematical symbols input in various ways to Unicode, and uses/displays the unicode symbol. Therefore, if your desired symbol exists in Unicode, there is a chance that you could use it directly (i.e. ctrl-c ctrl-v the symbol). For example, the following allows you to define "not exists":

    abbreviation notexists :: "(('a ⇒ bool) ⇒ bool)" ("∄") where "∄ Φ ≡ (¬ (∃x. Φ(x)))"
    

    However, not all unicode symbols are available. For instance, the italic nabla does not display correctly in jedit.

    Now to the second part of your question: as far as I know, such a macro doesn't exist. However, Isabelle has a similar macro mechanism for making symbols boldface. For example, \<bold> \<exists> will be displayed as a bold "exists" symbol. This shows that the macro functionality exists, and it could be possible to have a macro for negating symbols, as you suggested, in the future.