Tutorial to Locales and Locale Interpretation

Locales are Isabelle’s approach for dealing with parametric theories. They have been designed as a module system for a theorem prover that can adequately represent the complex inter-dependencies between structures found in abstract algebra, but have proven fruitful also in other applications — for example, software verification. Both design and implementation of locales have evolved consider-ably since Kammüller did his initial experiments. Today, locales are a simple yet powerful extension of the Isar proof language. The present tutorial covers all major facilities of locales. It is intended for locale novices; familiarity with Isabelle and Isar is presumed.