61656
|
1 |
(*:maxLineLen=78:*)
|
|
2 |
|
60484
|
3 |
theory Proof_Script
|
|
4 |
imports Base Main
|
|
5 |
begin
|
|
6 |
|
|
7 |
chapter \<open>Proof scripts\<close>
|
|
8 |
|
|
9 |
text \<open>
|
|
10 |
Interactive theorem proving is traditionally associated with ``proof
|
61477
|
11 |
scripts'', but Isabelle/Isar is centered around structured \<^emph>\<open>proof
|
|
12 |
documents\<close> instead (see also \chref{ch:proofs}).
|
60484
|
13 |
|
|
14 |
Nonetheless, it is possible to emulate proof scripts by sequential
|
|
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
|
|
17 |
proof methods that allow to refer to implicit goal state information that
|
|
18 |
is normally not accessible to structured Isar proofs (see
|
|
19 |
\secref{sec:tactics}).
|
|
20 |
\<close>
|
|
21 |
|
|
22 |
|
|
23 |
section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
|
|
24 |
|
|
25 |
text \<open>
|
|
26 |
\begin{matharray}{rcl}
|
61493
|
27 |
@{command_def "supply"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
|
|
28 |
@{command_def "apply"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
|
|
29 |
@{command_def "apply_end"}\<open>\<^sup>*\<close> & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
|
|
30 |
@{command_def "done"}\<open>\<^sup>*\<close> & : & \<open>proof(prove) \<rightarrow> proof(state) | local_theory | theory\<close> \\
|
|
31 |
@{command_def "defer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
|
|
32 |
@{command_def "prefer"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
|
|
33 |
@{command_def "back"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
|
60484
|
34 |
\end{matharray}
|
|
35 |
|
|
36 |
@{rail \<open>
|
|
37 |
@@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
|
|
38 |
;
|
|
39 |
( @@{command apply} | @@{command apply_end} ) @{syntax method}
|
|
40 |
;
|
|
41 |
@@{command defer} @{syntax nat}?
|
|
42 |
;
|
|
43 |
@@{command prefer} @{syntax nat}
|
|
44 |
\<close>}
|
|
45 |
|
61439
|
46 |
\<^descr> @{command "supply"} supports fact definitions during goal
|
60484
|
47 |
refinement: it is similar to @{command "note"}, but it operates in
|
|
48 |
backwards mode and does not have any impact on chained facts.
|
|
49 |
|
61493
|
50 |
\<^descr> @{command "apply"}~\<open>m\<close> applies proof method \<open>m\<close> in
|
|
51 |
initial position, but unlike @{command "proof"} it retains ``\<open>proof(prove)\<close>'' mode. Thus consecutive method applications may be
|
60484
|
52 |
given just as in tactic scripts.
|
|
53 |
|
61493
|
54 |
Facts are passed to \<open>m\<close> as indicated by the goal's
|
61477
|
55 |
forward-chain mode, and are \<^emph>\<open>consumed\<close> afterwards. Thus any
|
60484
|
56 |
further @{command "apply"} command would always work in a purely
|
|
57 |
backward manner.
|
|
58 |
|
61493
|
59 |
\<^descr> @{command "apply_end"}~\<open>m\<close> applies proof method \<open>m\<close> as if in terminal position. Basically, this simulates a
|
60484
|
60 |
multi-step tactic script for @{command "qed"}, but may be given
|
|
61 |
anywhere within the proof body.
|
|
62 |
|
61493
|
63 |
No facts are passed to \<open>m\<close> here. Furthermore, the static
|
60484
|
64 |
context is that of the enclosing goal (as for actual @{command
|
|
65 |
"qed"}). Thus the proof method may not refer to any assumptions
|
|
66 |
introduced in the current body, for example.
|
|
67 |
|
61439
|
68 |
\<^descr> @{command "done"} completes a proof script, provided that the
|
60484
|
69 |
current goal state is solved completely. Note that actual
|
|
70 |
structured proof commands (e.g.\ ``@{command "."}'' or @{command
|
|
71 |
"sorry"}) may be used to conclude proof scripts as well.
|
|
72 |
|
61493
|
73 |
\<^descr> @{command "defer"}~\<open>n\<close> and @{command "prefer"}~\<open>n\<close>
|
60484
|
74 |
shuffle the list of pending goals: @{command "defer"} puts off
|
61493
|
75 |
sub-goal \<open>n\<close> to the end of the list (\<open>n = 1\<close> by
|
|
76 |
default), while @{command "prefer"} brings sub-goal \<open>n\<close> to the
|
60484
|
77 |
front.
|
|
78 |
|
61439
|
79 |
\<^descr> @{command "back"} does back-tracking over the result sequence
|
60484
|
80 |
of the latest proof command. Any proof command may return multiple
|
|
81 |
results, and this command explores the possibilities step-by-step.
|
|
82 |
It is mainly useful for experimentation and interactive exploration,
|
|
83 |
and should be avoided in finished proofs.
|
|
84 |
\<close>
|
|
85 |
|
|
86 |
|
60631
|
87 |
section \<open>Explicit subgoal structure\<close>
|
|
88 |
|
|
89 |
text \<open>
|
|
90 |
\begin{matharray}{rcl}
|
61493
|
91 |
@{command_def "subgoal"}\<open>\<^sup>*\<close> & : & \<open>proof \<rightarrow> proof\<close> \\
|
60631
|
92 |
\end{matharray}
|
|
93 |
|
|
94 |
@{rail \<open>
|
|
95 |
@@{command subgoal} @{syntax thmbind}? prems? params?
|
|
96 |
;
|
|
97 |
prems: @'premises' @{syntax thmbind}?
|
|
98 |
;
|
|
99 |
params: @'for' '\<dots>'? (('_' | @{syntax name})+)
|
|
100 |
\<close>}
|
|
101 |
|
61439
|
102 |
\<^descr> @{command "subgoal"} allows to impose some structure on backward
|
60631
|
103 |
refinements, to avoid proof scripts degenerating into long of @{command
|
|
104 |
apply} sequences.
|
|
105 |
|
|
106 |
The current goal state, which is essentially a hidden part of the Isar/VM
|
|
107 |
configurtation, is turned into a proof context and remaining conclusion.
|
|
108 |
This correponds to @{command fix}~/ @{command assume}~/ @{command show} in
|
|
109 |
structured proofs, but the text of the parameters, premises and conclusion
|
|
110 |
is not given explicitly.
|
|
111 |
|
|
112 |
Goal parameters may be specified separately, in order to allow referring
|
61493
|
113 |
to them in the proof body: ``@{command subgoal}~@{keyword "for"}~\<open>x
|
|
114 |
y z\<close>'' names a \<^emph>\<open>prefix\<close>, and ``@{command subgoal}~@{keyword
|
|
115 |
"for"}~\<open>\<dots> x y z\<close>'' names a \<^emph>\<open>suffix\<close> of goal parameters. The
|
61503
|
116 |
latter uses a literal \<^verbatim>\<open>\<dots>\<close> symbol as notation. Parameter
|
60631
|
117 |
positions may be skipped via dummies (underscore). Unspecified names
|
|
118 |
remain internal, and thus inaccessible in the proof text.
|
|
119 |
|
61493
|
120 |
``@{command subgoal}~@{keyword "premises"}~\<open>prems\<close>'' indicates that
|
60631
|
121 |
goal premises should be turned into assumptions of the context (otherwise
|
|
122 |
the remaining conclusion is a Pure implication). The fact name and
|
61493
|
123 |
attributes are optional; the particular name ``\<open>prems\<close>'' is a common
|
60631
|
124 |
convention for the premises of an arbitrary goal context in proof scripts.
|
|
125 |
|
61493
|
126 |
``@{command subgoal}~\<open>result\<close>'' indicates a fact name for the result
|
60631
|
127 |
of a proven subgoal. Thus it may be re-used in further reasoning, similar
|
|
128 |
to the result of @{command show} in structured Isar proofs.
|
|
129 |
|
|
130 |
|
|
131 |
Here are some abstract examples:
|
|
132 |
\<close>
|
|
133 |
|
|
134 |
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
|
|
135 |
and "\<And>u v. X u \<Longrightarrow> Y v"
|
|
136 |
subgoal sorry
|
|
137 |
subgoal sorry
|
|
138 |
done
|
|
139 |
|
|
140 |
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
|
|
141 |
and "\<And>u v. X u \<Longrightarrow> Y v"
|
|
142 |
subgoal for x y z sorry
|
|
143 |
subgoal for u v sorry
|
|
144 |
done
|
|
145 |
|
|
146 |
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
|
|
147 |
and "\<And>u v. X u \<Longrightarrow> Y v"
|
|
148 |
subgoal premises for x y z
|
|
149 |
using \<open>A x\<close> \<open>B y\<close>
|
|
150 |
sorry
|
|
151 |
subgoal premises for u v
|
|
152 |
using \<open>X u\<close>
|
|
153 |
sorry
|
|
154 |
done
|
|
155 |
|
|
156 |
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
|
|
157 |
and "\<And>u v. X u \<Longrightarrow> Y v"
|
|
158 |
subgoal r premises prems for x y z
|
|
159 |
proof -
|
|
160 |
have "A x" by (fact prems)
|
|
161 |
moreover have "B y" by (fact prems)
|
|
162 |
ultimately show ?thesis sorry
|
|
163 |
qed
|
|
164 |
subgoal premises prems for u v
|
|
165 |
proof -
|
|
166 |
have "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z" by (fact r)
|
|
167 |
moreover
|
|
168 |
have "X u" by (fact prems)
|
|
169 |
ultimately show ?thesis sorry
|
|
170 |
qed
|
|
171 |
done
|
|
172 |
|
|
173 |
lemma "\<And>x y z. A x \<Longrightarrow> B y \<Longrightarrow> C z"
|
|
174 |
subgoal premises prems for \<dots> z
|
|
175 |
proof -
|
|
176 |
from prems show "C z" sorry
|
|
177 |
qed
|
|
178 |
done
|
|
179 |
|
|
180 |
|
60484
|
181 |
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
|
|
182 |
|
|
183 |
text \<open>
|
|
184 |
The following improper proof methods emulate traditional tactics.
|
|
185 |
These admit direct access to the goal state, which is normally
|
|
186 |
considered harmful! In particular, this may involve both numbered
|
|
187 |
goal addressing (default 1), and dynamic instantiation within the
|
|
188 |
scope of some subgoal.
|
|
189 |
|
|
190 |
\begin{warn}
|
|
191 |
Dynamic instantiations refer to universally quantified parameters
|
|
192 |
of a subgoal (the dynamic context) rather than fixed variables and
|
|
193 |
term abbreviations of a (static) Isar context.
|
|
194 |
\end{warn}
|
|
195 |
|
|
196 |
Tactic emulation methods, unlike their ML counterparts, admit
|
|
197 |
simultaneous instantiation from both dynamic and static contexts.
|
|
198 |
If names occur in both contexts goal parameters hide locally fixed
|
|
199 |
variables. Likewise, schematic variables refer to term
|
|
200 |
abbreviations, if present in the static context. Otherwise the
|
|
201 |
schematic variable is interpreted as a schematic variable and left
|
|
202 |
to be solved by unification with certain parts of the subgoal.
|
|
203 |
|
|
204 |
Note that the tactic emulation proof methods in Isabelle/Isar are
|
61493
|
205 |
consistently named \<open>foo_tac\<close>. Note also that variable names
|
60484
|
206 |
occurring on left hand sides of instantiations must be preceded by a
|
|
207 |
question mark if they coincide with a keyword or contain dots. This
|
|
208 |
is consistent with the attribute @{attribute "where"} (see
|
|
209 |
\secref{sec:pure-meth-att}).
|
|
210 |
|
|
211 |
\begin{matharray}{rcl}
|
61493
|
212 |
@{method_def rule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
213 |
@{method_def erule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
214 |
@{method_def drule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
215 |
@{method_def frule_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
216 |
@{method_def cut_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
217 |
@{method_def thin_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
218 |
@{method_def subgoal_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
219 |
@{method_def rename_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
220 |
@{method_def rotate_tac}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
221 |
@{method_def tactic}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
|
222 |
@{method_def raw_tactic}\<open>\<^sup>*\<close> & : & \<open>method\<close> \\
|
60484
|
223 |
\end{matharray}
|
|
224 |
|
|
225 |
@{rail \<open>
|
|
226 |
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
|
|
227 |
@@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
|
|
228 |
(@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
|
|
229 |
;
|
|
230 |
@@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
|
|
231 |
;
|
|
232 |
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
|
|
233 |
;
|
|
234 |
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
|
|
235 |
;
|
|
236 |
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
|
|
237 |
;
|
|
238 |
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
|
|
239 |
\<close>}
|
|
240 |
|
61439
|
241 |
\<^descr> @{method rule_tac} etc. do resolution of rules with explicit
|
60484
|
242 |
instantiation. This works the same way as the ML tactics @{ML
|
|
243 |
Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
|
|
244 |
|
|
245 |
Multiple rules may be only given if there is no instantiation; then
|
|
246 |
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
|
|
247 |
@{cite "isabelle-implementation"}).
|
|
248 |
|
61439
|
249 |
\<^descr> @{method cut_tac} inserts facts into the proof state as
|
60484
|
250 |
assumption of a subgoal; instantiations may be given as well. Note
|
|
251 |
that the scope of schematic variables is spread over the main goal
|
|
252 |
statement and rule premises are turned into new subgoals. This is
|
|
253 |
in contrast to the regular method @{method insert} which inserts
|
|
254 |
closed rule statements.
|
|
255 |
|
61493
|
256 |
\<^descr> @{method thin_tac}~\<open>\<phi>\<close> deletes the specified premise
|
|
257 |
from a subgoal. Note that \<open>\<phi>\<close> may contain schematic
|
60484
|
258 |
variables, to abbreviate the intended proposition; the first
|
|
259 |
matching subgoal premise will be deleted. Removing useless premises
|
|
260 |
from a subgoal increases its readability and can make search tactics
|
|
261 |
run faster.
|
|
262 |
|
61493
|
263 |
\<^descr> @{method subgoal_tac}~\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> adds the propositions
|
|
264 |
\<open>\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> as local premises to a subgoal, and poses the same
|
60484
|
265 |
as new subgoals (in the original context).
|
|
266 |
|
61493
|
267 |
\<^descr> @{method rename_tac}~\<open>x\<^sub>1 \<dots> x\<^sub>n\<close> renames parameters of a
|
|
268 |
goal according to the list \<open>x\<^sub>1, \<dots>, x\<^sub>n\<close>, which refers to the
|
61477
|
269 |
\<^emph>\<open>suffix\<close> of variables.
|
60484
|
270 |
|
61493
|
271 |
\<^descr> @{method rotate_tac}~\<open>n\<close> rotates the premises of a
|
|
272 |
subgoal by \<open>n\<close> positions: from right to left if \<open>n\<close> is
|
|
273 |
positive, and from left to right if \<open>n\<close> is negative; the
|
60484
|
274 |
default value is 1.
|
|
275 |
|
61493
|
276 |
\<^descr> @{method tactic}~\<open>text\<close> produces a proof method from
|
60484
|
277 |
any ML text of type @{ML_type tactic}. Apart from the usual ML
|
|
278 |
environment and the current proof context, the ML code may refer to
|
|
279 |
the locally bound values @{ML_text facts}, which indicates any
|
|
280 |
current facts used for forward-chaining.
|
|
281 |
|
61439
|
282 |
\<^descr> @{method raw_tactic} is similar to @{method tactic}, but
|
60484
|
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>
|
|
289 |
|
|
290 |
end |