3 \def\isabellecontext{Local{\isacharunderscore}Theory}%
10 \isacommand{theory}\isamarkupfalse%
11 \ Local{\isacharunderscore}Theory\isanewline
12 \isakeyword{imports}\ Base\isanewline
21 \isamarkupchapter{Local theory specifications%
25 \begin{isamarkuptext}%
26 A \emph{local theory} combines aspects of both theory and proof
27 context (cf.\ \secref{sec:context}), such that definitional
28 specifications may be given relatively to parameters and
29 assumptions. A local theory is represented as a regular proof
30 context, augmented by administrative data about the \emph{target
33 The target is usually derived from the background theory by adding
34 local \isa{{\isasymFIX}} and \isa{{\isasymASSUME}} elements, plus
35 suitable modifications of non-logical context data (e.g.\ a special
36 type-checking discipline). Once initialized, the target is ready to
37 absorb definitional primitives: \isa{{\isasymDEFINE}} for terms and
38 \isa{{\isasymNOTE}} for theorems. Such definitions may get
39 transformed in a target-specific way, but the programming interface
42 Isabelle/Pure provides target mechanisms for locales, type-classes,
43 type-class instantiations, and general overloading. In principle,
44 users can implement new targets as well, but this rather arcane
45 discipline is beyond the scope of this manual. In contrast,
46 implementing derived definitional packages to be used within a local
47 theory context is quite easy: the interfaces are even simpler and
48 more abstract than the underlying primitives for raw theories.
50 Many definitional packages for local theories are available in
51 Isabelle. Although a few old packages only work for global
52 theories, the local theory interface is already the standard way of
53 implementing definitional packages in Isabelle.%
57 \isamarkupsection{Definitional elements%
61 \begin{isamarkuptext}%
62 There are separate elements \isa{{\isasymDEFINE}\ c\ {\isasymequiv}\ t} for terms, and
63 \isa{{\isasymNOTE}\ b\ {\isacharequal}\ thm} for theorems. Types are treated
64 implicitly, according to Hindley-Milner discipline (cf.\
65 \secref{sec:variables}). These definitional primitives essentially
66 act like \isa{let}-bindings within a local context that may
67 already contain earlier \isa{let}-bindings and some initial
68 \isa{{\isasymlambda}}-bindings. Thus we gain \emph{dependent definitions}
69 that are relative to an initial axiomatic context. The following
70 diagram illustrates this idea of axiomatic elements versus
71 definitional elements:
74 \begin{tabular}{|l|l|l|}
76 & \isa{{\isasymlambda}}-binding & \isa{let}-binding \\
78 types & fixed \isa{{\isasymalpha}} & arbitrary \isa{{\isasymbeta}} \\
79 terms & \isa{{\isasymFIX}\ x\ {\isacharcolon}{\isacharcolon}\ {\isasymtau}} & \isa{{\isasymDEFINE}\ c\ {\isasymequiv}\ t} \\
80 theorems & \isa{{\isasymASSUME}\ a{\isacharcolon}\ A} & \isa{{\isasymNOTE}\ b\ {\isacharequal}\ \isactrlBG B\isactrlEN } \\
85 A user package merely needs to produce suitable \isa{{\isasymDEFINE}}
86 and \isa{{\isasymNOTE}} elements according to the application. For
87 example, a package for inductive definitions might first \isa{{\isasymDEFINE}} a certain predicate as some fixed-point construction,
88 then \isa{{\isasymNOTE}} a proven result about monotonicity of the
89 functor involved here, and then produce further derived concepts via
90 additional \isa{{\isasymDEFINE}} and \isa{{\isasymNOTE}} elements.
92 The cumulative sequence of \isa{{\isasymDEFINE}} and \isa{{\isasymNOTE}}
93 produced at package runtime is managed by the local theory
94 infrastructure by means of an \emph{auxiliary context}. Thus the
95 system holds up the impression of working within a fully abstract
96 situation with hypothetical entities: \isa{{\isasymDEFINE}\ c\ {\isasymequiv}\ t}
97 always results in a literal fact \isa{\isactrlBG c\ {\isasymequiv}\ t\isactrlEN }, where
98 \isa{c} is a fixed variable \isa{c}. The details about
99 global constants, name spaces etc. are handled internally.
101 So the general structure of a local theory is a sandwich of three
105 \framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}}
108 \noindent When a definitional package is finished, the auxiliary
109 context is reset to the target context. The target now holds
110 definitions for terms and theorems that stem from the hypothetical
111 \isa{{\isasymDEFINE}} and \isa{{\isasymNOTE}} elements, transformed by
112 the particular target policy (see
113 \cite[\S4--5]{Haftmann-Wenzel:2009} for details).%
123 \begin{isamarkuptext}%
125 \indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\
126 \indexdef{}{ML}{Theory\_Target.init}\verb|Theory_Target.init: string option -> theory -> local_theory| \\[1ex]
127 \indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline%
128 \verb| local_theory -> (term * (string * thm)) * local_theory| \\
129 \indexdef{}{ML}{Local\_Theory.note}\verb|Local_Theory.note: Attrib.binding * thm list ->|\isasep\isanewline%
130 \verb| local_theory -> (string * thm list) * local_theory| \\
135 \item \verb|local_theory| represents local theories. Although
136 this is merely an alias for \verb|Proof.context|, it is
137 semantically a subtype of the same: a \verb|local_theory| holds
138 target information as special context data. Subtyping means that
139 any value \isa{lthy{\isacharcolon}}~\verb|local_theory| can be also used
140 with operations on expecting a regular \isa{ctxt{\isacharcolon}}~\verb|Proof.context|.
142 \item \verb|Theory_Target.init|~\isa{NONE\ thy} initializes a
143 trivial local theory from the given background theory.
144 Alternatively, \isa{SOME\ name} may be given to initialize a
145 \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a fully-qualified
146 internal name is expected here). This is useful for experimentation
147 --- normally the Isar toplevel already takes care to initialize the
148 local theory context.
150 \item \verb|Local_Theory.define|~\isa{{\isacharparenleft}{\isacharparenleft}b{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isacharparenleft}a{\isacharcomma}\ rhs{\isacharparenright}{\isacharparenright}\ lthy} defines a local entity according to the specification that is
151 given relatively to the current \isa{lthy} context. In
152 particular the term of the RHS may refer to earlier local entities
153 from the auxiliary context, or hypothetical parameters from the
154 target context. The result is the newly defined term (which is
155 always a fixed variable with exactly the same name as specified for
156 the LHS), together with an equational theorem that states the
157 definition as a hypothetical fact.
159 Unless an explicit name binding is given for the RHS, the resulting
160 fact will be called \isa{b{\isacharunderscore}def}. Any given attributes are
161 applied to that same fact --- immediately in the auxiliary context
162 \emph{and} in any transformed versions stemming from target-specific
163 policies or any later interpretations of results from the target
164 context (think of \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} and \hyperlink{command.interpretation}{\mbox{\isa{\isacommand{interpretation}}}},
165 for example). This means that attributes should be usually plain
166 declarations such as \hyperlink{attribute.simp}{\mbox{\isa{simp}}}, while non-trivial rules like
167 \hyperlink{attribute.simplified}{\mbox{\isa{simplified}}} are better avoided.
169 \item \verb|Local_Theory.note|~\isa{{\isacharparenleft}a{\isacharcomma}\ ths{\isacharparenright}\ lthy} is
170 analogous to \verb|Local_Theory.define|, but defines facts instead of
171 terms. There is also a slightly more general variant \verb|Local_Theory.notes| that defines several facts (with attribute
172 expressions) simultaneously.
174 This is essentially the internal version of the \hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}
175 command, or \hyperlink{command.declare}{\mbox{\isa{\isacommand{declare}}}} if an empty name binding is given.
188 \isamarkupsection{Morphisms and declarations%
192 \begin{isamarkuptext}%
202 \isacommand{end}\isamarkupfalse%
214 %%% TeX-master: "root"