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