author | wenzelm |
Fri, 13 Nov 2015 14:49:30 +0100 | |
changeset 61656 | cfabbc083977 |
parent 61493 | 0debd22f0c0e |
child 61854 | 38b049cd3aad |
permissions | -rw-r--r-- |
61656 | 1 |
(*:maxLineLen=78:*) |
2 |
||
29755 | 3 |
theory Local_Theory |
4 |
imports Base |
|
5 |
begin |
|
18537 | 6 |
|
58618 | 7 |
chapter \<open>Local theory specifications \label{ch:local-theory}\<close> |
29759 | 8 |
|
58618 | 9 |
text \<open> |
61477 | 10 |
A \<^emph>\<open>local theory\<close> combines aspects of both theory and proof |
29764 | 11 |
context (cf.\ \secref{sec:context}), such that definitional |
12 |
specifications may be given relatively to parameters and |
|
13 |
assumptions. A local theory is represented as a regular proof |
|
61477 | 14 |
context, augmented by administrative data about the \<^emph>\<open>target |
15 |
context\<close>. |
|
29764 | 16 |
|
17 |
The target is usually derived from the background theory by adding |
|
61493 | 18 |
local \<open>\<FIX>\<close> and \<open>\<ASSUME>\<close> elements, plus |
29764 | 19 |
suitable modifications of non-logical context data (e.g.\ a special |
20 |
type-checking discipline). Once initialized, the target is ready to |
|
61493 | 21 |
absorb definitional primitives: \<open>\<DEFINE>\<close> for terms and |
22 |
\<open>\<NOTE>\<close> for theorems. Such definitions may get |
|
29764 | 23 |
transformed in a target-specific way, but the programming interface |
24 |
hides such details. |
|
25 |
||
26 |
Isabelle/Pure provides target mechanisms for locales, type-classes, |
|
27 |
type-class instantiations, and general overloading. In principle, |
|
28 |
users can implement new targets as well, but this rather arcane |
|
29 |
discipline is beyond the scope of this manual. In contrast, |
|
30 |
implementing derived definitional packages to be used within a local |
|
29765 | 31 |
theory context is quite easy: the interfaces are even simpler and |
32 |
more abstract than the underlying primitives for raw theories. |
|
29764 | 33 |
|
34 |
Many definitional packages for local theories are available in |
|
29765 | 35 |
Isabelle. Although a few old packages only work for global |
39839 | 36 |
theories, the standard way of implementing definitional packages in |
37 |
Isabelle is via the local theory interface. |
|
58618 | 38 |
\<close> |
29764 | 39 |
|
40 |
||
58618 | 41 |
section \<open>Definitional elements\<close> |
18537 | 42 |
|
58618 | 43 |
text \<open> |
61493 | 44 |
There are separate elements \<open>\<DEFINE> c \<equiv> t\<close> for terms, and |
45 |
\<open>\<NOTE> b = thm\<close> for theorems. Types are treated |
|
29765 | 46 |
implicitly, according to Hindley-Milner discipline (cf.\ |
29764 | 47 |
\secref{sec:variables}). These definitional primitives essentially |
61493 | 48 |
act like \<open>let\<close>-bindings within a local context that may |
49 |
already contain earlier \<open>let\<close>-bindings and some initial |
|
50 |
\<open>\<lambda>\<close>-bindings. Thus we gain \<^emph>\<open>dependent definitions\<close> |
|
29765 | 51 |
that are relative to an initial axiomatic context. The following |
52 |
diagram illustrates this idea of axiomatic elements versus |
|
53 |
definitional elements: |
|
29764 | 54 |
|
55 |
\begin{center} |
|
56 |
\begin{tabular}{|l|l|l|} |
|
57 |
\hline |
|
61493 | 58 |
& \<open>\<lambda>\<close>-binding & \<open>let\<close>-binding \\ |
29764 | 59 |
\hline |
61493 | 60 |
types & fixed \<open>\<alpha>\<close> & arbitrary \<open>\<beta>\<close> \\ |
61 |
terms & \<open>\<FIX> x :: \<tau>\<close> & \<open>\<DEFINE> c \<equiv> t\<close> \\ |
|
62 |
theorems & \<open>\<ASSUME> a: A\<close> & \<open>\<NOTE> b = \<^BG>B\<^EN>\<close> \\ |
|
29764 | 63 |
\hline |
64 |
\end{tabular} |
|
65 |
\end{center} |
|
66 |
||
61493 | 67 |
A user package merely needs to produce suitable \<open>\<DEFINE>\<close> |
68 |
and \<open>\<NOTE>\<close> elements according to the application. For |
|
69 |
example, a package for inductive definitions might first \<open>\<DEFINE>\<close> a certain predicate as some fixed-point construction, |
|
70 |
then \<open>\<NOTE>\<close> a proven result about monotonicity of the |
|
29765 | 71 |
functor involved here, and then produce further derived concepts via |
61493 | 72 |
additional \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements. |
29764 | 73 |
|
61493 | 74 |
The cumulative sequence of \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> |
29764 | 75 |
produced at package runtime is managed by the local theory |
61477 | 76 |
infrastructure by means of an \<^emph>\<open>auxiliary context\<close>. Thus the |
29764 | 77 |
system holds up the impression of working within a fully abstract |
61493 | 78 |
situation with hypothetical entities: \<open>\<DEFINE> c \<equiv> t\<close> |
79 |
always results in a literal fact \<open>\<^BG>c \<equiv> t\<^EN>\<close>, where |
|
80 |
\<open>c\<close> is a fixed variable \<open>c\<close>. The details about |
|
29764 | 81 |
global constants, name spaces etc. are handled internally. |
82 |
||
83 |
So the general structure of a local theory is a sandwich of three |
|
84 |
layers: |
|
85 |
||
86 |
\begin{center} |
|
87 |
\framebox{\quad auxiliary context \quad\framebox{\quad target context \quad\framebox{\quad background theory\quad}}} |
|
88 |
\end{center} |
|
89 |
||
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset
|
90 |
When a definitional package is finished, the auxiliary context is |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39849
diff
changeset
|
91 |
reset to the target context. The target now holds definitions for |
61493 | 92 |
terms and theorems that stem from the hypothetical \<open>\<DEFINE>\<close> and \<open>\<NOTE>\<close> elements, transformed by the |
58555 | 93 |
particular target policy (see @{cite \<open>\S4--5\<close> "Haftmann-Wenzel:2009"} |
58618 | 94 |
for details).\<close> |
29764 | 95 |
|
58618 | 96 |
text %mlref \<open> |
29764 | 97 |
\begin{mldecls} |
29765 | 98 |
@{index_ML_type local_theory: Proof.context} \\ |
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
56420
diff
changeset
|
99 |
@{index_ML Named_Target.init: "string -> theory -> local_theory"} \\[1ex] |
33834
7c06e19f717c
adapted local theory operations -- eliminated odd kind;
wenzelm
parents:
33672
diff
changeset
|
100 |
@{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
7c06e19f717c
adapted local theory operations -- eliminated odd kind;
wenzelm
parents:
33672
diff
changeset
|
101 |
local_theory -> (term * (string * thm)) * local_theory"} \\ |
33672 | 102 |
@{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
103 |
local_theory -> (string * thm list) * local_theory"} \\ |
|
29764 | 104 |
\end{mldecls} |
105 |
||
61439 | 106 |
\<^descr> Type @{ML_type local_theory} represents local theories. |
39864 | 107 |
Although this is merely an alias for @{ML_type Proof.context}, it is |
29765 | 108 |
semantically a subtype of the same: a @{ML_type local_theory} holds |
109 |
target information as special context data. Subtyping means that |
|
61493 | 110 |
any value \<open>lthy:\<close>~@{ML_type local_theory} can be also used |
111 |
with operations on expecting a regular \<open>ctxt:\<close>~@{ML_type |
|
29765 | 112 |
Proof.context}. |
113 |
||
61493 | 114 |
\<^descr> @{ML Named_Target.init}~\<open>before_exit name thy\<close> |
41621 | 115 |
initializes a local theory derived from the given background theory. |
61477 | 116 |
An empty name refers to a \<^emph>\<open>global theory\<close> context, and a |
41621 | 117 |
non-empty name refers to a @{command locale} or @{command class} |
118 |
context (a fully-qualified internal name is expected here). This is |
|
119 |
useful for experimentation --- normally the Isar toplevel already |
|
57181
2d13bf9ea77b
dropped obscure and unused ad-hoc before_exit hook for named targets
haftmann
parents:
56420
diff
changeset
|
120 |
takes care to initialize the local theory context. |
29764 | 121 |
|
61493 | 122 |
\<^descr> @{ML Local_Theory.define}~\<open>((b, mx), (a, rhs)) |
123 |
lthy\<close> defines a local entity according to the specification that is |
|
124 |
given relatively to the current \<open>lthy\<close> context. In |
|
29765 | 125 |
particular the term of the RHS may refer to earlier local entities |
29766 | 126 |
from the auxiliary context, or hypothetical parameters from the |
29765 | 127 |
target context. The result is the newly defined term (which is |
128 |
always a fixed variable with exactly the same name as specified for |
|
129 |
the LHS), together with an equational theorem that states the |
|
130 |
definition as a hypothetical fact. |
|
131 |
||
132 |
Unless an explicit name binding is given for the RHS, the resulting |
|
61493 | 133 |
fact will be called \<open>b_def\<close>. Any given attributes are |
29765 | 134 |
applied to that same fact --- immediately in the auxiliary context |
61477 | 135 |
\<^emph>\<open>and\<close> in any transformed versions stemming from target-specific |
29765 | 136 |
policies or any later interpretations of results from the target |
137 |
context (think of @{command locale} and @{command interpretation}, |
|
138 |
for example). This means that attributes should be usually plain |
|
139 |
declarations such as @{attribute simp}, while non-trivial rules like |
|
140 |
@{attribute simplified} are better avoided. |
|
141 |
||
61493 | 142 |
\<^descr> @{ML Local_Theory.note}~\<open>(a, ths) lthy\<close> is |
33672 | 143 |
analogous to @{ML Local_Theory.define}, but defines facts instead of |
29765 | 144 |
terms. There is also a slightly more general variant @{ML |
33672 | 145 |
Local_Theory.notes} that defines several facts (with attribute |
29765 | 146 |
expressions) simultaneously. |
147 |
||
148 |
This is essentially the internal version of the @{command lemmas} |
|
149 |
command, or @{command declare} if an empty name binding is given. |
|
58618 | 150 |
\<close> |
18537 | 151 |
|
20451 | 152 |
|
58618 | 153 |
section \<open>Morphisms and declarations \label{sec:morphisms}\<close> |
18537 | 154 |
|
58618 | 155 |
text \<open> |
52422 | 156 |
%FIXME |
39877 | 157 |
|
58555 | 158 |
See also @{cite "Chaieb-Wenzel:2007"}. |
58618 | 159 |
\<close> |
30272 | 160 |
|
18537 | 161 |
end |