Stream: General

Topic: Isar


view this post on Zulip Anthony Bordg (Jul 05 2019 at 09:21):

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

view this post on Zulip 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.

view this post on Zulip 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: Aug 15 2022 at 02:13 UTC