1

I'm trying to learn to use Isabelle/HOL. I thought, "Hey, a tutorial written by some of the folks who developed it would be great", and so looked at https://isabelle.in.tum.de/doc/tutorial.pdf which has a publication date of Aug 15, 2018. In trying to work through examples, though, I find things like this in the text:

"The classic Isabelle user interface is Proof General / Emacs by David Aspinall’s. This book says very little about Proof General, which has its own documentation." (page iii)

"If anything strange happens, we recommend that you ask Isabelle to display all type information via the Proof General menu item Isabelle > Settings > Show Types (see Sect. 1.5 for details)." (page 5)

The problem is that Proof General appears to no longer work with Isabelle (see Isabelle2016 and Proof General). I'm baffled on why a tutorial would base itself on out-of-date software, but my real question is this:

"Is there somewhere that I can learn to do even the simplest things in Isabelle 2017?"

John
  • 509
  • 1
  • 6
  • 18

1 Answers1

4

As of 2018, the only IDE that is supported for Isabelle is Isabelle/jEdit, which is included in the distribution you can download from the Isabelle website. There is an experimental VSCode plugin that is under active development, but I would recommend using Isabelle/jEdit for the time being.

The tutorial you found is listed on the website as one of the ‘Old Manuals’. It is severely outdated in many respects and should not be used anymore. The publication date is probably meaningless since it is the date of when the PDF was generated, not when the text was written. Some people have lobbied to have that tutorial removed from the website entirely, and your experience seems to confirm that we should indeed do that.

One of the best ways to start learning Isabelle is probably the book ‘Concrete Semantics’ (free online version available). Its first half is basically an introduction to Isabelle/HOL with lots of exercises. There is also the ‘Programming and Proving’ tutorial on the Isabelle website, which is almost identical to the first half of ‘Concrete Semantics’.

However, it focuses on applications in computer science (semantics of programming languages and a bit of functional programming). I'm not sure if there is a good tutorial about how to do mathematics in Isabelle; in any case, mathematics tends to be more difficult to do in a theorem prover for beginners because the gap to informal paper reasoning is larger. So I recommend ‘Concrete Semantics’ even if you are ultimately interested in formalising mathematics.

By the way: You mentioned Isabelle2017, but there really is no reason to use that instead of Isabelle2018, which is the most recent version at the time of writing this answer.

Manuel Eberl
  • 7,858
  • 15
  • 24
  • I'm supposed to trust a bunch of folks who can't distinguish between an authorship date and a pdf-creation date as the folks who'll tell me if software is correct? :) Anyhow, thanks for the pointer. I asked about 2017 because that's the version I worked with when last this frustrated me enough to make me give up. (Sigh.) – John Dec 13 '18 at 17:21
  • There IS a rather nice tutorial on doing math in Isabelle at https://dream.inf.ed.ac.uk/projects/isabelle/Isabelle_Primer.pdf ... but it's unfortunately tied to Proof General (although I'm sure that an advanced user could read past this). – John Dec 13 '18 at 17:28
  • Indeed you can just ignore all the references to Proof General. It doesn't change much. However, the precise names of certain theorems/definitions of concepts can sometimes change slightly between releases of Isabelle. Also, that maths tutorial covers only fairly basic things; to do ‘real’ mathematical proofs in isabelle, it is very helpful to be already proficient in Isar proofs and how to use the automation. Moreover, using things like limits and integrals require quite some getting used to. – Manuel Eberl Dec 13 '18 at 21:28
  • Fortunately my goal is to do some proofs in synthetic projective geometry, so nothing terribly fancy -- certainly no fancier than the kind of group theory stuff that's well-documented on the Isabelle website, for instance. But as you point out, some understanding of Isar and automation is clearly useful even there. – John Dec 14 '18 at 02:00
  • Hi, do you have suggestions of tutorial/learning materials in 2022? Thank you! – ch271828n Nov 26 '22 at 01:55