author | wenzelm |
Tue, 17 Aug 2010 17:01:46 +0200 | |
changeset 38466 | fef3c24bb8d3 |
parent 38354 | fed4e71a8c0f |
child 39885 | 6a3f7941c3a0 |
permissions | -rw-r--r-- |
18537 | 1 |
% |
2 |
\begin{isabellebody}% |
|
29756 | 3 |
\def\isabellecontext{Local{\isacharunderscore}Theory}% |
18537 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
29756 | 11 |
\ Local{\isacharunderscore}Theory\isanewline |
12 |
\isakeyword{imports}\ Base\isanewline |
|
13 |
\isakeyword{begin}% |
|
18537 | 14 |
\endisatagtheory |
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
35001 | 21 |
\isamarkupchapter{Local theory specifications \label{ch:local-theory}% |
18537 | 22 |
} |
23 |
\isamarkuptrue% |
|
24 |
% |
|
29767 | 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 |
|
31 |
context}. |
|
32 |
||
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 |
|
40 |
hides such details. |
|
41 |
||
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. |
|
49 |
||
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.% |
|
54 |
\end{isamarkuptext}% |
|
55 |
\isamarkuptrue% |
|
56 |
% |
|
29762 | 57 |
\isamarkupsection{Definitional elements% |
18537 | 58 |
} |
59 |
\isamarkuptrue% |
|
60 |
% |
|
61 |
\begin{isamarkuptext}% |
|
29767 | 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: |
|
72 |
||
73 |
\begin{center} |
|
74 |
\begin{tabular}{|l|l|l|} |
|
75 |
\hline |
|
76 |
& \isa{{\isasymlambda}}-binding & \isa{let}-binding \\ |
|
77 |
\hline |
|
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 } \\ |
|
81 |
\hline |
|
82 |
\end{tabular} |
|
83 |
\end{center} |
|
84 |
||
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. |
|
91 |
||
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. |
|
100 |
||
101 |
So the general structure of a local theory is a sandwich of three |
|
102 |
layers: |
|
103 |
||
104 |
\begin{center} |
|
105 |
\framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}} |
|
106 |
\end{center} |
|
107 |
||
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).% |
|
18537 | 114 |
\end{isamarkuptext}% |
115 |
\isamarkuptrue% |
|
116 |
% |
|
29767 | 117 |
\isadelimmlref |
118 |
% |
|
119 |
\endisadelimmlref |
|
120 |
% |
|
121 |
\isatagmlref |
|
122 |
% |
|
123 |
\begin{isamarkuptext}% |
|
124 |
\begin{mldecls} |
|
30121 | 125 |
\indexdef{}{ML type}{local\_theory}\verb|type local_theory = Proof.context| \\ |
38466 | 126 |
\indexdef{}{ML}{Named\_Target.init}\verb|Named_Target.init: string -> theory -> local_theory| \\[1ex] |
33834
7c06e19f717c
adapted local theory operations -- eliminated odd kind;
wenzelm
parents:
33672
diff
changeset
|
127 |
\indexdef{}{ML}{Local\_Theory.define}\verb|Local_Theory.define: (binding * mixfix) * (Attrib.binding * term) ->|\isasep\isanewline% |
7c06e19f717c
adapted local theory operations -- eliminated odd kind;
wenzelm
parents:
33672
diff
changeset
|
128 |
\verb| local_theory -> (term * (string * thm)) * local_theory| \\ |
33672 | 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| \\ |
|
29767 | 131 |
\end{mldecls} |
132 |
||
133 |
\begin{description} |
|
134 |
||
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|. |
|
141 |
||
38466 | 142 |
\item \verb|Named_Target.init|~\isa{name\ thy} initializes a local |
143 |
theory derived from the given background theory. An empty name |
|
144 |
refers to a \emph{global theory} context, and a non-empty name |
|
145 |
refers to a \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}} or \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}} context (a |
|
146 |
fully-qualified internal name is expected here). This is useful for |
|
147 |
experimentation --- normally the Isar toplevel already takes care to |
|
148 |
initialize the local theory context. |
|
29767 | 149 |
|
33834
7c06e19f717c
adapted local theory operations -- eliminated odd kind;
wenzelm
parents:
33672
diff
changeset
|
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 |
29767 | 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. |
|
158 |
||
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. |
|
168 |
||
33672 | 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 |
|
29767 | 172 |
expressions) simultaneously. |
173 |
||
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. |
|
176 |
||
177 |
\end{description}% |
|
178 |
\end{isamarkuptext}% |
|
179 |
\isamarkuptrue% |
|
180 |
% |
|
181 |
\endisatagmlref |
|
182 |
{\isafoldmlref}% |
|
183 |
% |
|
184 |
\isadelimmlref |
|
185 |
% |
|
186 |
\endisadelimmlref |
|
187 |
% |
|
29762 | 188 |
\isamarkupsection{Morphisms and declarations% |
18537 | 189 |
} |
190 |
\isamarkuptrue% |
|
191 |
% |
|
192 |
\begin{isamarkuptext}% |
|
193 |
FIXME% |
|
194 |
\end{isamarkuptext}% |
|
195 |
\isamarkuptrue% |
|
196 |
% |
|
197 |
\isadelimtheory |
|
198 |
% |
|
199 |
\endisadelimtheory |
|
200 |
% |
|
201 |
\isatagtheory |
|
202 |
\isacommand{end}\isamarkupfalse% |
|
203 |
% |
|
204 |
\endisatagtheory |
|
205 |
{\isafoldtheory}% |
|
206 |
% |
|
207 |
\isadelimtheory |
|
208 |
% |
|
209 |
\endisadelimtheory |
|
210 |
\isanewline |
|
211 |
\end{isabellebody}% |
|
212 |
%%% Local Variables: |
|
213 |
%%% mode: latex |
|
214 |
%%% TeX-master: "root" |
|
215 |
%%% End: |