Re: [isabelle] Overriding reason not to use single quote or camelcase in identifiers?


Thanks for the interest, but first, please allow me to clarify why I won't be able to use antiquotations such as @{text foo_bar} at the point I start using Isabelle to create PDFs.

The limitation is that Acrobat's bookmarks can only predictably take basic ASCII characters, which I constantly forget until I see "stuff" or the "lack of stuff" in my PDF bookmarks. The bookmarks for chapter 4 of functions.pdf demonstrates the problem.

The antiquotation for section 4.2 resulted in numeric trash in the bookmark. I use the hyperref package, so I know about the problem from trying to use macros in section titles. My solution is to not get fancy in section titles; to not have a bookmark made from a complicated Latex macro, or use something like @{text foo_bar} in the title.

I heavily use PDF bookmarks. I have Latex macros which use the theorem environment for Isabelle theorems, lemmas, definitions, etc.. These macros also create a subsection entry into the bookmarks/table_of_contents using the name of the theorem. Consequently, I have to hard code the name so I don't get "stuff" or the "lack of stuff" in the PDF bookmarks. It's not an option to use fancy characters in the name, or to figure out later what character I want to use to separate words.

Secondly, it's obvious to me that the Isabelle Latex document processing is very powerful and should be the Latex tool of choice for most people producing Isabelle documents. However, for my needs, without having spent the time to get what I want through Isabelle, I have to stick with what I'm doing.

SHOW-STOPPER: It's vaguely coming back to me, but I'm pretty sure that
the show-stopper was my need for the Verbatim environment...

can you give a hint for which sake you are using verbatim?  In LaTeX it
mixes up to purposes

a) interpret source more or less literally

b) present result in typewriter

For each of these, there are different possibilities; especially b) can
be achieved with Isabelle without relying on verbatim.  a) is not so
simple, but there are ways to cope with involving ML (depending how
general it is supposed to be).

In looking at functions.pdf, I can see that Alexander is using a different font than other documentation PDFs. I guess this would be an example of your "b)". The italicized roman font hasn't always been to my liking for the Isar code, though typewriter font isn't all upside either, but I could probably find out how to make basic font changes by looking at the Isabelle Latex packages.

Bullet "a)" kind of represents why I want the Isar in a Verbatim environment. I'll say a little more below.

If your primary concern is how identifiers appear in natural language,
you can consider using your specific set of antiquotations where you can
modify identifiers programatically, in the extreme case using an
explicit substitution table.


This is an example of where, because of my multiple wants, in emphasizing one want, I forget another want that has a higher priority.

It's true that I want Isar identifiers to look good when mixed into a paragraph of natural language, but more importantly, I want Isar to look extraordinarily mathematical even in its raw form in a Verbatim environment, or on the jEdit screen. It happens to be that Isar gives me a good start. Even Latex doesn't guarantee you a good looking document. To get Latex looking really good, you have to make lots of artistic decisions, and do lots of builds, and stare at the screen a lot.

As to natural language, using my example "is_bounded_by", I wouldn't have to use that in an informal discussion, I could just say "is bounded by" and let the reader make the connection if it was obvious. Function over form, or form over function? It's always a compromise.

But back to why I want the Isar in a Verbatim environment. It's because, being in the student mode right now, I'm sympathetic with a student's needs. Code in a verbatim environment is basically saying, "This is what the code really looks like in the editor. If you open the source file, this is almost exactly what you will see. This is to make sure that you, as a student, don't have any questions about what exactly the code is."

Replacing identifiers with something significantly different is not something I would do. Clarity is more important to me than traditional looking language. More levels of abstraction, or more words requiring interpretation require more work from the reader, and more work to teach them what the vocabulary means.

Someday I could decide that line numbers in a Verbatim environment are just noise. What I'm doing will serve its purpose until I switch to something else.

Learning a little Latex here and there helps out. There's this Latex package for Fitch style diagrams: <>

Like most array type environments, it doesn't break well over multiple pages. I know just enough Latex to where I figured out how to modify it so that it uses longtable. Now, I can use page after page after page to do a natural deduction proof using a Fitch diagram.

Thanks for the suggestions.


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