author | wenzelm |
Sat, 28 Feb 2009 17:09:32 +0100 | |
changeset 30172 | afdf7808cfd0 |
parent 29896 | 97ba7a7651de |
child 33515 | d066e8369a33 |
permissions | -rw-r--r-- |
27052 | 1 |
% |
2 |
\begin{isabellebody}% |
|
3 |
\def\isabellecontext{Misc}% |
|
4 |
% |
|
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
\isacommand{theory}\isamarkupfalse% |
|
11 |
\ Misc\isanewline |
|
12 |
\isakeyword{imports}\ Main\isanewline |
|
13 |
\isakeyword{begin}% |
|
14 |
\endisatagtheory |
|
15 |
{\isafoldtheory}% |
|
16 |
% |
|
17 |
\isadelimtheory |
|
18 |
% |
|
19 |
\endisadelimtheory |
|
20 |
% |
|
28788 | 21 |
\isamarkupchapter{Other commands% |
27052 | 22 |
} |
23 |
\isamarkuptrue% |
|
24 |
% |
|
25 |
\isamarkupsection{Inspecting the context% |
|
26 |
} |
|
27 |
\isamarkuptrue% |
|
28 |
% |
|
29 |
\begin{isamarkuptext}% |
|
30 |
\begin{matharray}{rcl} |
|
28788 | 31 |
\indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
32 |
\indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
33 |
\indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
34 |
\indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
35 |
\indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
36 |
\indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
29894 | 37 |
\indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
28788 | 38 |
\indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
39 |
\indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
40 |
\indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
27052 | 41 |
\end{matharray} |
42 |
||
43 |
\begin{rail} |
|
44 |
'print\_theory' ( '!'?) |
|
45 |
; |
|
46 |
||
29894 | 47 |
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (thmcriterion *) |
27052 | 48 |
; |
29894 | 49 |
thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | |
29893
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
50 |
'solves' | 'simp' ':' term | term) |
27052 | 51 |
; |
29896 | 52 |
'find\_consts' (constcriterion *) |
29894 | 53 |
; |
54 |
constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type) |
|
55 |
; |
|
27052 | 56 |
'thm\_deps' thmrefs |
57 |
; |
|
58 |
\end{rail} |
|
59 |
||
60 |
These commands print certain parts of the theory and proof context. |
|
61 |
Note that there are some further ones available, such as for the set |
|
62 |
of rules declared for simplifications. |
|
63 |
||
28788 | 64 |
\begin{description} |
27052 | 65 |
|
28788 | 66 |
\item \hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}} prints Isabelle's outer theory |
27052 | 67 |
syntax, including keywords and command. |
68 |
||
28788 | 69 |
\item \hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}} prints the main logical content of |
27052 | 70 |
the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra |
71 |
verbosity. |
|
72 |
||
28788 | 73 |
\item \hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}} prints all proof methods |
27052 | 74 |
available in the current theory context. |
75 |
||
28788 | 76 |
\item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}} prints all attributes |
27052 | 77 |
available in the current theory context. |
78 |
||
28788 | 79 |
\item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}} prints theorems resulting from |
27052 | 80 |
the last command. |
81 |
||
28788 | 82 |
\item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria} retrieves facts |
27052 | 83 |
from the theory or proof context matching all of given search |
84 |
criteria. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems |
|
85 |
whose fully qualified name matches pattern \isa{p}, which may |
|
86 |
contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards. The criteria \isa{intro}, |
|
87 |
\isa{elim}, and \isa{dest} select theorems that match the |
|
88 |
current goal as introduction, elimination or destruction rules, |
|
29896 | 89 |
respectively. The criterion \isa{{\isachardoublequote}solves{\isachardoublequote}} returns all rules |
29893
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
90 |
that would directly solve the current goal. The criterion |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
91 |
\isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite rules whose left-hand side |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
92 |
matches the given term. The criterion term \isa{t} selects all |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
93 |
theorems that contain the pattern \isa{t} -- as usual, patterns |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
94 |
may contain occurrences of the dummy ``\isa{{\isacharunderscore}}'', schematic |
defab1c6a6b5
FindTheorems solves: update documentation (by Timothy Bourke)
kleing
parents:
28788
diff
changeset
|
95 |
variables, and type constraints. |
27052 | 96 |
|
97 |
Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that |
|
98 |
do \emph{not} match. Note that giving the empty list of criteria |
|
99 |
yields \emph{all} currently known facts. An optional limit for the |
|
100 |
number of printed facts may be given; the default is 40. By |
|
101 |
default, duplicates are removed from the search result. Use |
|
102 |
\isa{with{\isacharunderscore}dups} to display duplicates. |
|
29894 | 103 |
|
104 |
\item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}~\isa{criteria} prints all constants |
|
105 |
whose type meets all of the given criteria. The criterion \isa{{\isachardoublequote}strict{\isacharcolon}\ ty{\isachardoublequote}} is met by any type that matches the type pattern |
|
106 |
\isa{ty}. Patterns may contain both the dummy type ``\isa{{\isacharunderscore}}'' |
|
107 |
and sort constraints. The criterion \isa{ty} is similar, but it |
|
108 |
also matches against subtypes. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} and |
|
109 |
the prefix ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}. |
|
110 |
||
28788 | 111 |
\item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}} |
27052 | 112 |
visualizes dependencies of facts, using Isabelle's graph browser |
113 |
tool (see also \cite{isabelle-sys}). |
|
114 |
||
28788 | 115 |
\item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}} prints all local facts of the |
27052 | 116 |
current context, both named and unnamed ones. |
117 |
||
28788 | 118 |
\item \hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}} prints all term abbreviations |
27052 | 119 |
present in the context. |
120 |
||
28788 | 121 |
\end{description}% |
27052 | 122 |
\end{isamarkuptext}% |
123 |
\isamarkuptrue% |
|
124 |
% |
|
125 |
\isamarkupsection{History commands \label{sec:history}% |
|
126 |
} |
|
127 |
\isamarkuptrue% |
|
128 |
% |
|
129 |
\begin{isamarkuptext}% |
|
130 |
\begin{matharray}{rcl} |
|
28788 | 131 |
\indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}\ any{\isachardoublequote}} \\ |
132 |
\indexdef{}{command}{linear\_undo}\hypertarget{command.linear-undo}{\hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}}}^{{ * }{ * }} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}\ any{\isachardoublequote}} \\ |
|
133 |
\indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}\ any{\isachardoublequote}} \\ |
|
27052 | 134 |
\end{matharray} |
135 |
||
136 |
The Isabelle/Isar top-level maintains a two-stage history, for |
|
137 |
theory and proof state transformation. Basically, any command can |
|
138 |
be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic |
|
27598 | 139 |
elements. Note that a theorem statement with a \emph{finished} |
140 |
proof is treated as a single unit by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}. In |
|
141 |
contrast, the variant \hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}} admits to step back |
|
142 |
into the middle of a proof. The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts |
|
143 |
the current history node altogether, discontinuing a proof or even |
|
144 |
the whole theory. This operation is \emph{not} undo-able. |
|
27052 | 145 |
|
146 |
\begin{warn} |
|
147 |
History commands should never be used with user interfaces such as |
|
148 |
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes |
|
149 |
care of stepping forth and back itself. Interfering by manual |
|
27598 | 150 |
\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} commands would quickly result in utter confusion. |
27052 | 151 |
\end{warn}% |
152 |
\end{isamarkuptext}% |
|
153 |
\isamarkuptrue% |
|
154 |
% |
|
27054 | 155 |
\isamarkupsection{System commands% |
27052 | 156 |
} |
157 |
\isamarkuptrue% |
|
158 |
% |
|
159 |
\begin{isamarkuptext}% |
|
160 |
\begin{matharray}{rcl} |
|
28788 | 161 |
\indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
162 |
\indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
163 |
\indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\ |
|
27052 | 164 |
\end{matharray} |
165 |
||
166 |
\begin{rail} |
|
167 |
('cd' | 'use\_thy' | 'update\_thy') name |
|
168 |
; |
|
169 |
\end{rail} |
|
170 |
||
28788 | 171 |
\begin{description} |
27052 | 172 |
|
28788 | 173 |
\item \hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path} changes the current directory |
27052 | 174 |
of the Isabelle process. |
175 |
||
28788 | 176 |
\item \hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}} prints the current working directory. |
27052 | 177 |
|
28788 | 178 |
\item \hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A} preload theory \isa{A}. |
27052 | 179 |
These system commands are scarcely used when working interactively, |
180 |
since loading of theories is done automatically as required. |
|
181 |
||
28788 | 182 |
\end{description}% |
27052 | 183 |
\end{isamarkuptext}% |
184 |
\isamarkuptrue% |
|
185 |
% |
|
186 |
\isadelimtheory |
|
187 |
% |
|
188 |
\endisadelimtheory |
|
189 |
% |
|
190 |
\isatagtheory |
|
191 |
\isacommand{end}\isamarkupfalse% |
|
192 |
% |
|
193 |
\endisatagtheory |
|
194 |
{\isafoldtheory}% |
|
195 |
% |
|
196 |
\isadelimtheory |
|
197 |
% |
|
198 |
\endisadelimtheory |
|
199 |
\isanewline |
|
200 |
\end{isabellebody}% |
|
201 |
%%% Local Variables: |
|
202 |
%%% mode: latex |
|
203 |
%%% TeX-master: "root" |
|
204 |
%%% End: |