doc-src/IsarRef/Thy/document/Misc.tex

Typo fixed.

%
\begin{isabellebody}%
\def\isabellecontext{Misc}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{theory}\isamarkupfalse%
\ Misc\isanewline
\isakeyword{imports}\ Base\ Main\isanewline
\isakeyword{begin}%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
%
\isamarkupchapter{Other commands%
}
\isamarkuptrue%
%
\isamarkupsection{Inspecting the context%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
    \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}commands}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}methods}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}attributes}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{unused\_thms}\hypertarget{command.unused-thms}{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
  \end{matharray}

  \begin{railoutput}
\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}}}[]
\rail@nextbar{1}
\rail@term{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{21}{\isacharbang}}}}[]
\rail@endbar
\rail@end
\rail@begin{6}{}
\rail@term{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{28}{\isacharparenleft}}}}[]
\rail@bar
\rail@nextbar{2}
\rail@nont{\hyperlink{syntax.nat}{\mbox{\isa{nat}}}}[]
\rail@endbar
\rail@bar
\rail@nextbar{2}
\rail@term{\isa{with{\isaliteral{5F}{\isacharunderscore}}dups}}[]
\rail@endbar
\rail@term{\isa{{\isaliteral{29}{\isacharparenright}}}}[]
\rail@endbar
\rail@cr{4}
\rail@plus
\rail@nextplus{5}
\rail@cnont{\isa{thmcriterion}}[]
\rail@endplus
\rail@end
\rail@begin{7}{\isa{thmcriterion}}
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
\rail@endbar
\rail@bar
\rail@term{\isa{name}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@nextbar{1}
\rail@term{\isa{intro}}[]
\rail@nextbar{2}
\rail@term{\isa{elim}}[]
\rail@nextbar{3}
\rail@term{\isa{dest}}[]
\rail@nextbar{4}
\rail@term{\isa{solves}}[]
\rail@nextbar{5}
\rail@term{\isa{simp}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{6}
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@endbar
\rail@end
\rail@begin{2}{}
\rail@term{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}}[]
\rail@plus
\rail@nextplus{1}
\rail@cnont{\isa{constcriterion}}[]
\rail@endplus
\rail@end
\rail@begin{3}{\isa{constcriterion}}
\rail@bar
\rail@nextbar{1}
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
\rail@endbar
\rail@bar
\rail@term{\isa{name}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
\rail@nextbar{1}
\rail@term{\isa{strict}}[]
\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}}}[]
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
\rail@nextbar{2}
\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
\rail@endbar
\rail@end
\rail@begin{1}{}
\rail@term{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}}[]
\rail@nont{\hyperlink{syntax.thmrefs}{\mbox{\isa{thmrefs}}}}[]
\rail@end
\rail@begin{3}{}
\rail@term{\hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@nextplus{2}
\rail@endplus
\rail@term{\isa{{\isaliteral{2D}{\isacharminus}}}}[]
\rail@plus
\rail@nextplus{2}
\rail@cnont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@endplus
\rail@endbar
\rail@end
\end{railoutput}


  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 \hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}commands}}}} prints Isabelle's outer theory
  syntax, including keywords and command.
  
  \item \hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theory}}}} prints the main logical content of
  the theory context; the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' option indicates extra
  verbosity.

  \item \hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}methods}}}} prints all proof methods
  available in the current theory context.
  
  \item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}attributes}}}} prints all attributes
  available in the current theory context.
  
  \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}theorems}}}} prints theorems resulting from the
  last command; the ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{21}{\isacharbang}}{\isaliteral{22}{\isachardoublequote}}}'' option indicates extra verbosity.
  
  \item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}~\isa{criteria} retrieves facts
  from the theory or proof context matching all of given search
  criteria.  The criterion \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ p{\isaliteral{22}{\isachardoublequote}}} selects all theorems
  whose fully qualified name matches pattern \isa{p}, which may
  contain ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}'' wildcards.  The criteria \isa{intro},
  \isa{elim}, and \isa{dest} select theorems that match the
  current goal as introduction, elimination or destruction rules,
  respectively.  The criterion \isa{{\isaliteral{22}{\isachardoublequote}}solves{\isaliteral{22}{\isachardoublequote}}} returns all rules
  that would directly solve the current goal.  The criterion
  \isa{{\isaliteral{22}{\isachardoublequote}}simp{\isaliteral{3A}{\isacharcolon}}\ t{\isaliteral{22}{\isachardoublequote}}} selects all rewrite rules whose left-hand side
  matches the given term.  The criterion term \isa{t} selects all
  theorems that contain the pattern \isa{t} -- as usual, patterns
  may contain occurrences of the dummy ``\isa{{\isaliteral{5F}{\isacharunderscore}}}'', schematic
  variables, and type constraints.
  
  Criteria can be preceded by ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' 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
  \isa{with{\isaliteral{5F}{\isacharunderscore}}dups} to display duplicates.

  \item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}consts}}}}~\isa{criteria} prints all constants
  whose type meets all of the given criteria. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}strict{\isaliteral{3A}{\isacharcolon}}\ ty{\isaliteral{22}{\isachardoublequote}}} is met by any type that matches the type pattern
  \isa{ty}.  Patterns may contain both the dummy type ``\isa{{\isaliteral{5F}{\isacharunderscore}}}''
  and sort constraints. The criterion \isa{ty} is similar, but it
  also matches against subtypes. The criterion \isa{{\isaliteral{22}{\isachardoublequote}}name{\isaliteral{3A}{\isacharcolon}}\ p{\isaliteral{22}{\isachardoublequote}}} and
  the prefix ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isaliteral{5F}{\isacharunderscore}}theorems}}}}.

  \item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isaliteral{5F}{\isacharunderscore}}deps}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}a\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ a\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{22}{\isachardoublequote}}}
  visualizes dependencies of facts, using Isabelle's graph browser
  tool (see also \cite{isabelle-sys}).

  \item \hyperlink{command.unused-thms}{\mbox{\isa{\isacommand{unused{\isaliteral{5F}{\isacharunderscore}}thms}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m\ {\isaliteral{2D}{\isacharminus}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}
  displays all unused theorems in theories \isa{{\isaliteral{22}{\isachardoublequote}}B\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ B\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{22}{\isachardoublequote}}}
  or their parents, but not in \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub m{\isaliteral{22}{\isachardoublequote}}} or their parents.
  If \isa{n} is \isa{{\isadigit{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.
  
  \item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}facts}}}} prints all local facts of the
  current context, both named and unnamed ones.
  
  \item \hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isaliteral{5F}{\isacharunderscore}}binds}}}} prints all term abbreviations
  present in the context.

  \end{description}%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isamarkupsection{System commands%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
\begin{matharray}{rcl}
    \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
    \indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}}\isa{{\isaliteral{22}{\isachardoublequote}}\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}any\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}{\isaliteral{22}{\isachardoublequote}}} \\
  \end{matharray}

  \begin{railoutput}
\rail@begin{2}{}
\rail@bar
\rail@term{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}[]
\rail@nextbar{1}
\rail@term{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}}[]
\rail@endbar
\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
\rail@end
\end{railoutput}


  \begin{description}

  \item \hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path} changes the current directory
  of the Isabelle process.

  \item \hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}} prints the current working directory.

  \item \hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isaliteral{5F}{\isacharunderscore}}thy}}}}~\isa{A} preload theory \isa{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.\
  \verb|$ISABELLE_HOME|) that are expanded accordingly.  Note
  that \verb|~| abbreviates \verb|$USER_HOME|, and
  \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The
  general syntax for path specifications follows POSIX conventions.%
\end{isamarkuptext}%
\isamarkuptrue%
%
\isadelimtheory
%
\endisadelimtheory
%
\isatagtheory
\isacommand{end}\isamarkupfalse%
%
\endisatagtheory
{\isafoldtheory}%
%
\isadelimtheory
%
\endisadelimtheory
\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: