lcp@104
|
1 |
%% $Id$
|
lcp@104
|
2 |
\chapter{Proof Management: The Subgoal Module}
|
lcp@104
|
3 |
\index{proofs|(}
|
lcp@104
|
4 |
\index{subgoal module|(}
|
lcp@104
|
5 |
\index{reading!goals|see{proofs, starting}}
|
lcp@321
|
6 |
|
lcp@321
|
7 |
The subgoal module stores the current proof state\index{proof state} and
|
lcp@321
|
8 |
many previous states; commands can produce new states or return to previous
|
lcp@321
|
9 |
ones. The {\em state list\/} at level $n$ is a list of pairs
|
lcp@104
|
10 |
\[ [(\psi@n,\Psi@n),\; (\psi@{n-1},\Psi@{n-1}),\; \ldots,\; (\psi@0,[])] \]
|
lcp@104
|
11 |
where $\psi@n$ is the current proof state, $\psi@{n-1}$ is the previous
|
lcp@104
|
12 |
one, \ldots, and $\psi@0$ is the initial proof state. The $\Psi@i$ are
|
lcp@104
|
13 |
sequences (lazy lists) of proof states, storing branch points where a
|
lcp@104
|
14 |
tactic returned a list longer than one. The state lists permit various
|
lcp@104
|
15 |
forms of backtracking.
|
lcp@104
|
16 |
|
lcp@104
|
17 |
Chopping elements from the state list reverts to previous proof states.
|
lcp@104
|
18 |
Besides this, the \ttindex{undo} command keeps a list of state lists. The
|
lcp@104
|
19 |
module actually maintains a stack of state lists, to support several
|
lcp@104
|
20 |
proofs at the same time.
|
lcp@104
|
21 |
|
lcp@104
|
22 |
The subgoal module always contains some proof state. At the start of the
|
lcp@104
|
23 |
Isabelle session, this state consists of a dummy formula.
|
lcp@104
|
24 |
|
lcp@104
|
25 |
|
lcp@104
|
26 |
\section{Basic commands}
|
wenzelm@5391
|
27 |
Most proofs begin with \texttt{Goal} or \texttt{Goalw} and require no other
|
paulson@5205
|
28 |
commands than \texttt{by}, \texttt{chop} and \texttt{undo}. They typically end
|
paulson@5205
|
29 |
with a call to \texttt{qed}.
|
lcp@104
|
30 |
\subsection{Starting a backward proof}
|
lcp@321
|
31 |
\index{proofs!starting}
|
wenzelm@5391
|
32 |
\begin{ttbox}
|
wenzelm@5391
|
33 |
Goal : string -> thm list
|
wenzelm@5391
|
34 |
Goalw : thm list -> string -> thm list
|
wenzelm@5391
|
35 |
goal : theory -> string -> thm list
|
lcp@104
|
36 |
goalw : theory -> thm list -> string -> thm list
|
paulson@8968
|
37 |
goalw_cterm : thm list -> cterm -> thm list
|
lcp@104
|
38 |
premises : unit -> thm list
|
lcp@104
|
39 |
\end{ttbox}
|
wenzelm@5391
|
40 |
|
wenzelm@5391
|
41 |
The goal commands start a new proof by setting the goal. They replace
|
wenzelm@5391
|
42 |
the current state list by a new one consisting of the initial proof
|
wenzelm@5391
|
43 |
state. They also empty the \ttindex{undo} list; this command cannot
|
wenzelm@5391
|
44 |
be undone!
|
lcp@104
|
45 |
|
lcp@104
|
46 |
They all return a list of meta-hypotheses taken from the main goal. If
|
lcp@104
|
47 |
this list is non-empty, bind its value to an \ML{} identifier by typing
|
lcp@104
|
48 |
something like
|
lcp@104
|
49 |
\begin{ttbox}
|
lcp@332
|
50 |
val prems = goal{\it theory\/ formula};
|
lcp@321
|
51 |
\end{ttbox}\index{assumptions!of main goal}
|
wenzelm@5391
|
52 |
These assumptions typically serve as the premises when you are
|
wenzelm@5391
|
53 |
deriving a rule. They are also stored internally and can be retrieved
|
wenzelm@5391
|
54 |
later by the function \texttt{premises}. When the proof is finished,
|
wenzelm@5391
|
55 |
\texttt{qed} compares the stored assumptions with the actual
|
wenzelm@5391
|
56 |
assumptions in the proof state.
|
wenzelm@5391
|
57 |
|
wenzelm@5391
|
58 |
The capital versions of \texttt{Goal} are the basic user level
|
wenzelm@5391
|
59 |
commands and should be preferred over the more primitive lowercase
|
wenzelm@5391
|
60 |
\texttt{goal} commands. Apart from taking the current theory context
|
wenzelm@5391
|
61 |
as implicit argument, the former ones try to be smart in handling
|
wenzelm@5391
|
62 |
meta-hypotheses when deriving rules. Thus \texttt{prems} have to be
|
wenzelm@5391
|
63 |
seldom bound explicitly, the effect is as if \texttt{cut_facts_tac}
|
wenzelm@5391
|
64 |
had been called automatically.
|
lcp@104
|
65 |
|
lcp@321
|
66 |
\index{definitions!unfolding}
|
lcp@104
|
67 |
Some of the commands unfold definitions using meta-rewrite rules. This
|
lcp@332
|
68 |
expansion affects both the initial subgoal and the premises, which would
|
paulson@5205
|
69 |
otherwise require use of \texttt{rewrite_goals_tac} and
|
paulson@5205
|
70 |
\texttt{rewrite_rule}.
|
lcp@104
|
71 |
|
lcp@321
|
72 |
\begin{ttdescription}
|
wenzelm@5391
|
73 |
\item[\ttindexbold{Goal} {\it formula};] begins a new proof, where
|
wenzelm@5391
|
74 |
{\it formula\/} is written as an \ML\ string.
|
wenzelm@5391
|
75 |
|
wenzelm@5391
|
76 |
\item[\ttindexbold{Goalw} {\it defs} {\it formula};] is like
|
wenzelm@5391
|
77 |
\texttt{Goal} but also applies the list of {\it defs\/} as
|
wenzelm@5391
|
78 |
meta-rewrite rules to the first subgoal and the premises.
|
wenzelm@5391
|
79 |
\index{meta-rewriting}
|
wenzelm@5391
|
80 |
|
lcp@321
|
81 |
\item[\ttindexbold{goal} {\it theory} {\it formula};]
|
lcp@104
|
82 |
begins a new proof, where {\it theory} is usually an \ML\ identifier
|
lcp@104
|
83 |
and the {\it formula\/} is written as an \ML\ string.
|
lcp@104
|
84 |
|
lcp@321
|
85 |
\item[\ttindexbold{goalw} {\it theory} {\it defs} {\it formula};]
|
paulson@5205
|
86 |
is like \texttt{goal} but also applies the list of {\it defs\/} as
|
lcp@104
|
87 |
meta-rewrite rules to the first subgoal and the premises.
|
lcp@321
|
88 |
\index{meta-rewriting}
|
lcp@104
|
89 |
|
paulson@8978
|
90 |
\item[\ttindexbold{goalw_cterm} {\it defs} {\it ct};] is
|
paulson@8978
|
91 |
a version of \texttt{goalw} intended for programming. The main
|
paulson@8978
|
92 |
goal is supplied as a cterm, not as a string. See also
|
paulson@8978
|
93 |
\texttt{prove_goalw_cterm}, \S\ref{sec:executing-batch}.
|
lcp@104
|
94 |
|
lcp@104
|
95 |
\item[\ttindexbold{premises}()]
|
lcp@321
|
96 |
returns the list of meta-hypotheses associated with the current proof (in
|
lcp@321
|
97 |
case you forgot to bind them to an \ML{} identifier).
|
lcp@321
|
98 |
\end{ttdescription}
|
lcp@321
|
99 |
|
lcp@104
|
100 |
|
lcp@104
|
101 |
\subsection{Applying a tactic}
|
lcp@321
|
102 |
\index{tactics!commands for applying}
|
lcp@104
|
103 |
\begin{ttbox}
|
lcp@104
|
104 |
by : tactic -> unit
|
lcp@104
|
105 |
byev : tactic list -> unit
|
lcp@104
|
106 |
\end{ttbox}
|
lcp@104
|
107 |
These commands extend the state list. They apply a tactic to the current
|
lcp@104
|
108 |
proof state. If the tactic succeeds, it returns a non-empty sequence of
|
lcp@104
|
109 |
next states. The head of the sequence becomes the next state, while the
|
paulson@5205
|
110 |
tail is retained for backtracking (see~\texttt{back}).
|
lcp@321
|
111 |
\begin{ttdescription} \item[\ttindexbold{by} {\it tactic};]
|
lcp@104
|
112 |
applies the {\it tactic\/} to the proof state.
|
lcp@104
|
113 |
|
lcp@321
|
114 |
\item[\ttindexbold{byev} {\it tactics};]
|
lcp@104
|
115 |
applies the list of {\it tactics}, one at a time. It is useful for testing
|
paulson@5205
|
116 |
calls to \texttt{prove_goal}, and abbreviates \texttt{by (EVERY {\it
|
lcp@104
|
117 |
tactics})}.
|
lcp@321
|
118 |
\end{ttdescription}
|
lcp@104
|
119 |
|
lcp@286
|
120 |
\noindent{\it Error indications:}\nobreak
|
lcp@104
|
121 |
\begin{itemize}
|
lcp@286
|
122 |
\item {\footnotesize\tt "by:\ tactic failed"} means that the tactic
|
lcp@286
|
123 |
returned an empty sequence when applied to the current proof state.
|
lcp@286
|
124 |
\item {\footnotesize\tt "Warning:\ same as previous level"} means that the
|
lcp@286
|
125 |
new proof state is identical to the previous state.
|
lcp@286
|
126 |
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
|
lcp@286
|
127 |
means that some rule was applied whose theory is outside the theory of
|
lcp@286
|
128 |
the initial proof state. This could signify a mistake such as expressing
|
lcp@286
|
129 |
the goal in intuitionistic logic and proving it using classical logic.
|
lcp@104
|
130 |
\end{itemize}
|
lcp@104
|
131 |
|
clasohm@866
|
132 |
\subsection{Extracting and storing the proved theorem}
|
clasohm@866
|
133 |
\label{ExtractingAndStoringTheProvedTheorem}
|
paulson@1233
|
134 |
\index{theorems!extracting proved}
|
lcp@104
|
135 |
\begin{ttbox}
|
wenzelm@7421
|
136 |
qed : string -> unit
|
wenzelm@7446
|
137 |
no_qed : unit -> unit
|
wenzelm@7421
|
138 |
result : unit -> thm
|
wenzelm@7421
|
139 |
uresult : unit -> thm
|
wenzelm@7421
|
140 |
bind_thm : string * thm -> unit
|
wenzelm@7421
|
141 |
bind_thms : string * thm list -> unit
|
wenzelm@7421
|
142 |
store_thm : string * thm -> thm
|
wenzelm@7421
|
143 |
store_thms : string * thm list -> thm list
|
lcp@104
|
144 |
\end{ttbox}
|
lcp@321
|
145 |
\begin{ttdescription}
|
wenzelm@4317
|
146 |
\item[\ttindexbold{qed} $name$;] is the usual way of ending a proof.
|
paulson@5205
|
147 |
It combines \texttt{result} and \texttt{bind_thm}: it gets the theorem
|
paulson@5205
|
148 |
using \texttt{result()} and stores it the theorem database associated
|
wenzelm@4317
|
149 |
with its theory. See below for details.
|
wenzelm@7446
|
150 |
|
wenzelm@7446
|
151 |
\item[\ttindexbold{no_qed}();] indicates that the proof is not concluded by a
|
wenzelm@7446
|
152 |
proper \texttt{qed} command. This is a do-nothing operation, it merely
|
wenzelm@7446
|
153 |
helps user interfaces such as Proof~General \cite{proofgeneral} to figure
|
wenzelm@7446
|
154 |
out the structure of the {\ML} text.
|
paulson@1283
|
155 |
|
lcp@321
|
156 |
\item[\ttindexbold{result}()]\index{assumptions!of main goal}
|
clasohm@866
|
157 |
returns the final theorem, after converting the free variables to
|
clasohm@866
|
158 |
schematics. It discharges the assumptions supplied to the matching
|
paulson@5205
|
159 |
\texttt{goal} command.
|
lcp@104
|
160 |
|
clasohm@866
|
161 |
It raises an exception unless the proof state passes certain checks. There
|
paulson@5205
|
162 |
must be no assumptions other than those supplied to \texttt{goal}. There
|
clasohm@866
|
163 |
must be no subgoals. The theorem proved must be a (first-order) instance
|
paulson@5205
|
164 |
of the original goal, as stated in the \texttt{goal} command. This allows
|
clasohm@866
|
165 |
{\bf answer extraction} --- instantiation of variables --- but no other
|
clasohm@866
|
166 |
changes to the main goal. The theorem proved must have the same signature
|
clasohm@866
|
167 |
as the initial proof state.
|
lcp@104
|
168 |
|
clasohm@866
|
169 |
These checks are needed because an Isabelle tactic can return any proof
|
clasohm@866
|
170 |
state at all.
|
lcp@321
|
171 |
|
paulson@5205
|
172 |
\item[\ttindexbold{uresult}()] is like \texttt{result()} but omits the checks.
|
lcp@321
|
173 |
It is needed when the initial goal contains function unknowns, when
|
lcp@321
|
174 |
definitions are unfolded in the main goal (by calling
|
lcp@321
|
175 |
\ttindex{rewrite_tac}),\index{definitions!unfolding} or when
|
lcp@321
|
176 |
\ttindex{assume_ax} has been used.
|
wenzelm@4317
|
177 |
|
wenzelm@4317
|
178 |
\item[\ttindexbold{bind_thm} ($name$, $thm$);]\index{theorems!storing}
|
paulson@5205
|
179 |
stores \texttt{standard $thm$} (see \S\ref{MiscellaneousForwardRules})
|
wenzelm@4317
|
180 |
in the theorem database associated with its theory and in the {\ML}
|
wenzelm@4317
|
181 |
variable $name$. The theorem can be retrieved from the database
|
paulson@5205
|
182 |
using \texttt{get_thm} (see \S\ref{BasicOperationsOnTheories}).
|
wenzelm@4317
|
183 |
|
wenzelm@4317
|
184 |
\item[\ttindexbold{store_thm} ($name$, $thm$)]\index{theorems!storing}
|
wenzelm@4317
|
185 |
stores $thm$ in the theorem database associated with its theory and
|
wenzelm@4317
|
186 |
returns that theorem.
|
wenzelm@7421
|
187 |
|
wenzelm@7990
|
188 |
\item[\ttindexbold{bind_thms} \textrm{and} \ttindexbold{store_thms}] are similar to
|
wenzelm@7421
|
189 |
\texttt{bind_thm} and \texttt{store_thm}, but store lists of theorems.
|
wenzelm@7421
|
190 |
|
lcp@321
|
191 |
\end{ttdescription}
|
lcp@104
|
192 |
|
wenzelm@7990
|
193 |
The name argument of \texttt{qed}, \texttt{bind_thm} etc.\ may be the empty
|
wenzelm@7990
|
194 |
string as well; in that case the result is \emph{not} stored, but proper
|
wenzelm@7990
|
195 |
checks and presentation of the result still apply.
|
wenzelm@7591
|
196 |
|
lcp@104
|
197 |
|
wenzelm@5391
|
198 |
\subsection{Extracting axioms and stored theorems}
|
wenzelm@5391
|
199 |
\index{theories!axioms of}\index{axioms!extracting}
|
wenzelm@5391
|
200 |
\index{theories!theorems of}\index{theorems!extracting}
|
wenzelm@5391
|
201 |
\begin{ttbox}
|
wenzelm@5391
|
202 |
thm : xstring -> thm
|
wenzelm@5391
|
203 |
thms : xstring -> thm list
|
wenzelm@5391
|
204 |
get_axiom : theory -> xstring -> thm
|
wenzelm@5391
|
205 |
get_thm : theory -> xstring -> thm
|
wenzelm@5391
|
206 |
get_thms : theory -> xstring -> thm list
|
wenzelm@5391
|
207 |
axioms_of : theory -> (string * thm) list
|
wenzelm@5391
|
208 |
thms_of : theory -> (string * thm) list
|
wenzelm@5391
|
209 |
assume_ax : theory -> string -> thm
|
wenzelm@5391
|
210 |
\end{ttbox}
|
wenzelm@5391
|
211 |
\begin{ttdescription}
|
wenzelm@5391
|
212 |
|
wenzelm@5391
|
213 |
\item[\ttindexbold{thm} $name$] is the basic user function for
|
wenzelm@5391
|
214 |
extracting stored theorems from the current theory context.
|
wenzelm@5391
|
215 |
|
wenzelm@5391
|
216 |
\item[\ttindexbold{thms} $name$] is like \texttt{thm}, but returns a
|
wenzelm@5391
|
217 |
whole list associated with $name$ rather than a single theorem.
|
wenzelm@5391
|
218 |
Typically this will be collections stored by packages, e.g.\
|
wenzelm@5391
|
219 |
\verb|list.simps|.
|
wenzelm@5391
|
220 |
|
wenzelm@5391
|
221 |
\item[\ttindexbold{get_axiom} $thy$ $name$] returns an axiom with the
|
wenzelm@5391
|
222 |
given $name$ from $thy$ or any of its ancestors, raising exception
|
wenzelm@5391
|
223 |
\xdx{THEORY} if none exists. Merging theories can cause several
|
wenzelm@5391
|
224 |
axioms to have the same name; {\tt get_axiom} returns an arbitrary
|
wenzelm@5391
|
225 |
one. Usually, axioms are also stored as theorems and may be
|
wenzelm@5391
|
226 |
retrieved via \texttt{get_thm} as well.
|
wenzelm@5391
|
227 |
|
wenzelm@5391
|
228 |
\item[\ttindexbold{get_thm} $thy$ $name$] is analogous to {\tt
|
wenzelm@5391
|
229 |
get_axiom}, but looks for a theorem stored in the theory's
|
wenzelm@5391
|
230 |
database. Like {\tt get_axiom} it searches all parents of a theory
|
wenzelm@5391
|
231 |
if the theorem is not found directly in $thy$.
|
wenzelm@5391
|
232 |
|
wenzelm@5391
|
233 |
\item[\ttindexbold{get_thms} $thy$ $name$] is like \texttt{get_thm}
|
wenzelm@5391
|
234 |
for retrieving theorem lists stored within the theory. It returns a
|
wenzelm@5391
|
235 |
singleton list if $name$ actually refers to a theorem rather than a
|
wenzelm@5391
|
236 |
theorem list.
|
wenzelm@5391
|
237 |
|
wenzelm@5391
|
238 |
\item[\ttindexbold{axioms_of} $thy$] returns the axioms of this theory
|
wenzelm@5391
|
239 |
node, not including the ones of its ancestors.
|
wenzelm@5391
|
240 |
|
wenzelm@5391
|
241 |
\item[\ttindexbold{thms_of} $thy$] returns all theorems stored within
|
wenzelm@5391
|
242 |
the database of this theory node, not including the ones of its
|
wenzelm@5391
|
243 |
ancestors.
|
wenzelm@5391
|
244 |
|
wenzelm@5391
|
245 |
\item[\ttindexbold{assume_ax} $thy$ $formula$] reads the {\it formula}
|
wenzelm@5391
|
246 |
using the syntax of $thy$, following the same conventions as axioms
|
wenzelm@5391
|
247 |
in a theory definition. You can thus pretend that {\it formula} is
|
wenzelm@5391
|
248 |
an axiom and use the resulting theorem like an axiom. Actually {\tt
|
wenzelm@5391
|
249 |
assume_ax} returns an assumption; \ttindex{qed} and
|
wenzelm@5391
|
250 |
\ttindex{result} complain about additional assumptions, but
|
wenzelm@5391
|
251 |
\ttindex{uresult} does not.
|
wenzelm@5391
|
252 |
|
wenzelm@5391
|
253 |
For example, if {\it formula} is
|
wenzelm@5391
|
254 |
\hbox{\tt a=b ==> b=a} then the resulting theorem has the form
|
wenzelm@5391
|
255 |
\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
|
wenzelm@5391
|
256 |
\end{ttdescription}
|
wenzelm@5391
|
257 |
|
wenzelm@5391
|
258 |
|
nipkow@1222
|
259 |
\subsection{Retrieving theorems}
|
nipkow@1222
|
260 |
\index{theorems!retrieving}
|
nipkow@1222
|
261 |
|
wenzelm@4317
|
262 |
The following functions retrieve theorems (together with their names)
|
wenzelm@4317
|
263 |
from the theorem database that is associated with the current proof
|
wenzelm@4317
|
264 |
state's theory. They can only find theorems that have explicitly been
|
wenzelm@4317
|
265 |
stored in the database using \ttindex{qed}, \ttindex{bind_thm} or
|
nipkow@1222
|
266 |
related functions.
|
nipkow@1222
|
267 |
\begin{ttbox}
|
wenzelm@4317
|
268 |
findI : int -> (string * thm) list
|
wenzelm@4317
|
269 |
findE : int -> int -> (string * thm) list
|
wenzelm@4317
|
270 |
findEs : int -> (string * thm) list
|
wenzelm@4317
|
271 |
thms_containing : xstring list -> (string * thm) list
|
nipkow@1222
|
272 |
\end{ttbox}
|
nipkow@1222
|
273 |
\begin{ttdescription}
|
nipkow@1222
|
274 |
\item[\ttindexbold{findI} $i$]\index{assumptions!of main goal}
|
paulson@1225
|
275 |
returns all ``introduction rules'' applicable to subgoal $i$ --- all
|
nipkow@1222
|
276 |
theorems whose conclusion matches (rather than unifies with) subgoal
|
paulson@5205
|
277 |
$i$. Useful in connection with \texttt{resolve_tac}.
|
nipkow@1222
|
278 |
|
nipkow@1222
|
279 |
\item[\ttindexbold{findE} $n$ $i$] returns all ``elimination rules''
|
paulson@1225
|
280 |
applicable to premise $n$ of subgoal $i$ --- all those theorems whose
|
paulson@1225
|
281 |
first premise matches premise $n$ of subgoal $i$. Useful in connection with
|
paulson@5205
|
282 |
\texttt{eresolve_tac} and \texttt{dresolve_tac}.
|
nipkow@1222
|
283 |
|
nipkow@1222
|
284 |
\item[\ttindexbold{findEs} $i$] returns all ``elimination rules'' applicable
|
paulson@1225
|
285 |
to subgoal $i$ --- all those theorems whose first premise matches some
|
paulson@5205
|
286 |
premise of subgoal $i$. Useful in connection with \texttt{eresolve_tac} and
|
paulson@5205
|
287 |
\texttt{dresolve_tac}.
|
wenzelm@4317
|
288 |
|
wenzelm@7805
|
289 |
\item[\ttindexbold{thms_containing} $consts$] returns all theorems that
|
wenzelm@7805
|
290 |
contain \emph{all} of the given constants.
|
nipkow@1222
|
291 |
\end{ttdescription}
|
nipkow@1222
|
292 |
|
nipkow@1222
|
293 |
|
lcp@104
|
294 |
\subsection{Undoing and backtracking}
|
lcp@104
|
295 |
\begin{ttbox}
|
lcp@104
|
296 |
chop : unit -> unit
|
lcp@104
|
297 |
choplev : int -> unit
|
lcp@104
|
298 |
back : unit -> unit
|
lcp@104
|
299 |
undo : unit -> unit
|
lcp@104
|
300 |
\end{ttbox}
|
lcp@321
|
301 |
\begin{ttdescription}
|
lcp@104
|
302 |
\item[\ttindexbold{chop}();]
|
lcp@104
|
303 |
deletes the top level of the state list, cancelling the last \ttindex{by}
|
paulson@5205
|
304 |
command. It provides a limited undo facility, and the \texttt{undo} command
|
lcp@104
|
305 |
can cancel it.
|
lcp@104
|
306 |
|
lcp@104
|
307 |
\item[\ttindexbold{choplev} {\it n};]
|
paulson@2128
|
308 |
truncates the state list to level~{\it n}, if $n\geq0$. A negative value
|
paulson@2128
|
309 |
of~$n$ refers to the $n$th previous level:
|
paulson@5205
|
310 |
\hbox{\verb|choplev ~1|} has the same effect as \texttt{chop}.
|
lcp@104
|
311 |
|
lcp@104
|
312 |
\item[\ttindexbold{back}();]
|
lcp@104
|
313 |
searches the state list for a non-empty branch point, starting from the top
|
lcp@104
|
314 |
level. The first one found becomes the current proof state --- the most
|
lcp@286
|
315 |
recent alternative branch is taken. This is a form of interactive
|
lcp@286
|
316 |
backtracking.
|
lcp@104
|
317 |
|
lcp@104
|
318 |
\item[\ttindexbold{undo}();]
|
lcp@104
|
319 |
cancels the most recent change to the proof state by the commands \ttindex{by},
|
paulson@5205
|
320 |
\texttt{chop}, \texttt{choplev}, and~\texttt{back}. It {\bf cannot}
|
paulson@5205
|
321 |
cancel \texttt{goal} or \texttt{undo} itself. It can be repeated to
|
lcp@104
|
322 |
cancel a series of commands.
|
lcp@321
|
323 |
\end{ttdescription}
|
lcp@286
|
324 |
|
lcp@286
|
325 |
\goodbreak
|
wenzelm@6569
|
326 |
\noindent{\it Error indications for {\tt back}:}\par\nobreak
|
lcp@104
|
327 |
\begin{itemize}
|
lcp@286
|
328 |
\item{\footnotesize\tt"Warning:\ same as previous choice at this level"}
|
paulson@5205
|
329 |
means \texttt{back} found a non-empty branch point, but that it contained
|
lcp@286
|
330 |
the same proof state as the current one.
|
lcp@286
|
331 |
\item{\footnotesize\tt "Warning:\ signature of proof state has changed"}
|
lcp@286
|
332 |
means the signature of the alternative proof state differs from that of
|
lcp@286
|
333 |
the current state.
|
paulson@5205
|
334 |
\item {\footnotesize\tt "back:\ no alternatives"} means \texttt{back} could
|
lcp@286
|
335 |
find no alternative proof state.
|
lcp@104
|
336 |
\end{itemize}
|
lcp@104
|
337 |
|
lcp@507
|
338 |
\subsection{Printing the proof state}\label{sec:goals-printing}
|
lcp@321
|
339 |
\index{proof state!printing of}
|
lcp@104
|
340 |
\begin{ttbox}
|
lcp@104
|
341 |
pr : unit -> unit
|
lcp@104
|
342 |
prlev : int -> unit
|
paulson@2528
|
343 |
prlim : int -> unit
|
lcp@104
|
344 |
goals_limit: int ref \hfill{\bf initially 10}
|
lcp@104
|
345 |
\end{ttbox}
|
paulson@2528
|
346 |
See also the printing control options described
|
paulson@2528
|
347 |
in~\S\ref{sec:printing-control}.
|
lcp@321
|
348 |
\begin{ttdescription}
|
lcp@104
|
349 |
\item[\ttindexbold{pr}();]
|
lcp@104
|
350 |
prints the current proof state.
|
lcp@104
|
351 |
|
lcp@104
|
352 |
\item[\ttindexbold{prlev} {\it n};]
|
paulson@2128
|
353 |
prints the proof state at level {\it n}, if $n\geq0$. A negative value
|
paulson@2128
|
354 |
of~$n$ refers to the $n$th previous level. This command allows
|
paulson@2128
|
355 |
you to review earlier stages of the proof.
|
lcp@104
|
356 |
|
paulson@2528
|
357 |
\item[\ttindexbold{prlim} {\it k};]
|
paulson@2528
|
358 |
prints the current proof state, limiting the number of subgoals to~$k$. It
|
paulson@5205
|
359 |
updates \texttt{goals_limit} (see below) and is helpful when there are many
|
paulson@2528
|
360 |
subgoals.
|
paulson@2528
|
361 |
|
lcp@321
|
362 |
\item[\ttindexbold{goals_limit} := {\it k};]
|
lcp@104
|
363 |
specifies~$k$ as the maximum number of subgoals to print.
|
lcp@321
|
364 |
\end{ttdescription}
|
lcp@104
|
365 |
|
lcp@104
|
366 |
|
lcp@104
|
367 |
\subsection{Timing}
|
lcp@321
|
368 |
\index{timing statistics}\index{proofs!timing}
|
lcp@104
|
369 |
\begin{ttbox}
|
wenzelm@8995
|
370 |
timing: bool ref \hfill{\bf initially false}
|
lcp@104
|
371 |
\end{ttbox}
|
lcp@104
|
372 |
|
lcp@321
|
373 |
\begin{ttdescription}
|
wenzelm@8995
|
374 |
\item[set \ttindexbold{timing};] enables global timing in Isabelle. In
|
wenzelm@8995
|
375 |
particular, this makes the \ttindex{by} and \ttindex{prove_goal} commands
|
wenzelm@8995
|
376 |
display how much processor time was spent. This information is
|
wenzelm@8995
|
377 |
compiler-dependent.
|
lcp@321
|
378 |
\end{ttdescription}
|
lcp@104
|
379 |
|
lcp@104
|
380 |
|
lcp@104
|
381 |
\section{Shortcuts for applying tactics}
|
paulson@5205
|
382 |
\index{shortcuts!for \texttt{by} commands}
|
lcp@104
|
383 |
These commands call \ttindex{by} with common tactics. Their chief purpose
|
lcp@104
|
384 |
is to minimise typing, although the scanning shortcuts are useful in their
|
lcp@104
|
385 |
own right. Chapter~\ref{tactics} explains the tactics themselves.
|
lcp@104
|
386 |
|
lcp@104
|
387 |
\subsection{Refining a given subgoal}
|
lcp@104
|
388 |
\begin{ttbox}
|
lcp@321
|
389 |
ba : int -> unit
|
lcp@321
|
390 |
br : thm -> int -> unit
|
lcp@321
|
391 |
be : thm -> int -> unit
|
lcp@321
|
392 |
bd : thm -> int -> unit
|
lcp@321
|
393 |
brs : thm list -> int -> unit
|
lcp@321
|
394 |
bes : thm list -> int -> unit
|
lcp@321
|
395 |
bds : thm list -> int -> unit
|
lcp@104
|
396 |
\end{ttbox}
|
lcp@104
|
397 |
|
lcp@321
|
398 |
\begin{ttdescription}
|
lcp@104
|
399 |
\item[\ttindexbold{ba} {\it i};]
|
paulson@5205
|
400 |
performs \texttt{by (assume_tac {\it i});}
|
lcp@104
|
401 |
|
lcp@104
|
402 |
\item[\ttindexbold{br} {\it thm} {\it i};]
|
paulson@5205
|
403 |
performs \texttt{by (resolve_tac [{\it thm}] {\it i});}
|
lcp@104
|
404 |
|
lcp@104
|
405 |
\item[\ttindexbold{be} {\it thm} {\it i};]
|
paulson@5205
|
406 |
performs \texttt{by (eresolve_tac [{\it thm}] {\it i});}
|
lcp@104
|
407 |
|
lcp@104
|
408 |
\item[\ttindexbold{bd} {\it thm} {\it i};]
|
paulson@5205
|
409 |
performs \texttt{by (dresolve_tac [{\it thm}] {\it i});}
|
lcp@104
|
410 |
|
lcp@104
|
411 |
\item[\ttindexbold{brs} {\it thms} {\it i};]
|
paulson@5205
|
412 |
performs \texttt{by (resolve_tac {\it thms} {\it i});}
|
lcp@104
|
413 |
|
lcp@104
|
414 |
\item[\ttindexbold{bes} {\it thms} {\it i};]
|
paulson@5205
|
415 |
performs \texttt{by (eresolve_tac {\it thms} {\it i});}
|
lcp@104
|
416 |
|
lcp@104
|
417 |
\item[\ttindexbold{bds} {\it thms} {\it i};]
|
paulson@5205
|
418 |
performs \texttt{by (dresolve_tac {\it thms} {\it i});}
|
lcp@321
|
419 |
\end{ttdescription}
|
lcp@104
|
420 |
|
lcp@104
|
421 |
|
lcp@104
|
422 |
\subsection{Scanning shortcuts}
|
lcp@104
|
423 |
These shortcuts scan for a suitable subgoal (starting from subgoal~1).
|
lcp@104
|
424 |
They refine the first subgoal for which the tactic succeeds. Thus, they
|
paulson@5205
|
425 |
require less typing than \texttt{br}, etc. They display the selected
|
lcp@104
|
426 |
subgoal's number; please watch this, for it may not be what you expect!
|
lcp@104
|
427 |
|
lcp@104
|
428 |
\begin{ttbox}
|
lcp@321
|
429 |
fa : unit -> unit
|
lcp@321
|
430 |
fr : thm -> unit
|
lcp@321
|
431 |
fe : thm -> unit
|
lcp@321
|
432 |
fd : thm -> unit
|
lcp@321
|
433 |
frs : thm list -> unit
|
lcp@321
|
434 |
fes : thm list -> unit
|
lcp@321
|
435 |
fds : thm list -> unit
|
lcp@104
|
436 |
\end{ttbox}
|
lcp@104
|
437 |
|
lcp@321
|
438 |
\begin{ttdescription}
|
lcp@104
|
439 |
\item[\ttindexbold{fa}();]
|
lcp@321
|
440 |
solves some subgoal by assumption.
|
lcp@104
|
441 |
|
lcp@104
|
442 |
\item[\ttindexbold{fr} {\it thm};]
|
paulson@5205
|
443 |
refines some subgoal using \texttt{resolve_tac [{\it thm}]}
|
lcp@104
|
444 |
|
lcp@104
|
445 |
\item[\ttindexbold{fe} {\it thm};]
|
paulson@5205
|
446 |
refines some subgoal using \texttt{eresolve_tac [{\it thm}]}
|
lcp@104
|
447 |
|
lcp@104
|
448 |
\item[\ttindexbold{fd} {\it thm};]
|
paulson@5205
|
449 |
refines some subgoal using \texttt{dresolve_tac [{\it thm}]}
|
lcp@104
|
450 |
|
lcp@104
|
451 |
\item[\ttindexbold{frs} {\it thms};]
|
paulson@5205
|
452 |
refines some subgoal using \texttt{resolve_tac {\it thms}}
|
lcp@104
|
453 |
|
lcp@104
|
454 |
\item[\ttindexbold{fes} {\it thms};]
|
paulson@5205
|
455 |
refines some subgoal using \texttt{eresolve_tac {\it thms}}
|
lcp@104
|
456 |
|
lcp@104
|
457 |
\item[\ttindexbold{fds} {\it thms};]
|
paulson@5205
|
458 |
refines some subgoal using \texttt{dresolve_tac {\it thms}}
|
lcp@321
|
459 |
\end{ttdescription}
|
lcp@104
|
460 |
|
lcp@104
|
461 |
\subsection{Other shortcuts}
|
lcp@104
|
462 |
\begin{ttbox}
|
lcp@104
|
463 |
bw : thm -> unit
|
lcp@104
|
464 |
bws : thm list -> unit
|
lcp@104
|
465 |
ren : string -> int -> unit
|
lcp@104
|
466 |
\end{ttbox}
|
lcp@321
|
467 |
\begin{ttdescription}
|
paulson@5205
|
468 |
\item[\ttindexbold{bw} {\it def};] performs \texttt{by
|
wenzelm@4317
|
469 |
(rewrite_goals_tac [{\it def}]);} It unfolds definitions in the
|
wenzelm@4317
|
470 |
subgoals (but not the main goal), by meta-rewriting with the given
|
wenzelm@4317
|
471 |
definition (see also \S\ref{sec:rewrite_goals}).
|
wenzelm@4317
|
472 |
\index{meta-rewriting}
|
lcp@104
|
473 |
|
lcp@104
|
474 |
\item[\ttindexbold{bws}]
|
paulson@5205
|
475 |
is like \texttt{bw} but takes a list of definitions.
|
lcp@104
|
476 |
|
lcp@104
|
477 |
\item[\ttindexbold{ren} {\it names} {\it i};]
|
paulson@5205
|
478 |
performs \texttt{by (rename_tac {\it names} {\it i});} it renames
|
lcp@332
|
479 |
parameters in subgoal~$i$. (Ignore the message {\footnotesize\tt Warning:\
|
lcp@332
|
480 |
same as previous level}.)
|
lcp@321
|
481 |
\index{parameters!renaming}
|
lcp@321
|
482 |
\end{ttdescription}
|
lcp@104
|
483 |
|
lcp@104
|
484 |
|
paulson@8978
|
485 |
\section{Executing batch proofs}\label{sec:executing-batch}
|
paulson@3128
|
486 |
\index{batch execution}%
|
paulson@8136
|
487 |
To save space below, let type \texttt{tacfn} abbreviate \texttt{thm list ->
|
paulson@3128
|
488 |
tactic list}, which is the type of a tactical proof.
|
lcp@286
|
489 |
\begin{ttbox}
|
paulson@8136
|
490 |
prove_goal : theory -> string -> tacfn -> thm
|
paulson@8136
|
491 |
qed_goal : string -> theory -> string -> tacfn -> unit
|
paulson@8136
|
492 |
prove_goalw: theory -> thm list -> string -> tacfn -> thm
|
paulson@8136
|
493 |
qed_goalw : string -> theory -> thm list -> string -> tacfn -> unit
|
paulson@8136
|
494 |
prove_goalw_cterm: thm list -> cterm -> tacfn -> thm
|
lcp@104
|
495 |
\end{ttbox}
|
lcp@321
|
496 |
These batch functions create an initial proof state, then apply a tactic to
|
lcp@321
|
497 |
it, yielding a sequence of final proof states. The head of the sequence is
|
lcp@104
|
498 |
returned, provided it is an instance of the theorem originally proposed.
|
paulson@8978
|
499 |
The forms \texttt{prove_goal}, \texttt{prove_goalw} and
|
paulson@8978
|
500 |
\texttt{prove_goalw_cterm} are analogous to \texttt{goal}, \texttt{goalw} and
|
paulson@8978
|
501 |
\texttt{goalw_cterm}.
|
lcp@104
|
502 |
|
lcp@104
|
503 |
The tactic is specified by a function from theorem lists to tactic lists.
|
lcp@332
|
504 |
The function is applied to the list of meta-assumptions taken from
|
lcp@332
|
505 |
the main goal. The resulting tactics are applied in sequence (using {\tt
|
lcp@332
|
506 |
EVERY}). For example, a proof consisting of the commands
|
lcp@104
|
507 |
\begin{ttbox}
|
lcp@104
|
508 |
val prems = goal {\it theory} {\it formula};
|
lcp@104
|
509 |
by \(tac@1\); \ldots by \(tac@n\);
|
wenzelm@3108
|
510 |
qed "my_thm";
|
lcp@104
|
511 |
\end{ttbox}
|
lcp@104
|
512 |
can be transformed to an expression as follows:
|
lcp@104
|
513 |
\begin{ttbox}
|
wenzelm@3108
|
514 |
qed_goal "my_thm" {\it theory} {\it formula}
|
lcp@104
|
515 |
(fn prems=> [ \(tac@1\), \ldots, \(tac@n\) ]);
|
lcp@104
|
516 |
\end{ttbox}
|
lcp@104
|
517 |
The methods perform identical processing of the initial {\it formula} and
|
paulson@5205
|
518 |
the final proof state. But \texttt{prove_goal} executes the tactic as a
|
lcp@332
|
519 |
atomic operation, bypassing the subgoal module; the current interactive
|
lcp@332
|
520 |
proof is unaffected.
|
lcp@332
|
521 |
%
|
lcp@321
|
522 |
\begin{ttdescription}
|
lcp@321
|
523 |
\item[\ttindexbold{prove_goal} {\it theory} {\it formula} {\it tacsf};]
|
lcp@104
|
524 |
executes a proof of the {\it formula\/} in the given {\it theory}, using
|
lcp@104
|
525 |
the given tactic function.
|
lcp@104
|
526 |
|
wenzelm@4317
|
527 |
\item[\ttindexbold{qed_goal} $name$ $theory$ $formula$ $tacsf$;] acts
|
paulson@8136
|
528 |
like \texttt{prove_goal} but it also stores the resulting theorem in the
|
wenzelm@4317
|
529 |
theorem database associated with its theory and in the {\ML}
|
wenzelm@4317
|
530 |
variable $name$ (see \S\ref{ExtractingAndStoringTheProvedTheorem}).
|
clasohm@866
|
531 |
|
lcp@104
|
532 |
\item[\ttindexbold{prove_goalw} {\it theory} {\it defs} {\it formula}
|
lcp@321
|
533 |
{\it tacsf};]\index{meta-rewriting}
|
paulson@5205
|
534 |
is like \texttt{prove_goal} but also applies the list of {\it defs\/} as
|
lcp@104
|
535 |
meta-rewrite rules to the first subgoal and the premises.
|
lcp@104
|
536 |
|
clasohm@866
|
537 |
\item[\ttindexbold{qed_goalw} $name$ $theory$ $defs$ $formula$ $tacsf$;]
|
paulson@5205
|
538 |
is analogous to \texttt{qed_goal}.
|
clasohm@866
|
539 |
|
paulson@8978
|
540 |
\item[\ttindexbold{prove_goalw_cterm} {\it defs} {\it ct}
|
lcp@321
|
541 |
{\it tacsf};]
|
paulson@8978
|
542 |
is a version of \texttt{prove_goalw} intended for programming. The main
|
paulson@8978
|
543 |
goal is supplied as a cterm, not as a string. A cterm carries a theory with
|
paulson@8978
|
544 |
it, and can be created from a term~$t$ by
|
lcp@286
|
545 |
\begin{ttbox}
|
paulson@8978
|
546 |
cterm_of (sign_of thy) \(t\)
|
lcp@286
|
547 |
\end{ttbox}
|
paulson@8978
|
548 |
\index{*cterm_of}\index{*sign_of}
|
lcp@321
|
549 |
\end{ttdescription}
|
lcp@104
|
550 |
|
lcp@104
|
551 |
|
wenzelm@13479
|
552 |
\section{Internal proofs}
|
wenzelm@13479
|
553 |
|
wenzelm@13479
|
554 |
\begin{ttbox}
|
wenzelm@13479
|
555 |
Tactic.prove: Sign.sg -> string list -> term list -> term ->
|
wenzelm@13479
|
556 |
(thm list -> tactic) -> thm
|
wenzelm@13479
|
557 |
Tactic.prove_standard: Sign.sg -> string list -> term list -> term ->
|
wenzelm@13479
|
558 |
(thm list -> tactic) -> thm
|
wenzelm@13479
|
559 |
\end{ttbox}
|
wenzelm@13479
|
560 |
|
wenzelm@13479
|
561 |
These functions provide a clean internal interface for programmed proofs. The
|
wenzelm@13479
|
562 |
special overhead of top-level statements (cf.\ \verb,prove_goalw_cterm,) is
|
wenzelm@13479
|
563 |
omitted. Statements may be established within a local contexts of fixed
|
wenzelm@13479
|
564 |
variables and assumptions, which are the only hypotheses to be discharged in
|
wenzelm@13479
|
565 |
the result.
|
wenzelm@13479
|
566 |
|
wenzelm@13479
|
567 |
\begin{ttdescription}
|
wenzelm@13479
|
568 |
\item[\ttindexbold{Tactic.prove}~$sg~xs~As~C~tacf$] establishes the result
|
wenzelm@13479
|
569 |
$\Forall xs. As \Imp C$ via the given tactic (which is a function taking the
|
wenzelm@13479
|
570 |
assumptions as local premises).
|
wenzelm@13479
|
571 |
|
wenzelm@13479
|
572 |
\item[\ttindexbold{Tactic.prove_standard}] is simular to \verb,Tactic.prove,,
|
wenzelm@13479
|
573 |
but performs the \verb,standard, operation on the result, essentially
|
wenzelm@13479
|
574 |
turning it into a top-level statement. Never do this for local proofs
|
wenzelm@13479
|
575 |
within other proof tools!
|
wenzelm@13479
|
576 |
|
wenzelm@13479
|
577 |
\end{ttdescription}
|
wenzelm@13479
|
578 |
|
wenzelm@13479
|
579 |
|
lcp@321
|
580 |
\section{Managing multiple proofs}
|
lcp@321
|
581 |
\index{proofs!managing multiple}
|
lcp@104
|
582 |
You may save the current state of the subgoal module and resume work on it
|
lcp@104
|
583 |
later. This serves two purposes.
|
lcp@104
|
584 |
\begin{enumerate}
|
lcp@104
|
585 |
\item At some point, you may be uncertain of the next step, and
|
lcp@104
|
586 |
wish to experiment.
|
lcp@104
|
587 |
|
lcp@104
|
588 |
\item During a proof, you may see that a lemma should be proved first.
|
lcp@104
|
589 |
\end{enumerate}
|
lcp@104
|
590 |
Each saved proof state consists of a list of levels; \ttindex{chop} behaves
|
lcp@104
|
591 |
independently for each of the saved proofs. In addition, each saved state
|
lcp@104
|
592 |
carries a separate \ttindex{undo} list.
|
lcp@104
|
593 |
|
lcp@321
|
594 |
\subsection{The stack of proof states}
|
lcp@321
|
595 |
\index{proofs!stacking}
|
lcp@104
|
596 |
\begin{ttbox}
|
lcp@104
|
597 |
push_proof : unit -> unit
|
lcp@104
|
598 |
pop_proof : unit -> thm list
|
lcp@104
|
599 |
rotate_proof : unit -> thm list
|
lcp@104
|
600 |
\end{ttbox}
|
lcp@104
|
601 |
The subgoal module maintains a stack of proof states. Most subgoal
|
paulson@5205
|
602 |
commands affect only the top of the stack. The \ttindex{Goal} command {\em
|
lcp@321
|
603 |
replaces\/} the top of the stack; the only command that pushes a proof on the
|
paulson@5205
|
604 |
stack is \texttt{push_proof}.
|
lcp@104
|
605 |
|
paulson@5205
|
606 |
To save some point of the proof, call \texttt{push_proof}. You may now
|
paulson@5205
|
607 |
state a lemma using \texttt{goal}, or simply continue to apply tactics.
|
paulson@5205
|
608 |
Later, you can return to the saved point by calling \texttt{pop_proof} or
|
paulson@5205
|
609 |
\texttt{rotate_proof}.
|
lcp@104
|
610 |
|
paulson@5205
|
611 |
To view the entire stack, call \texttt{rotate_proof} repeatedly; as it rotates
|
lcp@104
|
612 |
the stack, it prints the new top element.
|
lcp@104
|
613 |
|
lcp@321
|
614 |
\begin{ttdescription}
|
lcp@104
|
615 |
\item[\ttindexbold{push_proof}();]
|
lcp@104
|
616 |
duplicates the top element of the stack, pushing a copy of the current
|
lcp@104
|
617 |
proof state on to the stack.
|
lcp@104
|
618 |
|
lcp@104
|
619 |
\item[\ttindexbold{pop_proof}();]
|
lcp@104
|
620 |
discards the top element of the stack. It returns the list of
|
lcp@332
|
621 |
assumptions associated with the new proof; you should bind these to an
|
lcp@104
|
622 |
\ML\ identifier. They can also be obtained by calling \ttindex{premises}.
|
lcp@104
|
623 |
|
lcp@321
|
624 |
\item[\ttindexbold{rotate_proof}();]
|
lcp@321
|
625 |
\index{assumptions!of main goal}
|
lcp@104
|
626 |
rotates the stack, moving the top element to the bottom. It returns the
|
lcp@104
|
627 |
list of assumptions associated with the new proof.
|
lcp@321
|
628 |
\end{ttdescription}
|
lcp@104
|
629 |
|
lcp@104
|
630 |
|
lcp@321
|
631 |
\subsection{Saving and restoring proof states}
|
lcp@321
|
632 |
\index{proofs!saving and restoring}
|
lcp@104
|
633 |
\begin{ttbox}
|
lcp@104
|
634 |
save_proof : unit -> proof
|
lcp@104
|
635 |
restore_proof : proof -> thm list
|
lcp@104
|
636 |
\end{ttbox}
|
lcp@104
|
637 |
States of the subgoal module may be saved as \ML\ values of
|
lcp@321
|
638 |
type~\mltydx{proof}, and later restored.
|
lcp@104
|
639 |
|
lcp@321
|
640 |
\begin{ttdescription}
|
lcp@104
|
641 |
\item[\ttindexbold{save_proof}();]
|
lcp@104
|
642 |
returns the current state, which is on top of the stack.
|
lcp@104
|
643 |
|
lcp@321
|
644 |
\item[\ttindexbold{restore_proof} {\it prf};]\index{assumptions!of main goal}
|
lcp@321
|
645 |
replaces the top of the stack by~{\it prf}. It returns the list of
|
lcp@321
|
646 |
assumptions associated with the new proof.
|
lcp@321
|
647 |
\end{ttdescription}
|
lcp@104
|
648 |
|
lcp@104
|
649 |
|
wenzelm@4317
|
650 |
\section{*Debugging and inspecting}
|
lcp@321
|
651 |
\index{tactics!debugging}
|
paulson@2611
|
652 |
These functions can be useful when you are debugging a tactic. They refer
|
paulson@2611
|
653 |
to the current proof state stored in the subgoal module. A tactic
|
paulson@2611
|
654 |
should never call them; it should operate on the proof state supplied as its
|
paulson@2611
|
655 |
argument.
|
lcp@104
|
656 |
|
lcp@321
|
657 |
\subsection{Reading and printing terms}
|
lcp@321
|
658 |
\index{terms!reading of}\index{terms!printing of}\index{types!printing of}
|
lcp@104
|
659 |
\begin{ttbox}
|
lcp@104
|
660 |
read : string -> term
|
lcp@104
|
661 |
prin : term -> unit
|
lcp@104
|
662 |
printyp : typ -> unit
|
lcp@104
|
663 |
\end{ttbox}
|
lcp@104
|
664 |
These read and print terms (or types) using the syntax associated with the
|
lcp@104
|
665 |
proof state.
|
lcp@104
|
666 |
|
lcp@321
|
667 |
\begin{ttdescription}
|
lcp@104
|
668 |
\item[\ttindexbold{read} {\it string}]
|
paulson@6170
|
669 |
reads the {\it string} as a term, without type-checking.
|
lcp@104
|
670 |
|
lcp@104
|
671 |
\item[\ttindexbold{prin} {\it t};]
|
lcp@104
|
672 |
prints the term~$t$ at the terminal.
|
lcp@104
|
673 |
|
lcp@104
|
674 |
\item[\ttindexbold{printyp} {\it T};]
|
lcp@104
|
675 |
prints the type~$T$ at the terminal.
|
lcp@321
|
676 |
\end{ttdescription}
|
lcp@104
|
677 |
|
lcp@321
|
678 |
\subsection{Inspecting the proof state}
|
lcp@321
|
679 |
\index{proofs!inspecting the state}
|
lcp@104
|
680 |
\begin{ttbox}
|
lcp@104
|
681 |
topthm : unit -> thm
|
lcp@104
|
682 |
getgoal : int -> term
|
lcp@104
|
683 |
gethyps : int -> thm list
|
lcp@104
|
684 |
\end{ttbox}
|
lcp@104
|
685 |
|
lcp@321
|
686 |
\begin{ttdescription}
|
lcp@104
|
687 |
\item[\ttindexbold{topthm}()]
|
lcp@104
|
688 |
returns the proof state as an Isabelle theorem. This is what \ttindex{by}
|
lcp@104
|
689 |
would supply to a tactic at this point. It omits the post-processing of
|
lcp@104
|
690 |
\ttindex{result} and \ttindex{uresult}.
|
lcp@104
|
691 |
|
lcp@104
|
692 |
\item[\ttindexbold{getgoal} {\it i}]
|
lcp@104
|
693 |
returns subgoal~$i$ of the proof state, as a term. You may print
|
paulson@5205
|
694 |
this using \texttt{prin}, though you may have to examine the internal
|
lcp@104
|
695 |
data structure in order to locate the problem!
|
lcp@104
|
696 |
|
lcp@321
|
697 |
\item[\ttindexbold{gethyps} {\it i}]
|
lcp@321
|
698 |
returns the hypotheses of subgoal~$i$ as meta-level assumptions. In
|
lcp@321
|
699 |
these theorems, the subgoal's parameters become free variables. This
|
lcp@321
|
700 |
command is supplied for debugging uses of \ttindex{METAHYPS}.
|
lcp@321
|
701 |
\end{ttdescription}
|
lcp@104
|
702 |
|
paulson@2611
|
703 |
|
lcp@321
|
704 |
\subsection{Filtering lists of rules}
|
lcp@104
|
705 |
\begin{ttbox}
|
lcp@104
|
706 |
filter_goal: (term*term->bool) -> thm list -> int -> thm list
|
lcp@104
|
707 |
\end{ttbox}
|
lcp@104
|
708 |
|
lcp@321
|
709 |
\begin{ttdescription}
|
lcp@104
|
710 |
\item[\ttindexbold{filter_goal} {\it could} {\it ths} {\it i}]
|
paulson@5205
|
711 |
applies \texttt{filter_thms {\it could}} to subgoal~$i$ of the proof
|
lcp@104
|
712 |
state and returns the list of theorems that survive the filtering.
|
lcp@321
|
713 |
\end{ttdescription}
|
lcp@104
|
714 |
|
lcp@104
|
715 |
\index{subgoal module|)}
|
lcp@104
|
716 |
\index{proofs|)}
|
wenzelm@5371
|
717 |
|
wenzelm@5371
|
718 |
|
wenzelm@5371
|
719 |
%%% Local Variables:
|
wenzelm@5371
|
720 |
%%% mode: latex
|
wenzelm@5371
|
721 |
%%% TeX-master: "ref"
|
wenzelm@5371
|
722 |
%%% End:
|