author wenzelm Wed, 24 Jul 2002 00:09:44 +0200 changeset 13411 181a293aa37a parent 13410 f2cd09766864 child 13412 666137b488a4
locales: predicate defs;
--- a/doc-src/IsarRef/generic.tex	Wed Jul 24 00:08:52 2002 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed Jul 24 00:09:44 2002 +0200
@@ -88,9 +88,14 @@
only that the fact emerges through the subsequent proof, which may refer to
the full infrastructure of the locale context (covering local parameters with
typing and concrete syntax, assumptions, definitions etc.).  Most notably,
-fact declarations of the locale are active during the proof as well (e.g.\
+fact declarations of the locale are active during the proof as well (e.g.\
local $simp$ rules).

+As a general principle, results exported from a locale context acquire
+additional premises according to the specification.  Usually this is only a
+single predicate according to the standard closed'' view of locale
+specifications.
+

\subsubsection{Locale specifications}

@@ -107,7 +112,7 @@
\railterm{printlocale}

\begin{rail}
-  'locale' name ('=' localeexpr)?
+  'locale' ('(open)')? name ('=' localeexpr)?
;
printlocale localeexpr
;
@@ -132,8 +137,8 @@
\end{rail}

\begin{descr}
-
-\item [$\LOCALE~loc~=~import~+~body$] defines new locale $loc$ as a context
+
+\item [$\LOCALE~loc~=~import~+~body$] defines a new locale $loc$ as a context
consisting of a certain view of existing locales ($import$) plus some
additional elements ($body$).  Both $import$ and $body$ are optional; the
degenerate form $\LOCALE~loc$ defines an empty locale, which may still be
@@ -181,11 +186,31 @@
maintains a dynamic relation to the locales being referenced (benefiting
from any later fact declarations in the obvious manner).
\end{descr}
-
+
Note that $\IS{p}$'' patterns given in the syntax of $\ASSUMESNAME$ and
-  $\DEFINESNAME$ above are actually illegal in locale definitions.  In the
-  long goal format of \S\ref{sec:goals}, term bindings may be included as
-  expected, though.
+  $\DEFINESNAME$ above are illegal in locale definitions.  In the long goal
+  format of \S\ref{sec:goals}, term bindings may be included as expected,
+  though.
+
+  \medskip By default, locale specifications are closed up'' by turning the
+  given text into a predicate definition $loc_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 expressions.  The full cumulative view is
+  only provided on export, involving another predicate $loc$ that refers to
+  the complete specification text.
+
+  In any case, the predicate arguments are those locale parameters that
+  actually occur in the respective piece of text.  Also note that these
+  predicates operate at the meta-level in theory, but the locale packages
+  attempts to internalize statements according to the object-logic setup
+  (e.g.\ replacing $\Forall$ by $\forall$, and $\Imp$ by $\imp$ in HOL; see
+  also \S\ref{sec:object-logic}).  Separate introduction rules
+  $loc_axioms.intro$ and $loc.intro$ are declared as well.
+
+  The $(open)$ option of a locale specification prevents both the current
+  $loc_axioms$ and cumulative $loc$ predicate constructions.  Predicates are
+  also omitted for empty specification texts.

\item [$\isarkeyword{print_locale}~import~+~body$] prints the specified locale
expression in a flattened form.  The notable special case