author  paulson 
Fri, 27 Nov 1998 13:13:22 +0100  
changeset 5980  2e9314c07146 
parent 5391  8b22b93dba2c 
child 6170  9a59cf8ae9b5 
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 
3108  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 

3108  90 
\item[\ttindexbold{goalw_cterm} {\it theory} {\it defs} {\it ct};] is 
5205  91 
a version of \texttt{goalw} for programming applications. The main 
3108  92 
goal is supplied as a cterm, not as a string. Typically, the cterm 
5205  93 
is created from a term~$t$ by \texttt{cterm_of (sign_of thy) $t$}. 
3108  94 
\index{*cterm_of}\index{*sign_of} 
104  95 

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

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

99 
\end{ttdescription} 

100 

104  101 

102 
\subsection{Applying a tactic} 

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

106 
byev : tactic list > unit 

107 
\end{ttbox} 

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

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

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

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

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

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

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

126 
new proof state is identical to the previous state. 

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

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

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

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

104  131 
\end{itemize} 
132 

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

133 
\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

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

135 
\index{theorems!extracting proved} 
104  136 
\begin{ttbox} 
1283  137 
qed : string > unit 
866
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

138 
result : unit > thm 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

139 
uresult : unit > thm 
2d3d020eef11
added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents:
507
diff
changeset

140 
bind_thm : string * thm > unit 
1283  141 
store_thm : string * thm > thm 
104  142 
\end{ttbox} 
321  143 
\begin{ttdescription} 
4317  144 
\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof. 
5205  145 
It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem 
146 
using \texttt{result()} and stores it the theorem database associated 

4317  147 
with its theory. See below for details. 
1283  148 

321  149 
\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

150 
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

151 
schematics. It discharges the assumptions supplied to the matching 
5205  152 
\texttt{goal} command. 
104  153 

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

154 
It raises an exception unless the proof state passes certain checks. There 
5205  155 
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

156 
must be no subgoals. The theorem proved must be a (firstorder) instance 
5205  157 
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

158 
{\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

159 
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

160 
as the initial proof state. 
104  161 

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

162 
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

163 
state at all. 
321  164 

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

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

169 
\ttindex{assume_ax} has been used. 

4317  170 

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

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

5205  175 
using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}). 
4317  176 

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

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

179 
returns that theorem. 

321  180 
\end{ttdescription} 
104  181 

182 

5391  183 
\subsection{Extracting axioms and stored theorems} 
184 
\index{theories!axioms of}\index{axioms!extracting} 

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

186 
\begin{ttbox} 

187 
thm : xstring > thm 

188 
thms : xstring > thm list 

189 
get_axiom : theory > xstring > thm 

190 
get_thm : theory > xstring > thm 

191 
get_thms : theory > xstring > thm list 

192 
axioms_of : theory > (string * thm) list 

193 
thms_of : theory > (string * thm) list 

194 
assume_ax : theory > string > thm 

195 
\end{ttbox} 

196 
\begin{ttdescription} 

197 

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

199 
extracting stored theorems from the current theory context. 

200 

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

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

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

204 
\verblist.simps. 

205 

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

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

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

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

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

211 
retrieved via \texttt{get_thm} as well. 

212 

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

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

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

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

217 

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

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

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

221 
theorem list. 

222 

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

224 
node, not including the ones of its ancestors. 

225 

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

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

228 
ancestors. 

229 

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

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

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

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

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

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

236 
\ttindex{uresult} does not. 

237 

238 
For example, if {\it formula} is 

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

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

241 
\end{ttdescription} 

242 

243 

1222  244 
\subsection{Retrieving theorems} 
245 
\index{theorems!retrieving} 

246 

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

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

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

1222  251 
related functions. 
252 
\begin{ttbox} 

4317  253 
findI : int > (string * thm) list 
254 
findE : int > int > (string * thm) list 

255 
findEs : int > (string * thm) list 

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

1222  257 
\end{ttbox} 
258 
\begin{ttdescription} 

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

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

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

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

5205  267 
\texttt{eresolve_tac} and \texttt{dresolve_tac}. 
1222  268 

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

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

4317  273 

274 
\item[\ttindexbold{thms_containing} $consts$] returns all theorems 

275 
that contain all of a given set of constants. Note that a few basic 

276 
constants like \verb$==>$ are ignored. 

1222  277 
\end{ttdescription} 
278 

279 

104  280 
\subsection{Undoing and backtracking} 
281 
\begin{ttbox} 

282 
chop : unit > unit 

283 
choplev : int > unit 

284 
back : unit > unit 

285 
undo : unit > unit 

286 
\end{ttbox} 

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

5205  290 
command. It provides a limited undo facility, and the \texttt{undo} command 
104  291 
can cancel it. 
292 

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

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

294 
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

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

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

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

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

286  301 
recent alternative branch is taken. This is a form of interactive 
302 
backtracking. 

104  303 

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

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

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

104  308 
cancel a series of commands. 
321  309 
\end{ttdescription} 
286  310 

311 
\goodbreak 

5205  312 
\noindent{\it Error indications for \texttt{back}:}\par\nobreak 
104  313 
\begin{itemize} 
286  314 
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"} 
5205  315 
means \texttt{back} found a nonempty branch point, but that it contained 
286  316 
the same proof state as the current one. 
317 
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"} 

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

319 
the current state. 

5205  320 
\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could 
286  321 
find no alternative proof state. 
104  322 
\end{itemize} 
323 

507  324 
\subsection{Printing the proof state}\label{sec:goalsprinting} 
321  325 
\index{proof state!printing of} 
104  326 
\begin{ttbox} 
327 
pr : unit > unit 

328 
prlev : int > unit 

2528  329 
prlim : int > unit 
104  330 
goals_limit: int ref \hfill{\bf initially 10} 
331 
\end{ttbox} 

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

321  334 
\begin{ttdescription} 
104  335 
\item[\ttindexbold{pr}();] 
336 
prints the current proof state. 

337 

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

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

339 
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

340 
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

341 
you to review earlier stages of the proof. 
104  342 

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

5205  345 
updates \texttt{goals_limit} (see below) and is helpful when there are many 
2528  346 
subgoals. 
347 

321  348 
\item[\ttindexbold{goals_limit} := {\it k};] 
104  349 
specifies~$k$ as the maximum number of subgoals to print. 
321  350 
\end{ttdescription} 
104  351 

352 

353 
\subsection{Timing} 

321  354 
\index{timing statistics}\index{proofs!timing} 
104  355 
\begin{ttbox} 
356 
proof_timing: bool ref \hfill{\bf initially false} 

357 
\end{ttbox} 

358 

321  359 
\begin{ttdescription} 
4317  360 
\item[set \ttindexbold{proof_timing};] 
104  361 
makes the \ttindex{by} and \ttindex{prove_goal} commands display how much 
362 
processor time was spent. This information is compilerdependent. 

321  363 
\end{ttdescription} 
104  364 

365 

366 
\section{Shortcuts for applying tactics} 

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

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

371 

372 
\subsection{Refining a given subgoal} 

373 
\begin{ttbox} 

321  374 
ba : int > unit 
375 
br : thm > int > unit 

376 
be : thm > int > unit 

377 
bd : thm > int > unit 

378 
brs : thm list > int > unit 

379 
bes : thm list > int > unit 

380 
bds : thm list > int > unit 

104  381 
\end{ttbox} 
382 

321  383 
\begin{ttdescription} 
104  384 
\item[\ttindexbold{ba} {\it i};] 
5205  385 
performs \texttt{by (assume_tac {\it i});} 
104  386 

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

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

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

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

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

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

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

5205  397 
performs \texttt{by (resolve_tac {\it thms} {\it i});} 
104  398 

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

5205  400 
performs \texttt{by (eresolve_tac {\it thms} {\it i});} 
104  401 

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

5205  403 
performs \texttt{by (dresolve_tac {\it thms} {\it i});} 
321  404 
\end{ttdescription} 
104  405 

406 

407 
\subsection{Scanning shortcuts} 

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

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

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

413 
\begin{ttbox} 

321  414 
fa : unit > unit 
415 
fr : thm > unit 

416 
fe : thm > unit 

417 
fd : thm > unit 

418 
frs : thm list > unit 

419 
fes : thm list > unit 

420 
fds : thm list > unit 

104  421 
\end{ttbox} 
422 

321  423 
\begin{ttdescription} 
104  424 
\item[\ttindexbold{fa}();] 
321  425 
solves some subgoal by assumption. 
104  426 

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

5205  428 
refines some subgoal using \texttt{resolve_tac [{\it thm}]} 
104  429 

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

5205  431 
refines some subgoal using \texttt{eresolve_tac [{\it thm}]} 
104  432 

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

5205  434 
refines some subgoal using \texttt{dresolve_tac [{\it thm}]} 
104  435 

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

5205  437 
refines some subgoal using \texttt{resolve_tac {\it thms}} 
104  438 

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

5205  440 
refines some subgoal using \texttt{eresolve_tac {\it thms}} 
104  441 

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

5205  443 
refines some subgoal using \texttt{dresolve_tac {\it thms}} 
321  444 
\end{ttdescription} 
104  445 

446 
\subsection{Other shortcuts} 

447 
\begin{ttbox} 

448 
bw : thm > unit 

449 
bws : thm list > unit 

450 
ren : string > int > unit 

451 
\end{ttbox} 

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

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

457 
\index{metarewriting} 

104  458 

459 
\item[\ttindexbold{bws}] 

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

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

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

321  466 
\index{parameters!renaming} 
467 
\end{ttdescription} 

104  468 

469 

321  470 
\section{Executing batch proofs} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

471 
\index{batch execution}% 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

472 
To save space below, let type \texttt{tacfun} abbreviate \texttt{thm list > 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

473 
tactic list}, which is the type of a tactical proof. 
286  474 
\begin{ttbox} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

475 
prove_goal : theory > string > tacfun > thm 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

476 
qed_goal : string > theory > string > tacfun > unit 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

477 
prove_goalw: theory > thm list > string > tacfun > thm 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

478 
qed_goalw : string > theory > thm list > string > tacfun > unit 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

479 
prove_goalw_cterm: thm list > cterm > tacfun > thm 
104  480 
\end{ttbox} 
321  481 
These batch functions create an initial proof state, then apply a tactic to 
482 
it, yielding a sequence of final proof states. The head of the sequence is 

104  483 
returned, provided it is an instance of the theorem originally proposed. 
5205  484 
The forms \texttt{prove_goal}, \texttt{prove_goalw} and \texttt{prove_goalw_cterm} 
485 
are analogous to \texttt{goal}, \texttt{goalw} and \texttt{goalw_cterm}. 

104  486 

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

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

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

104  491 
\begin{ttbox} 
492 
val prems = goal {\it theory} {\it formula}; 

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

3108  494 
qed "my_thm"; 
104  495 
\end{ttbox} 
496 
can be transformed to an expression as follows: 

497 
\begin{ttbox} 

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

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

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

505 
% 

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

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

510 

4317  511 
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts 
5205  512 
like \texttt{prove_goal} but also stores the resulting theorem in the 
4317  513 
theorem database associated with its theory and in the {\ML} 
514 
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

515 

104  516 
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula} 
321  517 
{\it tacsf};]\index{metarewriting} 
5205  518 
is like \texttt{prove_goal} but also applies the list of {\it defs\/} as 
104  519 
metarewrite rules to the first subgoal and the premises. 
520 

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

521 
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;] 
5205  522 
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

523 

104  524 
\item[\ttindexbold{prove_goalw_cterm} {\it theory} {\it defs} {\it ct} 
321  525 
{\it tacsf};] 
5205  526 
is a version of \texttt{prove_goalw} for programming applications. The main 
104  527 
goal is supplied as a cterm, not as a string. Typically, the cterm is 
286  528 
created from a term~$t$ as follows: 
529 
\begin{ttbox} 

3108  530 
cterm_of (sign_of thy) \(t\) 
286  531 
\end{ttbox} 
3108  532 
\index{*cterm_of}\index{*sign_of} 
321  533 
\end{ttdescription} 
104  534 

535 

321  536 
\section{Managing multiple proofs} 
537 
\index{proofs!managing multiple} 

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

540 
\begin{enumerate} 

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

542 
wish to experiment. 

543 

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

545 
\end{enumerate} 

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

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

548 
carries a separate \ttindex{undo} list. 

549 

321  550 
\subsection{The stack of proof states} 
551 
\index{proofs!stacking} 

104  552 
\begin{ttbox} 
553 
push_proof : unit > unit 

554 
pop_proof : unit > thm list 

555 
rotate_proof : unit > thm list 

556 
\end{ttbox} 

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

5205  558 
commands affect only the top of the stack. The \ttindex{Goal} command {\em 
321  559 
replaces\/} the top of the stack; the only command that pushes a proof on the 
5205  560 
stack is \texttt{push_proof}. 
104  561 

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

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

565 
\texttt{rotate_proof}. 

104  566 

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

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

573 
proof state on to the stack. 

574 

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

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

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

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

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

321  584 
\end{ttdescription} 
104  585 

586 

321  587 
\subsection{Saving and restoring proof states} 
588 
\index{proofs!saving and restoring} 

104  589 
\begin{ttbox} 
590 
save_proof : unit > proof 

591 
restore_proof : proof > thm list 

592 
\end{ttbox} 

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

321  594 
type~\mltydx{proof}, and later restored. 
104  595 

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

599 

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

602 
assumptions associated with the new proof. 

603 
\end{ttdescription} 

104  604 

605 

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

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

611 
argument. 

104  612 

321  613 
\subsection{Reading and printing terms} 
614 
\index{terms!reading of}\index{terms!printing of}\index{types!printing of} 

104  615 
\begin{ttbox} 
616 
read : string > term 

617 
prin : term > unit 

618 
printyp : typ > unit 

619 
\end{ttbox} 

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

621 
proof state. 

622 

321  623 
\begin{ttdescription} 
104  624 
\item[\ttindexbold{read} {\it string}] 
625 
reads the {\it string} as a term, without type checking. 

626 

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

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

629 

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

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

321  632 
\end{ttdescription} 
104  633 

321  634 
\subsection{Inspecting the proof state} 
635 
\index{proofs!inspecting the state} 

104  636 
\begin{ttbox} 
637 
topthm : unit > thm 

638 
getgoal : int > term 

639 
gethyps : int > thm list 

640 
\end{ttbox} 

641 

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

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

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

647 

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

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

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

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

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

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

657 
\end{ttdescription} 

104  658 

2611  659 

321  660 
\subsection{Filtering lists of rules} 
104  661 
\begin{ttbox} 
662 
filter_goal: (term*term>bool) > thm list > int > thm list 

663 
\end{ttbox} 

664 

321  665 
\begin{ttdescription} 
104  666 
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}] 
5205  667 
applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof 
104  668 
state and returns the list of theorems that survive the filtering. 
321  669 
\end{ttdescription} 
104  670 

671 
\index{subgoal module)} 

672 
\index{proofs)} 

5371  673 

674 

675 
%%% Local Variables: 

676 
%%% mode: latex 

677 
%%% TeXmaster: "ref" 

678 
%%% End: 