--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarRef/Thy/Misc.thy Tue Jun 03 00:05:06 2008 +0200
@@ -0,0 +1,245 @@
+(* $Id$ *)
+
+theory Misc
+imports Main
+begin
+
+chapter {* Other commands \label{ch:pure-syntax} *}
+
+section {* Diagnostics *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "pr"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ @{command_def "thm"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "term"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "prop"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "typ"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "full_prf"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ \end{matharray}
+
+ These diagnostic commands assist interactive development. Note that
+ @{command undo} does not apply here, the theory or proof
+ configuration is not changed.
+
+ \begin{rail}
+ 'pr' modes? nat? (',' nat)?
+ ;
+ 'thm' modes? thmrefs
+ ;
+ 'term' modes? term
+ ;
+ 'prop' modes? prop
+ ;
+ 'typ' modes? type
+ ;
+ 'prf' modes? thmrefs?
+ ;
+ 'full\_prf' modes? thmrefs?
+ ;
+
+ modes: '(' (name + ) ')'
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "pr"}~@{text "goals, prems"}] prints the current
+ proof state (if present), including the proof context, current facts
+ and goals. The optional limit arguments affect the number of goals
+ and premises to be displayed, which is initially 10 for both.
+ Omitting limit values leaves the current setting unchanged.
+
+ \item [@{command "thm"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}] retrieves
+ theorems from the current theory or proof context. Note that any
+ attributes included in the theorem specifications are applied to a
+ temporary context derived from the current theory or proof; the
+ result is discarded, i.e.\ attributes involved in @{text "a\<^sub>1,
+ \<dots>, a\<^sub>n"} do not have any permanent effect.
+
+ \item [@{command "term"}~@{text t} and @{command "prop"}~@{text \<phi>}]
+ read, type-check and print terms or propositions according to the
+ current theory or proof context; the inferred type of @{text t} is
+ output as well. Note that these commands are also useful in
+ inspecting the current environment of term abbreviations.
+
+ \item [@{command "typ"}~@{text \<tau>}] reads and prints types of the
+ meta-logic according to the current theory or proof context.
+
+ \item [@{command "prf"}] displays the (compact) proof term of the
+ current proof state (if present), or of the given theorems. Note
+ that this requires proof terms to be switched on for the current
+ object logic (see the ``Proof terms'' section of the Isabelle
+ reference manual for information on how to do this).
+
+ \item [@{command "full_prf"}] is like @{command "prf"}, but displays
+ the full proof term, i.e.\ also displays information omitted in the
+ compact proof term, which is denoted by ``@{text _}'' placeholders
+ there.
+
+ \end{descr}
+
+ All of the diagnostic commands above admit a list of @{text modes}
+ to be specified, which is appended to the current print mode (see
+ also \cite{isabelle-ref}). Thus the output behavior may be modified
+ according particular print mode features. For example, @{command
+ "pr"}~@{text "(latex xsymbols symbols)"} would print the current
+ proof state with mathematical symbols and special characters
+ represented in {\LaTeX} source, according to the Isabelle style
+ \cite{isabelle-sys}.
+
+ Note that antiquotations (cf.\ \secref{sec:antiq}) provide a more
+ systematic way to include formal items into the printed text
+ document.
+*}
+
+
+section {* Inspecting the context *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "print_commands"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ @{command_def "print_theory"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_syntax"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_methods"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_attributes"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "find_theorems"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "thm_deps"}@{text "\<^sup>*"} & : & \isarkeep{theory~|~proof} \\
+ @{command_def "print_facts"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
+ @{command_def "print_binds"}@{text "\<^sup>*"} & : & \isarkeep{proof} \\
+ \end{matharray}
+
+ \begin{rail}
+ 'print\_theory' ( '!'?)
+ ;
+
+ 'find\_theorems' (('(' (nat)? ('with\_dups')? ')')?) (criterion *)
+ ;
+ criterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
+ 'simp' ':' term | term)
+ ;
+ 'thm\_deps' thmrefs
+ ;
+ \end{rail}
+
+ These commands print certain parts of the theory and proof context.
+ Note that there are some further ones available, such as for the set
+ of rules declared for simplifications.
+
+ \begin{descr}
+
+ \item [@{command "print_commands"}] prints Isabelle's outer theory
+ syntax, including keywords and command.
+
+ \item [@{command "print_theory"}] prints the main logical content of
+ the theory context; the ``@{text "!"}'' option indicates extra
+ verbosity.
+
+ \item [@{command "print_syntax"}] prints the inner syntax of types
+ and terms, depending on the current context. The output can be very
+ verbose, including grammar tables and syntax translation rules. See
+ \cite[\S7, \S8]{isabelle-ref} for further information on Isabelle's
+ inner syntax.
+
+ \item [@{command "print_methods"}] prints all proof methods
+ available in the current theory context.
+
+ \item [@{command "print_attributes"}] prints all attributes
+ available in the current theory context.
+
+ \item [@{command "print_theorems"}] prints theorems resulting from
+ the last command.
+
+ \item [@{command "find_theorems"}~@{text criteria}] retrieves facts
+ from the theory or proof context matching all of given search
+ criteria. The criterion @{text "name: p"} selects all theorems
+ whose fully qualified name matches pattern @{text p}, which may
+ contain ``@{text "*"}'' wildcards. The criteria @{text intro},
+ @{text elim}, and @{text dest} select theorems that match the
+ current goal as introduction, elimination or destruction rules,
+ respectively. The criterion @{text "simp: t"} selects all rewrite
+ rules whose left-hand side matches the given term. The criterion
+ term @{text t} selects all theorems that contain the pattern @{text
+ t} -- as usual, patterns may contain occurrences of the dummy
+ ``@{text _}'', schematic variables, and type constraints.
+
+ Criteria can be preceded by ``@{text "-"}'' to select theorems that
+ do \emph{not} match. Note that giving the empty list of criteria
+ yields \emph{all} currently known facts. An optional limit for the
+ number of printed facts may be given; the default is 40. By
+ default, duplicates are removed from the search result. Use
+ @{text with_dups} to display duplicates.
+
+ \item [@{command "thm_deps"}~@{text "a\<^sub>1 \<dots> a\<^sub>n"}]
+ visualizes dependencies of facts, using Isabelle's graph browser
+ tool (see also \cite{isabelle-sys}).
+
+ \item [@{command "print_facts"}] prints all local facts of the
+ current context, both named and unnamed ones.
+
+ \item [@{command "print_binds"}] prints all term abbreviations
+ present in the context.
+
+ \end{descr}
+*}
+
+
+section {* History commands \label{sec:history} *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "undo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ @{command_def "redo"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ @{command_def "kill"}^{{ * }{ * }} & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ The Isabelle/Isar top-level maintains a two-stage history, for
+ theory and proof state transformation. Basically, any command can
+ be undone using @{command "undo"}, excluding mere diagnostic
+ elements. Its effect may be revoked via @{command "redo"}, unless
+ the corresponding @{command "undo"} step has crossed the beginning
+ of a proof or theory. The @{command "kill"} command aborts the
+ current history node altogether, discontinuing a proof or even the
+ whole theory. This operation is \emph{not} undo-able.
+
+ \begin{warn}
+ History commands should never be used with user interfaces such as
+ Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
+ care of stepping forth and back itself. Interfering by manual
+ @{command "undo"}, @{command "redo"}, or even @{command "kill"}
+ commands would quickly result in utter confusion.
+ \end{warn}
+*}
+
+
+section {* System commands *}
+
+text {*
+ \begin{matharray}{rcl}
+ @{command_def "cd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ @{command_def "pwd"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ @{command_def "use_thy"}@{text "\<^sup>*"} & : & \isarkeep{\cdot} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('cd' | 'use\_thy' | 'update\_thy') name
+ ;
+ \end{rail}
+
+ \begin{descr}
+
+ \item [@{command "cd"}~@{text path}] changes the current directory
+ of the Isabelle process.
+
+ \item [@{command "pwd"}] prints the current working directory.
+
+ \item [@{command "use_thy"}~@{text A}] preload theory @{text A}.
+ These system commands are scarcely used when working interactively,
+ since loading of theories is done automatically as required.
+
+ \end{descr}
+*}
+
+end