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