27052
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
|
3 |
\def\isabellecontext{Misc}%
|
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
\isanewline
|
|
7 |
\isanewline
|
|
8 |
%
|
|
9 |
\endisadelimtheory
|
|
10 |
%
|
|
11 |
\isatagtheory
|
|
12 |
\isacommand{theory}\isamarkupfalse%
|
|
13 |
\ Misc\isanewline
|
|
14 |
\isakeyword{imports}\ Main\isanewline
|
|
15 |
\isakeyword{begin}%
|
|
16 |
\endisatagtheory
|
|
17 |
{\isafoldtheory}%
|
|
18 |
%
|
|
19 |
\isadelimtheory
|
|
20 |
%
|
|
21 |
\endisadelimtheory
|
|
22 |
%
|
|
23 |
\isamarkupchapter{Other commands \label{ch:pure-syntax}%
|
|
24 |
}
|
|
25 |
\isamarkuptrue%
|
|
26 |
%
|
|
27 |
\isamarkupsection{Diagnostics%
|
|
28 |
}
|
|
29 |
\isamarkuptrue%
|
|
30 |
%
|
|
31 |
\begin{isamarkuptext}%
|
|
32 |
\begin{matharray}{rcl}
|
|
33 |
\indexdef{}{command}{pr}\hypertarget{command.pr}{\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
|
|
34 |
\indexdef{}{command}{thm}\hypertarget{command.thm}{\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
35 |
\indexdef{}{command}{term}\hypertarget{command.term}{\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
36 |
\indexdef{}{command}{prop}\hypertarget{command.prop}{\hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
37 |
\indexdef{}{command}{typ}\hypertarget{command.typ}{\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
38 |
\indexdef{}{command}{prf}\hypertarget{command.prf}{\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
39 |
\indexdef{}{command}{full\_prf}\hypertarget{command.full-prf}{\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
40 |
\end{matharray}
|
|
41 |
|
|
42 |
These diagnostic commands assist interactive development. Note that
|
|
43 |
\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} does not apply here, the theory or proof
|
|
44 |
configuration is not changed.
|
|
45 |
|
|
46 |
\begin{rail}
|
|
47 |
'pr' modes? nat? (',' nat)?
|
|
48 |
;
|
|
49 |
'thm' modes? thmrefs
|
|
50 |
;
|
|
51 |
'term' modes? term
|
|
52 |
;
|
|
53 |
'prop' modes? prop
|
|
54 |
;
|
|
55 |
'typ' modes? type
|
|
56 |
;
|
|
57 |
'prf' modes? thmrefs?
|
|
58 |
;
|
|
59 |
'full\_prf' modes? thmrefs?
|
|
60 |
;
|
|
61 |
|
|
62 |
modes: '(' (name + ) ')'
|
|
63 |
;
|
|
64 |
\end{rail}
|
|
65 |
|
|
66 |
\begin{descr}
|
|
67 |
|
|
68 |
\item [\hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}}] prints the current
|
|
69 |
proof state (if present), including the proof context, current facts
|
|
70 |
and goals. The optional limit arguments affect the number of goals
|
|
71 |
and premises to be displayed, which is initially 10 for both.
|
|
72 |
Omitting limit values leaves the current setting unchanged.
|
|
73 |
|
|
74 |
\item [\hyperlink{command.thm}{\mbox{\isa{\isacommand{thm}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] retrieves
|
|
75 |
theorems from the current theory or proof context. Note that any
|
|
76 |
attributes included in the theorem specifications are applied to a
|
|
77 |
temporary context derived from the current theory or proof; the
|
|
78 |
result is discarded, i.e.\ attributes involved in \isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ a\isactrlsub n{\isachardoublequote}} do not have any permanent effect.
|
|
79 |
|
|
80 |
\item [\hyperlink{command.term}{\mbox{\isa{\isacommand{term}}}}~\isa{t} and \hyperlink{command.prop}{\mbox{\isa{\isacommand{prop}}}}~\isa{{\isasymphi}}]
|
|
81 |
read, type-check and print terms or propositions according to the
|
|
82 |
current theory or proof context; the inferred type of \isa{t} is
|
|
83 |
output as well. Note that these commands are also useful in
|
|
84 |
inspecting the current environment of term abbreviations.
|
|
85 |
|
|
86 |
\item [\hyperlink{command.typ}{\mbox{\isa{\isacommand{typ}}}}~\isa{{\isasymtau}}] reads and prints types of the
|
|
87 |
meta-logic according to the current theory or proof context.
|
|
88 |
|
|
89 |
\item [\hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}] displays the (compact) proof term of the
|
|
90 |
current proof state (if present), or of the given theorems. Note
|
|
91 |
that this requires proof terms to be switched on for the current
|
|
92 |
object logic (see the ``Proof terms'' section of the Isabelle
|
|
93 |
reference manual for information on how to do this).
|
|
94 |
|
|
95 |
\item [\hyperlink{command.full-prf}{\mbox{\isa{\isacommand{full{\isacharunderscore}prf}}}}] is like \hyperlink{command.prf}{\mbox{\isa{\isacommand{prf}}}}, but displays
|
|
96 |
the full proof term, i.e.\ also displays information omitted in the
|
|
97 |
compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
|
|
98 |
there.
|
|
99 |
|
|
100 |
\end{descr}
|
|
101 |
|
|
102 |
All of the diagnostic commands above admit a list of \isa{modes}
|
|
103 |
to be specified, which is appended to the current print mode (see
|
|
104 |
also \cite{isabelle-ref}). Thus the output behavior may be modified
|
|
105 |
according particular print mode features. For example, \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}{\isacharparenleft}latex\ xsymbols\ symbols{\isacharparenright}{\isachardoublequote}} would print the current
|
|
106 |
proof state with mathematical symbols and special characters
|
|
107 |
represented in {\LaTeX} source, according to the Isabelle style
|
|
108 |
\cite{isabelle-sys}.
|
|
109 |
|
|
110 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
|
|
111 |
systematic way to include formal items into the printed text
|
|
112 |
document.%
|
|
113 |
\end{isamarkuptext}%
|
|
114 |
\isamarkuptrue%
|
|
115 |
%
|
|
116 |
\isamarkupsection{Inspecting the context%
|
|
117 |
}
|
|
118 |
\isamarkuptrue%
|
|
119 |
%
|
|
120 |
\begin{isamarkuptext}%
|
|
121 |
\begin{matharray}{rcl}
|
|
122 |
\indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
|
|
123 |
\indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
124 |
\indexdef{}{command}{print\_syntax}\hypertarget{command.print-syntax}{\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
125 |
\indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
126 |
\indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
127 |
\indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
128 |
\indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
129 |
\indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{theory~|~proof} \\
|
|
130 |
\indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
|
|
131 |
\indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{proof} \\
|
|
132 |
\end{matharray}
|
|
133 |
|
|
134 |
\begin{rail}
|
|
135 |
'print\_theory' ( '!'?)
|
|
136 |
;
|
|
137 |
|
|
138 |
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
|
|
139 |
;
|
|
140 |
criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
|
|
141 |
'simp' ':' term | term)
|
|
142 |
;
|
|
143 |
'thm\_deps' thmrefs
|
|
144 |
;
|
|
145 |
\end{rail}
|
|
146 |
|
|
147 |
These commands print certain parts of the theory and proof context.
|
|
148 |
Note that there are some further ones available, such as for the set
|
|
149 |
of rules declared for simplifications.
|
|
150 |
|
|
151 |
\begin{descr}
|
|
152 |
|
|
153 |
\item [\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}] prints Isabelle's outer theory
|
|
154 |
syntax, including keywords and command.
|
|
155 |
|
|
156 |
\item [\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}] prints the main logical content of
|
|
157 |
the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
|
|
158 |
verbosity.
|
|
159 |
|
|
160 |
\item [\hyperlink{command.print-syntax}{\mbox{\isa{\isacommand{print{\isacharunderscore}syntax}}}}] prints the inner syntax of types
|
|
161 |
and terms, depending on the current context. The output can be very
|
|
162 |
verbose, including grammar tables and syntax translation rules. See
|
|
163 |
\cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
|
|
164 |
inner syntax.
|
|
165 |
|
|
166 |
\item [\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}] prints all proof methods
|
|
167 |
available in the current theory context.
|
|
168 |
|
|
169 |
\item [\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}] prints all attributes
|
|
170 |
available in the current theory context.
|
|
171 |
|
|
172 |
\item [\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}] prints theorems resulting from
|
|
173 |
the last command.
|
|
174 |
|
|
175 |
\item [\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria}] retrieves facts
|
|
176 |
from the theory or proof context matching all of given search
|
|
177 |
criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
|
|
178 |
whose fully qualified name matches pattern \isa{p}, which may
|
|
179 |
contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro},
|
|
180 |
\isa{elim}, and \isa{dest} select theorems that match the
|
|
181 |
current goal as introduction, elimination or destruction rules,
|
|
182 |
respectively. The criterion \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite
|
|
183 |
rules whose left-hand side matches the given term. The criterion
|
|
184 |
term \isa{t} selects all theorems that contain the pattern \isa{t} -- as usual, patterns may contain occurrences of the dummy
|
|
185 |
``\isa{{\isacharunderscore}}'', schematic variables, and type constraints.
|
|
186 |
|
|
187 |
Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
|
|
188 |
do \emph{not} match. Note that giving the empty list of criteria
|
|
189 |
yields \emph{all} currently known facts. An optional limit for the
|
|
190 |
number of printed facts may be given; the default is 40. By
|
|
191 |
default, duplicates are removed from the search result. Use
|
|
192 |
\isa{with{\isacharunderscore}dups} to display duplicates.
|
|
193 |
|
|
194 |
\item [\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}]
|
|
195 |
visualizes dependencies of facts, using Isabelle's graph browser
|
|
196 |
tool (see also \cite{isabelle-sys}).
|
|
197 |
|
|
198 |
\item [\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}] prints all local facts of the
|
|
199 |
current context, both named and unnamed ones.
|
|
200 |
|
|
201 |
\item [\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}] prints all term abbreviations
|
|
202 |
present in the context.
|
|
203 |
|
|
204 |
\end{descr}%
|
|
205 |
\end{isamarkuptext}%
|
|
206 |
\isamarkuptrue%
|
|
207 |
%
|
|
208 |
\isamarkupsection{History commands \label{sec:history}%
|
|
209 |
}
|
|
210 |
\isamarkuptrue%
|
|
211 |
%
|
|
212 |
\begin{isamarkuptext}%
|
|
213 |
\begin{matharray}{rcl}
|
|
214 |
\indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
|
|
215 |
\indexdef{}{command}{redo}\hypertarget{command.redo}{\hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
|
|
216 |
\indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
|
|
217 |
\end{matharray}
|
|
218 |
|
|
219 |
The Isabelle/Isar top-level maintains a two-stage history, for
|
|
220 |
theory and proof state transformation. Basically, any command can
|
|
221 |
be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic
|
|
222 |
elements. Its effect may be revoked via \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, unless
|
|
223 |
the corresponding \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}} step has crossed the beginning
|
|
224 |
of a proof or theory. The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts the
|
|
225 |
current history node altogether, discontinuing a proof or even the
|
|
226 |
whole theory. This operation is \emph{not} undo-able.
|
|
227 |
|
|
228 |
\begin{warn}
|
|
229 |
History commands should never be used with user interfaces such as
|
|
230 |
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
|
|
231 |
care of stepping forth and back itself. Interfering by manual
|
|
232 |
\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.redo}{\mbox{\isa{\isacommand{redo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}
|
|
233 |
commands would quickly result in utter confusion.
|
|
234 |
\end{warn}%
|
|
235 |
\end{isamarkuptext}%
|
|
236 |
\isamarkuptrue%
|
|
237 |
%
|
|
238 |
\isamarkupsection{System operations%
|
|
239 |
}
|
|
240 |
\isamarkuptrue%
|
|
241 |
%
|
|
242 |
\begin{isamarkuptext}%
|
|
243 |
\begin{matharray}{rcl}
|
|
244 |
\indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
|
|
245 |
\indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
|
|
246 |
\indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarkeep{\cdot} \\
|
|
247 |
\end{matharray}
|
|
248 |
|
|
249 |
\begin{rail}
|
|
250 |
('cd' | 'use\_thy' | 'update\_thy') name
|
|
251 |
;
|
|
252 |
\end{rail}
|
|
253 |
|
|
254 |
\begin{descr}
|
|
255 |
|
|
256 |
\item [\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path}] changes the current directory
|
|
257 |
of the Isabelle process.
|
|
258 |
|
|
259 |
\item [\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}] prints the current working directory.
|
|
260 |
|
|
261 |
\item [\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A}] preload theory \isa{A}.
|
|
262 |
These system commands are scarcely used when working interactively,
|
|
263 |
since loading of theories is done automatically as required.
|
|
264 |
|
|
265 |
\end{descr}%
|
|
266 |
\end{isamarkuptext}%
|
|
267 |
\isamarkuptrue%
|
|
268 |
%
|
|
269 |
\isadelimtheory
|
|
270 |
%
|
|
271 |
\endisadelimtheory
|
|
272 |
%
|
|
273 |
\isatagtheory
|
|
274 |
\isacommand{end}\isamarkupfalse%
|
|
275 |
%
|
|
276 |
\endisatagtheory
|
|
277 |
{\isafoldtheory}%
|
|
278 |
%
|
|
279 |
\isadelimtheory
|
|
280 |
%
|
|
281 |
\endisadelimtheory
|
|
282 |
\isanewline
|
|
283 |
\end{isabellebody}%
|
|
284 |
%%% Local Variables:
|
|
285 |
%%% mode: latex
|
|
286 |
%%% TeX-master: "root"
|
|
287 |
%%% End:
|