
diff -r e7418f8d49fe -r d468d72a458f doc-src/IsarImplementation/Thy/document/Local_Theory.tex
--- a/doc-src/IsarImplementation/Thy/document/Local_Theory.tex	Mon Aug 27 16:48:41 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,218 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Local{\isaliteral{5F}{\isacharunderscore}}Theory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{theory}\isamarkupfalse%
-\ Local{\isaliteral{5F}{\isacharunderscore}}Theory\isanewline
-\isakeyword{imports}\ Base\isanewline
-\isakeyword{begin}%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupchapter{Local theory specifications \label{ch:local-theory}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-A \emph{local theory} combines aspects of both theory and proof
-  context (cf.\ \secref{sec:context}), such that definitional
-  specifications may be given relatively to parameters and
-  assumptions.  A local theory is represented as a regular proof
-  context, augmented by administrative data about the \emph{target
-  context}.
-
-  The target is usually derived from the background theory by adding
-  local \isa{{\isaliteral{5C3C4649583E}{\isasymFIX}}} and \isa{{\isaliteral{5C3C415353554D453E}{\isasymASSUME}}} elements, plus
-  suitable modifications of non-logical context data (e.g.\ a special
-  type-checking discipline).  Once initialized, the target is ready to
-  absorb definitional primitives: \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}} for terms and
-  \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}} for theorems.  Such definitions may get
-  transformed in a target-specific way, but the programming interface
-  hides such details.
-
-  Isabelle/Pure provides target mechanisms for locales, type-classes,
-  type-class instantiations, and general overloading.  In principle,
-  users can implement new targets as well, but this rather arcane
-  discipline is beyond the scope of this manual.  In contrast,
-  implementing derived definitional packages to be used within a local
-  theory context is quite easy: the interfaces are even simpler and
-  more abstract than the underlying primitives for raw theories.
-
-  Many definitional packages for local theories are available in
-  Isabelle.  Although a few old packages only work for global
-  theories, the standard way of implementing definitional packages in
-  Isabelle is via the local theory interface.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Definitional elements%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-There are separate elements \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}\ c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} for terms, and
-  \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}\ b\ {\isaliteral{3D}{\isacharequal}}\ thm} for theorems.  Types are treated
-  implicitly, according to Hindley-Milner discipline (cf.\
-  \secref{sec:variables}).  These definitional primitives essentially
-  act like \isa{let}-bindings within a local context that may
-  already contain earlier \isa{let}-bindings and some initial
-  \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-bindings.  Thus we gain \emph{dependent definitions}
-  that are relative to an initial axiomatic context.  The following
-  diagram illustrates this idea of axiomatic elements versus
-  definitional elements:
-
-  \begin{center}
-  \begin{tabular}{|l|l|l|}
-  \hline
-  & \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-binding & \isa{let}-binding \\
-  \hline
-  types & fixed \isa{{\isaliteral{5C3C616C7068613E}{\isasymalpha}}} & arbitrary \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}} \\
-  terms & \isa{{\isaliteral{5C3C4649583E}{\isasymFIX}}\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}} & \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}\ c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t} \\
-  theorems & \isa{{\isaliteral{5C3C415353554D453E}{\isasymASSUME}}\ a{\isaliteral{3A}{\isacharcolon}}\ A} & \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}\ b\ {\isaliteral{3D}{\isacharequal}}\ \isaliteral{5C3C5E42473E}{}\isactrlBG B\isaliteral{5C3C5E454E3E}{}\isactrlEN } \\
-  \hline
-  \end{tabular}
-  \end{center}
-
-  A user package merely needs to produce suitable \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}}
-  and \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}} elements according to the application.  For
-  example, a package for inductive definitions might first \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}} a certain predicate as some fixed-point construction,
-  then \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}} a proven result about monotonicity of the
-  functor involved here, and then produce further derived concepts via
-  additional \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}} and \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}} elements.
-
-  The cumulative sequence of \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}} and \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}}
-  produced at package runtime is managed by the local theory
-  infrastructure by means of an \emph{auxiliary context}.  Thus the
-  system holds up the impression of working within a fully abstract
-  situation with hypothetical entities: \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}\ c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}
-  always results in a literal fact \isa{\isaliteral{5C3C5E42473E}{}\isactrlBG c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isaliteral{5C3C5E454E3E}{}\isactrlEN }, where
-  \isa{c} is a fixed variable \isa{c}.  The details about
-  global constants, name spaces etc. are handled internally.
-
-  So the general structure of a local theory is a sandwich of three
-  layers:
-
-  \begin{center}
-  \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
-  \end{center}
-
-  When a definitional package is finished, the auxiliary context is
-  reset to the target context.  The target now holds definitions for
-  terms and theorems that stem from the hypothetical \isa{{\isaliteral{5C3C444546494E453E}{\isasymDEFINE}}} and \isa{{\isaliteral{5C3C4E4F54453E}{\isasymNOTE}}} elements, transformed by the
-  particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009}
-  for details).%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isatagmlref
-%
-\begin{isamarkuptext}%
-\begin{mldecls}
-  \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
-  \indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: (local_theory -> local_theory) ->|\isasep\isanewline%
-\verb|    string -> theory -> local_theory| \\[1ex]
-  \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
-\verb|    local_theory -> (term * (string * thm)) * local_theory| \\
-  \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
-\verb|    local_theory -> (string * thm list) * local_theory| \\
-  \end{mldecls}
-
-  \begin{description}
-
-  \item Type \verb|local_theory| represents local theories.
-  Although this is merely an alias for \verb|Proof.context|, it is
-  semantically a subtype of the same: a \verb|local_theory| holds
-  target information as special context data.  Subtyping means that
-  any value \isa{lthy{\isaliteral{3A}{\isacharcolon}}}~\verb|local_theory| can be also used
-  with operations on expecting a regular \isa{ctxt{\isaliteral{3A}{\isacharcolon}}}~\verb|Proof.context|.
-
-  \item \verb|Named_Target.init|~\isa{before{\isaliteral{5F}{\isacharunderscore}}exit\ name\ thy}
-  initializes a local theory derived from the given background theory.
-  An empty name refers to a \emph{global theory} context, and a
-  non-empty name refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}
-  context (a fully-qualified internal name is expected here).  This is
-  useful for experimentation --- normally the Isar toplevel already
-  takes care to initialize the local theory context.  The given \isa{before{\isaliteral{5F}{\isacharunderscore}}exit} function is invoked before leaving the context; in
-  most situations plain identity \verb|I| is sufficient.
-
-  \item \verb|Local_Theory.define|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}b{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ rhs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ lthy} defines a local entity according to the specification that is
-  given relatively to the current \isa{lthy} context.  In
-  particular the term of the RHS may refer to earlier local entities
-  from the auxiliary context, or hypothetical parameters from the
-  target context.  The result is the newly defined term (which is
-  always a fixed variable with exactly the same name as specified for
-  the LHS), together with an equational theorem that states the
-  definition as a hypothetical fact.
-
-  Unless an explicit name binding is given for the RHS, the resulting
-  fact will be called \isa{b{\isaliteral{5F}{\isacharunderscore}}def}.  Any given attributes are
-  applied to that same fact --- immediately in the auxiliary context
-  \emph{and} in any transformed versions stemming from target-specific
-  policies or any later interpretations of results from the target
-  context (think of \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}},
-  for example).  This means that attributes should be usually plain
-  declarations such as \hyperlink{attribute.simp}{\mbox{\isa{simp}}}, while non-trivial rules like
-  \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}} are better avoided.
-
-  \item \verb|Local_Theory.note|~\isa{{\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ ths{\isaliteral{29}{\isacharparenright}}\ lthy} is
-  analogous to \verb|Local_Theory.define|, but defines facts instead of
-  terms.  There is also a slightly more general variant \verb|Local_Theory.notes| that defines several facts (with attribute
-  expressions) simultaneously.
-
-  This is essentially the internal version of the \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}
-  command, or \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} if an empty name binding is given.
-
-  \end{description}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\endisatagmlref
-{\isafoldmlref}%
-%
-\isadelimmlref
-%
-\endisadelimmlref
-%
-\isamarkupsection{Morphisms and declarations \label{sec:morphisms}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME
-
-  \medskip See also \cite{Chaieb-Wenzel:2007}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-\isacommand{end}\isamarkupfalse%
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\isanewline
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End:




