theory Misc
imports Base Main
begin
chapter {* Other commands *}
section {* Inspecting the context *}
text {*
\begin{matharray}{rcl}
@{command_def "print_theory"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_methods"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_attributes"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "find_theorems"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "find_consts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "thm_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@{rail \<open>
(@@{command print_theory} | @@{command print_theorems} | @@{command print_facts}) ('!'?)
;
@@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
;
thmcriterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
'solves' | 'simp' ':' @{syntax term} | @{syntax term})
;
@@{command find_consts} (constcriterion * )
;
constcriterion: ('-'?)
('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
;
@@{command thm_deps} @{syntax thmrefs}
;
@@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
\<close>}
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{description}
\item @{command "print_theory"} prints the main logical content of
the background theory; the ``@{text "!"}'' option indicates extra
verbosity.
\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 of the background
theory resulting from the last command; the ``@{text "!"}'' option
indicates extra verbosity.
\item @{command "print_facts"} prints all local facts of the
current context, both named and unnamed ones; the ``@{text "!"}''
option indicates extra verbosity.
\item @{command "print_binds"} prints all term abbreviations
present in the context.
\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 "solves"} returns all rules
that would directly solve the current goal. 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 "find_consts"}~@{text criteria} prints all constants
whose type meets all of the given criteria. The criterion @{text
"strict: ty"} is met by any type that matches the type pattern
@{text ty}. Patterns may contain both the dummy type ``@{text _}''
and sort constraints. The criterion @{text ty} is similar, but it
also matches against subtypes. The criterion @{text "name: p"} and
the prefix ``@{text "-"}'' function as described for @{command
"find_theorems"}.
\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 "unused_thms"}~@{text "A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n"}
displays all theorems that are proved in theories @{text "B\<^sub>1 \<dots> B\<^sub>n"}
or their parents but not in @{text "A\<^sub>1 \<dots> A\<^sub>m"} or their parents and
that are never used.
If @{text n} is @{text 0}, the end of the range of theories
defaults to the current theory. If no range is specified,
only the unused theorems in the current theory are displayed.
\end{description}
*}
section {* System commands *}
text {*
\begin{matharray}{rcl}
@{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
@{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
@{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
\end{matharray}
@{rail \<open>
(@@{command cd} | @@{command use_thy}) @{syntax name}
\<close>}
\begin{description}
\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{description}
%FIXME proper place (!?)
Isabelle file specification may contain path variables (e.g.\
@{verbatim "$ISABELLE_HOME"}) that are expanded accordingly. Note
that @{verbatim "~"} abbreviates @{verbatim "$USER_HOME"}, and
@{verbatim "~~"} abbreviates @{verbatim "$ISABELLE_HOME"}. The
general syntax for path specifications follows POSIX conventions.
*}
end