Re: [isabelle] Overriding... [Problem solved by \<^isub> art]



So you might think, or me, that there's really only two non-alpha-greek-numeric characters available for separating words in identifiers: tick and underscore.

But then you, or I, would be wrong because of \<^isub> and \<^isup>. These would bump up the use of tick and underscore to 6 available characters.

Well, once it's occurred to you, or me, that \<^isub> and \<^isup> can be useful for naming tricks, like creating space in a more subtle way, then surely you think, or I think, there are other possibilities for using \<^isub> and \<^isup> for identifier tricks.

The solution is simple. I introduce a function, such as "be bounded by", in a LaTeX theorem environment, named using spaces. It's understood that "be bounded by" will be named in Isar with different characters to separate the words. And, after all, the Isar code will be shown to them. It's not too much to expect that people will make the connection between "be bounded by" in some formal-non-formal natural language proof, and the "be_bounded_by" in the Isar proof (or be_bounded_by with something else in place of "_").

And typing \<^isub>' isn't that bad with the "-_" shortcut.

It's also not a trivial thing to have subscripts available for use in identifiers, in general.

I attached a screen shot of the Verbatim environment with \<^isub>' being used for spacing. It looks good in jEdit too. These kind of options are always good to have, even if you decide not to use them.

--GB

theorem emS\<^isub>'is\<^isub>'unique: "u = emS \<longleftrightarrow> (\<forall>x::sT. \<not>(inS x u))"
  apply(auto)
  oops

Let A be'bounded'by b.

Let A be\<^isub>'bounded\<^isub>'by b.


Attachment: isub'forSpace.jpg
Description: JPEG image



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