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