# HG changeset patch
# User ballarin
# Date 1258900669 -3600
# Node ID e4b55a8de812cbf4e2daae0eb8e89aa228ff463f
# Parent  cff41e82e3df69a3270a43906a6ad017a17b80bf
Generated latex code.

diff -r cff41e82e3df -r e4b55a8de812 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 22 15:37:14 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sun Nov 22 15:37:49 2009 +0100
@@ -310,13 +310,63 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Locales are named local contexts, consisting of a list of
+Locales are parametric named local contexts, consisting of a list of
   declaration elements that are modeled after the Isar proof context
   commands (cf.\ \secref{sec:proof-context}).%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Locale specifications%
+\isamarkupsubsection{Locale expressions \label{sec:locale-expr}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A \emph{locale expression} denotes a structured context composed of
+  instances of existing locales.  The context consists of a list of
+  instances of declaration elements from the locales.  Two locale
+  instances are equal if they are of the same locale and the
+  parameters are instantiated with equivalent terms.  Declaration
+  elements from equal instances are never repeated, thus avoiding
+  duplicate declarations.
+
+  \indexouternonterm{localeexpr}
+  \begin{rail}
+    localeexpr: (instance + '+') ('for' (fixes + 'and'))?
+    ;
+    instance: (qualifier ':')? nameref (posinsts | namedinsts)
+    ;
+    qualifier: name ('?' | '!')?
+    ;
+    posinsts: (term | '_')*
+    ;
+    namedinsts: 'where' (name '=' term + 'and')
+    ;
+  \end{rail}
+
+  A locale instance consists of a reference to a locale and either
+  positional or named parameter instantiations.  Identical
+  instantiations (that is, those that instante a parameter by itself)
+  may be omitted.  The notation `\_' enables to omit the instantiation
+  for a parameter inside a positional instantiation.
+
+  Terms in instantiations are from the context the locale expressions
+  is declared in.  Local names may be added to this context with the
+  optional for clause.  In addition, syntax declarations from one
+  instance are effective when parsing subsequent instances of the same
+  expression.
+
+  Instances have an optional qualifier which applies to names in
+  declarations.  Names include local definitions and theorem names.
+  If present, the qualifier itself is either optional
+  (``\texttt{?}''), which means that it may be omitted on input of the
+  qualified name, or mandatory (``\texttt{!}'').  If neither
+  ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
+  is used.  For \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} and \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}
+  the default is ``mandatory'', for \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}} the default is ``optional''.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Locale declarations%
 }
 \isamarkuptrue%
 %
@@ -329,31 +379,22 @@
     \indexdef{}{method}{unfold\_locales}\hypertarget{method.unfold-locales}{\hyperlink{method.unfold-locales}{\mbox{\isa{unfold{\isacharunderscore}locales}}}} & : & \isa{method} \\
   \end{matharray}
 
-  \indexouternonterm{contextexpr}\indexouternonterm{contextelem}
+  \indexouternonterm{contextelem}
   \indexisarelem{fixes}\indexisarelem{constrains}\indexisarelem{assumes}
   \indexisarelem{defines}\indexisarelem{notes}
   \begin{rail}
-    'locale' name ('=' localeexpr)? 'begin'?
-    ;
-    'print\_locale' '!'? localeexpr
+    'locale' name ('=' locale)? 'begin'?
     ;
-    localeexpr: ((contextexpr '+' (contextelem+)) | contextexpr | (contextelem+))
+    'print\_locale' '!'? nameref
     ;
-
-    contextexpr: nameref | '(' contextexpr ')' |
-    (contextexpr (name mixfix? +)) | (contextexpr + '+')
+    locale: contextelem+ | localeexpr ('+' (contextelem+))?
     ;
-    contextelem: fixes | constrains | assumes | defines | notes
-    ;
-    fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
-    ;
-    constrains: 'constrains' (name '::' type + 'and')
-    ;
-    assumes: 'assumes' (thmdecl? props + 'and')
-    ;
-    defines: 'defines' (thmdecl? prop proppat? + 'and')
-    ;
-    notes: 'notes' (thmdef? thmrefs + 'and')
+    contextelem:
+    'fixes' (fixes + 'and')
+    | 'constrains' (name '::' type + 'and')
+    | 'assumes' (props + 'and')
+    | 'defines' (thmdecl? prop proppat? + 'and')
+    | 'notes' (thmdef? thmrefs + 'and')
     ;
   \end{rail}
 
@@ -369,19 +410,17 @@
   care of the most general typing that the combined context elements
   may acquire.
 
-  The \isa{import} consists of a structured context expression,
-  consisting of references to existing locales, renamed contexts, or
-  merged contexts.  Renaming uses positional notation: \isa{{\isachardoublequote}c\ x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}} means that (a prefix of) the fixed
-  parameters of context \isa{c} are named \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}; a ``\isa{{\isacharunderscore}}'' (underscore) means to skip that
-  position.  Renaming by default deletes concrete syntax, but new
-  syntax may by specified with a mixfix annotation.  An exeption of
-  this rule is the special syntax declared with ``\isa{{\isachardoublequote}{\isacharparenleft}{\isasymSTRUCTURE}{\isacharparenright}{\isachardoublequote}}'' (see below), which is neither deleted nor can it
-  be changed.  Merging proceeds from left-to-right, suppressing any
-  duplicates stemming from different paths through the import
-  hierarchy.
+  The \isa{import} consists of a structured locale expression; see
+  \secref{sec:proof-context} above.  Its for clause defines the local
+  parameters of the \isa{import}.  In addition, locale parameters
+  whose instantance is omitted automatically extend the (possibly
+  empty) for clause: they are inserted at its beginning.  This means
+  that these parameters may be referred to from within the expression
+  and also in the subsequent context elements and provides a
+  notational convenience for the inheritance of parameters in locale
+  declarations.
 
-  The \isa{body} consists of basic context elements, further context
-  expressions may be included as well.
+  The \isa{body} consists of context elements.
 
   \begin{description}
 
@@ -391,7 +430,9 @@
   implicitly in this context.
 
   \item \hyperlink{element.constrains}{\mbox{\isa{\isakeyword{constrains}}}}~\isa{{\isachardoublequote}x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}{\isachardoublequote}} introduces a type
-  constraint \isa{{\isasymtau}} on the local parameter \isa{x}.
+  constraint \isa{{\isasymtau}} on the local parameter \isa{x}.  This
+  element is deprecated.  The type constaint should be introduced in
+  the for clause or the relevant \hyperlink{element.fixes}{\mbox{\isa{\isakeyword{fixes}}}} element.
 
   \item \hyperlink{element.assumes}{\mbox{\isa{\isakeyword{assumes}}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymphi}\isactrlsub n{\isachardoublequote}}
   introduces local premises, similar to \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} within a
@@ -421,7 +462,7 @@
   \secref{sec:goals}, term bindings may be included as expected,
   though.
   
-  \medskip By default, locale specifications are ``closed up'' by
+  \medskip Locale specifications are ``closed up'' by
   turning the given text into a predicate definition \isa{loc{\isacharunderscore}axioms} and deriving the original assumptions as local lemmas
   (modulo local definitions).  The predicate statement covers only the
   newly specified assumptions, omitting the content of included locale
@@ -461,56 +502,73 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsubsection{Interpretation of locales%
+\isamarkupsubsection{Locale interpretations%
 }
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-Locale expressions (more precisely, \emph{context expressions}) may
-  be instantiated, and the instantiated facts added to the current
-  context.  This requires a proof of the instantiated specification
-  and is called \emph{locale interpretation}.  Interpretation is
-  possible in theories and locales (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
+Locale expressions may be instantiated, and the instantiated facts
+  added to the current context.  This requires a proof of the
+  instantiated specification and is called \emph{locale
+  interpretation}.  Interpretation is possible in locales \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}, theories (command \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}) and
+  also within a proof body (command \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}).
 
   \begin{matharray}{rcl}
+    \indexdef{}{command}{sublocale}\hypertarget{command.sublocale}{\hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
     \indexdef{}{command}{interpretation}\hypertarget{command.interpretation}{\hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
-    \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+    \indexdef{}{command}{interpret}\hypertarget{command.interpret}{\hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}} & : & \isa{{\isachardoublequote}proof{\isacharparenleft}state{\isacharparenright}\ {\isacharbar}\ proof{\isacharparenleft}chain{\isacharparenright}\ {\isasymrightarrow}\ proof{\isacharparenleft}prove{\isacharparenright}{\isachardoublequote}} \\
+    \indexdef{}{command}{print\_interps}\hypertarget{command.print-interps}{\hyperlink{command.print-interps}{\mbox{\isa{\isacommand{print{\isacharunderscore}interps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   \end{matharray}
 
   \indexouternonterm{interp}
   \begin{rail}
-    'interpretation' (interp | name ('<' | subseteq) contextexpr)
+    'sublocale' nameref ('<' | subseteq) localeexpr
     ;
-    'interpret' interp
+    'interpretation' localeepxr equations?
     ;
-    instantiation: ('[' (inst+) ']')?
+    'interpret' localeexpr
     ;
-    interp: (name ':')? \\ (contextexpr instantiation |
-      name instantiation 'where' (thmdecl? prop + 'and'))
+    'print\_interps' nameref
+    ;
+    equations: 'where' (thmdecl? prop + 'and')
     ;
   \end{rail}
 
   \begin{description}
 
-  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+  \item \hyperlink{command.sublocale}{\mbox{\isa{\isacommand{sublocale}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
+  interprets \isa{expr} in the locale \isa{name}.  A proof that
+  the specification of \isa{name} implies the specification of
+  \isa{expr} is required.  As in the localized version of the
+  theorem command, the proof is in the context of \isa{name}.  After
+  the proof obligation has been dischared, the facts of \isa{expr}
+  become part of locale \isa{name} as \emph{derived} context
+  elements and are available when the context \isa{name} is
+  subsequently entered.  Note that, like import, this is dynamic:
+  facts added to a locale part of \isa{expr} after interpretation
+  become also available in \isa{name}.
 
-  The first form of \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}} interprets \isa{expr} in the theory.  The instantiation is given as a list of terms
-  \isa{insts} and is positional.  All parameters must receive an
-  instantiation term --- with the exception of defined parameters.
-  These are, if omitted, derived from the defining equation and other
-  instantiations.  Use ``\isa{{\isacharunderscore}}'' to omit an instantiation term.
+  Only specification fragments of \isa{expr} that are not already
+  part of \isa{name} (be it imported, derived or a derived fragment
+  of the import) are considered in this process.  This enables
+  circular interpretations to the extent that no infinite chains are
+  generated in the locale hierarchy.
 
-  The command generates proof obligations for the instantiated
-  specifications (assumes and defines elements).  Once these are
-  discharged by the user, instantiated facts are added to the theory
-  in a post-processing phase.
+  If interpretations of \isa{name} exist in the current theory, the
+  command adds interpretations for \isa{expr} as well, with the same
+  qualifier, although only for fragments of \isa{expr} that are not
+  interpreted in the theory already.
 
-  Additional equations, which are unfolded in facts during
+  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+  interprets \isa{expr} in the theory.  The command generates proof
+  obligations for the instantiated specifications (assumes and defines
+  elements).  Once these are discharged by the user, instantiated
+  facts are added to the theory in a post-processing phase.
+
+  Additional equations, which are unfolded during
   post-processing, may be given after the keyword \hyperlink{keyword.where}{\mbox{\isa{\isakeyword{where}}}}.
   This is useful for interpreting concepts introduced through
   definition specification elements.  The equations must be proved.
-  Note that if equations are present, the context expression is
-  restricted to a locale name.
 
   The command is aware of interpretations already active in the
   theory, but does not simplify the goal automatically.  In order to
@@ -522,43 +580,12 @@
   already be active.  The command will only process facts for new
   parts.
 
-  The context expression may be preceded by a name, which takes effect
-  in the post-processing of facts.  It is used to prefix fact names,
-  for example to avoid accidental hiding of other facts.
-
   Adding facts to locales has the effect of adding interpreted facts
   to the theory for all active interpretations also.  That is,
   interpretations dynamically participate in any facts added to
   locales.
 
-  \item \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}}~\isa{{\isachardoublequote}name\ {\isasymsubseteq}\ expr{\isachardoublequote}}
-
-  This form of the command interprets \isa{expr} in the locale
-  \isa{name}.  It requires a proof that the specification of \isa{name} implies the specification of \isa{expr}.  As in the
-  localized version of the theorem command, the proof is in the
-  context of \isa{name}.  After the proof obligation has been
-  dischared, the facts of \isa{expr} become part of locale \isa{name} as \emph{derived} context elements and are available when the
-  context \isa{name} is subsequently entered.  Note that, like
-  import, this is dynamic: facts added to a locale part of \isa{expr} after interpretation become also available in \isa{name}.
-  Like facts of renamed context elements, facts obtained by
-  interpretation may be accessed by prefixing with the parameter
-  renaming (where the parameters are separated by ``\isa{{\isacharunderscore}}'').
-
-  Unlike interpretation in theories, instantiation is confined to the
-  renaming of parameters, which may be specified as part of the
-  context expression \isa{expr}.  Using defined parameters in \isa{name} one may achieve an effect similar to instantiation, though.
-
-  Only specification fragments of \isa{expr} that are not already
-  part of \isa{name} (be it imported, derived or a derived fragment
-  of the import) are considered by interpretation.  This enables
-  circular interpretations.
-
-  If interpretations of \isa{name} exist in the current theory, the
-  command adds interpretations for \isa{expr} as well, with the same
-  prefix and attributes, although only for fragments of \isa{expr}
-  that are not interpreted in the theory already.
-
-  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts\ {\isasymWHERE}\ eqns{\isachardoublequote}}
+  \item \hyperlink{command.interpret}{\mbox{\isa{\isacommand{interpret}}}}~\isa{{\isachardoublequote}expr\ insts{\isachardoublequote}}
   interprets \isa{expr} in the proof context and is otherwise
   similar to interpretation in theories.
 
@@ -570,7 +597,7 @@
     the Simplifier or Classical Reasoner.  Since the behavior of such
     automated reasoning tools is \emph{not} stable under
     interpretation morphisms, manual declarations might have to be
-    issued.
+    added to revert such declarations.
   \end{warn}
 
   \begin{warn}
@@ -578,9 +605,8 @@
     interpretations.  This happens if the same specification fragment
     is interpreted twice and the instantiation of the second
     interpretation is more general than the interpretation of the
-    first.  A warning is issued, since it is likely that these could
-    have been generalized in the first place.  The locale package does
-    not attempt to remove subsumed interpretations.
+    first.  The locale package does not attempt to remove subsumed
+    interpretations.
   \end{warn}%
 \end{isamarkuptext}%
 \isamarkuptrue%