At some point, someone familiar with Isar should provide guidance for newcomers. :writing:

At least the key idea: Isar allows **structured proofs**. Hence, proofs in Isabelle are somewhat close to textbook-like mathematical proofs.

So, make use of Isar full capabilities and your proofs will look nice. In particular, you should be able to reflect something of the mathematical structure of a proof in a textbook or an article. Ultimately, this leads to **easy-to-maintain code**.

That's why the structured style is the preferred style in Isabelle. The alternative `apply`

style is fine when there is not much of a structure to reflect, for instance to perform computations.

I find Chapter 4 of Prog-Prove is a good introduction to Isar. Especially the proof patterns in Section 4.2 are helpful for beginners.

Last updated: Aug 15 2022 at 02:13 UTC