author | wenzelm |
Sun, 23 Jan 2011 13:28:10 +0100 | |
changeset 41625 | e4a9ea748bd2 |
parent 40964 | 482a8334ee9e |
child 45414 | 8ca612982014 |
permissions | -rw-r--r-- |
29755 | 1 |
theory Isar |
2 |
imports Base |
|
3 |
begin |
|
20472 | 4 |
|
29759 | 5 |
chapter {* Isar language elements *} |
6 |
||
40126 | 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. |
|
29759 | 10 |
|
11 |
\begin{enumerate} |
|
12 |
||
39842 | 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 |
|
39844 | 16 |
"show"}, @{command "proof"}, and @{command "qed"}. |
39842 | 17 |
|
39844 | 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. |
|
20472 | 21 |
|
39842 | 22 |
\item Proof \emph{methods} define a secondary language of mixed |
23 |
forward-backward refinement steps involving facts and goals. |
|
39846 | 24 |
Typical examples are @{method rule}, @{method unfold}, and @{method |
39844 | 25 |
simp}. |
29759 | 26 |
|
39842 | 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 |
|
39849 | 32 |
annotations to theorems being defined or referenced. Attributes can |
33 |
modify both the context and the theorem. |
|
39842 | 34 |
|
39849 | 35 |
Typical examples are @{attribute intro} (which affects the context), |
36 |
and @{attribute symmetric} (which affects the theorem). |
|
29759 | 37 |
|
38 |
\end{enumerate} |
|
39 |
*} |
|
40 |
||
41 |
||
42 |
section {* Proof commands *} |
|
20520 | 43 |
|
39849 | 44 |
text {* A \emph{proof command} is state transition of the Isar/VM |
45 |
proof interpreter. |
|
46 |
||
40126 | 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. |
|
39842 | 53 |
|
54 |
What can be done realistically is to define some diagnostic commands |
|
39844 | 55 |
that inspect the general state of the Isar/VM, and report some |
56 |
feedback to the user. Typically this involves checking of the |
|
39842 | 57 |
linguistic \emph{mode} of a proof state, or peeking at the pending |
58 |
goals (if available). |
|
39845 | 59 |
|
60 |
Another common application is to define a toplevel command that |
|
40126 | 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 |
|
39845 | 63 |
incorporated into the context of some user-space tool, without |
40126 | 64 |
modifying the Isar proof language itself. *} |
39842 | 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}"} \\ |
|
39845 | 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"} \\ |
|
39842 | 80 |
\end{mldecls} |
81 |
||
82 |
\begin{description} |
|
83 |
||
39864 | 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}). |
|
39842 | 89 |
|
90 |
The general idea is that the facts shall contribute to the |
|
39844 | 91 |
refinement of some parts of the tactical goal --- how exactly is |
92 |
defined by the proof method that is applied in that situation. |
|
39842 | 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 |
|
39846 | 106 |
(like @{method simp} or @{method blast}). The Isar goal facts are |
39842 | 107 |
already inserted as premises into the subgoals, which are presented |
39844 | 108 |
individually as in @{ML Proof.goal}. |
39842 | 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'' |
|
39846 | 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. |
|
39842 | 120 |
|
39845 | 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 |
|
40126 | 133 |
@{ML_type local_theory} here (\chref{ch:local-theory}). This |
134 |
affects the way how results are stored. |
|
39845 | 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 |
|
40126 | 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. |
|
39845 | 141 |
|
39842 | 142 |
\end{description} |
143 |
*} |
|
144 |
||
20520 | 145 |
|
39843 | 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 |
||
40964 | 165 |
notepad |
166 |
begin |
|
39846 | 167 |
have A and B and C |
39866
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset
|
168 |
ML_val {* |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset
|
169 |
val n = Thm.nprems_of (#goal @{Isar.goal}); |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset
|
170 |
@{assert} (n = 3); |
5ec01d5acd0c
more robust examples: explicit @{assert} instead of unchecked output;
wenzelm
parents:
39865
diff
changeset
|
171 |
*} |
39843 | 172 |
oops |
173 |
||
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
174 |
text {* Here we see 3 individual subgoals in the same way as regular |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
175 |
proof methods would do. *} |
39843 | 176 |
|
20520 | 177 |
|
20472 | 178 |
section {* Proof methods *} |
179 |
||
39847 | 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 |
|
39843 | 183 |
enumerates possible follow-up goal states, with the potential |
39844 | 184 |
addition of named extensions of the proof context (\emph{cases}). |
39847 | 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 |
||
40126 | 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. |
|
39843 | 221 |
|
39844 | 222 |
To get a better idea about the range of possibilities, consider the |
40126 | 223 |
following Isar proof schemes. This is the general form of |
224 |
structured proof text: |
|
39843 | 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 |
||
40126 | 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 |
|
39843 | 241 |
subgoals, but it does not see the facts of the initial step. |
242 |
||
40126 | 243 |
\medskip This pattern illustrates unstructured proof scripts: |
39843 | 244 |
|
39844 | 245 |
\medskip |
39843 | 246 |
\begin{tabular}{l} |
247 |
@{command have}~@{text "props"} \\ |
|
39844 | 248 |
\quad@{command using}~@{text "facts\<^sub>1"}~@{command apply}~@{text "method\<^sub>1"} \\ |
39843 | 249 |
\quad@{command apply}~@{text "method\<^sub>2"} \\ |
39844 | 250 |
\quad@{command using}~@{text "facts\<^sub>3"}~@{command apply}~@{text "method\<^sub>3"} \\ |
39843 | 251 |
\quad@{command done} \\ |
252 |
\end{tabular} |
|
253 |
\medskip |
|
254 |
||
40126 | 255 |
The @{text "method\<^sub>1"} operates on the original claim while |
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
256 |
using @{text "facts\<^sub>1"}. Since the @{command apply} command |
40126 | 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. |
|
39843 | 261 |
|
40126 | 262 |
\medskip Empirically, any Isar proof method can be categorized as |
39847 | 263 |
follows. |
39843 | 264 |
|
265 |
\begin{enumerate} |
|
266 |
||
39847 | 267 |
\item \emph{Special method with cases} with named context additions |
268 |
associated with the follow-up goal state. |
|
39843 | 269 |
|
39847 | 270 |
Example: @{method "induct"}, which is also a ``raw'' method since it |
271 |
operates on the internal representation of simultaneous claims as |
|
40126 | 272 |
Pure conjunction (\secref{{sec:logic-aux}}), instead of separate |
273 |
subgoals (\secref{sec::tactical-goals}). |
|
39843 | 274 |
|
39847 | 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. |
|
39843 | 280 |
|
39847 | 281 |
\item \emph{Simple method} with weaker emphasis on facts, which are |
282 |
inserted into subgoals to emulate old-style tactical as |
|
283 |
``premises''. |
|
39843 | 284 |
|
39847 | 285 |
Examples: @{method "simp"}, @{method "blast"}, @{method "auto"}. |
39843 | 286 |
|
39847 | 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). |
|
40126 | 290 |
The naming convention @{text "foo_tac"} makes this special |
291 |
non-standard status clear. |
|
39843 | 292 |
|
39847 | 293 |
Example: @{method "rule_tac"}. |
39843 | 294 |
|
295 |
\end{enumerate} |
|
296 |
||
39847 | 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 |
|
39848 | 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.} |
|
39847 | 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 HEADGOAL: "(int -> tactic) -> tactic"} \\ |
|
315 |
@{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\ |
|
316 |
@{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser -> |
|
317 |
string -> theory -> theory"} \\ |
|
318 |
\end{mldecls} |
|
319 |
||
320 |
\begin{description} |
|
321 |
||
39864 | 322 |
\item Type @{ML_type Proof.method} represents proof methods as |
323 |
abstract type. |
|
39847 | 324 |
|
325 |
\item @{ML METHOD_CASES}~@{text "(fn facts => cases_tactic)"} wraps |
|
326 |
@{text cases_tactic} depending on goal facts as proof method with |
|
327 |
cases; the goal context is passed via method syntax. |
|
328 |
||
329 |
\item @{ML METHOD}~@{text "(fn facts => tactic)"} wraps @{text |
|
330 |
tactic} depending on goal facts as regular proof method; the goal |
|
331 |
context is passed via method syntax. |
|
332 |
||
333 |
\item @{ML SIMPLE_METHOD}~@{text "tactic"} wraps a tactic that |
|
334 |
addresses all subgoals uniformly as simple proof method. Goal facts |
|
335 |
are already inserted into all subgoals before @{text "tactic"} is |
|
336 |
applied. |
|
337 |
||
338 |
\item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that |
|
339 |
addresses a specific subgoal as simple proof method. Goal facts are |
|
340 |
already inserted into the first subgoal before @{text "tactic"} is |
|
341 |
applied to the same. |
|
342 |
||
343 |
\item @{ML HEADGOAL}~@{text "tactic"} applies @{text "tactic"} to |
|
344 |
the first subgoal. This is convenient to reproduce part the @{ML |
|
345 |
SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example. |
|
346 |
||
347 |
\item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text |
|
348 |
"facts"} into subgoal @{text "i"}. This is convenient to reproduce |
|
349 |
part of the @{ML SIMPLE_METHOD} or @{ML SIMPLE_METHOD'} wrapping |
|
350 |
within regular @{ML METHOD}, for example. |
|
351 |
||
352 |
\item @{ML Method.setup}~@{text "name parser description"} provides |
|
39848 | 353 |
the functionality of the Isar command @{command method_setup} as ML |
354 |
function. |
|
39847 | 355 |
|
356 |
\end{description} |
|
357 |
*} |
|
358 |
||
39851 | 359 |
text %mlex {* See also @{command method_setup} in |
360 |
\cite{isabelle-isar-ref} which includes some abstract examples. |
|
361 |
||
362 |
\medskip The following toy examples illustrate how the goal facts |
|
39848 | 363 |
and state are passed to proof methods. The pre-defined proof method |
364 |
called ``@{method tactic}'' wraps ML source of type @{ML_type |
|
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
40126
diff
changeset
|
365 |
tactic} (abstracted over @{ML_text facts}). This allows immediate |
39848 | 366 |
experimentation without parsing of concrete syntax. *} |
20472 | 367 |
|
40964 | 368 |
notepad |
369 |
begin |
|
39847 | 370 |
assume a: A and b: B |
371 |
||
372 |
have "A \<and> B" |
|
373 |
apply (tactic {* rtac @{thm conjI} 1 *}) |
|
374 |
using a apply (tactic {* resolve_tac facts 1 *}) |
|
375 |
using b apply (tactic {* resolve_tac facts 1 *}) |
|
376 |
done |
|
377 |
||
378 |
have "A \<and> B" |
|
379 |
using a and b |
|
380 |
ML_val "@{Isar.goal}" |
|
381 |
apply (tactic {* Method.insert_tac facts 1 *}) |
|
382 |
apply (tactic {* (rtac @{thm conjI} THEN_ALL_NEW atac) 1 *}) |
|
383 |
done |
|
40964 | 384 |
end |
39847 | 385 |
|
39848 | 386 |
text {* \medskip The next example implements a method that simplifies |
387 |
the first subgoal by rewrite rules given as arguments. *} |
|
388 |
||
389 |
method_setup my_simp = {* |
|
390 |
Attrib.thms >> (fn thms => fn ctxt => |
|
391 |
SIMPLE_METHOD' (fn i => |
|
392 |
CHANGED (asm_full_simp_tac |
|
393 |
(HOL_basic_ss addsimps thms) i))) |
|
394 |
*} "rewrite subgoal by given rules" |
|
395 |
||
396 |
text {* The concrete syntax wrapping of @{command method_setup} always |
|
397 |
passes-through the proof context at the end of parsing, but it is |
|
398 |
not used in this example. |
|
399 |
||
400 |
The @{ML Attrib.thms} parser produces a list of theorems from the |
|
401 |
usual Isar syntax involving attribute expressions etc.\ (syntax |
|
40126 | 402 |
category @{syntax thmrefs}) \cite{isabelle-isar-ref}. The resulting |
40149
4c35be108990
proper markup of uninterpreted ML text as @{ML_text}, not @{verbatim};
wenzelm
parents:
40126
diff
changeset
|
403 |
@{ML_text thms} are added to @{ML HOL_basic_ss} which already |
40126 | 404 |
contains the basic Simplifier setup for HOL. |
39848 | 405 |
|
406 |
The tactic @{ML asm_full_simp_tac} is the one that is also used in |
|
407 |
method @{method simp} by default. The extra wrapping by the @{ML |
|
408 |
CHANGED} tactical ensures progress of simplification: identical goal |
|
409 |
states are filtered out explicitly to make the raw tactic conform to |
|
410 |
standard Isar method behaviour. |
|
411 |
||
412 |
\medskip Method @{method my_simp} can be used in Isar proofs like |
|
413 |
this: |
|
39847 | 414 |
*} |
415 |
||
40964 | 416 |
notepad |
417 |
begin |
|
39848 | 418 |
fix a b c |
39851 | 419 |
assume a: "a = b" |
420 |
assume b: "b = c" |
|
421 |
have "a = c" by (my_simp a b) |
|
40964 | 422 |
end |
39851 | 423 |
|
424 |
text {* Here is a similar method that operates on all subgoals, |
|
425 |
instead of just the first one. *} |
|
426 |
||
427 |
method_setup my_simp_all = {* |
|
428 |
Attrib.thms >> (fn thms => fn ctxt => |
|
429 |
SIMPLE_METHOD |
|
430 |
(CHANGED |
|
431 |
(ALLGOALS (asm_full_simp_tac |
|
432 |
(HOL_basic_ss addsimps thms))))) |
|
433 |
*} "rewrite all subgoals by given rules" |
|
434 |
||
40964 | 435 |
notepad |
436 |
begin |
|
39851 | 437 |
fix a b c |
438 |
assume a: "a = b" |
|
439 |
assume b: "b = c" |
|
440 |
have "a = c" and "c = b" by (my_simp_all a b) |
|
40964 | 441 |
end |
39848 | 442 |
|
443 |
text {* \medskip Apart from explicit arguments, common proof methods |
|
444 |
typically work with a default configuration provided by the context. |
|
445 |
As a shortcut to rule management we use a cheap solution via functor |
|
40800
330eb65c9469
Parse.liberal_name for document antiquotations and attributes;
wenzelm
parents:
40149
diff
changeset
|
446 |
@{ML_functor Named_Thms} (see also @{file |
39848 | 447 |
"~~/src/Pure/Tools/named_thms.ML"}). *} |
448 |
||
39847 | 449 |
ML {* |
450 |
structure My_Simps = |
|
451 |
Named_Thms |
|
452 |
(val name = "my_simp" val description = "my_simp rule") |
|
453 |
*} |
|
454 |
setup My_Simps.setup |
|
455 |
||
39861
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
456 |
text {* This provides ML access to a list of theorems in canonical |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
457 |
declaration order via @{ML My_Simps.get}. The user can add or |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
458 |
delete rules via the attribute @{attribute my_simp}. The actual |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
459 |
proof method is now defined as before, but we append the explicit |
b8d89db3e238
use continental paragraph style, which works better with mixture of (in)formal text;
wenzelm
parents:
39851
diff
changeset
|
460 |
arguments and the rules from the context. *} |
39847 | 461 |
|
39848 | 462 |
method_setup my_simp' = {* |
463 |
Attrib.thms >> (fn thms => fn ctxt => |
|
39847 | 464 |
SIMPLE_METHOD' (fn i => |
465 |
CHANGED (asm_full_simp_tac |
|
39848 | 466 |
(HOL_basic_ss addsimps (thms @ My_Simps.get ctxt)) i))) |
467 |
*} "rewrite subgoal by given rules and my_simp rules from the context" |
|
39847 | 468 |
|
39848 | 469 |
text {* |
470 |
\medskip Method @{method my_simp'} can be used in Isar proofs |
|
471 |
like this: |
|
472 |
*} |
|
39847 | 473 |
|
40964 | 474 |
notepad |
475 |
begin |
|
39847 | 476 |
fix a b c |
477 |
assume [my_simp]: "a \<equiv> b" |
|
478 |
assume [my_simp]: "b \<equiv> c" |
|
39848 | 479 |
have "a \<equiv> c" by my_simp' |
40964 | 480 |
end |
39847 | 481 |
|
39851 | 482 |
text {* \medskip The @{method my_simp} variants defined above are |
483 |
``simple'' methods, i.e.\ the goal facts are merely inserted as goal |
|
484 |
premises by the @{ML SIMPLE_METHOD'} or @{ML SIMPLE_METHOD} wrapper. |
|
485 |
For proof methods that are similar to the standard collection of |
|
40126 | 486 |
@{method simp}, @{method blast}, @{method fast}, @{method auto} |
487 |
there is little more that can be done. |
|
39847 | 488 |
|
489 |
Note that using the primary goal facts in the same manner as the |
|
39848 | 490 |
method arguments obtained via concrete syntax or the context does |
491 |
not meet the requirement of ``strong emphasis on facts'' of regular |
|
492 |
proof methods, because rewrite rules as used above can be easily |
|
493 |
ignored. A proof text ``@{command using}~@{text "foo"}~@{command |
|
494 |
"by"}~@{text "my_simp"}'' where @{text "foo"} is not used would |
|
495 |
deceive the reader. |
|
39847 | 496 |
|
497 |
\medskip The technical treatment of rules from the context requires |
|
498 |
further attention. Above we rebuild a fresh @{ML_type simpset} from |
|
39848 | 499 |
the arguments and \emph{all} rules retrieved from the context on |
500 |
every invocation of the method. This does not scale to really large |
|
501 |
collections of rules, which easily emerges in the context of a big |
|
502 |
theory library, for example. |
|
39847 | 503 |
|
39848 | 504 |
This is an inherent limitation of the simplistic rule management via |
505 |
functor @{ML_functor Named_Thms}, because it lacks tool-specific |
|
39847 | 506 |
storage and retrieval. More realistic applications require |
507 |
efficient index-structures that organize theorems in a customized |
|
508 |
manner, such as a discrimination net that is indexed by the |
|
39848 | 509 |
left-hand sides of rewrite rules. For variations on the Simplifier, |
510 |
re-use of the existing type @{ML_type simpset} is adequate, but |
|
40126 | 511 |
scalability would require it be maintained statically within the |
512 |
context data, not dynamically on each tool invocation. *} |
|
39847 | 513 |
|
29759 | 514 |
|
39865 | 515 |
section {* Attributes \label{sec:attributes} *} |
20472 | 516 |
|
39849 | 517 |
text {* An \emph{attribute} is a function @{text "context \<times> thm \<rightarrow> |
518 |
context \<times> thm"}, which means both a (generic) context and a theorem |
|
519 |
can be modified simultaneously. In practice this fully general form |
|
520 |
is very rare, instead attributes are presented either as |
|
521 |
\emph{declaration attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or |
|
522 |
\emph{rule attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}. |
|
523 |
||
524 |
Attributes can have additional arguments via concrete syntax. There |
|
525 |
is a collection of context-sensitive parsers for various logical |
|
526 |
entities (types, terms, theorems). These already take care of |
|
527 |
applying morphisms to the arguments when attribute expressions are |
|
528 |
moved into a different context (see also \secref{sec:morphisms}). |
|
529 |
||
530 |
When implementing declaration attributes, it is important to operate |
|
531 |
exactly on the variant of the generic context that is provided by |
|
532 |
the system, which is either global theory context or local proof |
|
533 |
context. In particular, the background theory of a local context |
|
534 |
must not be modified in this situation! *} |
|
535 |
||
536 |
text %mlref {* |
|
537 |
\begin{mldecls} |
|
538 |
@{index_ML_type attribute: "Context.generic * thm -> Context.generic * thm"} \\ |
|
539 |
@{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\ |
|
540 |
@{index_ML Thm.declaration_attribute: " |
|
541 |
(thm -> Context.generic -> Context.generic) -> attribute"} \\ |
|
542 |
@{index_ML Attrib.setup: "binding -> attribute context_parser -> |
|
543 |
string -> theory -> theory"} \\ |
|
544 |
\end{mldecls} |
|
545 |
||
546 |
\begin{description} |
|
547 |
||
39864 | 548 |
\item Type @{ML_type attribute} represents attributes as concrete |
549 |
type alias. |
|
39849 | 550 |
|
551 |
\item @{ML Thm.rule_attribute}~@{text "(fn context => rule)"} wraps |
|
552 |
a context-dependent rule (mapping on @{ML_type thm}) as attribute. |
|
553 |
||
554 |
\item @{ML Thm.declaration_attribute}~@{text "(fn thm => decl)"} |
|
555 |
wraps a theorem-dependent declaration (mapping on @{ML_type |
|
556 |
Context.generic}) as attribute. |
|
557 |
||
558 |
\item @{ML Attrib.setup}~@{text "name parser description"} provides |
|
559 |
the functionality of the Isar command @{command attribute_setup} as |
|
560 |
ML function. |
|
561 |
||
562 |
\end{description} |
|
563 |
*} |
|
564 |
||
565 |
text %mlex {* See also @{command attribute_setup} in |
|
566 |
\cite{isabelle-isar-ref} which includes some abstract examples. *} |
|
30272 | 567 |
|
20472 | 568 |
end |