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.

### Like this:

Like Loading...

*Related*

Tags: Isabelle, Isabelle 2009, readability

This entry was posted on April 22, 2009 at 12:06 am and is filed under announcements. You can follow any responses to this entry through the RSS 2.0 feed.
You can leave a response, or trackback from your own site.

## Leave a Reply