Isabelle 2009 released

The Isabelle team has released version 2009. Updating IsarMathLib to Isabelle 2009 was very easy. I only had to make a couple of corrections to proofs that used assumptions implicitly. The only more complicated change was related to renaming variables in the locale syntax.

Isabelle supports “locales” that are constructs that allow to limit the scope of definitions and notation. In IsarMathLib locales are used as kind of contexts  that hold certain assumptions and define notation specific to the some area of mathematics. For example, an IsarMathLib locale called ring0 contains an assumption that the sets form a ring. This locale assumption is then implicitly added to all theorems  proven in the locale. In case of the ring0 locale the set is the “carrier” of the ring, represents the addition and is the multiplication (recall that in ZF set theory binary operations are sets). Locales can form hierarchies in a way similar to classes in OO programming languages, inheriting assumptions and notation. In IsarMathLib locale field0 extends locale ring0 by adding an assumption that multiplicative inverses exist for all non-zero elements. Locales also allow to rename the variables inherited from the parent. In case of the field0 locale the carrier is named rather that , as is customary for fields. It is the syntax for renaming that got changed in Isabelle 2009. In Isabelle 2008 I could write

locale field0 = ring0 K

and the first variable in the ring0 locale could be used as in the field0 locale. For Isabelle 2009 it seems I have to write

locale field0 = ring0 K A M for K A M,

repeating the fixed sets of the locale twice. I can live with it, but it looks weird and programmish. The main reason I like the Isar proof language is that it is typically similar to what one would write in a standard (informal) mathematical proof. This change is a step away from this idea. I think it would be better to be able to write something like

locale field0 =  ring0 renaming R to K .

This way it would look a bit like Cobol and I am saying there is nothing wrong with that.

In addition to the old ProofGeneral interface the 2009 release contains an experimental interface written in Scala as a Jedit plugin. I am planning on checking that out.

Tags: Isabelle, Isabelle 2009, readability