60484
|
1 |
theory Proof_Script
|
|
2 |
imports Base Main
|
|
3 |
begin
|
|
4 |
|
|
5 |
chapter \<open>Proof scripts\<close>
|
|
6 |
|
|
7 |
text \<open>
|
|
8 |
Interactive theorem proving is traditionally associated with ``proof
|
|
9 |
scripts'', but Isabelle/Isar is centered around structured \emph{proof
|
|
10 |
documents} instead (see also \chref{ch:proofs}).
|
|
11 |
|
|
12 |
Nonetheless, it is possible to emulate proof scripts by sequential
|
|
13 |
refinements of a proof state in backwards mode, notably with the @{command
|
|
14 |
apply} command (see \secref{sec:tactic-commands}). There are also various
|
|
15 |
proof methods that allow to refer to implicit goal state information that
|
|
16 |
is normally not accessible to structured Isar proofs (see
|
|
17 |
\secref{sec:tactics}).
|
|
18 |
\<close>
|
|
19 |
|
|
20 |
|
|
21 |
section \<open>Commands for step-wise refinement \label{sec:tactic-commands}\<close>
|
|
22 |
|
|
23 |
text \<open>
|
|
24 |
\begin{matharray}{rcl}
|
|
25 |
@{command_def "supply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
|
|
26 |
@{command_def "apply"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(prove)"} \\
|
|
27 |
@{command_def "apply_end"}@{text "\<^sup>*"} & : & @{text "proof(state) \<rightarrow> proof(state)"} \\
|
|
28 |
@{command_def "done"}@{text "\<^sup>*"} & : & @{text "proof(prove) \<rightarrow> proof(state) | local_theory | theory"} \\
|
|
29 |
@{command_def "defer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
|
|
30 |
@{command_def "prefer"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
|
|
31 |
@{command_def "back"}@{text "\<^sup>*"} & : & @{text "proof \<rightarrow> proof"} \\
|
|
32 |
\end{matharray}
|
|
33 |
|
|
34 |
@{rail \<open>
|
|
35 |
@@{command supply} (@{syntax thmdef}? @{syntax thmrefs} + @'and')
|
|
36 |
;
|
|
37 |
( @@{command apply} | @@{command apply_end} ) @{syntax method}
|
|
38 |
;
|
|
39 |
@@{command defer} @{syntax nat}?
|
|
40 |
;
|
|
41 |
@@{command prefer} @{syntax nat}
|
|
42 |
\<close>}
|
|
43 |
|
|
44 |
\begin{description}
|
|
45 |
|
|
46 |
\item @{command "supply"} supports fact definitions during goal
|
|
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 |
|
|
50 |
\item @{command "apply"}~@{text m} applies proof method @{text m} in
|
|
51 |
initial position, but unlike @{command "proof"} it retains ``@{text
|
|
52 |
"proof(prove)"}'' mode. Thus consecutive method applications may be
|
|
53 |
given just as in tactic scripts.
|
|
54 |
|
|
55 |
Facts are passed to @{text m} as indicated by the goal's
|
|
56 |
forward-chain mode, and are \emph{consumed} afterwards. Thus any
|
|
57 |
further @{command "apply"} command would always work in a purely
|
|
58 |
backward manner.
|
|
59 |
|
|
60 |
\item @{command "apply_end"}~@{text "m"} applies proof method @{text
|
|
61 |
m} as if in terminal position. Basically, this simulates a
|
|
62 |
multi-step tactic script for @{command "qed"}, but may be given
|
|
63 |
anywhere within the proof body.
|
|
64 |
|
|
65 |
No facts are passed to @{text m} here. Furthermore, the static
|
|
66 |
context is that of the enclosing goal (as for actual @{command
|
|
67 |
"qed"}). Thus the proof method may not refer to any assumptions
|
|
68 |
introduced in the current body, for example.
|
|
69 |
|
|
70 |
\item @{command "done"} completes a proof script, provided that the
|
|
71 |
current goal state is solved completely. Note that actual
|
|
72 |
structured proof commands (e.g.\ ``@{command "."}'' or @{command
|
|
73 |
"sorry"}) may be used to conclude proof scripts as well.
|
|
74 |
|
|
75 |
\item @{command "defer"}~@{text n} and @{command "prefer"}~@{text n}
|
|
76 |
shuffle the list of pending goals: @{command "defer"} puts off
|
|
77 |
sub-goal @{text n} to the end of the list (@{text "n = 1"} by
|
|
78 |
default), while @{command "prefer"} brings sub-goal @{text n} to the
|
|
79 |
front.
|
|
80 |
|
|
81 |
\item @{command "back"} does back-tracking over the result sequence
|
|
82 |
of the latest proof command. Any proof command may return multiple
|
|
83 |
results, and this command explores the possibilities step-by-step.
|
|
84 |
It is mainly useful for experimentation and interactive exploration,
|
|
85 |
and should be avoided in finished proofs.
|
|
86 |
|
|
87 |
\end{description}
|
|
88 |
\<close>
|
|
89 |
|
|
90 |
|
|
91 |
section \<open>Tactics: improper proof methods \label{sec:tactics}\<close>
|
|
92 |
|
|
93 |
text \<open>
|
|
94 |
The following improper proof methods emulate traditional tactics.
|
|
95 |
These admit direct access to the goal state, which is normally
|
|
96 |
considered harmful! In particular, this may involve both numbered
|
|
97 |
goal addressing (default 1), and dynamic instantiation within the
|
|
98 |
scope of some subgoal.
|
|
99 |
|
|
100 |
\begin{warn}
|
|
101 |
Dynamic instantiations refer to universally quantified parameters
|
|
102 |
of a subgoal (the dynamic context) rather than fixed variables and
|
|
103 |
term abbreviations of a (static) Isar context.
|
|
104 |
\end{warn}
|
|
105 |
|
|
106 |
Tactic emulation methods, unlike their ML counterparts, admit
|
|
107 |
simultaneous instantiation from both dynamic and static contexts.
|
|
108 |
If names occur in both contexts goal parameters hide locally fixed
|
|
109 |
variables. Likewise, schematic variables refer to term
|
|
110 |
abbreviations, if present in the static context. Otherwise the
|
|
111 |
schematic variable is interpreted as a schematic variable and left
|
|
112 |
to be solved by unification with certain parts of the subgoal.
|
|
113 |
|
|
114 |
Note that the tactic emulation proof methods in Isabelle/Isar are
|
|
115 |
consistently named @{text foo_tac}. Note also that variable names
|
|
116 |
occurring on left hand sides of instantiations must be preceded by a
|
|
117 |
question mark if they coincide with a keyword or contain dots. This
|
|
118 |
is consistent with the attribute @{attribute "where"} (see
|
|
119 |
\secref{sec:pure-meth-att}).
|
|
120 |
|
|
121 |
\begin{matharray}{rcl}
|
|
122 |
@{method_def rule_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
123 |
@{method_def erule_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
124 |
@{method_def drule_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
125 |
@{method_def frule_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
126 |
@{method_def cut_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
127 |
@{method_def thin_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
128 |
@{method_def subgoal_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
129 |
@{method_def rename_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
130 |
@{method_def rotate_tac}@{text "\<^sup>*"} & : & @{text method} \\
|
|
131 |
@{method_def tactic}@{text "\<^sup>*"} & : & @{text method} \\
|
|
132 |
@{method_def raw_tactic}@{text "\<^sup>*"} & : & @{text method} \\
|
|
133 |
\end{matharray}
|
|
134 |
|
|
135 |
@{rail \<open>
|
|
136 |
(@@{method rule_tac} | @@{method erule_tac} | @@{method drule_tac} |
|
|
137 |
@@{method frule_tac} | @@{method cut_tac}) @{syntax goal_spec}? \<newline>
|
|
138 |
(@{syntax named_insts} @{syntax for_fixes} @'in' @{syntax thmref} | @{syntax thmrefs} )
|
|
139 |
;
|
|
140 |
@@{method thin_tac} @{syntax goal_spec}? @{syntax prop} @{syntax for_fixes}
|
|
141 |
;
|
|
142 |
@@{method subgoal_tac} @{syntax goal_spec}? (@{syntax prop} +) @{syntax for_fixes}
|
|
143 |
;
|
|
144 |
@@{method rename_tac} @{syntax goal_spec}? (@{syntax name} +)
|
|
145 |
;
|
|
146 |
@@{method rotate_tac} @{syntax goal_spec}? @{syntax int}?
|
|
147 |
;
|
|
148 |
(@@{method tactic} | @@{method raw_tactic}) @{syntax text}
|
|
149 |
\<close>}
|
|
150 |
|
|
151 |
\begin{description}
|
|
152 |
|
|
153 |
\item @{method rule_tac} etc. do resolution of rules with explicit
|
|
154 |
instantiation. This works the same way as the ML tactics @{ML
|
|
155 |
Rule_Insts.res_inst_tac} etc.\ (see @{cite "isabelle-implementation"}).
|
|
156 |
|
|
157 |
Multiple rules may be only given if there is no instantiation; then
|
|
158 |
@{method rule_tac} is the same as @{ML resolve_tac} in ML (see
|
|
159 |
@{cite "isabelle-implementation"}).
|
|
160 |
|
|
161 |
\item @{method cut_tac} inserts facts into the proof state as
|
|
162 |
assumption of a subgoal; instantiations may be given as well. Note
|
|
163 |
that the scope of schematic variables is spread over the main goal
|
|
164 |
statement and rule premises are turned into new subgoals. This is
|
|
165 |
in contrast to the regular method @{method insert} which inserts
|
|
166 |
closed rule statements.
|
|
167 |
|
|
168 |
\item @{method thin_tac}~@{text \<phi>} deletes the specified premise
|
|
169 |
from a subgoal. Note that @{text \<phi>} may contain schematic
|
|
170 |
variables, to abbreviate the intended proposition; the first
|
|
171 |
matching subgoal premise will be deleted. Removing useless premises
|
|
172 |
from a subgoal increases its readability and can make search tactics
|
|
173 |
run faster.
|
|
174 |
|
|
175 |
\item @{method subgoal_tac}~@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} adds the propositions
|
|
176 |
@{text "\<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"} as local premises to a subgoal, and poses the same
|
|
177 |
as new subgoals (in the original context).
|
|
178 |
|
|
179 |
\item @{method rename_tac}~@{text "x\<^sub>1 \<dots> x\<^sub>n"} renames parameters of a
|
|
180 |
goal according to the list @{text "x\<^sub>1, \<dots>, x\<^sub>n"}, which refers to the
|
|
181 |
\emph{suffix} of variables.
|
|
182 |
|
|
183 |
\item @{method rotate_tac}~@{text n} rotates the premises of a
|
|
184 |
subgoal by @{text n} positions: from right to left if @{text n} is
|
|
185 |
positive, and from left to right if @{text n} is negative; the
|
|
186 |
default value is 1.
|
|
187 |
|
|
188 |
\item @{method tactic}~@{text "text"} produces a proof method from
|
|
189 |
any ML text of type @{ML_type tactic}. Apart from the usual ML
|
|
190 |
environment and the current proof context, the ML code may refer to
|
|
191 |
the locally bound values @{ML_text facts}, which indicates any
|
|
192 |
current facts used for forward-chaining.
|
|
193 |
|
|
194 |
\item @{method raw_tactic} is similar to @{method tactic}, but
|
|
195 |
presents the goal state in its raw internal form, where simultaneous
|
|
196 |
subgoals appear as conjunction of the logical framework instead of
|
|
197 |
the usual split into several subgoals. While feature this is useful
|
|
198 |
for debugging of complex method definitions, it should not never
|
|
199 |
appear in production theories.
|
|
200 |
|
|
201 |
\end{description}
|
|
202 |
\<close>
|
|
203 |
|
|
204 |
end |