This question was closed as off topic:
Some have said now that "off topic" was not the right choice for closure, but with it's x minutes of fame, the question is now being rejected on other grounds.
I'm not going to edit the question to try and make it more acceptable, but I try to counter the claim that this question has very little or no real substance to it, the question being, "Is there a way of making this more readable?"
Below, I provide primary and secondary evidence to support my case. The primary evidence will be the PhD dissertation of Makarius Wenzel, who is one of the three principal developers of Isabelle, and who I have no affiliation with.
The secondary evidence is my own use of Isabelle, and the importance to me that Isar can be tweaked to be more readable than most programming languages. At the bottom, I will include an image showing a little bit of Isar as I've used it.
Isar - readability was on Wenzel's mind a long time ago
Wenzel's dissertation was published about 2002, and the link is here:
By doing more than mentioning the title of his dissertation, I'm probably belaboring the point. The document title is Isabelle/Isar - a versatile environment for human-readable formal proof documents.
"Isar" is actually an acronym, and it means "Intelligible semi-automated reasoning", where it appears that "intelligible" is a synonym for "human-readable".
A little context
It might help to know some of the history of Isabelle to understand where Isar fits into the scheme of things.
Larry Paulson graduated from CalTech with a B.S. in math, then received a PhD in computer science from Stanford, where afterwards, at Cambridge, he extended the work of Robert Milner and Mike Gordon by developing a generic "proof machine" called Isabelle/Pure (From LCF to HOL: A Shorty History, by Mike Gordon).
Tobias Nipkow from TUM then got involved and was instrumental in developing a logic called Isabelle/HOL on top of Isabelle/Pure. Isabelle/HOL has gained a relatively big following, since it caters more to the programming crowd, where Paulson's Isabelle/ZF never caught on much. Wenzel then got his PhD under Nipkow at TUM, where he put the high-level language Isar on top of Isabelle/Pure.
The three developers are still actively developing Isabelle, along with lots of other developers around the world. If you were to call them all software gurus, they would feign modesty and tell you that you're mistaken.
Structured proofs, did I forget to mention that?
There is the graphical syntax of Isar, but readability is, even more probably, heavily tied into the fact that Isar facilitates structured proofs. A structured proof is a forward proof which is geared more to how humans think. Basically, it's a series of implications,
A ==> B ==> ... ==> Q, therefore, A ==> Q.
Please correct me if I'm wrong.
I gave the short history lesson so I could tie it into my point here about structured proofs. This thing about readability being a big part of Isabelle isn't an accident. The principal developers and their legions made it happen. The older code from the 1980's is based on tactics rather than structured proofs, and it's heavy in ML rather than Isar.
Do I sound like I'm an authority on all this? I'm not.
Me and my preferences
I'm gone on too long, but I wouldn't be using Isabelle as a product if it didn't have features which allow me to produce code that is somewhat meant to be read, rather being like normal code, which is only read if necessary.
I include an image below. It's of a very simple, structured proof. If you think that's the way everyone does things, you would be thinking wrong. If you look at the source code for Isabelle/HOL, which is on the Web, they didn't concern themselves with making it extraordinarily readable. Even with an essay, you have to work to make it readable.
If the code in my image doesn't look like any coding is really being done, it's because the automatic proof methods, such as
metis hide most of it.
Also, Isabelle is not all sugar coated candy for coding wimps, there's ML to be used, which has syntax which isn't nearly as nice as Haskell, though they're both functional programming languages.
When you close questions like the OP's, you potentially deprive me of an easy lesson
The learning curve for Isabelle is huge. With Isabelle, you have at your disposal detailed proofs, then automatic proof methods, like
metis, and then automatic theorem provers, which Sledgehammer uses to find
I have a need to learn how to do detailed, structured proofs, but the power of the automated methods keeps me going, so I learn a little here and there about structured proofs, which ultimately is all tied into natural deduction logic, which ends up being one more thing on the learning curve.
Simply put, the simple code template that the OP used was instructive to me.
The slight variation he gave as his own answer will be useful to me. I could have already worked through numerous Isabelle manuals and tutorials, yet not have seen Isar syntax used in that way. It's like Perl, there's lots of ways to do things
Did he ask a good question? It was good enough for me. If he wouldn't have asked the question, he wouldn't have given the answer, and it will be a very useful tip.
People can edit this for brevity if that's what's needed.
Most people will not be familiar with Isabelle as language, so here are a few links. It's a great product.
- Isabelle is a language/platform that is primarily categorized as a a proof assistant, another major proof assistant being Coq.
- [Isabelle web site] isabelle.in.tum.de.
- [Isabelle wiki] en.wikipedia.org/wiki/Isabelle_(proof_assistant)
- [Coq web site] coq.inria.fr
- There is Isabelle/Isar as the proof language, and Isabelle/HOL as the programming language.
- [Isabelle/HOL web page] isabelle.in.tum.de/dist/library/HOL/index.html
- The foundation for Isabelle/HOL is Isabelle/Pure and Isabelle/ML.
- The cornerstone of everything is ML, a functional programming language that preceded and influenced Haskell as a functional programming language.
- [ML wiki page] en.wikipedia.org/wiki/ML_(programming_language)