
diff -r 154b14fbc1d6 -r cc36d5da9bc0 src/HOL/ex/Locales.thy
--- a/src/HOL/ex/Locales.thy	Fri Dec 14 22:27:20 2001 +0100
+++ b/src/HOL/ex/Locales.thy	Fri Dec 14 22:27:43 2001 +0100
@@ -4,31 +4,87 @@
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 *)
 
-header {* Basic use of locales in Isabelle/Isar *}
+header {* Using locales in Isabelle/Isar *}
 
 theory Locales = Main:
 
+text_raw {*
+  \newcommand{\isasyminv}{\isasyminverse}
+  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
+  \newcommand{\isasymUSES}{\isatext{\isakeyword{uses}}}
+*}
+
+subsection {* Overview *}
+
 text {*
   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).
+  refers directly to the raw meta-logic of Isabelle.  Semantically, a
+  locale is just a (curried) predicate of the pure meta-logic
+  \cite{Paulson:1989}.
+
+  The present version for Isabelle/Isar builds on top of the rich
+  infrastructure of proof contexts
+  \cite{Wenzel:1999,Wenzel:2001:isar-ref,Wenzel:2001:Thesis},
+  achieving a tight integration with Isar proof texts, and a slightly
+  more abstract view of the underlying concepts.  An Isar proof
+  context encapsulates certain language elements that correspond to
+  @{text \<And>} (universal quantification), @{text \<Longrightarrow>} (implication), and
+  @{text "\<equiv>"} (definitions) of the pure Isabelle framework.  Moreover,
+  there are extra-logical concepts like term abbreviations or local
+  theorem attributes (declarations of simplification rules etc.) that
+  are indispensable in realistic applications.
+
+  Locales support concrete syntax, providing a localized version of
+  the existing concept of mixfix annotations of Isabelle
+  \cite{Paulson:1994:Isabelle}.  Furthermore, there is a separate
+  concept of ``implicit structures'' that admits to refer to
+  particular locale parameters in a casual manner (essentially derived
+  from the basic idea of ``anti-quotations'' or generalized de-Bruijn
+  indexes demonstrated in \cite[\S13--14]{Wenzel:2001:Isar-examples}).
 
-  Subsequently, we demonstrate basic use of locales to model
-  mathematical structures (by the inevitable group theory example).
-*}
+  Implicit structures work particular well together with extensible
+  records in HOL \cite{Naraschewski-Wenzel:1998} (the
+  ``object-oriented'' features discussed there are not required here).
+  Thus we shall essentially use record types to represent polymorphic
+  signatures of mathematical structures, while locales describe their
+  logical properties as a predicate.  Due to type inference of
+  simply-typed records we are able to give succinct specifications,
+  without caring about signature morphisms ourselves.  Further
+  eye-candy is provided by the independent concept of ``indexed
+  concrete syntax'' for record selectors.
+
+  Operations for building up locale contexts from existing definitions
+  cover common operations of \emph{merge} (disjunctive union in
+  canonical order) and \emph{rename} (of term parameters; types are
+  always inferred automatically).
+
+  \medskip Note that the following further concepts are still
+  \emph{absent}:
+  \begin{itemize}
 
-text_raw {*
-  \newcommand{\isasyminv}{\isasyminverse}
-  \newcommand{\isasymIN}{\isatext{\isakeyword{in}}}
+  \item Specific language elements for \emph{instantiation} of
+  locales.
+
+  Currently users may simulate this to some extend by having primitive
+  Isabelle/Isar operations (@{text of} for substitution and @{text OF}
+  for composition, \cite{Wenzel:2001:isar-ref}) act on the
+  automatically exported results stemming from different contexts.
+
+  \item Interpretation of locales, analogous to ``functors'' in
+  abstract algebra.
+
+  In principle one could directly work with functions over structures
+  (extensible records), and predicates being derived from locale
+  definitions.
+
+  \end{itemize}
+
+  \medskip Subsequently, we demonstrate some readily available
+  concepts of Isabelle/Isar locales by some simple examples of
+  abstract algebraic reasoning.
 *}
 
-
 subsection {* Local contexts as mathematical structures *}
 
 text {*
@@ -139,8 +195,16 @@
 qed
 
 text {*
-  \medskip Some further properties of inversion in general group
-  theory follow.
+  We see that the initial import of @{text group} within the
+  definition of @{text abelian_group} is actually evaluated
+  dynamically.  Thus any results in @{text group} are made available
+  to the derived context of @{text abelian_group} as well.  Note that
+  the alternative context element @{text \<USES>} would import
+  existing locales in a static fashion, without participating in
+  further facts emerging later on.
+
+  \medskip Some more properties of inversion in general group theory
+  follow.
 *}
 
 theorem (in group)
@@ -173,69 +237,67 @@
   meta-theoretical studies (involving functors from groups to groups,
   for example).
 
-  Another drawback of the naive approach above is that concrete syntax
-  will get lost on any kind of operation on the locale itself (such as
-  renaming, copying, or instantiation).  Whenever the particular
-  terminology of local parameters is affected the associated syntax
-  would have to be changed as well, which is hard to achieve formally.
+  Another minor drawback of the naive approach above is that concrete
+  syntax will get lost on any kind of operation on the locale itself
+  (such as renaming, copying, or instantiation).  Whenever the
+  particular terminology of local parameters is affected the
+  associated syntax would have to be changed as well, which is hard to
+  achieve formally.
 *}
 
 
 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.  See
-  \cite{Naraschewski-Wenzel:1998,Nipkow-et-al:2001:HOL} on
-  (extensible) record types in Isabelle/HOL.
+  We introduce the same hierarchy of basic group structures as above,
+  this time using extensible record types for the signature part,
+  together with concrete syntax for selector functions.
 *}
 
-record 'a group =
-  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-  inv :: "'a \<Rightarrow> 'a"
-  one :: 'a
+record 'a semigroup =
+  prod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>\<index>" 70)
+
+record 'a group = "'a semigroup" +
+  inv :: "'a \<Rightarrow> 'a"    ("(_\<inv>\<index>)" [1000] 999)
+  one :: 'a    ("\<one>\<index>")
 
 text {*
-  Now concrete syntax essentially needs refer to record selections;
-  this is possible by giving defined operations with private syntax
-  within the locale (e.g.\ see appropriate examples by Kamm\"uller).
+  The mixfix annotations above include a special ``structure index
+  indicator'' @{text \<index>} that makes grammer productions dependent on
+  certain parameters that have been declared as ``structure'' in a
+  locale context later on.  Thus we achieve casual notation as
+  encountered in informal mathematics, e.g.\ @{text "x \<cdot> y"} for
+  @{text "prod G x y"}.
 
-  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).
+  \medskip The following locale definitions introduce operate on a
+  single parameter declared as ``\isakeyword{structure}''.  Type
+  inference takes care to fill in the appropriate record type schemes
+  internally.
 *}
 
-syntax
-  "_prod" :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"    (infixl "\<cdot>" 70)
-  "_inv" :: "'a \<Rightarrow> 'a"    ("(_\<inv>)" [1000] 999)
-  "_one" :: 'a    ("\<one>")
-translations
-  "x \<cdot> y"  \<rightleftharpoons>  "prod \<struct> x y"
-  "x\<inv>"  \<rightleftharpoons>  "inv \<struct> x"
-  "\<one>"  \<rightleftharpoons>  "one \<struct>"
+locale semigroup_struct =
+  fixes S :: "'a group"    (structure)
+  assumes assoc: "(x \<cdot> y) \<cdot> z = x \<cdot> (y \<cdot> z)"
 
-text {*
-  The following locale definition introduces a single parameter, which
-  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>"
+locale group_struct = semigroup_struct G +
+  assumes left_inv: "x\<inv> \<cdot> x = \<one>"
     and left_one: "\<one> \<cdot> x = x"
 
 text {*
-  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.
+  Note that we prefer to call the @{text group} record structure
+  @{text G} rather than @{text S} inherited from @{text semigroup}.
+  This does not affect our concrete syntax, which is only dependent on
+  the \emph{positional} arrangements of currently active structures
+  (actually only one above), rather than names.  In fact, these
+  parameter names rarely occur in the term language at all (due to the
+  ``indexed syntax'' facility of Isabelle).  On the other hand, names
+  of locale facts will get qualified accordingly, e.g. @{text S.assoc}
+  versus @{text G.assoc}.
+
+  \medskip We may now proceed to prove results within @{text
+  group_struct} just as before for @{text group}.  The subsequent
+  proof texts are exactly the same as despite the more advanced
+  internal arrangement.
 *}
 
 theorem (in group_struct)
@@ -263,27 +325,14 @@
 qed
 
 text {*
+  FIXME
   \medskip Several implicit structures may be active at the same time
   (say up to 3 in practice).  The concrete syntax facility for locales
   actually maintains indexed dummies @{text "\<struct>\<^sub>1"}, @{text
   "\<struct>\<^sub>2"}, @{text "\<struct>\<^sub>3"}, \dots (@{text \<struct>} is the same as
   @{text "\<struct>\<^sub>1"}).  So we are able to provide concrete syntax to
   cover the 2nd and 3rd group structure as well.
-*}
 
-syntax
-  "_prod'" :: "'a \<Rightarrow> index \<Rightarrow> 'a \<Rightarrow> 'a"    ("(_ \<cdot>_/ _)" [70, 1000, 71] 70)
-  "_inv'" :: "'a \<Rightarrow> index \<Rightarrow> 'a"    ("(_\<inv>_)" [1000] 999)
-  "_one'" :: "index \<Rightarrow> 'a"    ("\<one>_")
-translations
-  "x \<cdot>\<^sub>2 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>2 x y"
-  "x \<cdot>\<^sub>3 y"  \<rightleftharpoons>  "prod \<struct>\<^sub>3 x y"
-  "x\<inv>\<^sub>2"  \<rightleftharpoons>  "inv \<struct>\<^sub>2 x"
-  "x\<inv>\<^sub>3"  \<rightleftharpoons>  "inv \<struct>\<^sub>3 x"
-  "\<one>\<^sub>2"  \<rightleftharpoons>  "one \<struct>\<^sub>2"
-  "\<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 several renamed versions of the @{text
@@ -292,7 +341,7 @@
 
 lemma
   (fixes G :: "'a group" (structure)
-    and H :: "'a group" (structure))
+    and H :: "'a group" (structure))  (* FIXME (uses group_struct G + group_struct H) *)
   True
 proof
   have "x \<cdot> y \<cdot> \<one> = prod G (prod G x y) (one G)" ..
@@ -300,13 +349,4 @@
   have "x \<cdot> \<one>\<^sub>2 = prod G x (one H)" ..
 qed
 
-text {*
-  \medskip As a minor drawback of this advanced technique we require
-  slightly more work to setup abstract and concrete syntax properly
-  (but only once in the beginning).  The resulting casual mode of
-  writing @{text "x \<cdot> y"} for @{text "prod G x y"} etc.\ mimics common
-  practice of informal mathematics quite nicely, while using a simple
-  and robust formal representation.
-*}
-
 end




