|
1 theory Local_Theory |
|
2 imports Base |
|
3 begin |
|
4 |
|
5 chapter {* Local theory specifications \label{ch:local-theory} *} |
|
6 |
|
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 |
|
29 theory context is quite easy: the interfaces are even simpler and |
|
30 more abstract than the underlying primitives for raw theories. |
|
31 |
|
32 Many definitional packages for local theories are available in |
|
33 Isabelle. Although a few old packages only work for global |
|
34 theories, the standard way of implementing definitional packages in |
|
35 Isabelle is via the local theory interface. |
|
36 *} |
|
37 |
|
38 |
|
39 section {* Definitional elements *} |
|
40 |
|
41 text {* |
|
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.\ |
|
45 \secref{sec:variables}). These definitional primitives essentially |
|
46 act like @{text "let"}-bindings within a local context that may |
|
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: |
|
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, |
|
69 then @{text "\<NOTE>"} a proven result about monotonicity of the |
|
70 functor involved here, and then produce further derived concepts via |
|
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 When a definitional package is finished, the auxiliary context is |
|
90 reset to the target context. The target now holds definitions for |
|
91 terms and theorems that stem from the hypothetical @{text |
|
92 "\<DEFINE>"} and @{text "\<NOTE>"} elements, transformed by the |
|
93 particular target policy (see \cite[\S4--5]{Haftmann-Wenzel:2009} |
|
94 for details). *} |
|
95 |
|
96 text %mlref {* |
|
97 \begin{mldecls} |
|
98 @{index_ML_type local_theory: Proof.context} \\ |
|
99 @{index_ML Named_Target.init: "(local_theory -> local_theory) -> |
|
100 string -> theory -> local_theory"} \\[1ex] |
|
101 @{index_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> |
|
102 local_theory -> (term * (string * thm)) * local_theory"} \\ |
|
103 @{index_ML Local_Theory.note: "Attrib.binding * thm list -> |
|
104 local_theory -> (string * thm list) * local_theory"} \\ |
|
105 \end{mldecls} |
|
106 |
|
107 \begin{description} |
|
108 |
|
109 \item Type @{ML_type local_theory} represents local theories. |
|
110 Although this is merely an alias for @{ML_type Proof.context}, it is |
|
111 semantically a subtype of the same: a @{ML_type local_theory} holds |
|
112 target information as special context data. Subtyping means that |
|
113 any value @{text "lthy:"}~@{ML_type local_theory} can be also used |
|
114 with operations on expecting a regular @{text "ctxt:"}~@{ML_type |
|
115 Proof.context}. |
|
116 |
|
117 \item @{ML Named_Target.init}~@{text "before_exit name thy"} |
|
118 initializes a local theory derived from the given background theory. |
|
119 An empty name refers to a \emph{global theory} context, and a |
|
120 non-empty name refers to a @{command locale} or @{command class} |
|
121 context (a fully-qualified internal name is expected here). This is |
|
122 useful for experimentation --- normally the Isar toplevel already |
|
123 takes care to initialize the local theory context. The given @{text |
|
124 "before_exit"} function is invoked before leaving the context; in |
|
125 most situations plain identity @{ML I} is sufficient. |
|
126 |
|
127 \item @{ML Local_Theory.define}~@{text "((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 |
|
131 from the auxiliary context, or hypothetical parameters from the |
|
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 |
|
140 \emph{and} in any transformed versions stemming from target-specific |
|
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 |
|
147 \item @{ML Local_Theory.note}~@{text "(a, ths) lthy"} is |
|
148 analogous to @{ML Local_Theory.define}, but defines facts instead of |
|
149 terms. There is also a slightly more general variant @{ML |
|
150 Local_Theory.notes} that defines several facts (with attribute |
|
151 expressions) simultaneously. |
|
152 |
|
153 This is essentially the internal version of the @{command lemmas} |
|
154 command, or @{command declare} if an empty name binding is given. |
|
155 |
|
156 \end{description} |
|
157 *} |
|
158 |
|
159 |
|
160 section {* Morphisms and declarations \label{sec:morphisms} *} |
|
161 |
|
162 text {* |
|
163 %FIXME |
|
164 |
|
165 See also \cite{Chaieb-Wenzel:2007}. |
|
166 *} |
|
167 |
|
168 end |