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: