author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 13479  7123ae179212 
permissions  rwrr 
104  1 
%% $Id$ 
2 
\chapter{Proof Management: The Subgoal Module} 

3 
\index{proofs(} 

4 
\index{subgoal module(} 

5 
\index{reading!goalssee{proofs, starting}} 

321  6 

7 
The subgoal module stores the current proof state\index{proof state} and 

8 
many previous states; commands can produce new states or return to previous 

9 
ones. The {\em state list\/} at level $n$ is a list of pairs 

104  10 
\[ [(\psi@n,\Psi@n),\; (\psi@{n1},\Psi@{n1}),\; \ldots,\; (\psi@0,[])] \] 
11 
where $\psi@n$ is the current proof state, $\psi@{n1}$ is the previous 

12 
one, \ldots, and $\psi@0$ is the initial proof state. The $\Psi@i$ are 

13 
sequences (lazy lists) of proof states, storing branch points where a 

14 
tactic returned a list longer than one. The state lists permit various 

15 
forms of backtracking. 

16 

17 
Chopping elements from the state list reverts to previous proof states. 

18 
Besides this, the \ttindex{undo} command keeps a list of state lists. The 

19 
module actually maintains a stack of state lists, to support several 

20 
proofs at the same time. 

21 

22 
The subgoal module always contains some proof state. At the start of the 

23 
Isabelle session, this state consists of a dummy formula. 

24 

25 

26 
\section{Basic commands} 

5391  27 
Most proofs begin with \texttt{Goal} or \texttt{Goalw} and require no other 
5205  28 
commands than \texttt{by}, \texttt{chop} and \texttt{undo}. They typically end 
29 
with a call to \texttt{qed}. 

104  30 
\subsection{Starting a backward proof} 
321  31 
\index{proofs!starting} 
5391  32 
\begin{ttbox} 
33 
Goal : string > thm list 

34 
Goalw : thm list > string > thm list 

35 
goal : theory > string > thm list 

104  36 
goalw : theory > thm list > string > thm list 
8968  37 
goalw_cterm : thm list > cterm > thm list 
104  38 
premises : unit > thm list 
39 
\end{ttbox} 

5391  40 

41 
The goal commands start a new proof by setting the goal. They replace 

42 
the current state list by a new one consisting of the initial proof 

43 
state. They also empty the \ttindex{undo} list; this command cannot 

44 
be undone! 

104  45 

46 
They all return a list of metahypotheses taken from the main goal. If 

47 
this list is nonempty, bind its value to an \ML{} identifier by typing 

48 
something like 

49 
\begin{ttbox} 

332  50 
val prems = goal{\it theory\/ formula}; 
321  51 
\end{ttbox}\index{assumptions!of main goal} 
5391  52 
These assumptions typically serve as the premises when you are 
53 
deriving a rule. They are also stored internally and can be retrieved 

54 
later by the function \texttt{premises}. When the proof is finished, 

55 
\texttt{qed} compares the stored assumptions with the actual 

56 
assumptions in the proof state. 

57 

58 
The capital versions of \texttt{Goal} are the basic user level 

59 
commands and should be preferred over the more primitive lowercase 

60 
\texttt{goal} commands. Apart from taking the current theory context 

61 
as implicit argument, the former ones try to be smart in handling 

62 
metahypotheses when deriving rules. Thus \texttt{prems} have to be 

63 
seldom bound explicitly, the effect is as if \texttt{cut_facts_tac} 

64 
had been called automatically. 

104  65 

321  66 
\index{definitions!unfolding} 
104  67 
Some of the commands unfold definitions using metarewrite rules. This 
332  68 
expansion affects both the initial subgoal and the premises, which would 
5205  69 
otherwise require use of \texttt{rewrite_goals_tac} and 
70 
\texttt{rewrite_rule}. 

104  71 

321  72 
\begin{ttdescription} 
5391  73 
\item[\ttindexbold{Goal} {\it formula};] begins a new proof, where 
74 
{\it formula\/} is written as an \ML\ string. 

75 

76 
\item[\ttindexbold{Goalw} {\it defs} {\it formula};] is like 

77 
\texttt{Goal} but also applies the list of {\it defs\/} as 

78 
metarewrite rules to the first subgoal and the premises. 

79 
\index{metarewriting} 

80 

321  81 
\item[\ttindexbold{goal} {\it theory} {\it formula};] 
104  82 
begins a new proof, where {\it theory} is usually an \ML\ identifier 
83 
and the {\it formula\/} is written as an \ML\ string. 

84 

321  85 
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};] 
5205  86 
is like \texttt{goal} but also applies the list of {\it defs\/} as 
104  87 
metarewrite rules to the first subgoal and the premises. 
321  88 
\index{metarewriting} 
104  89 

8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

90 
\item[\ttindexbold{goalw_cterm} {\it defs} {\it ct};] is 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

91 
a version of \texttt{goalw} intended for programming. The main 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

92 
goal is supplied as a cterm, not as a string. See also 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

93 
\texttt{prove_goalw_cterm}, \S\ref{sec:executingbatch}. 
104  94 

95 
\item[\ttindexbold{premises}()] 

321  96 
returns the list of metahypotheses associated with the current proof (in 
97 
case you forgot to bind them to an \ML{} identifier). 

98 
\end{ttdescription} 

99 

104  100 

101 
\subsection{Applying a tactic} 

321  102 
\index{tactics!commands for applying} 
104  103 
\begin{ttbox} 
104 
by : tactic > unit 

105 
byev : tactic list > unit 

106 
\end{ttbox} 

107 
These commands extend the state list. They apply a tactic to the current 

108 
proof state. If the tactic succeeds, it returns a nonempty sequence of 

109 
next states. The head of the sequence becomes the next state, while the 

5205  110 
tail is retained for backtracking (see~\texttt{back}). 
321  111 
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};] 
104  112 
applies the {\it tactic\/} to the proof state. 
113 

321  114 
\item[\ttindexbold{byev} {\it tactics};] 
104  115 
applies the list of {\it tactics}, one at a time. It is useful for testing 
5205  116 
calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it 
104  117 
tactics})}. 
321  118 
\end{ttdescription} 
104  119 

286  120 
\noindent{\it Error indications:}\nobreak 
104  121 
\begin{itemize} 
286  122 
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic 
123 
returned an empty sequence when applied to the current proof state. 

124 
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the 

125 
new proof state is identical to the previous state. 

126 
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} 

127 
means that some rule was applied whose theory is outside the theory of 

128 
the initial proof state. This could signify a mistake such as expressing 

129 
the goal in intuitionistic logic and proving it using classical logic. 

104  130 
\end{itemize} 
131 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

132 
\subsection{Extracting and storing the proved theorem} 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

133 
\label{ExtractingAndStoringTheProvedTheorem} 
1233
2856f382f033
minor corrections to indexing; added thms_containing
paulson
parents:
1225
diff
changeset

134 
\index{theorems!extracting proved} 
104  135 
\begin{ttbox} 
7421  136 
qed : string > unit 
7446  137 
no_qed : unit > unit 
7421  138 
result : unit > thm 
139 
uresult : unit > thm 

140 
bind_thm : string * thm > unit 

141 
bind_thms : string * thm list > unit 

142 
store_thm : string * thm > thm 

143 
store_thms : string * thm list > thm list 

104  144 
\end{ttbox} 
321  145 
\begin{ttdescription} 
4317  146 
\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof. 
5205  147 
It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem 
148 
using \texttt{result()} and stores it the theorem database associated 

4317  149 
with its theory. See below for details. 
7446  150 

151 
\item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a 

152 
proper \texttt{qed} command. This is a donothing operation, it merely 

153 
helps user interfaces such as Proof~General \cite{proofgeneral} to figure 

154 
out the structure of the {\ML} text. 

1283  155 

321  156 
\item[\ttindexbold{result}()]\index{assumptions!of main goal} 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

157 
returns the final theorem, after converting the free variables to 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

158 
schematics. It discharges the assumptions supplied to the matching 
5205  159 
\texttt{goal} command. 
104  160 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

161 
It raises an exception unless the proof state passes certain checks. There 
5205  162 
must be no assumptions other than those supplied to \texttt{goal}. There 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

163 
must be no subgoals. The theorem proved must be a (firstorder) instance 
5205  164 
of the original goal, as stated in the \texttt{goal} command. This allows 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

165 
{\bf answer extraction}  instantiation of variables  but no other 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

166 
changes to the main goal. The theorem proved must have the same signature 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

167 
as the initial proof state. 
104  168 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

169 
These checks are needed because an Isabelle tactic can return any proof 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

170 
state at all. 
321  171 

5205  172 
\item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks. 
321  173 
It is needed when the initial goal contains function unknowns, when 
174 
definitions are unfolded in the main goal (by calling 

175 
\ttindex{rewrite_tac}),\index{definitions!unfolding} or when 

176 
\ttindex{assume_ax} has been used. 

4317  177 

178 
\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing} 

5205  179 
stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules}) 
4317  180 
in the theorem database associated with its theory and in the {\ML} 
181 
variable $name$. The theorem can be retrieved from the database 

5205  182 
using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}). 
4317  183 

184 
\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing} 

185 
stores $thm$ in the theorem database associated with its theory and 

186 
returns that theorem. 

7421  187 

7990  188 
\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to 
7421  189 
\texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems. 
190 

321  191 
\end{ttdescription} 
104  192 

7990  193 
The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty 
194 
string as well; in that case the result is \emph{not} stored, but proper 

195 
checks and presentation of the result still apply. 

7591  196 

104  197 

5391  198 
\subsection{Extracting axioms and stored theorems} 
199 
\index{theories!axioms of}\index{axioms!extracting} 

200 
\index{theories!theorems of}\index{theorems!extracting} 

201 
\begin{ttbox} 

202 
thm : xstring > thm 

203 
thms : xstring > thm list 

204 
get_axiom : theory > xstring > thm 

205 
get_thm : theory > xstring > thm 

206 
get_thms : theory > xstring > thm list 

207 
axioms_of : theory > (string * thm) list 

208 
thms_of : theory > (string * thm) list 

209 
assume_ax : theory > string > thm 

210 
\end{ttbox} 

211 
\begin{ttdescription} 

212 

213 
\item[\ttindexbold{thm} $name$] is the basic user function for 

214 
extracting stored theorems from the current theory context. 

215 

216 
\item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a 

217 
whole list associated with $name$ rather than a single theorem. 

218 
Typically this will be collections stored by packages, e.g.\ 

219 
\verblist.simps. 

220 

221 
\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the 

222 
given $name$ from $thy$ or any of its ancestors, raising exception 

223 
\xdx{THEORY} if none exists. Merging theories can cause several 

224 
axioms to have the same name; {\tt get_axiom} returns an arbitrary 

225 
one. Usually, axioms are also stored as theorems and may be 

226 
retrieved via \texttt{get_thm} as well. 

227 

228 
\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt 

229 
get_axiom}, but looks for a theorem stored in the theory's 

230 
database. Like {\tt get_axiom} it searches all parents of a theory 

231 
if the theorem is not found directly in $thy$. 

232 

233 
\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm} 

234 
for retrieving theorem lists stored within the theory. It returns a 

235 
singleton list if $name$ actually refers to a theorem rather than a 

236 
theorem list. 

237 

238 
\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory 

239 
node, not including the ones of its ancestors. 

240 

241 
\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within 

242 
the database of this theory node, not including the ones of its 

243 
ancestors. 

244 

245 
\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula} 

246 
using the syntax of $thy$, following the same conventions as axioms 

247 
in a theory definition. You can thus pretend that {\it formula} is 

248 
an axiom and use the resulting theorem like an axiom. Actually {\tt 

249 
assume_ax} returns an assumption; \ttindex{qed} and 

250 
\ttindex{result} complain about additional assumptions, but 

251 
\ttindex{uresult} does not. 

252 

253 
For example, if {\it formula} is 

254 
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form 

255 
\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'} 

256 
\end{ttdescription} 

257 

258 

1222  259 
\subsection{Retrieving theorems} 
260 
\index{theorems!retrieving} 

261 

4317  262 
The following functions retrieve theorems (together with their names) 
263 
from the theorem database that is associated with the current proof 

264 
state's theory. They can only find theorems that have explicitly been 

265 
stored in the database using \ttindex{qed}, \ttindex{bind_thm} or 

1222  266 
related functions. 
267 
\begin{ttbox} 

4317  268 
findI : int > (string * thm) list 
269 
findE : int > int > (string * thm) list 

270 
findEs : int > (string * thm) list 

271 
thms_containing : xstring list > (string * thm) list 

1222  272 
\end{ttbox} 
273 
\begin{ttdescription} 

274 
\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal} 

1225  275 
returns all ``introduction rules'' applicable to subgoal $i$  all 
1222  276 
theorems whose conclusion matches (rather than unifies with) subgoal 
5205  277 
$i$. Useful in connection with \texttt{resolve_tac}. 
1222  278 

279 
\item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules'' 

1225  280 
applicable to premise $n$ of subgoal $i$  all those theorems whose 
281 
first premise matches premise $n$ of subgoal $i$. Useful in connection with 

5205  282 
\texttt{eresolve_tac} and \texttt{dresolve_tac}. 
1222  283 

284 
\item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable 

1225  285 
to subgoal $i$  all those theorems whose first premise matches some 
5205  286 
premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and 
287 
\texttt{dresolve_tac}. 

4317  288 

7805
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7591
diff
changeset

289 
\item[\ttindexbold{thms_containing} $consts$] returns all theorems that 
0ae9ddc36fe0
theorem database now also indexes constants "Trueprop", "all",
wenzelm
parents:
7591
diff
changeset

290 
contain \emph{all} of the given constants. 
1222  291 
\end{ttdescription} 
292 

293 

104  294 
\subsection{Undoing and backtracking} 
295 
\begin{ttbox} 

296 
chop : unit > unit 

297 
choplev : int > unit 

298 
back : unit > unit 

299 
undo : unit > unit 

300 
\end{ttbox} 

321  301 
\begin{ttdescription} 
104  302 
\item[\ttindexbold{chop}();] 
303 
deletes the top level of the state list, cancelling the last \ttindex{by} 

5205  304 
command. It provides a limited undo facility, and the \texttt{undo} command 
104  305 
can cancel it. 
306 

307 
\item[\ttindexbold{choplev} {\it n};] 

2128
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

308 
truncates the state list to level~{\it n}, if $n\geq0$. A negative value 
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

309 
of~$n$ refers to the $n$th previous level: 
5205  310 
\hbox{\verbchoplev ~1} has the same effect as \texttt{chop}. 
104  311 

312 
\item[\ttindexbold{back}();] 

313 
searches the state list for a nonempty branch point, starting from the top 

314 
level. The first one found becomes the current proof state  the most 

286  315 
recent alternative branch is taken. This is a form of interactive 
316 
backtracking. 

104  317 

318 
\item[\ttindexbold{undo}();] 

319 
cancels the most recent change to the proof state by the commands \ttindex{by}, 

5205  320 
\texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot} 
321 
cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to 

104  322 
cancel a series of commands. 
321  323 
\end{ttdescription} 
286  324 

325 
\goodbreak 

6569  326 
\noindent{\it Error indications for {\tt back}:}\par\nobreak 
104  327 
\begin{itemize} 
286  328 
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"} 
5205  329 
means \texttt{back} found a nonempty branch point, but that it contained 
286  330 
the same proof state as the current one. 
331 
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} 

332 
means the signature of the alternative proof state differs from that of 

333 
the current state. 

5205  334 
\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could 
286  335 
find no alternative proof state. 
104  336 
\end{itemize} 
337 

507  338 
\subsection{Printing the proof state}\label{sec:goalsprinting} 
321  339 
\index{proof state!printing of} 
104  340 
\begin{ttbox} 
341 
pr : unit > unit 

342 
prlev : int > unit 

2528  343 
prlim : int > unit 
104  344 
goals_limit: int ref \hfill{\bf initially 10} 
345 
\end{ttbox} 

2528  346 
See also the printing control options described 
347 
in~\S\ref{sec:printingcontrol}. 

321  348 
\begin{ttdescription} 
104  349 
\item[\ttindexbold{pr}();] 
350 
prints the current proof state. 

351 

352 
\item[\ttindexbold{prlev} {\it n};] 

2128
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

353 
prints the proof state at level {\it n}, if $n\geq0$. A negative value 
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

354 
of~$n$ refers to the $n$th previous level. This command allows 
4e8644805af2
Documents the use of negative arguments to choplev and prlev
paulson
parents:
1283
diff
changeset

355 
you to review earlier stages of the proof. 
104  356 

2528  357 
\item[\ttindexbold{prlim} {\it k};] 
358 
prints the current proof state, limiting the number of subgoals to~$k$. It 

5205  359 
updates \texttt{goals_limit} (see below) and is helpful when there are many 
2528  360 
subgoals. 
361 

321  362 
\item[\ttindexbold{goals_limit} := {\it k};] 
104  363 
specifies~$k$ as the maximum number of subgoals to print. 
321  364 
\end{ttdescription} 
104  365 

366 

367 
\subsection{Timing} 

321  368 
\index{timing statistics}\index{proofs!timing} 
104  369 
\begin{ttbox} 
8995  370 
timing: bool ref \hfill{\bf initially false} 
104  371 
\end{ttbox} 
372 

321  373 
\begin{ttdescription} 
8995  374 
\item[set \ttindexbold{timing};] enables global timing in Isabelle. In 
375 
particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands 

376 
display how much processor time was spent. This information is 

377 
compilerdependent. 

321  378 
\end{ttdescription} 
104  379 

380 

381 
\section{Shortcuts for applying tactics} 

5205  382 
\index{shortcuts!for \texttt{by} commands} 
104  383 
These commands call \ttindex{by} with common tactics. Their chief purpose 
384 
is to minimise typing, although the scanning shortcuts are useful in their 

385 
own right. Chapter~\ref{tactics} explains the tactics themselves. 

386 

387 
\subsection{Refining a given subgoal} 

388 
\begin{ttbox} 

321  389 
ba : int > unit 
390 
br : thm > int > unit 

391 
be : thm > int > unit 

392 
bd : thm > int > unit 

393 
brs : thm list > int > unit 

394 
bes : thm list > int > unit 

395 
bds : thm list > int > unit 

104  396 
\end{ttbox} 
397 

321  398 
\begin{ttdescription} 
104  399 
\item[\ttindexbold{ba} {\it i};] 
5205  400 
performs \texttt{by (assume_tac {\it i});} 
104  401 

402 
\item[\ttindexbold{br} {\it thm} {\it i};] 

5205  403 
performs \texttt{by (resolve_tac [{\it thm}] {\it i});} 
104  404 

405 
\item[\ttindexbold{be} {\it thm} {\it i};] 

5205  406 
performs \texttt{by (eresolve_tac [{\it thm}] {\it i});} 
104  407 

408 
\item[\ttindexbold{bd} {\it thm} {\it i};] 

5205  409 
performs \texttt{by (dresolve_tac [{\it thm}] {\it i});} 
104  410 

411 
\item[\ttindexbold{brs} {\it thms} {\it i};] 

5205  412 
performs \texttt{by (resolve_tac {\it thms} {\it i});} 
104  413 

414 
\item[\ttindexbold{bes} {\it thms} {\it i};] 

5205  415 
performs \texttt{by (eresolve_tac {\it thms} {\it i});} 
104  416 

417 
\item[\ttindexbold{bds} {\it thms} {\it i};] 

5205  418 
performs \texttt{by (dresolve_tac {\it thms} {\it i});} 
321  419 
\end{ttdescription} 
104  420 

421 

422 
\subsection{Scanning shortcuts} 

423 
These shortcuts scan for a suitable subgoal (starting from subgoal~1). 

424 
They refine the first subgoal for which the tactic succeeds. Thus, they 

5205  425 
require less typing than \texttt{br}, etc. They display the selected 
104  426 
subgoal's number; please watch this, for it may not be what you expect! 
427 

428 
\begin{ttbox} 

321  429 
fa : unit > unit 
430 
fr : thm > unit 

431 
fe : thm > unit 

432 
fd : thm > unit 

433 
frs : thm list > unit 

434 
fes : thm list > unit 

435 
fds : thm list > unit 

104  436 
\end{ttbox} 
437 

321  438 
\begin{ttdescription} 
104  439 
\item[\ttindexbold{fa}();] 
321  440 
solves some subgoal by assumption. 
104  441 

442 
\item[\ttindexbold{fr} {\it thm};] 

5205  443 
refines some subgoal using \texttt{resolve_tac [{\it thm}]} 
104  444 

445 
\item[\ttindexbold{fe} {\it thm};] 

5205  446 
refines some subgoal using \texttt{eresolve_tac [{\it thm}]} 
104  447 

448 
\item[\ttindexbold{fd} {\it thm};] 

5205  449 
refines some subgoal using \texttt{dresolve_tac [{\it thm}]} 
104  450 

451 
\item[\ttindexbold{frs} {\it thms};] 

5205  452 
refines some subgoal using \texttt{resolve_tac {\it thms}} 
104  453 

454 
\item[\ttindexbold{fes} {\it thms};] 

5205  455 
refines some subgoal using \texttt{eresolve_tac {\it thms}} 
104  456 

457 
\item[\ttindexbold{fds} {\it thms};] 

5205  458 
refines some subgoal using \texttt{dresolve_tac {\it thms}} 
321  459 
\end{ttdescription} 
104  460 

461 
\subsection{Other shortcuts} 

462 
\begin{ttbox} 

463 
bw : thm > unit 

464 
bws : thm list > unit 

465 
ren : string > int > unit 

466 
\end{ttbox} 

321  467 
\begin{ttdescription} 
5205  468 
\item[\ttindexbold{bw} {\it def};] performs \texttt{by 
4317  469 
(rewrite_goals_tac [{\it def}]);} It unfolds definitions in the 
470 
subgoals (but not the main goal), by metarewriting with the given 

471 
definition (see also \S\ref{sec:rewrite_goals}). 

472 
\index{metarewriting} 

104  473 

474 
\item[\ttindexbold{bws}] 

5205  475 
is like \texttt{bw} but takes a list of definitions. 
104  476 

477 
\item[\ttindexbold{ren} {\it names} {\it i};] 

5205  478 
performs \texttt{by (rename_tac {\it names} {\it i});} it renames 
332  479 
parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\ 
480 
same as previous level}.) 

321  481 
\index{parameters!renaming} 
482 
\end{ttdescription} 

104  483 

484 

8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

485 
\section{Executing batch proofs}\label{sec:executingbatch} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

486 
\index{batch execution}% 
8136  487 
To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list > 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

488 
tactic list}, which is the type of a tactical proof. 
286  489 
\begin{ttbox} 
8136  490 
prove_goal : theory > string > tacfn > thm 
491 
qed_goal : string > theory > string > tacfn > unit 

492 
prove_goalw: theory > thm list > string > tacfn > thm 

493 
qed_goalw : string > theory > thm list > string > tacfn > unit 

494 
prove_goalw_cterm: thm list > cterm > tacfn > thm 

104  495 
\end{ttbox} 
321  496 
These batch functions create an initial proof state, then apply a tactic to 
497 
it, yielding a sequence of final proof states. The head of the sequence is 

104  498 
returned, provided it is an instance of the theorem originally proposed. 
8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

499 
The forms \texttt{prove_goal}, \texttt{prove_goalw} and 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

500 
\texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

501 
\texttt{goalw_cterm}. 
104  502 

503 
The tactic is specified by a function from theorem lists to tactic lists. 

332  504 
The function is applied to the list of metaassumptions taken from 
505 
the main goal. The resulting tactics are applied in sequence (using {\tt 

506 
EVERY}). For example, a proof consisting of the commands 

104  507 
\begin{ttbox} 
508 
val prems = goal {\it theory} {\it formula}; 

509 
by \(tac@1\); \ldots by \(tac@n\); 

3108  510 
qed "my_thm"; 
104  511 
\end{ttbox} 
512 
can be transformed to an expression as follows: 

513 
\begin{ttbox} 

3108  514 
qed_goal "my_thm" {\it theory} {\it formula} 
104  515 
(fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]); 
516 
\end{ttbox} 

517 
The methods perform identical processing of the initial {\it formula} and 

5205  518 
the final proof state. But \texttt{prove_goal} executes the tactic as a 
332  519 
atomic operation, bypassing the subgoal module; the current interactive 
520 
proof is unaffected. 

521 
% 

321  522 
\begin{ttdescription} 
523 
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};] 

104  524 
executes a proof of the {\it formula\/} in the given {\it theory}, using 
525 
the given tactic function. 

526 

4317  527 
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts 
8136  528 
like \texttt{prove_goal} but it also stores the resulting theorem in the 
4317  529 
theorem database associated with its theory and in the {\ML} 
530 
variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}). 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

531 

104  532 
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
321  533 
{\it tacsf};]\index{metarewriting} 
5205  534 
is like \texttt{prove_goal} but also applies the list of {\it defs\/} as 
104  535 
metarewrite rules to the first subgoal and the premises. 
536 

866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

537 
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] 
5205  538 
is analogous to \texttt{qed_goal}. 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

539 

8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

540 
\item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct} 
321  541 
{\it tacsf};] 
8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

542 
is a version of \texttt{prove_goalw} intended for programming. The main 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

543 
goal is supplied as a cterm, not as a string. A cterm carries a theory with 
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

544 
it, and can be created from a term~$t$ by 
286  545 
\begin{ttbox} 
8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

546 
cterm_of (sign_of thy) \(t\) 
286  547 
\end{ttbox} 
8978
894d76cbf56d
fixed the documentation of goalw_cterm and prove_goalw_cterm
paulson
parents:
8968
diff
changeset

548 
\index{*cterm_of}\index{*sign_of} 
321  549 
\end{ttdescription} 
104  550 

551 

13479  552 
\section{Internal proofs} 
553 

554 
\begin{ttbox} 

555 
Tactic.prove: Sign.sg > string list > term list > term > 

556 
(thm list > tactic) > thm 

557 
Tactic.prove_standard: Sign.sg > string list > term list > term > 

558 
(thm list > tactic) > thm 

559 
\end{ttbox} 

560 

561 
These functions provide a clean internal interface for programmed proofs. The 

562 
special overhead of toplevel statements (cf.\ \verb,prove_goalw_cterm,) is 

563 
omitted. Statements may be established within a local contexts of fixed 

564 
variables and assumptions, which are the only hypotheses to be discharged in 

565 
the result. 

566 

567 
\begin{ttdescription} 

568 
\item[\ttindexbold{Tactic.prove}~$sg~xs~As~C~tacf$] establishes the result 

569 
$\Forall xs. As \Imp C$ via the given tactic (which is a function taking the 

570 
assumptions as local premises). 

571 

572 
\item[\ttindexbold{Tactic.prove_standard}] is simular to \verb,Tactic.prove,, 

573 
but performs the \verb,standard, operation on the result, essentially 

574 
turning it into a toplevel statement. Never do this for local proofs 

575 
within other proof tools! 

576 

577 
\end{ttdescription} 

578 

579 

321  580 
\section{Managing multiple proofs} 
581 
\index{proofs!managing multiple} 

104  582 
You may save the current state of the subgoal module and resume work on it 
583 
later. This serves two purposes. 

584 
\begin{enumerate} 

585 
\item At some point, you may be uncertain of the next step, and 

586 
wish to experiment. 

587 

588 
\item During a proof, you may see that a lemma should be proved first. 

589 
\end{enumerate} 

590 
Each saved proof state consists of a list of levels; \ttindex{chop} behaves 

591 
independently for each of the saved proofs. In addition, each saved state 

592 
carries a separate \ttindex{undo} list. 

593 

321  594 
\subsection{The stack of proof states} 
595 
\index{proofs!stacking} 

104  596 
\begin{ttbox} 
597 
push_proof : unit > unit 

598 
pop_proof : unit > thm list 

599 
rotate_proof : unit > thm list 

600 
\end{ttbox} 

601 
The subgoal module maintains a stack of proof states. Most subgoal 

5205  602 
commands affect only the top of the stack. The \ttindex{Goal} command {\em 
321  603 
replaces\/} the top of the stack; the only command that pushes a proof on the 
5205  604 
stack is \texttt{push_proof}. 
104  605 

5205  606 
To save some point of the proof, call \texttt{push_proof}. You may now 
607 
state a lemma using \texttt{goal}, or simply continue to apply tactics. 

608 
Later, you can return to the saved point by calling \texttt{pop_proof} or 

609 
\texttt{rotate_proof}. 

104  610 

5205  611 
To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates 
104  612 
the stack, it prints the new top element. 
613 

321  614 
\begin{ttdescription} 
104  615 
\item[\ttindexbold{push_proof}();] 
616 
duplicates the top element of the stack, pushing a copy of the current 

617 
proof state on to the stack. 

618 

619 
\item[\ttindexbold{pop_proof}();] 

620 
discards the top element of the stack. It returns the list of 

332  621 
assumptions associated with the new proof; you should bind these to an 
104  622 
\ML\ identifier. They can also be obtained by calling \ttindex{premises}. 
623 

321  624 
\item[\ttindexbold{rotate_proof}();] 
625 
\index{assumptions!of main goal} 

104  626 
rotates the stack, moving the top element to the bottom. It returns the 
627 
list of assumptions associated with the new proof. 

321  628 
\end{ttdescription} 
104  629 

630 

321  631 
\subsection{Saving and restoring proof states} 
632 
\index{proofs!saving and restoring} 

104  633 
\begin{ttbox} 
634 
save_proof : unit > proof 

635 
restore_proof : proof > thm list 

636 
\end{ttbox} 

637 
States of the subgoal module may be saved as \ML\ values of 

321  638 
type~\mltydx{proof}, and later restored. 
104  639 

321  640 
\begin{ttdescription} 
104  641 
\item[\ttindexbold{save_proof}();] 
642 
returns the current state, which is on top of the stack. 

643 

321  644 
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal} 
645 
replaces the top of the stack by~{\it prf}. It returns the list of 

646 
assumptions associated with the new proof. 

647 
\end{ttdescription} 

104  648 

649 

4317  650 
\section{*Debugging and inspecting} 
321  651 
\index{tactics!debugging} 
2611  652 
These functions can be useful when you are debugging a tactic. They refer 
653 
to the current proof state stored in the subgoal module. A tactic 

654 
should never call them; it should operate on the proof state supplied as its 

655 
argument. 

104  656 

321  657 
\subsection{Reading and printing terms} 
658 
\index{terms!reading of}\index{terms!printing of}\index{types!printing of} 

104  659 
\begin{ttbox} 
660 
read : string > term 

661 
prin : term > unit 

662 
printyp : typ > unit 

663 
\end{ttbox} 

664 
These read and print terms (or types) using the syntax associated with the 

665 
proof state. 

666 

321  667 
\begin{ttdescription} 
104  668 
\item[\ttindexbold{read} {\it string}] 
6170  669 
reads the {\it string} as a term, without typechecking. 
104  670 

671 
\item[\ttindexbold{prin} {\it t};] 

672 
prints the term~$t$ at the terminal. 

673 

674 
\item[\ttindexbold{printyp} {\it T};] 

675 
prints the type~$T$ at the terminal. 

321  676 
\end{ttdescription} 
104  677 

321  678 
\subsection{Inspecting the proof state} 
679 
\index{proofs!inspecting the state} 

104  680 
\begin{ttbox} 
681 
topthm : unit > thm 

682 
getgoal : int > term 

683 
gethyps : int > thm list 

684 
\end{ttbox} 

685 

321  686 
\begin{ttdescription} 
104  687 
\item[\ttindexbold{topthm}()] 
688 
returns the proof state as an Isabelle theorem. This is what \ttindex{by} 

689 
would supply to a tactic at this point. It omits the postprocessing of 

690 
\ttindex{result} and \ttindex{uresult}. 

691 

692 
\item[\ttindexbold{getgoal} {\it i}] 

693 
returns subgoal~$i$ of the proof state, as a term. You may print 

5205  694 
this using \texttt{prin}, though you may have to examine the internal 
104  695 
data structure in order to locate the problem! 
696 

321  697 
\item[\ttindexbold{gethyps} {\it i}] 
698 
returns the hypotheses of subgoal~$i$ as metalevel assumptions. In 

699 
these theorems, the subgoal's parameters become free variables. This 

700 
command is supplied for debugging uses of \ttindex{METAHYPS}. 

701 
\end{ttdescription} 

104  702 

2611  703 

321  704 
\subsection{Filtering lists of rules} 
104  705 
\begin{ttbox} 
706 
filter_goal: (term*term>bool) > thm list > int > thm list 

707 
\end{ttbox} 

708 

321  709 
\begin{ttdescription} 
104  710 
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] 
5205  711 
applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof 
104  712 
state and returns the list of theorems that survive the filtering. 
321  713 
\end{ttdescription} 
104  714 

715 
\index{subgoal module)} 

716 
\index{proofs)} 

5371  717 

718 

719 
%%% Local Variables: 

720 
%%% mode: latex 

721 
%%% TeXmaster: "ref" 

722 
%%% End: 