Re: [isabelle] 5 proofs of concept satisfied and awesomeness revisited

On Thu, 12 Jul 2012, Gottfried Barrow wrote:

(3) Can the syntax of Isabelle be made to look very, very mathematical?

I already knew about the available math symbols, and the structured proofs, which was part of the initial attraction. I showed in a recent email that Isar identifiers can be made to look mathematical. Let no man or woman say that single, subscripted Latin, Greek, mathcal, or mathfrak alphabet characters do not meet the requirements of looking mathematical.

For those who don't know, an Isar identifier can use 0-9, ', and _, though it can't start with those characters. In addition, it can use a-z, A-Z, \<a> - \<z>, \<A> - \<Z>, \<aa> - \<zz>, \<AA> - \<ZZ> (but not II and RR) , and the lower and upper case Greek alphabet, such as \<alpha>. You can use \<^isub> and \<^isup> followed by the aforementioned characters anywhere you want, and as many times as you want. That's some major naming options, compared to most programming languages.

Note that concerning the prover backend, both \<II> \<RR> *are* allowed within identifiers; the prover gets these ASCII sequences only. You don't see the corresponding unicode glyph in Isabelle/jEdit, though. (The traditional dropout is \<lambda>, which is still not possible in identifiers as \<lambda>' etc.)

The problem of \<II> and \<RR> is an overlap with the Unicode rendering of \<Re> and \<Im>. Unlike TeX, the second copy of fraktur I and R is missing from the Unicode 6.1 standard, cf.

  "Fraktur symbols

  This style is sometimes known as black-letter. Black-letter symbols
  already encoded in the Letterlike Symbols block are omitted here to
  avoid duplicate encoding."

Donald Knuth and the AMS knew better, and provided separate copies, with slightly different shape.

Our IsabelleText font happens to have I and R glyphs in the Fraktur slot unofficially, but I did not use them in the default mapping of Isabelle2012/etc/symbols. Instead of stretching unicode too far, I am considering to remove the default rendering for \<Re> and \<Im> instead, to make the fraktur alphabet more uniform.

(And yes, Unicode is notorious to require long explanations and considerations for seemingly trivial things.)


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.