--- 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: