7 chapter {* Other commands \label{ch:pure-syntax} *}
9 section {* Diagnostics *}
12 \begin{matharray}{rcl}
13 @{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
14 @{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
15 @{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
16 @{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
17 @{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
18 @{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
19 @{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
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.
27 'pr' modes? nat? (',' nat)?
39 'full\_prf' modes? thmrefs?
42 modes: '(' (name + ) ')'
48 \item @{command "pr"}~@{text "goals, prems"} prints the current
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.
54 \item @{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"} retrieves
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.
61 \item @{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}
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.
67 \item @{command "typ"}~@{text \<tau>} reads and prints types of the
68 meta-logic according to the current theory or proof context.
70 \item @{command "prf"} displays the (compact) proof term of the
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).
76 \item @{command "full_prf"} is like @{command "prf"}, but displays
77 the full proof term, i.e.\ also displays information omitted in the
78 compact proof term, which is denoted by ``@{text _}'' placeholders
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
92 Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
93 systematic way to include formal items into the printed text
98 section {* Inspecting the context *}
101 \begin{matharray}{rcl}
102 @{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
103 @{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
104 @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
105 @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
106 @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
107 @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
108 @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
109 @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
110 @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
111 @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
115 'print\_theory' ( '!'?)
118 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
120 criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
121 'simp' ':' term | term)
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.
133 \item @{command "print_commands"} prints Isabelle's outer theory
134 syntax, including keywords and command.
136 \item @{command "print_theory"} prints the main logical content of
137 the theory context; the ``@{text "!"}'' option indicates extra
140 \item @{command "print_syntax"} prints the inner syntax of types
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
146 \item @{command "print_methods"} prints all proof methods
147 available in the current theory context.
149 \item @{command "print_attributes"} prints all attributes
150 available in the current theory context.
152 \item @{command "print_theorems"} prints theorems resulting from
155 \item @{command "find_theorems"}~@{text criteria} retrieves facts
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.
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.
175 \item @{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}
176 visualizes dependencies of facts, using Isabelle's graph browser
177 tool (see also \cite{isabelle-sys}).
179 \item @{command "print_facts"} prints all local facts of the
180 current context, both named and unnamed ones.
182 \item @{command "print_binds"} prints all term abbreviations
183 present in the context.
189 section {* History commands \label{sec:history} *}
192 \begin{matharray}{rcl}
193 @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
194 @{command_def "linear_undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
195 @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
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
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.
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
212 @{command "undo"}, @{command "linear_undo"}, or even @{command
213 "kill"} commands would quickly result in utter confusion.
218 section {* System commands *}
221 \begin{matharray}{rcl}
222 @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
223 @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
224 @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
228 ('cd' | 'use\_thy' | 'update\_thy') name
234 \item @{command "cd"}~@{text path} changes the current directory
235 of the Isabelle process.
237 \item @{command "pwd"} prints the current working directory.
239 \item @{command "use_thy"}~@{text A} preload theory @{text A}.
240 These system commands are scarcely used when working interactively,
241 since loading of theories is done automatically as required.