18537
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{tactic}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
\isanewline
|
|
7 |
\isanewline
|
|
8 |
\isanewline
|
|
9 |
%
|
|
10 |
\endisadelimtheory
|
|
11 |
%
|
|
12 |
\isatagtheory
|
|
13 |
\isacommand{theory}\isamarkupfalse%
|
|
14 |
\ tactic\ \isakeyword{imports}\ base\ \isakeyword{begin}%
|
|
15 |
\endisatagtheory
|
|
16 |
{\isafoldtheory}%
|
|
17 |
%
|
|
18 |
\isadelimtheory
|
|
19 |
%
|
|
20 |
\endisadelimtheory
|
|
21 |
%
|
|
22 |
\isamarkupchapter{Tactical theorem proving%
|
|
23 |
}
|
|
24 |
\isamarkuptrue%
|
|
25 |
%
|
|
26 |
\begin{isamarkuptext}%
|
|
27 |
The basic idea of tactical theorem proving is to refine the
|
|
28 |
initial claim in a backwards fashion, until a solved form is reached.
|
|
29 |
An intermediate goal consists of several subgoals that need to be
|
|
30 |
solved in order to achieve the main statement; zero subgoals means
|
|
31 |
that the proof may be finished. Goal refinement operations are called
|
|
32 |
tactics; combinators for composing tactics are called tacticals.%
|
|
33 |
\end{isamarkuptext}%
|
|
34 |
\isamarkuptrue%
|
|
35 |
%
|
|
36 |
\isamarkupsection{Goals \label{sec:tactical-goals}%
|
|
37 |
}
|
|
38 |
\isamarkuptrue%
|
|
39 |
%
|
|
40 |
\begin{isamarkuptext}%
|
|
41 |
Isabelle/Pure represents a goal\glossary{Tactical goal}{A
|
|
42 |
theorem of \seeglossary{Horn Clause} form stating that a number of
|
|
43 |
subgoals imply the main conclusion, which is marked as a protected
|
|
44 |
proposition.} as a theorem stating that the subgoals imply the main
|
|
45 |
goal: \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}. The outermost goal
|
|
46 |
structure is that of a Horn Clause\glossary{Horn Clause}{An iterated
|
|
47 |
implication \isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}, without any
|
|
48 |
outermost quantifiers. Strictly speaking, propositions \isa{A\isactrlsub i} need to be atomic in Horn Clauses, but Isabelle admits
|
|
49 |
arbitrary substructure here (nested \isa{{\isasymLongrightarrow}} and \isa{{\isasymAnd}}
|
|
50 |
connectives).}: an iterated implication without any
|
|
51 |
quantifiers\footnote{Recall that outermost \isa{{\isasymAnd}x{\isachardot}\ {\isasymphi}{\isacharbrackleft}x{\isacharbrackright}} is
|
|
52 |
always represented via schematic variables in the body: \isa{{\isasymphi}{\isacharbrackleft}{\isacharquery}x{\isacharbrackright}}. These may get instantiated during the course of
|
|
53 |
reasoning.}. For \isa{n\ {\isacharequal}\ {\isadigit{0}}} a goal is solved.
|
|
54 |
|
|
55 |
The structure of each subgoal \isa{A\isactrlsub i} is that of a general
|
|
56 |
Heriditary Harrop Formula \isa{{\isasymAnd}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ {\isasymAnd}x\isactrlsub k{\isachardot}\ H\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ H\isactrlsub m\ {\isasymLongrightarrow}\ B} according to the normal form where any local
|
|
57 |
\isa{{\isasymAnd}} is pulled before \isa{{\isasymLongrightarrow}}. Here \isa{x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub k} are goal parameters, i.e.\ arbitrary-but-fixed entities of
|
|
58 |
certain types, and \isa{H\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ H\isactrlsub m} are goal
|
|
59 |
hypotheses, i.e.\ facts that may be assumed locally. Together, this
|
|
60 |
forms the goal context of the conclusion \isa{B} to be established.
|
|
61 |
The goal hypotheses may be again arbitrary Harrop Formulas, although
|
|
62 |
the level of nesting rarely exceeds 1--2 in practice.
|
|
63 |
|
|
64 |
The main conclusion \isa{C} is internally marked as a protected
|
|
65 |
proposition\glossary{Protected proposition}{An arbitrarily structured
|
|
66 |
proposition \isa{C} which is forced to appear as atomic by
|
|
67 |
wrapping it into a propositional identity operator; notation \isa{{\isacharhash}C}. Protecting a proposition prevents basic inferences from
|
|
68 |
entering into that structure for the time being.}, which is
|
|
69 |
occasionally represented explicitly by the notation \isa{{\isacharhash}C}.
|
|
70 |
This ensures that the decomposition into subgoals and main conclusion
|
|
71 |
is well-defined for arbitrarily structured claims.
|
|
72 |
|
|
73 |
\medskip Basic goal management is performed via the following
|
|
74 |
Isabelle/Pure rules:
|
|
75 |
|
|
76 |
\[
|
|
77 |
\infer[\isa{{\isacharparenleft}init{\isacharparenright}}]{\isa{C\ {\isasymLongrightarrow}\ {\isacharhash}C}}{} \qquad
|
|
78 |
\infer[\isa{{\isacharparenleft}finish{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}}
|
|
79 |
\]
|
|
80 |
|
|
81 |
\medskip The following low-level variants admit general reasoning
|
|
82 |
with protected propositions:
|
|
83 |
|
|
84 |
\[
|
|
85 |
\infer[\isa{{\isacharparenleft}protect{\isacharparenright}}]{\isa{{\isacharhash}C}}{\isa{C}} \qquad
|
|
86 |
\infer[\isa{{\isacharparenleft}conclude{\isacharparenright}}]{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ C}}{\isa{A\isactrlsub {\isadigit{1}}\ {\isasymLongrightarrow}\ {\isasymdots}\ {\isasymLongrightarrow}\ A\isactrlsub n\ {\isasymLongrightarrow}\ {\isacharhash}C}}
|
|
87 |
\]%
|
|
88 |
\end{isamarkuptext}%
|
|
89 |
\isamarkuptrue%
|
|
90 |
%
|
|
91 |
\isadelimmlref
|
|
92 |
%
|
|
93 |
\endisadelimmlref
|
|
94 |
%
|
|
95 |
\isatagmlref
|
|
96 |
%
|
|
97 |
\begin{isamarkuptext}%
|
|
98 |
\begin{mldecls}
|
|
99 |
\indexml{Goal.init}\verb|Goal.init: cterm -> thm| \\
|
|
100 |
\indexml{Goal.finish}\verb|Goal.finish: thm -> thm| \\
|
|
101 |
\indexml{Goal.protect}\verb|Goal.protect: thm -> thm| \\
|
|
102 |
\indexml{Goal.conclude}\verb|Goal.conclude: thm -> thm| \\
|
|
103 |
\end{mldecls}
|
|
104 |
|
|
105 |
\begin{description}
|
|
106 |
|
|
107 |
\item \verb|Goal.init|~\isa{{\isasymphi}} initializes a tactical goal with
|
|
108 |
the type-checked proposition \isa{{\isasymphi}}.
|
|
109 |
|
|
110 |
\item \verb|Goal.finish|~\isa{th} checks whether theorem \isa{th} is a solved goal configuration (zero subgoals), and concludes
|
|
111 |
the result by removing the goal protection.
|
|
112 |
|
|
113 |
\item \verb|Goal.protect|~\isa{th} protects the whole statement
|
|
114 |
of theorem \isa{th}.
|
|
115 |
|
|
116 |
\item \verb|Goal.conclude|~\isa{th} removes the goal protection
|
|
117 |
for any number of pending subgoals.
|
|
118 |
|
|
119 |
\end{description}%
|
|
120 |
\end{isamarkuptext}%
|
|
121 |
\isamarkuptrue%
|
|
122 |
%
|
|
123 |
\endisatagmlref
|
|
124 |
{\isafoldmlref}%
|
|
125 |
%
|
|
126 |
\isadelimmlref
|
|
127 |
%
|
|
128 |
\endisadelimmlref
|
|
129 |
%
|
|
130 |
\isamarkupsection{Tactics%
|
|
131 |
}
|
|
132 |
\isamarkuptrue%
|
|
133 |
%
|
|
134 |
\begin{isamarkuptext}%
|
|
135 |
FIXME
|
|
136 |
|
|
137 |
\glossary{Tactic}{Any function that maps a \seeglossary{tactical goal}
|
|
138 |
to a lazy sequence of possible sucessors. This scheme subsumes
|
|
139 |
failure (empty result sequence), as well as lazy enumeration of proof
|
|
140 |
search results. Error conditions are usually mapped to an empty
|
|
141 |
result, which gives further tactics a chance to try in turn.
|
|
142 |
Commonly, tactics either take an argument to address a particular
|
|
143 |
subgoal, or operate on a certain range of subgoals in a uniform
|
|
144 |
fashion. In any case, the main conclusion is normally left untouched,
|
|
145 |
apart from instantiating \seeglossary{schematic variables}.}%
|
|
146 |
\end{isamarkuptext}%
|
|
147 |
\isamarkuptrue%
|
|
148 |
%
|
|
149 |
\isamarkupsection{Tacticals%
|
|
150 |
}
|
|
151 |
\isamarkuptrue%
|
|
152 |
%
|
|
153 |
\begin{isamarkuptext}%
|
|
154 |
FIXME
|
|
155 |
|
|
156 |
\glossary{Tactical}{A functional combinator for building up complex
|
|
157 |
tactics from simpler ones. Typical tactical perform sequential
|
|
158 |
composition, disjunction (choice), iteration, or goal addressing.
|
|
159 |
Various search strategies may be expressed via tacticals.}%
|
|
160 |
\end{isamarkuptext}%
|
|
161 |
\isamarkuptrue%
|
|
162 |
%
|
|
163 |
\isamarkupsection{Programmed proofs%
|
|
164 |
}
|
|
165 |
\isamarkuptrue%
|
|
166 |
%
|
|
167 |
\begin{isamarkuptext}%
|
|
168 |
In order to perform a complete tactical proof under program control,
|
|
169 |
one needs to set up an initial goal configuration, apply a tactic,
|
|
170 |
and finish the result, cf.\ the rules given in
|
|
171 |
\secref{sec:tactical-goals}. Further checks are required to ensure
|
|
172 |
that the result is actually an instance of the original claim --
|
|
173 |
ill-behaved tactics could have destroyed that information.
|
|
174 |
|
|
175 |
Several simultaneous claims may be handled within a single goal
|
|
176 |
statement by using meta-level conjunction internally.\footnote{This
|
|
177 |
is merely syntax for certain derived statements within
|
|
178 |
Isabelle/Pure, there is no need to introduce a separate conjunction
|
|
179 |
operator.} The whole configuration may be considered within a
|
|
180 |
context of arbitrary-but-fixed parameters and hypotheses, which will
|
|
181 |
be available as local facts during the proof and discharged into
|
|
182 |
implications in the result.
|
|
183 |
|
|
184 |
All of these administrative tasks are packaged into a separate
|
|
185 |
operation, such that the user merely needs to provide the statement
|
|
186 |
and tactic to be applied.%
|
|
187 |
\end{isamarkuptext}%
|
|
188 |
\isamarkuptrue%
|
|
189 |
%
|
|
190 |
\isadelimmlref
|
|
191 |
%
|
|
192 |
\endisadelimmlref
|
|
193 |
%
|
|
194 |
\isatagmlref
|
|
195 |
%
|
|
196 |
\begin{isamarkuptext}%
|
|
197 |
\begin{mldecls}
|
20043
|
198 |
\indexml{Goal.prove}\verb|Goal.prove: Proof.context -> string list -> term list -> term ->|\isasep\isanewline%
|
20316
|
199 |
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm| \\
|
20043
|
200 |
\indexml{Goal.prove-multi}\verb|Goal.prove_multi: Proof.context -> string list -> term list -> term list ->|\isasep\isanewline%
|
20316
|
201 |
\verb| ({prems: thm list, context: Proof.context} -> tactic) -> thm list| \\
|
20043
|
202 |
\indexml{Goal.prove-global}\verb|Goal.prove_global: theory -> string list -> term list -> term ->|\isasep\isanewline%
|
|
203 |
\verb| (thm list -> tactic) -> thm| \\
|
18537
|
204 |
\end{mldecls}
|
|
205 |
|
|
206 |
\begin{description}
|
|
207 |
|
20043
|
208 |
\item \verb|Goal.prove|~\isa{ctxt\ xs\ As\ C\ tac} states goal \isa{C} in the context of arbitrary-but-fixed parameters \isa{xs}
|
18537
|
209 |
and hypotheses \isa{As} and applies tactic \isa{tac} to
|
|
210 |
solve it. The latter may depend on the local assumptions being
|
|
211 |
presented as facts. The result is essentially \isa{{\isasymAnd}xs{\isachardot}\ As\ {\isasymLongrightarrow}\ C}, but is normalized by pulling \isa{{\isasymAnd}} before \isa{{\isasymLongrightarrow}}
|
|
212 |
(the conclusion \isa{C} itself may be a rule statement), turning
|
|
213 |
the quantifier prefix into schematic variables, and generalizing
|
|
214 |
implicit type-variables.
|
|
215 |
|
|
216 |
\item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
|
|
217 |
states several conclusions simultaneously. \verb|Tactic.conjunction_tac| may be used to split these into individual
|
|
218 |
subgoals before commencing the actual proof.
|
|
219 |
|
20043
|
220 |
\item \verb|Goal.prove_global| is a degraded version of \verb|Goal.prove| for theory level goals; it includes a global \verb|Drule.standard| for the result.
|
|
221 |
|
18537
|
222 |
\end{description}%
|
|
223 |
\end{isamarkuptext}%
|
|
224 |
\isamarkuptrue%
|
|
225 |
%
|
|
226 |
\endisatagmlref
|
|
227 |
{\isafoldmlref}%
|
|
228 |
%
|
|
229 |
\isadelimmlref
|
|
230 |
%
|
|
231 |
\endisadelimmlref
|
|
232 |
%
|
|
233 |
\isadelimtheory
|
|
234 |
%
|
|
235 |
\endisadelimtheory
|
|
236 |
%
|
|
237 |
\isatagtheory
|
|
238 |
\isacommand{end}\isamarkupfalse%
|
|
239 |
%
|
|
240 |
\endisatagtheory
|
|
241 |
{\isafoldtheory}%
|
|
242 |
%
|
|
243 |
\isadelimtheory
|
|
244 |
%
|
|
245 |
\endisadelimtheory
|
|
246 |
\isanewline
|
|
247 |
\isanewline
|
|
248 |
\end{isabellebody}%
|
|
249 |
%%% Local Variables:
|
|
250 |
%%% mode: latex
|
|
251 |
%%% TeX-master: "root"
|
|
252 |
%%% End:
|