# HG changeset patch # User wenzelm # Date 1163257900 -3600 # Node ID fa16e4bf8717154b301724eb207835280bff9597 # Parent 4c8f3dfc7124eec8ccf1a973bce75d122f9e814c updated local theory targets; added 'context' as local theory switch; tuned; diff -r 4c8f3dfc7124 -r fa16e4bf8717 doc-src/IsarRef/generic.tex --- a/doc-src/IsarRef/generic.tex Sat Nov 11 16:11:39 2006 +0100 +++ b/doc-src/IsarRef/generic.tex Sat Nov 11 16:11:40 2006 +0100 @@ -23,13 +23,13 @@ available, and result names need not be given. \begin{rail} - 'axiomatization' locale? consts? ('where' specs)? + 'axiomatization' target? consts? ('where' specs)? ; - 'definition' locale? (constdecl? constdef +) + 'definition' target? (constdecl? constdef +) ; - 'abbreviation' locale? mode? (constdecl? prop +) + 'abbreviation' target? mode? (constdecl? prop +) ; - 'notation' locale? mode? (nameref mixfix +) + 'notation' target? mode? (nameref mixfix +) ; consts: ((name ('::' type)? structmixfix? | vars) + 'and') @@ -64,9 +64,6 @@ \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 according to the meta-level equality $eq$. @@ -91,58 +88,82 @@ \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. +All of these specifications support local theory targets (cf.\ +\S\ref{sec:target}). -\subsection{Locales and local contexts}\label{sec:locale} +\subsection{Local theory targets}\label{sec:target} + +A local theory target is a context managed separately within the +enclosing theory. Contexts may introduce parameters (fixed variables) +and assumptions (hypotheses). Definitions and theorems depending on +the context may be added incrementally later on. Named contexts refer +to locales (cf.\ \S\ref{sec:locale}) or type classes (cf.\ +\S\ref{sec:class}); the name ``$-$'' signifies the global theory +context. + +\indexisarcmd{context}\indexisarcmd{end} +\begin{matharray}{rcll} + \isarcmd{context} & : & \isartrans{theory}{local{\dsh}theory} \\ + \isarcmd{end} & : & \isartrans{local{\dsh}theory}{theory} \\ +\end{matharray} + +\indexouternonterm{target} +\begin{rail} + 'context' name 'begin' + ; + + target: '(' 'in' name ')' + ; +\end{rail} + +\begin{descr} + +\item $\isarkeyword{context}~c~\isarkeyword{begin}$ recommences an + existing locale or class context $c$. Note that locale and class + definitions allow to include the $\isarkeyword{begin}$ keyword as + well, in order to continue the local theory immediately after the + initial specification. + +\item $\END$ concludes the current local theory and continues the + enclosing global theory. Note that a non-local $\END$ has a + different meaning: it concludes the theory itself + (\S\ref{sec:begin-thy}). + +\item $(\IN~loc)$ given after any local theory command specifies an + immediate target, e.g.\ + ``$\isarkeyword{definition}~(\IN~loc)~\dots$'' or + ``$\THEOREMNAME~(\IN~loc)~\dots$''. This works both in a local or + global theory context; the current target context will be suspended + for this command only. Note that $(\IN~-)$ will always produce a + global result independently of the current target context. + +\end{descr} + +The exact meaning of results produced within a local theory context +depends on the underlying target infrastructure (locale, type class +etc.). The general idea is as follows, considering a context named +$c$ with parameter $x$ and assumption $A[x]$. + +Definitions are exported by introducing a global version with +additional arguments; a syntactic abbreviation links the long form +with the abstract version of the target context. For example, $a +\equiv t[x]$ becomes $c\dtt a \; ?x \equiv t[?x]$ at the theory level +(for arbitrary $?x$), together with a local abbreviation $c \equiv +c\dtt a\; x$ in the target context (for fixed $x$). + +Theorems are exported by discharging the assumptions and generalizing +the parameters of the context. For example, $a: B[x]$ becomes $c\dtt +a: A[?x] \Imp B[?x]$ (for arbitrary $?x$). + + +\subsection{Locales}\label{sec:locale} Locales are named local contexts, consisting of a list of declaration elements that are modeled after the Isar proof context commands (cf.\ \S\ref{sec:proof-context}). -\subsubsection{Localized commands} - -Existing locales may be augmented later on by adding new facts. Note that the -actual context definition may not be changed! Several theory commands that -produce facts in some way are available in ``localized'' versions, referring -to a named locale instead of the global theory context. - -\indexouternonterm{locale} -\begin{rail} - locale: '(' 'in' name ')' - ; -\end{rail} - -Emerging facts of localized commands are stored in two versions, both in the -target locale and the theory (after export). The latter view produces a -qualified binding, using the locale name as a name space prefix. - -For example, ``$\LEMMAS~(\IN~loc)~a = \vec b$'' retrieves facts $\vec b$ from -the locale context of $loc$ and augments its body by an appropriate -``$\isarkeyword{notes}$'' element (see below). The exported view of $a$, -after discharging the locale context, is stored as $loc{.}a$ within the global -theory. A localized goal ``$\LEMMANAME~(\IN~loc)~a:~\phi$'' works similarly, -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.\ -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} \indexisarcmd{locale}\indexisarcmd{print-locale}\indexisarcmd{print-locales} @@ -159,7 +180,7 @@ \indexisarelem{defines}\indexisarelem{notes}\indexisarelem{includes} \begin{rail} - 'locale' ('(open)')? name ('=' localeexpr)? + 'locale' ('(open)')? name ('=' localeexpr)? 'begin'? ; 'print\_locale' '!'? localeexpr ; @@ -297,9 +318,8 @@ 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 $\isarcmd{interpretation}$) and also in proof contexts -($\isarcmd{interpret}$). +and locales (command $\isarcmd{interpretation}$) and also in proof +contexts ($\isarcmd{interpret}$). \indexisarcmd{interpretation}\indexisarcmd{interpret} \indexisarcmd{print-interps} @@ -411,29 +431,29 @@ \begin{warn} Since attributes are applied to interpreted theorems, interpretation - may modify the current simpset and claset. Take this into - account when choosing attributes for local theorems. + may modify the context of common proof tools, e.g.\ 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. \end{warn} \begin{warn} An interpretation in a theory may subsume previous 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. This situation is normally harmless, but - note that $blast$ gets confused by the presence of multiple axclass - instances of a rule. + 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. \end{warn} -\subsection{Type classes} +\subsection{Type classes}\label{sec:class} -A special case of locales are type classes. -Type classes -consist of a locale with \emph{exactly one} type variable -and an corresponding axclass. \cite{isabelle-classes} gives a substantial +A type class is a special case of a locale, with some additional +infrastructure (notably a link to type-inference). Type classes +consist of a locale with \emph{exactly one} type variable and an +corresponding axclass. \cite{isabelle-classes} gives a substantial introduction on type classes. \indexisarcmd{instance}\indexisarcmd{class}\indexisarcmd{print-classes} @@ -444,7 +464,7 @@ \end{matharray} \begin{rail} - 'class' name '=' classexpr + 'class' name '=' classexpr 'begin'? ; 'instance' (instarity | instsubsort) ;