# HG changeset patch
# User wenzelm
# Date 1140110754 -3600
# Node ID 99001616e0e29771d44c703c3660a57105cf7178
# Parent  a4b956f8b233598caab0bd2c40fc7d38cda0170d
derived specifications: definition, abbreviation, axiomatization;

diff -r a4b956f8b233 -r 99001616e0e2 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Thu Feb 16 18:25:52 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Thu Feb 16 18:25:54 2006 +0100
@@ -3,6 +3,92 @@
 
 \section{Theory specification commands}
 
+\subsection{Derived specifications}
+
+\indexisarcmd{definition}\indexisaratt{defn}
+\indexisarcmd{abbreviation}\indexisarcmd{axiomatization}
+\begin{matharray}{rcll}
+  \isarcmd{definition} & : & \isarkeep{local{\dsh}theory} \\
+  defn & : & \isaratt \\
+  \isarcmd{abbreviation} & : & \isarkeep{local{\dsh}theory} \\
+  \isarcmd{axiomatization} & : & \isarkeep{local{\dsh}theory} & (axiomatic!)\\
+\end{matharray}
+
+These specification mechanisms provide a slightly more abstract view
+than the underlying primitives of $\CONSTS$, $\DEFS$ (see
+\S\ref{sec:consts}), and $\isarkeyword{axioms}$ (see
+\S\ref{sec:axms-thms}).  In particular, type-inference is commonly
+available, and result names need not be given.
+
+\begin{rail}
+  'definition' locale? (constdecl? constdef +)
+  ;
+
+  'abbreviation' locale? '(output)'? (constdecl? prop +)
+  ;
+  'axiomatization' locale? consts? ('where' specs)?
+  ;
+
+  consts: ((name ('::' type)? structmixfix? | vars) + 'and')
+  ;
+  specs: (thmdecl? props + 'and')
+  ;
+\end{rail}
+
+\begin{descr}
+  
+\item $\isarkeyword{definition}~c~\isarkeyword{where}~eq$ produces an
+  internal definition $c \equiv t$ according to the specification
+  given as $eq$, which is then turned into a proven fact.  The given
+  proposition may deviate from internal meta-level equality according
+  to the rewrite rules declared as $defn$ by the object-logic.  This
+  typically covers object-level equality $x = t$ and equivalence $A
+  \leftrightarrow B$.  Users normally need not change the $defn$
+  setup.
+  
+  Definitions may be presented with explicit arguments on the LHS, as
+  well as additional conditions, e.g.\ $f\;x\;y = t$ instead of $f
+  \equiv \lambda x\;y. t$ and $y \not= 0 \Imp g\;x\;y = u$ instead of
+  an unguarded $g \equiv \lambda x\;y. u$.
+  
+  Multiple definitions are processed consecutively; no overloading is
+  supported here.
+  
+\item $\isarkeyword{abbreviation}~c~\isarkeyword{where}~eq$ introduces
+  a syntactic constant which is associated with a certain term derived
+  from the specification given as $eq$.  The very same transformations
+  as for $\isarkeyword{definition}$ are applied here, although
+  additional conditions are not supported.
+  
+  Abbreviations participate in the usual type-inference process, but
+  are expanded before the logic ever sees them.  The expansion is
+  one-way by default; the ``$(output)$'' option makes abbreviations
+  fold back whenever terms are pretty printed.  The latter needs some
+  care to avoid overlapping or looping syntactic replacements!
+  
+\item $\isarkeyword{axiomatization} ~ c@1 \dots c@n ~
+  \isarkeyword{where} ~ A@1 \dots A@m$ introduces several constants
+  simultaneously and states axiomatic properties for these.  The
+  constants are marked as being specified once and for all, which
+  prevents additional specifications being issued later on.
+  
+  Note that axiomatic specifications are only appropriate when
+  declaring a new logical system.  Normal applications should only use
+  definitional mechanisms!
+
+\end{descr}
+
+Any of these specifications support an optional target locale context
+(cf.\ \S\ref{sec:locale}).  In the latter case, constants being
+introduced depend on certain fixed parameters of the locale context;
+the constant name is qualified by the locale base name.  A syntactic
+abbreviation takes care for convenient input and output of such terms,
+making the parameters implicit and using the original short name.
+Outside the locale context, the specified entities are available in
+generalized form, with the parameters being open to explicit
+instantiation.
+
+
 \subsection{Axiomatic type classes}\label{sec:axclass}
 
 \indexisarcmd{axclass}\indexisarcmd{instance}\indexisarmeth{intro-classes}
@@ -101,7 +187,7 @@
 
 \indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales}
 \begin{matharray}{rcl}
-  \isarcmd{locale} & : & \isarkeep{theory} \\
+  \isarcmd{locale} & : & \isartrans{theory}{local{\dsh}theory} \\
   \isarcmd{print_locale}^* & : & \isarkeep{theory~|~proof} \\
   \isarcmd{print_locales}^* & : & \isarkeep{theory~|~proof} \\
 \end{matharray}