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