src/HOL/ex/Locales.thy

 header {* Basic use of locales in Isabelle/Isar *}
 
 theory Locales = Main:
 
 text {*
-  Locales provide a mechanism for encapsulating local contexts.  While
-  the original version by Florian Kamm\"uller refers to the raw
-  meta-logic, the present one of Isabelle/Isar builds on top of the
-  rich infrastructure of Isar proof contexts.  Subsequently, we
-  demonstrate basic use of locales to model mathematical structures
-  (by the inevitable group theory example).
+  Locales provide a mechanism for encapsulating local contexts.  The
+  original version due to Florian Kamm\"uller \cite{Kamm-et-al:1999}
+  refers directly to the raw meta-logic of Isabelle.  The present
+  version for Isabelle/Isar
+  \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis} builds on
+  top of the rich infrastructure of proof contexts instead; this also
+  covers essential extra-logical concepts like term abbreviations or
+  local theorem attributes (e.g.\ declarations of simplification
+  rules).
+
+  Subsequently, we demonstrate basic use of locales to model
+  mathematical structures (by the inevitable group theory example).
 *}
 
 text_raw {*
   \newcommand{\isasyminv}{\isasyminverse}
   \newcommand{\isasymone}{\isamath{1}}

 
 subsection {* Local contexts as mathematical structures *}
 
 text {*
   The following definitions of @{text group} and @{text abelian_group}
-  simply encapsulate local parameters (with private syntax) and
+  merely encapsulate local parameters (with private syntax) and
   assumptions; local definitions may be given as well, but are not
   shown here.
 *}
 
 locale group =

   also have "\<dots> = x" by (simp only: left_one)
   finally show ?thesis .
 qed
 
 text {*
-  \medskip Apart from the named locale context we may also refer to
-  further ad-hoc elements (parameters, assumptions, etc.); these are
-  discharged when the proof is finished.
+  \medskip Apart from the named context we may also refer to further
+  context elements (parameters, assumptions, etc.) in a casual manner;
+  these are discharged when the proof is finished.
 *}
 
 theorem (in group)
   (assumes eq: "e \<cdot> x = x")
   one_equality: "\<one> = e"

     finally show ?thesis .
   qed
 qed
 
 text {*
-  \medskip Results are automatically propagated through the hierarchy
-  of locales.  Below we establish a trivial fact of commutative
-  groups, while referring both to theorems of @{text group} and the
-  characteristic assumption of @{text abelian_group}.
+  \medskip Established results are automatically propagated through
+  the hierarchy of locales.  Below we establish a trivial fact in
+  commutative groups, while referring both to theorems of @{text
+  group} and the additional assumption of @{text abelian_group}.
 *}
 
 theorem (in abelian_group)
   inv_prod': "(x \<cdot> y)\<inv> = x\<inv> \<cdot> y\<inv>"
 proof -

   also have "\<dots> = x\<inv> \<cdot> y\<inv>" by (rule commute)
   finally show ?thesis .
 qed
 
 text {*
-  \medskip Some further facts of general group theory follow.
+  \medskip Some further properties of inversion in general group
+  theory follow.
 *}
 
 theorem (in group)
   inv_inv: "(x\<inv>)\<inv> = x"
 proof (rule inv_equality)

   terminology of local parameters is affected the associated syntax
   would have to be changed as well, which is hard to achieve formally.
 *}
 
 
-subsection {* Referencing explicit structures implicitly *}
+subsection {* Explicit structures referenced implicitly *}
 
 text {*
   The issue of multiple parameters raised above may be easily
   addressed by stating properties over a record of group operations,
-  instead of the individual constituents.
+  instead of the individual constituents.  See
+  \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on
+  (extensible) record types in Isabelle/HOL.
 *}
 
 record 'a group =
   prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   inv :: "'a \<Rightarrow> 'a"

 
   In the subsequent formulation of group structures we go one step
   further by using \emph{implicit} references to the underlying
   abstract entity.  To this end we define global syntax, which is
   translated to refer to the ``current'' structure at hand, denoted by
-  the dummy item ``@{text \<struct>}'' according to the builtin syntax
-  mechanism for locales.
+  the dummy item ``@{text \<struct>}'' (according to the builtin syntax
+  mechanism for locales).
 *}
 
 syntax
   "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
   "_inv" :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)

   "x\<inv>"  \<rightleftharpoons>  "inv \<struct> x"
   "\<one>"  \<rightleftharpoons>  "one \<struct>"
 
 text {*
   The following locale definition introduces a single parameter, which
-  is declared as ``\isakeyword{structure}''.
+  is declared as a ``\isakeyword{structure}''. In its context the
+  dummy ``@{text \<struct>}'' refers to this very parameter, independently of
+  the present naming.
 *}
 
 locale group_struct =
   fixes G :: "'a group"    (structure)
   assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
     and left_inv: "x\<inv> \<cdot> x = \<one>"
     and left_one: "\<one> \<cdot> x = x"
 
 text {*
-  In its context the dummy ``@{text \<struct>}'' refers to this very
-  parameter, independently of the present naming.  We may now proceed
-  to prove results within @{text group_struct} just as before for
-  @{text group}.  Proper treatment of ``@{text \<struct>}'' is hidden in
-  concrete syntax, so the proof text is exactly the same as for @{text
-  group} given before.
+  We may now proceed to prove results within @{text group_struct} just
+  as before for @{text group}.  Proper treatment of ``@{text \<struct>}'' is
+  hidden in concrete syntax, so the proof text is exactly the same as
+  before.
 *}
 
 theorem (in group_struct)
   right_inv: "x \<cdot> x\<inv> = \<one>"
 proof -

   "\<one>\<^sub>3"  \<rightleftharpoons>  "one \<struct>\<^sub>3"
 
 text {*
   \medskip The following synthetic example demonstrates how to refer
   to several structures of type @{text group} succinctly; one might
-  also think of working with renamed versions of the @{text
+  also think of working with several renamed versions of the @{text
   group_struct} locale above.
 *}
 
 lemma
   (fixes G :: "'a group" (structure)