[isabelle-dev] Deprecating legacy ASCII symbols?

[Michael Norrish]

> On 1 Jul 2015, at 00:57, Makarius <makarius at sketis.net> wrote:
>
> On Tue, 30 Jun 2015, Larry Paulson wrote:
>
>> It is interesting to look at competing systems and note that every one of them appears to be fully committed to a plain ASCII syntax as the only way of writing a formula. I think it may still be premature to abolish having ASCII even as an alternative syntax.
>
> Maybe some HOL4 guy can explain the details.  They certainly do have ways to use non-ASCII, probably not as pervasive as for Isabelle.  (I think they also have blue, green, brown variables.)
>

We’ve had support for arbitrary user-chosen UTF8-encoded Unicode symbols since 2008, both in input and output.  Emacs has pretty reasonable support for inputting Unicode if you turn on the TeX-input-method.  Our emacs and vim editing modes further provide keybindings for common symbols (C-S-1 for ∀ is one more modifier key to press than S-1 (assuming that ! is shift-1)).

We keep material under src/ as pure ASCII, but our examples/ directory is full of Unicode.  E.g.,

    val oleast_intro = store_thm(
      "oleast_intro",
      ``∀Q P. (∃α. P α) ∧ (∀α. (∀β. β < α ==> ¬ P β) ∧ P α ==> Q α) ==>
              Q ($oleast P)``,
      rw[oleast_def] >> SELECT_ELIM_TAC >> conj_tac >-
        (match_mp_tac ordlt_WF0 >> metis_tac[]) >>
      rw[]);

    val ordSUC_def = Define`
      ordSUC α = oleast β. α < β
    `

I’m not sure why I used the ASCII implication above rather than the Unicode version, but it does illustrate the way in which the input symbols can be freely mixed.

Perhaps as a leap of faith, we believe that UTF8-encoded Unicode will be just as readable as ASCII to the archaeologists of the future. Certainly, in the present day, it’s nice to be able to read and access sources with tools such as less, grep etc. and to see stuff like the above.

Michael



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.