|
1 theory Isar |
|
2 imports Base |
|
3 begin |
|
4 |
|
5 chapter {* Isar language elements *} |
|
6 |
|
7 text {* The Isar proof language (see also |
|
8 \cite[\S2]{isabelle-isar-ref}) consists of three main categories of |
|
9 language elements as follows. |
|
10 |
|
11 \begin{enumerate} |
|
12 |
|
13 \item Proof \emph{commands} define the primary language of |
|
14 transactions of the underlying Isar/VM interpreter. Typical |
|
15 examples are @{command "fix"}, @{command "assume"}, @{command |
|
16 "show"}, @{command "proof"}, and @{command "qed"}. |
|
17 |
|
18 Composing proof commands according to the rules of the Isar/VM leads |
|
19 to expressions of structured proof text, such that both the machine |
|
20 and the human reader can give it a meaning as formal reasoning. |
|
21 |
|
22 \item Proof \emph{methods} define a secondary language of mixed |
|
23 forward-backward refinement steps involving facts and goals. |
|
24 Typical examples are @{method rule}, @{method unfold}, and @{method |
|
25 simp}. |
|
26 |
|
27 Methods can occur in certain well-defined parts of the Isar proof |
|
28 language, say as arguments to @{command "proof"}, @{command "qed"}, |
|
29 or @{command "by"}. |
|
30 |
|
31 \item \emph{Attributes} define a tertiary language of small |
|
32 annotations to theorems being defined or referenced. Attributes can |
|
33 modify both the context and the theorem. |
|
34 |
|
35 Typical examples are @{attribute intro} (which affects the context), |
|
36 and @{attribute symmetric} (which affects the theorem). |
|
37 |
|
38 \end{enumerate} |
|
39 *} |
|
40 |
|
41 |
|
42 section {* Proof commands *} |
|
43 |
|
44 text {* A \emph{proof command} is state transition of the Isar/VM |
|
45 proof interpreter. |
|
46 |
|
47 In principle, Isar proof commands could be defined in user-space as |
|
48 well. The system is built like that in the first place: one part of |
|
49 the commands are primitive, the other part is defined as derived |
|
50 elements. Adding to the genuine structured proof language requires |
|
51 profound understanding of the Isar/VM machinery, though, so this is |
|
52 beyond the scope of this manual. |
|
53 |
|
54 What can be done realistically is to define some diagnostic commands |
|
55 that inspect the general state of the Isar/VM, and report some |
|
56 feedback to the user. Typically this involves checking of the |
|
57 linguistic \emph{mode} of a proof state, or peeking at the pending |
|
58 goals (if available). |
|
59 |
|
60 Another common application is to define a toplevel command that |
|
61 poses a problem to the user as Isar proof state and processes the |
|
62 final result relatively to the context. Thus a proof can be |
|
63 incorporated into the context of some user-space tool, without |
|
64 modifying the Isar proof language itself. *} |
|
65 |
|
66 text %mlref {* |
|
67 \begin{mldecls} |
|
68 @{index_ML_type Proof.state} \\ |
|
69 @{index_ML Proof.assert_forward: "Proof.state -> Proof.state"} \\ |
|
70 @{index_ML Proof.assert_chain: "Proof.state -> Proof.state"} \\ |
|
71 @{index_ML Proof.assert_backward: "Proof.state -> Proof.state"} \\ |
|
72 @{index_ML Proof.simple_goal: "Proof.state -> {context: Proof.context, goal: thm}"} \\ |
|
73 @{index_ML Proof.goal: "Proof.state -> |
|
74 {context: Proof.context, facts: thm list, goal: thm}"} \\ |
|
75 @{index_ML Proof.raw_goal: "Proof.state -> |
|
76 {context: Proof.context, facts: thm list, goal: thm}"} \\ |
|
77 @{index_ML Proof.theorem: "Method.text option -> |
|
78 (thm list list -> Proof.context -> Proof.context) -> |
|
79 (term * term list) list list -> Proof.context -> Proof.state"} \\ |
|
80 \end{mldecls} |
|
81 |
|
82 \begin{description} |
|
83 |
|
84 \item Type @{ML_type Proof.state} represents Isar proof states. |
|
85 This is a block-structured configuration with proof context, |
|
86 linguistic mode, and optional goal. The latter consists of goal |
|
87 context, goal facts (``@{text "using"}''), and tactical goal state |
|
88 (see \secref{sec:tactical-goals}). |
|
89 |
|
90 The general idea is that the facts shall contribute to the |
|
91 refinement of some parts of the tactical goal --- how exactly is |
|
92 defined by the proof method that is applied in that situation. |
|
93 |
|
94 \item @{ML Proof.assert_forward}, @{ML Proof.assert_chain}, @{ML |
|
95 Proof.assert_backward} are partial identity functions that fail |
|
96 unless a certain linguistic mode is active, namely ``@{text |
|
97 "proof(state)"}'', ``@{text "proof(chain)"}'', ``@{text |
|
98 "proof(prove)"}'', respectively (using the terminology of |
|
99 \cite{isabelle-isar-ref}). |
|
100 |
|
101 It is advisable study the implementations of existing proof commands |
|
102 for suitable modes to be asserted. |
|
103 |
|
104 \item @{ML Proof.simple_goal}~@{text "state"} returns the structured |
|
105 Isar goal (if available) in the form seen by ``simple'' methods |
|
106 (like @{method simp} or @{method blast}). The Isar goal facts are |
|
107 already inserted as premises into the subgoals, which are presented |
|
108 individually as in @{ML Proof.goal}. |
|
109 |
|
110 \item @{ML Proof.goal}~@{text "state"} returns the structured Isar |
|
111 goal (if available) in the form seen by regular methods (like |
|
112 @{method rule}). The auxiliary internal encoding of Pure |
|
113 conjunctions is split into individual subgoals as usual. |
|
114 |
|
115 \item @{ML Proof.raw_goal}~@{text "state"} returns the structured |
|
116 Isar goal (if available) in the raw internal form seen by ``raw'' |
|
117 methods (like @{method induct}). This form is rarely appropriate |
|
118 for dignostic tools; @{ML Proof.simple_goal} or @{ML Proof.goal} |
|
119 should be used in most situations. |
|
120 |
|
121 \item @{ML Proof.theorem}~@{text "before_qed after_qed statement ctxt"} |
|
122 initializes a toplevel Isar proof state within a given context. |
|
123 |
|
124 The optional @{text "before_qed"} method is applied at the end of |
|
125 the proof, just before extracting the result (this feature is rarely |
|
126 used). |
|
127 |
|
128 The @{text "after_qed"} continuation receives the extracted result |
|
129 in order to apply it to the final context in a suitable way (e.g.\ |
|
130 storing named facts). Note that at this generic level the target |
|
131 context is specified as @{ML_type Proof.context}, but the usual |
|
132 wrapping of toplevel proofs into command transactions will provide a |
|
133 @{ML_type local_theory} here (\chref{ch:local-theory}). This |
|
134 affects the way how results are stored. |
|
135 |
|
136 The @{text "statement"} is given as a nested list of terms, each |
|
137 associated with optional @{keyword "is"} patterns as usual in the |
|
138 Isar source language. The original nested list structure over terms |
|
139 is turned into one over theorems when @{text "after_qed"} is |
|
140 invoked. |
|
141 |
|
142 \end{description} |
|
143 *} |
|
144 |
|
145 |
|
146 text %mlantiq {* |
|
147 \begin{matharray}{rcl} |
|
148 @{ML_antiquotation_def "Isar.goal"} & : & @{text ML_antiquotation} \\ |
|
149 \end{matharray} |
|
150 |
|
151 \begin{description} |
|
152 |
|
153 \item @{text "@{Isar.goal}"} refers to the regular goal state (if |
|
154 available) of the current proof state managed by the Isar toplevel |
|
155 --- as abstract value. |
|
156 |
|
157 This only works for diagnostic ML commands, such as @{command |
|
158 ML_val} or @{command ML_command}. |
|
159 |
|
160 \end{description} |
|
161 *} |
|
162 |
|
163 text %mlex {* The following example peeks at a certain goal configuration. *} |
|
164 |
|
165 notepad |
|
166 begin |
|
167 have A and B and C |
|
168 ML_val {* |
|
169 val n = Thm.nprems_of (#goal @{Isar.goal}); |
|
170 @{assert} (n = 3); |
|
171 *} |
|
172 oops |
|
173 |
|
174 text {* Here we see 3 individual subgoals in the same way as regular |
|
175 proof methods would do. *} |
|
176 |
|
177 |
|
178 section {* Proof methods *} |
|
179 |
|
180 text {* A @{text "method"} is a function @{text "context \<rightarrow> thm\<^sup>* \<rightarrow> goal |
|
181 \<rightarrow> (cases \<times> goal)\<^sup>*\<^sup>*"} that operates on the full Isar goal |
|
182 configuration with context, goal facts, and tactical goal state and |
|
183 enumerates possible follow-up goal states, with the potential |
|
184 addition of named extensions of the proof context (\emph{cases}). |
|
185 The latter feature is rarely used. |
|
186 |
|
187 This means a proof method is like a structurally enhanced tactic |
|
188 (cf.\ \secref{sec:tactics}). The well-formedness conditions for |
|
189 tactics need to hold for methods accordingly, with the following |
|
190 additions. |
|
191 |
|
192 \begin{itemize} |
|
193 |
|
194 \item Goal addressing is further limited either to operate either |
|
195 uniformly on \emph{all} subgoals, or specifically on the |
|
196 \emph{first} subgoal. |
|
197 |
|
198 Exception: old-style tactic emulations that are embedded into the |
|
199 method space, e.g.\ @{method rule_tac}. |
|
200 |
|
201 \item A non-trivial method always needs to make progress: an |
|
202 identical follow-up goal state has to be avoided.\footnote{This |
|
203 enables the user to write method expressions like @{text "meth\<^sup>+"} |
|
204 without looping, while the trivial do-nothing case can be recovered |
|
205 via @{text "meth\<^sup>?"}.} |
|
206 |
|
207 Exception: trivial stuttering steps, such as ``@{method -}'' or |
|
208 @{method succeed}. |
|
209 |
|
210 \item Goal facts passed to the method must not be ignored. If there |
|
211 is no sensible use of facts outside the goal state, facts should be |
|
212 inserted into the subgoals that are addressed by the method. |
|
213 |
|
214 \end{itemize} |
|
215 |
|
216 \medskip Syntactically, the language of proof methods appears as |
|
217 arguments to Isar commands like @{command "by"} or @{command apply}. |
|
218 User-space additions are reasonably easy by plugging suitable |
|
219 method-valued parser functions into the framework, using the |
|
220 @{command method_setup} command, for example. |
|
221 |
|
222 To get a better idea about the range of possibilities, consider the |
|
223 following Isar proof schemes. This is the general form of |
|
224 structured proof text: |
|
225 |
|
226 \medskip |
|
227 \begin{tabular}{l} |
|
228 @{command from}~@{text "facts\<^sub>1"}~@{command have}~@{text "props"}~@{command using}~@{text "facts\<^sub>2"} \\ |
|
229 @{command proof}~@{text "(initial_method)"} \\ |
|
230 \quad@{text "body"} \\ |
|
231 @{command qed}~@{text "(terminal_method)"} \\ |
|
232 \end{tabular} |
|
233 \medskip |
|
234 |
|
235 The goal configuration consists of @{text "facts\<^sub>1"} and |
|
236 @{text "facts\<^sub>2"} appended in that order, and various @{text |
|
237 "props"} being claimed. The @{text "initial_method"} is invoked |
|
238 with facts and goals together and refines the problem to something |
|
239 that is handled recursively in the proof @{text "body"}. The @{text |
|
240 "terminal_method"} has another chance to finish any remaining |
|
241 subgoals, but it does not see the facts of the initial step. |
|
242 |
|
243 \medskip This pattern illustrates unstructured proof scripts: |
|
244 |
|
245 \medskip |
|
246 \begin{tabular}{l} |
|
247 @{command have}~@{text "props"} \\ |
|
248 \quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\ |
|
249 \quad@{command apply}~@{text "method\<^sub>2"} \\ |
|
250 \quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\ |
|
251 \quad@{command done} \\ |
|
252 \end{tabular} |
|
253 \medskip |
|
254 |
|
255 The @{text "method\<^sub>1"} operates on the original claim while |
|
256 using @{text "facts\<^sub>1"}. Since the @{command apply} command |
|
257 structurally resets the facts, the @{text "method\<^sub>2"} will |
|
258 operate on the remaining goal state without facts. The @{text |
|
259 "method\<^sub>3"} will see again a collection of @{text |
|
260 "facts\<^sub>3"} that has been inserted into the script explicitly. |
|
261 |
|
262 \medskip Empirically, any Isar proof method can be categorized as |
|
263 follows. |
|
264 |
|
265 \begin{enumerate} |
|
266 |
|
267 \item \emph{Special method with cases} with named context additions |
|
268 associated with the follow-up goal state. |
|
269 |
|
270 Example: @{method "induct"}, which is also a ``raw'' method since it |
|
271 operates on the internal representation of simultaneous claims as |
|
272 Pure conjunction (\secref{sec:logic-aux}), instead of separate |
|
273 subgoals (\secref{sec:tactical-goals}). |
|
274 |
|
275 \item \emph{Structured method} with strong emphasis on facts outside |
|
276 the goal state. |
|
277 |
|
278 Example: @{method "rule"}, which captures the key ideas behind |
|
279 structured reasoning in Isar in purest form. |
|
280 |
|
281 \item \emph{Simple method} with weaker emphasis on facts, which are |
|
282 inserted into subgoals to emulate old-style tactical as |
|
283 ``premises''. |
|
284 |
|
285 Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}. |
|
286 |
|
287 \item \emph{Old-style tactic emulation} with detailed numeric goal |
|
288 addressing and explicit references to entities of the internal goal |
|
289 state (which are otherwise invisible from proper Isar proof text). |
|
290 The naming convention @{text "foo_tac"} makes this special |
|
291 non-standard status clear. |
|
292 |
|
293 Example: @{method "rule_tac"}. |
|
294 |
|
295 \end{enumerate} |
|
296 |
|
297 When implementing proof methods, it is advisable to study existing |
|
298 implementations carefully and imitate the typical ``boiler plate'' |
|
299 for context-sensitive parsing and further combinators to wrap-up |
|
300 tactic expressions as methods.\footnote{Aliases or abbreviations of |
|
301 the standard method combinators should be avoided. Note that from |
|
302 Isabelle99 until Isabelle2009 the system did provide various odd |
|
303 combinations of method wrappers that made user applications more |
|
304 complicated than necessary.} |
|
305 *} |
|
306 |
|
307 text %mlref {* |
|
308 \begin{mldecls} |
|
309 @{index_ML_type Proof.method} \\ |
|
310 @{index_ML METHOD_CASES: "(thm list -> cases_tactic) -> Proof.method"} \\ |
|
311 @{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\ |
|
312 @{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\ |
|
313 @{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\ |
|
314 @{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\ |
|
315 @{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> |
|
316 string -> theory -> theory"} \\ |
|
317 \end{mldecls} |
|
318 |
|
319 \begin{description} |
|
320 |
|
321 \item Type @{ML_type Proof.method} represents proof methods as |
|
322 abstract type. |
|
323 |
|
324 \item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps |
|
325 @{text cases_tactic} depending on goal facts as proof method with |
|
326 cases; the goal context is passed via method syntax. |
|
327 |
|
328 \item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text |
|
329 tactic} depending on goal facts as regular proof method; the goal |
|
330 context is passed via method syntax. |
|
331 |
|
332 \item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that |
|
333 addresses all subgoals uniformly as simple proof method. Goal facts |
|
334 are already inserted into all subgoals before @{text "tactic"} is |
|
335 applied. |
|
336 |
|
337 \item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that |
|
338 addresses a specific subgoal as simple proof method that operates on |
|
339 subgoal 1. Goal facts are inserted into the subgoal then the @{text |
|
340 "tactic"} is applied. |
|
341 |
|
342 \item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text |
|
343 "facts"} into subgoal @{text "i"}. This is convenient to reproduce |
|
344 part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping |
|
345 within regular @{ML METHOD}, for example. |
|
346 |
|
347 \item @{ML Method.setup}~@{text "name parser description"} provides |
|
348 the functionality of the Isar command @{command method_setup} as ML |
|
349 function. |
|
350 |
|
351 \end{description} |
|
352 *} |
|
353 |
|
354 text %mlex {* See also @{command method_setup} in |
|
355 \cite{isabelle-isar-ref} which includes some abstract examples. |
|
356 |
|
357 \medskip The following toy examples illustrate how the goal facts |
|
358 and state are passed to proof methods. The pre-defined proof method |
|
359 called ``@{method tactic}'' wraps ML source of type @{ML_type |
|
360 tactic} (abstracted over @{ML_text facts}). This allows immediate |
|
361 experimentation without parsing of concrete syntax. *} |
|
362 |
|
363 notepad |
|
364 begin |
|
365 assume a: A and b: B |
|
366 |
|
367 have "A \<and> B" |
|
368 apply (tactic {* rtac @{thm conjI} 1 *}) |
|
369 using a apply (tactic {* resolve_tac facts 1 *}) |
|
370 using b apply (tactic {* resolve_tac facts 1 *}) |
|
371 done |
|
372 |
|
373 have "A \<and> B" |
|
374 using a and b |
|
375 ML_val "@{Isar.goal}" |
|
376 apply (tactic {* Method.insert_tac facts 1 *}) |
|
377 apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *}) |
|
378 done |
|
379 end |
|
380 |
|
381 text {* \medskip The next example implements a method that simplifies |
|
382 the first subgoal by rewrite rules given as arguments. *} |
|
383 |
|
384 method_setup my_simp = {* |
|
385 Attrib.thms >> (fn thms => fn ctxt => |
|
386 SIMPLE_METHOD' (fn i => |
|
387 CHANGED (asm_full_simp_tac |
|
388 (put_simpset HOL_basic_ss ctxt addsimps thms) i))) |
|
389 *} "rewrite subgoal by given rules" |
|
390 |
|
391 text {* The concrete syntax wrapping of @{command method_setup} always |
|
392 passes-through the proof context at the end of parsing, but it is |
|
393 not used in this example. |
|
394 |
|
395 The @{ML Attrib.thms} parser produces a list of theorems from the |
|
396 usual Isar syntax involving attribute expressions etc.\ (syntax |
|
397 category @{syntax thmrefs}) \cite{isabelle-isar-ref}. The resulting |
|
398 @{ML_text thms} are added to @{ML HOL_basic_ss} which already |
|
399 contains the basic Simplifier setup for HOL. |
|
400 |
|
401 The tactic @{ML asm_full_simp_tac} is the one that is also used in |
|
402 method @{method simp} by default. The extra wrapping by the @{ML |
|
403 CHANGED} tactical ensures progress of simplification: identical goal |
|
404 states are filtered out explicitly to make the raw tactic conform to |
|
405 standard Isar method behaviour. |
|
406 |
|
407 \medskip Method @{method my_simp} can be used in Isar proofs like |
|
408 this: |
|
409 *} |
|
410 |
|
411 notepad |
|
412 begin |
|
413 fix a b c |
|
414 assume a: "a = b" |
|
415 assume b: "b = c" |
|
416 have "a = c" by (my_simp a b) |
|
417 end |
|
418 |
|
419 text {* Here is a similar method that operates on all subgoals, |
|
420 instead of just the first one. *} |
|
421 |
|
422 method_setup my_simp_all = {* |
|
423 Attrib.thms >> (fn thms => fn ctxt => |
|
424 SIMPLE_METHOD |
|
425 (CHANGED |
|
426 (ALLGOALS (asm_full_simp_tac |
|
427 (put_simpset HOL_basic_ss ctxt addsimps thms))))) |
|
428 *} "rewrite all subgoals by given rules" |
|
429 |
|
430 notepad |
|
431 begin |
|
432 fix a b c |
|
433 assume a: "a = b" |
|
434 assume b: "b = c" |
|
435 have "a = c" and "c = b" by (my_simp_all a b) |
|
436 end |
|
437 |
|
438 text {* \medskip Apart from explicit arguments, common proof methods |
|
439 typically work with a default configuration provided by the context. |
|
440 As a shortcut to rule management we use a cheap solution via functor |
|
441 @{ML_functor Named_Thms} (see also @{file |
|
442 "~~/src/Pure/Tools/named_thms.ML"}). *} |
|
443 |
|
444 ML {* |
|
445 structure My_Simps = |
|
446 Named_Thms |
|
447 (val name = @{binding my_simp} val description = "my_simp rule") |
|
448 *} |
|
449 setup My_Simps.setup |
|
450 |
|
451 text {* This provides ML access to a list of theorems in canonical |
|
452 declaration order via @{ML My_Simps.get}. The user can add or |
|
453 delete rules via the attribute @{attribute my_simp}. The actual |
|
454 proof method is now defined as before, but we append the explicit |
|
455 arguments and the rules from the context. *} |
|
456 |
|
457 method_setup my_simp' = {* |
|
458 Attrib.thms >> (fn thms => fn ctxt => |
|
459 SIMPLE_METHOD' (fn i => |
|
460 CHANGED (asm_full_simp_tac |
|
461 (put_simpset HOL_basic_ss ctxt |
|
462 addsimps (thms @ My_Simps.get ctxt)) i))) |
|
463 *} "rewrite subgoal by given rules and my_simp rules from the context" |
|
464 |
|
465 text {* |
|
466 \medskip Method @{method my_simp'} can be used in Isar proofs |
|
467 like this: |
|
468 *} |
|
469 |
|
470 notepad |
|
471 begin |
|
472 fix a b c |
|
473 assume [my_simp]: "a \<equiv> b" |
|
474 assume [my_simp]: "b \<equiv> c" |
|
475 have "a \<equiv> c" by my_simp' |
|
476 end |
|
477 |
|
478 text {* \medskip The @{method my_simp} variants defined above are |
|
479 ``simple'' methods, i.e.\ the goal facts are merely inserted as goal |
|
480 premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper. |
|
481 For proof methods that are similar to the standard collection of |
|
482 @{method simp}, @{method blast}, @{method fast}, @{method auto} |
|
483 there is little more that can be done. |
|
484 |
|
485 Note that using the primary goal facts in the same manner as the |
|
486 method arguments obtained via concrete syntax or the context does |
|
487 not meet the requirement of ``strong emphasis on facts'' of regular |
|
488 proof methods, because rewrite rules as used above can be easily |
|
489 ignored. A proof text ``@{command using}~@{text "foo"}~@{command |
|
490 "by"}~@{text "my_simp"}'' where @{text "foo"} is not used would |
|
491 deceive the reader. |
|
492 |
|
493 \medskip The technical treatment of rules from the context requires |
|
494 further attention. Above we rebuild a fresh @{ML_type simpset} from |
|
495 the arguments and \emph{all} rules retrieved from the context on |
|
496 every invocation of the method. This does not scale to really large |
|
497 collections of rules, which easily emerges in the context of a big |
|
498 theory library, for example. |
|
499 |
|
500 This is an inherent limitation of the simplistic rule management via |
|
501 functor @{ML_functor Named_Thms}, because it lacks tool-specific |
|
502 storage and retrieval. More realistic applications require |
|
503 efficient index-structures that organize theorems in a customized |
|
504 manner, such as a discrimination net that is indexed by the |
|
505 left-hand sides of rewrite rules. For variations on the Simplifier, |
|
506 re-use of the existing type @{ML_type simpset} is adequate, but |
|
507 scalability would require it be maintained statically within the |
|
508 context data, not dynamically on each tool invocation. *} |
|
509 |
|
510 |
|
511 section {* Attributes \label{sec:attributes} *} |
|
512 |
|
513 text {* An \emph{attribute} is a function @{text "context \<times> thm \<rightarrow> |
|
514 context \<times> thm"}, which means both a (generic) context and a theorem |
|
515 can be modified simultaneously. In practice this mixed form is very |
|
516 rare, instead attributes are presented either as \emph{declaration |
|
517 attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or \emph{rule |
|
518 attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}. |
|
519 |
|
520 Attributes can have additional arguments via concrete syntax. There |
|
521 is a collection of context-sensitive parsers for various logical |
|
522 entities (types, terms, theorems). These already take care of |
|
523 applying morphisms to the arguments when attribute expressions are |
|
524 moved into a different context (see also \secref{sec:morphisms}). |
|
525 |
|
526 When implementing declaration attributes, it is important to operate |
|
527 exactly on the variant of the generic context that is provided by |
|
528 the system, which is either global theory context or local proof |
|
529 context. In particular, the background theory of a local context |
|
530 must not be modified in this situation! *} |
|
531 |
|
532 text %mlref {* |
|
533 \begin{mldecls} |
|
534 @{index_ML_type attribute} \\ |
|
535 @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\ |
|
536 @{index_ML Thm.declaration_attribute: " |
|
537 (thm -> Context.generic -> Context.generic) -> attribute"} \\ |
|
538 @{index_ML Attrib.setup: "binding -> attribute context_parser -> |
|
539 string -> theory -> theory"} \\ |
|
540 \end{mldecls} |
|
541 |
|
542 \begin{description} |
|
543 |
|
544 \item Type @{ML_type attribute} represents attributes as concrete |
|
545 type alias. |
|
546 |
|
547 \item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps |
|
548 a context-dependent rule (mapping on @{ML_type thm}) as attribute. |
|
549 |
|
550 \item @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"} |
|
551 wraps a theorem-dependent declaration (mapping on @{ML_type |
|
552 Context.generic}) as attribute. |
|
553 |
|
554 \item @{ML Attrib.setup}~@{text "name parser description"} provides |
|
555 the functionality of the Isar command @{command attribute_setup} as |
|
556 ML function. |
|
557 |
|
558 \end{description} |
|
559 *} |
|
560 |
|
561 text %mlantiq {* |
|
562 \begin{matharray}{rcl} |
|
563 @{ML_antiquotation_def attributes} & : & @{text ML_antiquotation} \\ |
|
564 \end{matharray} |
|
565 |
|
566 @{rail \<open> |
|
567 @@{ML_antiquotation attributes} attributes |
|
568 \<close>} |
|
569 |
|
570 \begin{description} |
|
571 |
|
572 \item @{text "@{attributes [\<dots>]}"} embeds attribute source |
|
573 representation into the ML text, which is particularly useful with |
|
574 declarations like @{ML Local_Theory.note}. Attribute names are |
|
575 internalized at compile time, but the source is unevaluated. This |
|
576 means attributes with formal arguments (types, terms, theorems) may |
|
577 be subject to odd effects of dynamic scoping! |
|
578 |
|
579 \end{description} |
|
580 *} |
|
581 |
|
582 text %mlex {* See also @{command attribute_setup} in |
|
583 \cite{isabelle-isar-ref} which includes some abstract examples. *} |
|
584 |
|
585 end |