updated local theory targets;
Sat, 11 Nov 2006 16:11:40 +0100
changeset 21303 fa16e4bf8717
parent 21302 4c8f3dfc7124
child 21304 01968a336533
updated local theory targets; added 'context' as local theory switch; tuned;
--- 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.
-  '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 @@
-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
+All of these specifications support local theory targets (cf.\ 
-\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
+  \isarcmd{context} & : & \isartrans{theory}{local{\dsh}theory} \\
+  \isarcmd{end} & : & \isartrans{local{\dsh}theory}{theory} \\
+  'context' name 'begin'
+  ;
+  target: '(' 'in' name ')'
+  ;
+\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.
+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$).
 Locales are named local contexts, consisting of a list of declaration elements
 that are modeled after the Isar proof context commands (cf.\
-\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.
-  locale: '(' 'in' name ')'
-  ;
-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
 \subsubsection{Locale specifications}
@@ -159,7 +180,7 @@
-  '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
+and locales (command $\isarcmd{interpretation}$) and also in proof
+contexts ($\isarcmd{interpret}$).
@@ -411,29 +431,29 @@
   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.
   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.
-\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.
@@ -444,7 +464,7 @@
-  'class' name '=' classexpr
+  'class' name '=' classexpr 'begin'?
   'instance' (instarity | instsubsort)