author | wenzelm |
Thu, 13 Nov 2008 21:45:40 +0100 | |
changeset 28761 | 9ec4482c9201 |
parent 28760 | cbc435f7b16b |
child 28762 | f5d79aeffd81 |
permissions | -rw-r--r-- |
27056 | 1 |
(* $Id$ *) |
2 |
||
3 |
theory Misc |
|
4 |
imports Main |
|
5 |
begin |
|
6 |
||
7 |
chapter {* Other commands \label{ch:pure-syntax} *} |
|
8 |
||
9 |
section {* Diagnostics *} |
|
10 |
||
11 |
text {* |
|
12 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
13 |
@{command_def "pr"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
14 |
@{command_def "thm"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
15 |
@{command_def "term"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
16 |
@{command_def "prop"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
17 |
@{command_def "typ"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
18 |
@{command_def "prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
19 |
@{command_def "full_prf"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
27056 | 20 |
\end{matharray} |
21 |
||
22 |
These diagnostic commands assist interactive development. Note that |
|
23 |
@{command undo} does not apply here, the theory or proof |
|
24 |
configuration is not changed. |
|
25 |
||
26 |
\begin{rail} |
|
27 |
'pr' modes? nat? (',' nat)? |
|
28 |
; |
|
29 |
'thm' modes? thmrefs |
|
30 |
; |
|
31 |
'term' modes? term |
|
32 |
; |
|
33 |
'prop' modes? prop |
|
34 |
; |
|
35 |
'typ' modes? type |
|
36 |
; |
|
37 |
'prf' modes? thmrefs? |
|
38 |
; |
|
39 |
'full\_prf' modes? thmrefs? |
|
40 |
; |
|
41 |
||
42 |
modes: '(' (name + ) ')' |
|
43 |
; |
|
44 |
\end{rail} |
|
45 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
46 |
\begin{description} |
27056 | 47 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
48 |
\item @{command "pr"}~@{text "goals, prems"} prints the current |
27056 | 49 |
proof state (if present), including the proof context, current facts |
50 |
and goals. The optional limit arguments affect the number of goals |
|
51 |
and premises to be displayed, which is initially 10 for both. |
|
52 |
Omitting limit values leaves the current setting unchanged. |
|
53 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
54 |
\item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves |
27056 | 55 |
theorems from the current theory or proof context. Note that any |
56 |
attributes included in the theorem specifications are applied to a |
|
57 |
temporary context derived from the current theory or proof; the |
|
58 |
result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1, |
|
59 |
\<dots>, a\<^sub>n"} do not have any permanent effect. |
|
60 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
61 |
\item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>} |
27056 | 62 |
read, type-check and print terms or propositions according to the |
63 |
current theory or proof context; the inferred type of @{text t} is |
|
64 |
output as well. Note that these commands are also useful in |
|
65 |
inspecting the current environment of term abbreviations. |
|
66 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
67 |
\item @{command "typ"}~@{text \<tau>} reads and prints types of the |
27056 | 68 |
meta-logic according to the current theory or proof context. |
69 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
70 |
\item @{command "prf"} displays the (compact) proof term of the |
27056 | 71 |
current proof state (if present), or of the given theorems. Note |
72 |
that this requires proof terms to be switched on for the current |
|
73 |
object logic (see the ``Proof terms'' section of the Isabelle |
|
74 |
reference manual for information on how to do this). |
|
75 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
76 |
\item @{command "full_prf"} is like @{command "prf"}, but displays |
27056 | 77 |
the full proof term, i.e.\ also displays information omitted in the |
78 |
compact proof term, which is denoted by ``@{text _}'' placeholders |
|
79 |
there. |
|
80 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
81 |
\end{description} |
27056 | 82 |
|
83 |
All of the diagnostic commands above admit a list of @{text modes} |
|
84 |
to be specified, which is appended to the current print mode (see |
|
85 |
also \cite{isabelle-ref}). Thus the output behavior may be modified |
|
86 |
according particular print mode features. For example, @{command |
|
87 |
"pr"}~@{text "(latex xsymbols symbols)"} would print the current |
|
88 |
proof state with mathematical symbols and special characters |
|
89 |
represented in {\LaTeX} source, according to the Isabelle style |
|
90 |
\cite{isabelle-sys}. |
|
91 |
||
92 |
Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more |
|
93 |
systematic way to include formal items into the printed text |
|
94 |
document. |
|
95 |
*} |
|
96 |
||
97 |
||
98 |
section {* Inspecting the context *} |
|
99 |
||
100 |
text {* |
|
101 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
102 |
@{command_def "print_commands"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
103 |
@{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
104 |
@{command_def "print_syntax"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
105 |
@{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
106 |
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
107 |
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
108 |
@{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
109 |
@{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
110 |
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
111 |
@{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\ |
27056 | 112 |
\end{matharray} |
113 |
||
114 |
\begin{rail} |
|
115 |
'print\_theory' ( '!'?) |
|
116 |
; |
|
117 |
||
118 |
'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *) |
|
119 |
; |
|
120 |
criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' | |
|
121 |
'simp' ':' term | term) |
|
122 |
; |
|
123 |
'thm\_deps' thmrefs |
|
124 |
; |
|
125 |
\end{rail} |
|
126 |
||
127 |
These commands print certain parts of the theory and proof context. |
|
128 |
Note that there are some further ones available, such as for the set |
|
129 |
of rules declared for simplifications. |
|
130 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
131 |
\begin{description} |
27056 | 132 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
133 |
\item @{command "print_commands"} prints Isabelle's outer theory |
27056 | 134 |
syntax, including keywords and command. |
135 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
136 |
\item @{command "print_theory"} prints the main logical content of |
27056 | 137 |
the theory context; the ``@{text "!"}'' option indicates extra |
138 |
verbosity. |
|
139 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
140 |
\item @{command "print_syntax"} prints the inner syntax of types |
27056 | 141 |
and terms, depending on the current context. The output can be very |
142 |
verbose, including grammar tables and syntax translation rules. See |
|
143 |
\cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's |
|
144 |
inner syntax. |
|
145 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
146 |
\item @{command "print_methods"} prints all proof methods |
27056 | 147 |
available in the current theory context. |
148 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
149 |
\item @{command "print_attributes"} prints all attributes |
27056 | 150 |
available in the current theory context. |
151 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
152 |
\item @{command "print_theorems"} prints theorems resulting from |
27056 | 153 |
the last command. |
154 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
155 |
\item @{command "find_theorems"}~@{text criteria} retrieves facts |
27056 | 156 |
from the theory or proof context matching all of given search |
157 |
criteria. The criterion @{text "name: p"} selects all theorems |
|
158 |
whose fully qualified name matches pattern @{text p}, which may |
|
159 |
contain ``@{text "*"}'' wildcards. The criteria @{text intro}, |
|
160 |
@{text elim}, and @{text dest} select theorems that match the |
|
161 |
current goal as introduction, elimination or destruction rules, |
|
162 |
respectively. The criterion @{text "simp: t"} selects all rewrite |
|
163 |
rules whose left-hand side matches the given term. The criterion |
|
164 |
term @{text t} selects all theorems that contain the pattern @{text |
|
165 |
t} -- as usual, patterns may contain occurrences of the dummy |
|
166 |
``@{text _}'', schematic variables, and type constraints. |
|
167 |
||
168 |
Criteria can be preceded by ``@{text "-"}'' to select theorems that |
|
169 |
do \emph{not} match. Note that giving the empty list of criteria |
|
170 |
yields \emph{all} currently known facts. An optional limit for the |
|
171 |
number of printed facts may be given; the default is 40. By |
|
172 |
default, duplicates are removed from the search result. Use |
|
173 |
@{text with_dups} to display duplicates. |
|
174 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
175 |
\item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} |
27056 | 176 |
visualizes dependencies of facts, using Isabelle's graph browser |
177 |
tool (see also \cite{isabelle-sys}). |
|
178 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
179 |
\item @{command "print_facts"} prints all local facts of the |
27056 | 180 |
current context, both named and unnamed ones. |
181 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
182 |
\item @{command "print_binds"} prints all term abbreviations |
27056 | 183 |
present in the context. |
184 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
185 |
\end{description} |
27056 | 186 |
*} |
187 |
||
188 |
||
189 |
section {* History commands \label{sec:history} *} |
|
190 |
||
191 |
text {* |
|
192 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
193 |
@{command_def "undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
194 |
@{command_def "linear_undo"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
195 |
@{command_def "kill"}^{{ * }{ * }} & : & @{text "any \<rightarrow> any"} \\ |
27056 | 196 |
\end{matharray} |
197 |
||
198 |
The Isabelle/Isar top-level maintains a two-stage history, for |
|
199 |
theory and proof state transformation. Basically, any command can |
|
200 |
be undone using @{command "undo"}, excluding mere diagnostic |
|
27598 | 201 |
elements. Note that a theorem statement with a \emph{finished} |
202 |
proof is treated as a single unit by @{command "undo"}. In |
|
203 |
contrast, the variant @{command "linear_undo"} admits to step back |
|
204 |
into the middle of a proof. The @{command "kill"} command aborts |
|
205 |
the current history node altogether, discontinuing a proof or even |
|
206 |
the whole theory. This operation is \emph{not} undo-able. |
|
27056 | 207 |
|
208 |
\begin{warn} |
|
209 |
History commands should never be used with user interfaces such as |
|
210 |
Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes |
|
211 |
care of stepping forth and back itself. Interfering by manual |
|
27598 | 212 |
@{command "undo"}, @{command "linear_undo"}, or even @{command |
213 |
"kill"} commands would quickly result in utter confusion. |
|
27056 | 214 |
\end{warn} |
215 |
*} |
|
216 |
||
217 |
||
218 |
section {* System commands *} |
|
219 |
||
220 |
text {* |
|
221 |
\begin{matharray}{rcl} |
|
28761
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
222 |
@{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
223 |
@{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
9ec4482c9201
updated/refined types of Isar language elements, removed special LaTeX macros;
wenzelm
parents:
28760
diff
changeset
|
224 |
@{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\ |
27056 | 225 |
\end{matharray} |
226 |
||
227 |
\begin{rail} |
|
228 |
('cd' | 'use\_thy' | 'update\_thy') name |
|
229 |
; |
|
230 |
\end{rail} |
|
231 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
232 |
\begin{description} |
27056 | 233 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
234 |
\item @{command "cd"}~@{text path} changes the current directory |
27056 | 235 |
of the Isabelle process. |
236 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
237 |
\item @{command "pwd"} prints the current working directory. |
27056 | 238 |
|
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
239 |
\item @{command "use_thy"}~@{text A} preload theory @{text A}. |
27056 | 240 |
These system commands are scarcely used when working interactively, |
241 |
since loading of theories is done automatically as required. |
|
242 |
||
28760
cbc435f7b16b
unified use of declaration environment with IsarImplementation;
wenzelm
parents:
27598
diff
changeset
|
243 |
\end{description} |
27056 | 244 |
*} |
245 |
||
246 |
end |