Anthony Bordg (Jul 05 2019 at 09:21): Anthony Bordg (Jul 05 2019 at 09:21):At some point, someone familiar with Isar should provide guidance for newcomers. :writing:
Anthony Bordg (Jul 06 2019 at 11:34):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.
maximilian p.l. haslbeck (Jul 31 2019 at 13:10):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: Apr 20 2024 at 01:05 UTC