12 documents\<close> instead (see also \chref{ch:proofs}). |
12 documents\<close> instead (see also \chref{ch:proofs}). |
13 |
13 |
14 Nonetheless, it is possible to emulate proof scripts by sequential |
14 Nonetheless, it is possible to emulate proof scripts by sequential |
15 refinements of a proof state in backwards mode, notably with the @{command |
15 refinements of a proof state in backwards mode, notably with the @{command |
16 apply} command (see \secref{sec:tactic-commands}). There are also various |
16 apply} command (see \secref{sec:tactic-commands}). There are also various |
17 proof methods that allow to refer to implicit goal state information that |
17 proof methods that allow to refer to implicit goal state information that is |
18 is normally not accessible to structured Isar proofs (see |
18 normally not accessible to structured Isar proofs (see |
19 \secref{sec:tactics}). |
19 \secref{sec:tactics}). |
20 \<close> |
20 \<close> |
21 |
21 |
22 |
22 |
23 section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close> |
23 section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close> |
41 @@{command defer} @{syntax nat}? |
41 @@{command defer} @{syntax nat}? |
42 ; |
42 ; |
43 @@{command prefer} @{syntax nat} |
43 @@{command prefer} @{syntax nat} |
44 \<close>} |
44 \<close>} |
45 |
45 |
46 \<^descr> @{command "supply"} supports fact definitions during goal |
46 \<^descr> @{command "supply"} supports fact definitions during goal refinement: it |
47 refinement: it is similar to @{command "note"}, but it operates in |
47 is similar to @{command "note"}, but it operates in backwards mode and does |
48 backwards mode and does not have any impact on chained facts. |
48 not have any impact on chained facts. |
49 |
49 |
50 \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in |
50 \<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in initial position, but |
51 initial position, but unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus consecutive method applications may be |
51 unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus |
52 given just as in tactic scripts. |
52 consecutive method applications may be given just as in tactic scripts. |
53 |
53 |
54 Facts are passed to \<open>m\<close> as indicated by the goal's |
54 Facts are passed to \<open>m\<close> as indicated by the goal's forward-chain mode, and |
55 forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards. Thus any |
55 are \<^emph>\<open>consumed\<close> afterwards. Thus any further @{command "apply"} command |
56 further @{command "apply"} command would always work in a purely |
56 would always work in a purely backward manner. |
57 backward manner. |
57 |
58 |
58 \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal |
59 \<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal position. Basically, this simulates a |
59 position. Basically, this simulates a multi-step tactic script for @{command |
60 multi-step tactic script for @{command "qed"}, but may be given |
60 "qed"}, but may be given anywhere within the proof body. |
61 anywhere within the proof body. |
61 |
62 |
62 No facts are passed to \<open>m\<close> here. Furthermore, the static context is that of |
63 No facts are passed to \<open>m\<close> here. Furthermore, the static |
63 the enclosing goal (as for actual @{command "qed"}). Thus the proof method |
64 context is that of the enclosing goal (as for actual @{command |
64 may not refer to any assumptions introduced in the current body, for |
65 "qed"}). Thus the proof method may not refer to any assumptions |
65 example. |
66 introduced in the current body, for example. |
66 |
67 |
67 \<^descr> @{command "done"} completes a proof script, provided that the current goal |
68 \<^descr> @{command "done"} completes a proof script, provided that the |
68 state is solved completely. Note that actual structured proof commands |
69 current goal state is solved completely. Note that actual |
69 (e.g.\ ``@{command "."}'' or @{command "sorry"}) may be used to conclude |
70 structured proof commands (e.g.\ ``@{command "."}'' or @{command |
70 proof scripts as well. |
71 "sorry"}) may be used to conclude proof scripts as well. |
71 |
72 |
72 \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> shuffle the list of |
73 \<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close> |
73 pending goals: @{command "defer"} puts off sub-goal \<open>n\<close> to the end of the |
74 shuffle the list of pending goals: @{command "defer"} puts off |
74 list (\<open>n = 1\<close> by default), while @{command "prefer"} brings sub-goal \<open>n\<close> to |
75 sub-goal \<open>n\<close> to the end of the list (\<open>n = 1\<close> by |
75 the front. |
76 default), while @{command "prefer"} brings sub-goal \<open>n\<close> to the |
76 |
77 front. |
77 \<^descr> @{command "back"} does back-tracking over the result sequence of the |
78 |
78 latest proof command. Any proof command may return multiple results, and |
79 \<^descr> @{command "back"} does back-tracking over the result sequence |
79 this command explores the possibilities step-by-step. It is mainly useful |
80 of the latest proof command. Any proof command may return multiple |
80 for experimentation and interactive exploration, and should be avoided in |
81 results, and this command explores the possibilities step-by-step. |
81 finished proofs. |
82 It is mainly useful for experimentation and interactive exploration, |
|
83 and should be avoided in finished proofs. |
|
84 \<close> |
82 \<close> |
85 |
83 |
86 |
84 |
87 section \<open>Explicit subgoal structure\<close> |
85 section \<open>Explicit subgoal structure\<close> |
88 |
86 |
107 configurtation, is turned into a proof context and remaining conclusion. |
105 configurtation, is turned into a proof context and remaining conclusion. |
108 This correponds to @{command fix}~/ @{command assume}~/ @{command show} in |
106 This correponds to @{command fix}~/ @{command assume}~/ @{command show} in |
109 structured proofs, but the text of the parameters, premises and conclusion |
107 structured proofs, but the text of the parameters, premises and conclusion |
110 is not given explicitly. |
108 is not given explicitly. |
111 |
109 |
112 Goal parameters may be specified separately, in order to allow referring |
110 Goal parameters may be specified separately, in order to allow referring to |
113 to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x |
111 them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x y z\<close>'' |
114 y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword |
112 names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword "for"}~\<open>\<dots> x y z\<close>'' |
115 "for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The |
113 names a \<^emph>\<open>suffix\<close> of goal parameters. The latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol |
116 latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter |
114 as notation. Parameter positions may be skipped via dummies (underscore). |
117 positions may be skipped via dummies (underscore). Unspecified names |
115 Unspecified names remain internal, and thus inaccessible in the proof text. |
118 remain internal, and thus inaccessible in the proof text. |
116 |
119 |
117 ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that goal |
120 ``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that |
118 premises should be turned into assumptions of the context (otherwise the |
121 goal premises should be turned into assumptions of the context (otherwise |
119 remaining conclusion is a Pure implication). The fact name and attributes |
122 the remaining conclusion is a Pure implication). The fact name and |
120 are optional; the particular name ``\<open>prems\<close>'' is a common convention for the |
123 attributes are optional; the particular name ``\<open>prems\<close>'' is a common |
121 premises of an arbitrary goal context in proof scripts. |
124 convention for the premises of an arbitrary goal context in proof scripts. |
122 |
125 |
123 ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result of a |
126 ``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result |
124 proven subgoal. Thus it may be re-used in further reasoning, similar to the |
127 of a proven subgoal. Thus it may be re-used in further reasoning, similar |
125 result of @{command show} in structured Isar proofs. |
128 to the result of @{command show} in structured Isar proofs. |
|
129 |
126 |
130 |
127 |
131 Here are some abstract examples: |
128 Here are some abstract examples: |
132 \<close> |
129 \<close> |
133 |
130 |
179 |
176 |
180 |
177 |
181 section \<open>Tactics: improper proof methods \label{sec:tactics}\<close> |
178 section \<open>Tactics: improper proof methods \label{sec:tactics}\<close> |
182 |
179 |
183 text \<open> |
180 text \<open> |
184 The following improper proof methods emulate traditional tactics. |
181 The following improper proof methods emulate traditional tactics. These |
185 These admit direct access to the goal state, which is normally |
182 admit direct access to the goal state, which is normally considered harmful! |
186 considered harmful! In particular, this may involve both numbered |
183 In particular, this may involve both numbered goal addressing (default 1), |
187 goal addressing (default 1), and dynamic instantiation within the |
184 and dynamic instantiation within the scope of some subgoal. |
188 scope of some subgoal. |
|
189 |
185 |
190 \begin{warn} |
186 \begin{warn} |
191 Dynamic instantiations refer to universally quantified parameters |
187 Dynamic instantiations refer to universally quantified parameters of a |
192 of a subgoal (the dynamic context) rather than fixed variables and |
188 subgoal (the dynamic context) rather than fixed variables and term |
193 term abbreviations of a (static) Isar context. |
189 abbreviations of a (static) Isar context. |
194 \end{warn} |
190 \end{warn} |
195 |
191 |
196 Tactic emulation methods, unlike their ML counterparts, admit |
192 Tactic emulation methods, unlike their ML counterparts, admit simultaneous |
197 simultaneous instantiation from both dynamic and static contexts. |
193 instantiation from both dynamic and static contexts. If names occur in both |
198 If names occur in both contexts goal parameters hide locally fixed |
194 contexts goal parameters hide locally fixed variables. Likewise, schematic |
199 variables. Likewise, schematic variables refer to term |
195 variables refer to term abbreviations, if present in the static context. |
200 abbreviations, if present in the static context. Otherwise the |
196 Otherwise the schematic variable is interpreted as a schematic variable and |
201 schematic variable is interpreted as a schematic variable and left |
197 left to be solved by unification with certain parts of the subgoal. |
202 to be solved by unification with certain parts of the subgoal. |
|
203 |
198 |
204 Note that the tactic emulation proof methods in Isabelle/Isar are |
199 Note that the tactic emulation proof methods in Isabelle/Isar are |
205 consistently named \<open>foo_tac\<close>. Note also that variable names |
200 consistently named \<open>foo_tac\<close>. Note also that variable names occurring on |
206 occurring on left hand sides of instantiations must be preceded by a |
201 left hand sides of instantiations must be preceded by a question mark if |
207 question mark if they coincide with a keyword or contain dots. This |
202 they coincide with a keyword or contain dots. This is consistent with the |
208 is consistent with the attribute @{attribute "where"} (see |
203 attribute @{attribute "where"} (see \secref{sec:pure-meth-att}). |
209 \secref{sec:pure-meth-att}). |
|
210 |
204 |
211 \begin{matharray}{rcl} |
205 \begin{matharray}{rcl} |
212 @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\ |
206 @{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\ |
213 @{method_def erule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\ |
207 @{method_def erule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\ |
214 @{method_def drule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\ |
208 @{method_def drule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\ |
237 ; |
231 ; |
238 (@@{method tactic} | @@{method raw_tactic}) @{syntax text} |
232 (@@{method tactic} | @@{method raw_tactic}) @{syntax text} |
239 \<close>} |
233 \<close>} |
240 |
234 |
241 \<^descr> @{method rule_tac} etc. do resolution of rules with explicit |
235 \<^descr> @{method rule_tac} etc. do resolution of rules with explicit |
242 instantiation. This works the same way as the ML tactics @{ML |
236 instantiation. This works the same way as the ML tactics @{ML |
243 Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}). |
237 Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}). |
244 |
238 |
245 Multiple rules may be only given if there is no instantiation; then |
239 Multiple rules may be only given if there is no instantiation; then @{method |
246 @{method rule_tac} is the same as @{ML resolve_tac} in ML (see |
240 rule_tac} is the same as @{ML resolve_tac} in ML (see @{cite |
247 @{cite "isabelle-implementation"}). |
241 "isabelle-implementation"}). |
248 |
242 |
249 \<^descr> @{method cut_tac} inserts facts into the proof state as |
243 \<^descr> @{method cut_tac} inserts facts into the proof state as assumption of a |
250 assumption of a subgoal; instantiations may be given as well. Note |
244 subgoal; instantiations may be given as well. Note that the scope of |
251 that the scope of schematic variables is spread over the main goal |
245 schematic variables is spread over the main goal statement and rule premises |
252 statement and rule premises are turned into new subgoals. This is |
246 are turned into new subgoals. This is in contrast to the regular method |
253 in contrast to the regular method @{method insert} which inserts |
247 @{method insert} which inserts closed rule statements. |
254 closed rule statements. |
248 |
255 |
249 \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise from a subgoal. Note |
256 \<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise |
250 that \<open>\<phi>\<close> may contain schematic variables, to abbreviate the intended |
257 from a subgoal. Note that \<open>\<phi>\<close> may contain schematic |
251 proposition; the first matching subgoal premise will be deleted. Removing |
258 variables, to abbreviate the intended proposition; the first |
252 useless premises from a subgoal increases its readability and can make |
259 matching subgoal premise will be deleted. Removing useless premises |
253 search tactics run faster. |
260 from a subgoal increases its readability and can make search tactics |
254 |
261 run faster. |
255 \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as |
262 |
256 local premises to a subgoal, and poses the same as new subgoals (in the |
263 \<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions |
257 original context). |
264 \<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as local premises to a subgoal, and poses the same |
258 |
265 as new subgoals (in the original context). |
259 \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a goal according to |
266 |
260 the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the \<^emph>\<open>suffix\<close> of variables. |
267 \<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a |
261 |
268 goal according to the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the |
262 \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a subgoal by \<open>n\<close> |
269 \<^emph>\<open>suffix\<close> of variables. |
263 positions: from right to left if \<open>n\<close> is positive, and from left to right if |
270 |
264 \<open>n\<close> is negative; the default value is 1. |
271 \<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a |
265 |
272 subgoal by \<open>n\<close> positions: from right to left if \<open>n\<close> is |
266 \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from any ML text of type |
273 positive, and from left to right if \<open>n\<close> is negative; the |
267 @{ML_type tactic}. Apart from the usual ML environment and the current proof |
274 default value is 1. |
268 context, the ML code may refer to the locally bound values @{ML_text facts}, |
275 |
269 which indicates any current facts used for forward-chaining. |
276 \<^descr> @{method tactic}~\<open>text\<close> produces a proof method from |
270 |
277 any ML text of type @{ML_type tactic}. Apart from the usual ML |
271 \<^descr> @{method raw_tactic} is similar to @{method tactic}, but presents the goal |
278 environment and the current proof context, the ML code may refer to |
272 state in its raw internal form, where simultaneous subgoals appear as |
279 the locally bound values @{ML_text facts}, which indicates any |
273 conjunction of the logical framework instead of the usual split into several |
280 current facts used for forward-chaining. |
274 subgoals. While feature this is useful for debugging of complex method |
281 |
275 definitions, it should not never appear in production theories. |
282 \<^descr> @{method raw_tactic} is similar to @{method tactic}, but |
|
283 presents the goal state in its raw internal form, where simultaneous |
|
284 subgoals appear as conjunction of the logical framework instead of |
|
285 the usual split into several subgoals. While feature this is useful |
|
286 for debugging of complex method definitions, it should not never |
|
287 appear in production theories. |
|
288 \<close> |
276 \<close> |
289 |
277 |
290 end |
278 end |