1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/doc-src/IsarRef/Thy/Misc.thy Tue Jun 03 00:05:06 2008 +0200
1.3 @@ -0,0 +1,245 @@
1.4 +(* $Id$ *)
1.5 +
1.6 +theory Misc
1.7 +imports Main
1.8 +begin
1.9 +
1.10 +chapter {* Other commands \label{ch:pure-syntax} *}
1.11 +
1.12 +section {* Diagnostics *}
1.13 +
1.14 +text {*
1.15 + \begin{matharray}{rcl}
1.16 + @{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
1.17 + @{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.18 + @{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.19 + @{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.20 + @{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.21 + @{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.22 + @{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.23 + \end{matharray}
1.24 +
1.25 + These diagnostic commands assist interactive development. Note that
1.26 + @{command undo} does not apply here, the theory or proof
1.27 + configuration is not changed.
1.28 +
1.29 + \begin{rail}
1.30 + 'pr' modes? nat? (',' nat)?
1.31 + ;
1.32 + 'thm' modes? thmrefs
1.33 + ;
1.34 + 'term' modes? term
1.35 + ;
1.36 + 'prop' modes? prop
1.37 + ;
1.38 + 'typ' modes? type
1.39 + ;
1.40 + 'prf' modes? thmrefs?
1.41 + ;
1.42 + 'full\_prf' modes? thmrefs?
1.43 + ;
1.44 +
1.45 + modes: '(' (name + ) ')'
1.46 + ;
1.47 + \end{rail}
1.48 +
1.49 + \begin{descr}
1.50 +
1.51 + \item [@{command "pr"}~@{text "goals, prems"}] prints the current
1.52 + proof state (if present), including the proof context, current facts
1.53 + and goals. The optional limit arguments affect the number of goals
1.54 + and premises to be displayed, which is initially 10 for both.
1.55 + Omitting limit values leaves the current setting unchanged.
1.56 +
1.57 + \item [@{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] retrieves
1.58 + theorems from the current theory or proof context. Note that any
1.59 + attributes included in the theorem specifications are applied to a
1.60 + temporary context derived from the current theory or proof; the
1.61 + result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
1.62 + \<dots>, a\<^sub>n"} do not have any permanent effect.
1.63 +
1.64 + \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}]
1.65 + read, type-check and print terms or propositions according to the
1.66 + current theory or proof context; the inferred type of @{text t} is
1.67 + output as well. Note that these commands are also useful in
1.68 + inspecting the current environment of term abbreviations.
1.69 +
1.70 + \item [@{command "typ"}~@{text \<tau>}] reads and prints types of the
1.71 + meta-logic according to the current theory or proof context.
1.72 +
1.73 + \item [@{command "prf"}] displays the (compact) proof term of the
1.74 + current proof state (if present), or of the given theorems. Note
1.75 + that this requires proof terms to be switched on for the current
1.76 + object logic (see the ``Proof terms'' section of the Isabelle
1.77 + reference manual for information on how to do this).
1.78 +
1.79 + \item [@{command "full_prf"}] is like @{command "prf"}, but displays
1.80 + the full proof term, i.e.\ also displays information omitted in the
1.81 + compact proof term, which is denoted by ``@{text _}'' placeholders
1.82 + there.
1.83 +
1.84 + \end{descr}
1.85 +
1.86 + All of the diagnostic commands above admit a list of @{text modes}
1.87 + to be specified, which is appended to the current print mode (see
1.88 + also \cite{isabelle-ref}). Thus the output behavior may be modified
1.89 + according particular print mode features. For example, @{command
1.90 + "pr"}~@{text "(latex xsymbols symbols)"} would print the current
1.91 + proof state with mathematical symbols and special characters
1.92 + represented in {\LaTeX} source, according to the Isabelle style
1.93 + \cite{isabelle-sys}.
1.94 +
1.95 + Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
1.96 + systematic way to include formal items into the printed text
1.97 + document.
1.98 +*}
1.99 +
1.100 +
1.101 +section {* Inspecting the context *}
1.102 +
1.103 +text {*
1.104 + \begin{matharray}{rcl}
1.105 + @{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
1.106 + @{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.107 + @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.108 + @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.109 + @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.110 + @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.111 + @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.112 + @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
1.113 + @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
1.114 + @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
1.115 + \end{matharray}
1.116 +
1.117 + \begin{rail}
1.118 + 'print\_theory' ( '!'?)
1.119 + ;
1.120 +
1.121 + 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
1.122 + ;
1.123 + criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
1.124 + 'simp' ':' term | term)
1.125 + ;
1.126 + 'thm\_deps' thmrefs
1.127 + ;
1.128 + \end{rail}
1.129 +
1.130 + These commands print certain parts of the theory and proof context.
1.131 + Note that there are some further ones available, such as for the set
1.132 + of rules declared for simplifications.
1.133 +
1.134 + \begin{descr}
1.135 +
1.136 + \item [@{command "print_commands"}] prints Isabelle's outer theory
1.137 + syntax, including keywords and command.
1.138 +
1.139 + \item [@{command "print_theory"}] prints the main logical content of
1.140 + the theory context; the ``@{text "!"}'' option indicates extra
1.141 + verbosity.
1.142 +
1.143 + \item [@{command "print_syntax"}] prints the inner syntax of types
1.144 + and terms, depending on the current context. The output can be very
1.145 + verbose, including grammar tables and syntax translation rules. See
1.146 + \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
1.147 + inner syntax.
1.148 +
1.149 + \item [@{command "print_methods"}] prints all proof methods
1.150 + available in the current theory context.
1.151 +
1.152 + \item [@{command "print_attributes"}] prints all attributes
1.153 + available in the current theory context.
1.154 +
1.155 + \item [@{command "print_theorems"}] prints theorems resulting from
1.156 + the last command.
1.157 +
1.158 + \item [@{command "find_theorems"}~@{text criteria}] retrieves facts
1.159 + from the theory or proof context matching all of given search
1.160 + criteria. The criterion @{text "name: p"} selects all theorems
1.161 + whose fully qualified name matches pattern @{text p}, which may
1.162 + contain ``@{text "*"}'' wildcards. The criteria @{text intro},
1.163 + @{text elim}, and @{text dest} select theorems that match the
1.164 + current goal as introduction, elimination or destruction rules,
1.165 + respectively. The criterion @{text "simp: t"} selects all rewrite
1.166 + rules whose left-hand side matches the given term. The criterion
1.167 + term @{text t} selects all theorems that contain the pattern @{text
1.168 + t} -- as usual, patterns may contain occurrences of the dummy
1.169 + ``@{text _}'', schematic variables, and type constraints.
1.170 +
1.171 + Criteria can be preceded by ``@{text "-"}'' to select theorems that
1.172 + do \emph{not} match. Note that giving the empty list of criteria
1.173 + yields \emph{all} currently known facts. An optional limit for the
1.174 + number of printed facts may be given; the default is 40. By
1.175 + default, duplicates are removed from the search result. Use
1.176 + @{text with_dups} to display duplicates.
1.177 +
1.178 + \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
1.179 + visualizes dependencies of facts, using Isabelle's graph browser
1.180 + tool (see also \cite{isabelle-sys}).
1.181 +
1.182 + \item [@{command "print_facts"}] prints all local facts of the
1.183 + current context, both named and unnamed ones.
1.184 +
1.185 + \item [@{command "print_binds"}] prints all term abbreviations
1.186 + present in the context.
1.187 +
1.188 + \end{descr}
1.189 +*}
1.190 +
1.191 +
1.192 +section {* History commands \label{sec:history} *}
1.193 +
1.194 +text {*
1.195 + \begin{matharray}{rcl}
1.196 + @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1.197 + @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1.198 + @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
1.199 + \end{matharray}
1.200 +
1.201 + The Isabelle/Isar top-level maintains a two-stage history, for
1.202 + theory and proof state transformation. Basically, any command can
1.203 + be undone using @{command "undo"}, excluding mere diagnostic
1.204 + elements. Its effect may be revoked via @{command "redo"}, unless
1.205 + the corresponding @{command "undo"} step has crossed the beginning
1.206 + of a proof or theory. The @{command "kill"} command aborts the
1.207 + current history node altogether, discontinuing a proof or even the
1.208 + whole theory. This operation is \emph{not} undo-able.
1.209 +
1.210 + \begin{warn}
1.211 + History commands should never be used with user interfaces such as
1.212 + Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
1.213 + care of stepping forth and back itself. Interfering by manual
1.214 + @{command "undo"}, @{command "redo"}, or even @{command "kill"}
1.215 + commands would quickly result in utter confusion.
1.216 + \end{warn}
1.217 +*}
1.218 +
1.219 +
1.220 +section {* System commands *}
1.221 +
1.222 +text {*
1.223 + \begin{matharray}{rcl}
1.224 + @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
1.225 + @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
1.226 + @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
1.227 + \end{matharray}
1.228 +
1.229 + \begin{rail}
1.230 + ('cd' | 'use\_thy' | 'update\_thy') name
1.231 + ;
1.232 + \end{rail}
1.233 +
1.234 + \begin{descr}
1.235 +
1.236 + \item [@{command "cd"}~@{text path}] changes the current directory
1.237 + of the Isabelle process.
1.238 +
1.239 + \item [@{command "pwd"}] prints the current working directory.
1.240 +
1.241 + \item [@{command "use_thy"}~@{text A}] preload theory @{text A}.
1.242 + These system commands are scarcely used when working interactively,
1.243 + since loading of theories is done automatically as required.
1.244 +
1.245 + \end{descr}
1.246 +*}
1.247 +
1.248 +end