doc-src/IsarRef/Thy/document/Misc.tex
author wenzelm
Fri Oct 29 11:49:56 2010 +0200 (2010-10-29)
changeset 40255 9ffbc25e1606
parent 39836 a194f39cfcb4
child 40406 313a24b66a8d
permissions -rw-r--r--
eliminated obsolete \_ escapes in rail environments;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Misc}%
     4 %
     5 \isadelimtheory
     6 %
     7 \endisadelimtheory
     8 %
     9 \isatagtheory
    10 \isacommand{theory}\isamarkupfalse%
    11 \ Misc\isanewline
    12 \isakeyword{imports}\ Main\isanewline
    13 \isakeyword{begin}%
    14 \endisatagtheory
    15 {\isafoldtheory}%
    16 %
    17 \isadelimtheory
    18 %
    19 \endisadelimtheory
    20 %
    21 \isamarkupchapter{Other commands%
    22 }
    23 \isamarkuptrue%
    24 %
    25 \isamarkupsection{Inspecting the context%
    26 }
    27 \isamarkuptrue%
    28 %
    29 \begin{isamarkuptext}%
    30 \begin{matharray}{rcl}
    31     \indexdef{}{command}{print\_commands}\hypertarget{command.print-commands}{\hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
    32     \indexdef{}{command}{print\_theory}\hypertarget{command.print-theory}{\hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    33     \indexdef{}{command}{print\_methods}\hypertarget{command.print-methods}{\hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    34     \indexdef{}{command}{print\_attributes}\hypertarget{command.print-attributes}{\hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    35     \indexdef{}{command}{print\_theorems}\hypertarget{command.print-theorems}{\hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    36     \indexdef{}{command}{find\_theorems}\hypertarget{command.find-theorems}{\hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    37     \indexdef{}{command}{find\_consts}\hypertarget{command.find-consts}{\hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    38     \indexdef{}{command}{thm\_deps}\hypertarget{command.thm-deps}{\hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    39     \indexdef{}{command}{print\_facts}\hypertarget{command.print-facts}{\hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    40     \indexdef{}{command}{print\_binds}\hypertarget{command.print-binds}{\hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
    41   \end{matharray}
    42 
    43   \begin{rail}
    44     ('print_theory' | 'print_theorems') ('!'?)
    45     ;
    46 
    47     'find_theorems' (('(' (nat)? ('with_dups')? ')')?) (thmcriterion *)
    48     ;
    49     thmcriterion: ('-'?) ('name' ':' nameref | 'intro' | 'elim' | 'dest' |
    50       'solves' | 'simp' ':' term | term)
    51     ;
    52     'find_consts' (constcriterion *)
    53     ;
    54     constcriterion: ('-'?) ('name' ':' nameref | 'strict' ':' type | type)
    55     ;
    56     'thm_deps' thmrefs
    57     ;
    58   \end{rail}
    59 
    60   These commands print certain parts of the theory and proof context.
    61   Note that there are some further ones available, such as for the set
    62   of rules declared for simplifications.
    63 
    64   \begin{description}
    65   
    66   \item \hyperlink{command.print-commands}{\mbox{\isa{\isacommand{print{\isacharunderscore}commands}}}} prints Isabelle's outer theory
    67   syntax, including keywords and command.
    68   
    69   \item \hyperlink{command.print-theory}{\mbox{\isa{\isacommand{print{\isacharunderscore}theory}}}} prints the main logical content of
    70   the theory context; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra
    71   verbosity.
    72 
    73   \item \hyperlink{command.print-methods}{\mbox{\isa{\isacommand{print{\isacharunderscore}methods}}}} prints all proof methods
    74   available in the current theory context.
    75   
    76   \item \hyperlink{command.print-attributes}{\mbox{\isa{\isacommand{print{\isacharunderscore}attributes}}}} prints all attributes
    77   available in the current theory context.
    78   
    79   \item \hyperlink{command.print-theorems}{\mbox{\isa{\isacommand{print{\isacharunderscore}theorems}}}} prints theorems resulting from the
    80   last command; the ``\isa{{\isachardoublequote}{\isacharbang}{\isachardoublequote}}'' option indicates extra verbosity.
    81   
    82   \item \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}~\isa{criteria} retrieves facts
    83   from the theory or proof context matching all of given search
    84   criteria.  The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} selects all theorems
    85   whose fully qualified name matches pattern \isa{p}, which may
    86   contain ``\isa{{\isachardoublequote}{\isacharasterisk}{\isachardoublequote}}'' wildcards.  The criteria \isa{intro},
    87   \isa{elim}, and \isa{dest} select theorems that match the
    88   current goal as introduction, elimination or destruction rules,
    89   respectively.  The criterion \isa{{\isachardoublequote}solves{\isachardoublequote}} returns all rules
    90   that would directly solve the current goal.  The criterion
    91   \isa{{\isachardoublequote}simp{\isacharcolon}\ t{\isachardoublequote}} selects all rewrite rules whose left-hand side
    92   matches the given term.  The criterion term \isa{t} selects all
    93   theorems that contain the pattern \isa{t} -- as usual, patterns
    94   may contain occurrences of the dummy ``\isa{{\isacharunderscore}}'', schematic
    95   variables, and type constraints.
    96   
    97   Criteria can be preceded by ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' to select theorems that
    98   do \emph{not} match. Note that giving the empty list of criteria
    99   yields \emph{all} currently known facts.  An optional limit for the
   100   number of printed facts may be given; the default is 40.  By
   101   default, duplicates are removed from the search result. Use
   102   \isa{with{\isacharunderscore}dups} to display duplicates.
   103 
   104   \item \hyperlink{command.find-consts}{\mbox{\isa{\isacommand{find{\isacharunderscore}consts}}}}~\isa{criteria} prints all constants
   105   whose type meets all of the given criteria. The criterion \isa{{\isachardoublequote}strict{\isacharcolon}\ ty{\isachardoublequote}} is met by any type that matches the type pattern
   106   \isa{ty}.  Patterns may contain both the dummy type ``\isa{{\isacharunderscore}}''
   107   and sort constraints. The criterion \isa{ty} is similar, but it
   108   also matches against subtypes. The criterion \isa{{\isachardoublequote}name{\isacharcolon}\ p{\isachardoublequote}} and
   109   the prefix ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' function as described for \hyperlink{command.find-theorems}{\mbox{\isa{\isacommand{find{\isacharunderscore}theorems}}}}.
   110 
   111   \item \hyperlink{command.thm-deps}{\mbox{\isa{\isacommand{thm{\isacharunderscore}deps}}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}
   112   visualizes dependencies of facts, using Isabelle's graph browser
   113   tool (see also \cite{isabelle-sys}).
   114   
   115   \item \hyperlink{command.print-facts}{\mbox{\isa{\isacommand{print{\isacharunderscore}facts}}}} prints all local facts of the
   116   current context, both named and unnamed ones.
   117   
   118   \item \hyperlink{command.print-binds}{\mbox{\isa{\isacommand{print{\isacharunderscore}binds}}}} prints all term abbreviations
   119   present in the context.
   120 
   121   \end{description}%
   122 \end{isamarkuptext}%
   123 \isamarkuptrue%
   124 %
   125 \isamarkupsection{History commands \label{sec:history}%
   126 }
   127 \isamarkuptrue%
   128 %
   129 \begin{isamarkuptext}%
   130 \begin{matharray}{rcl}
   131     \indexdef{}{command}{undo}\hypertarget{command.undo}{\hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}}^{{ * }{ * }} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}\ any{\isachardoublequote}} \\
   132     \indexdef{}{command}{linear\_undo}\hypertarget{command.linear-undo}{\hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}}}^{{ * }{ * }} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}\ any{\isachardoublequote}} \\
   133     \indexdef{}{command}{kill}\hypertarget{command.kill}{\hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}}}^{{ * }{ * }} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}\ any{\isachardoublequote}} \\
   134   \end{matharray}
   135 
   136   The Isabelle/Isar top-level maintains a two-stage history, for
   137   theory and proof state transformation.  Basically, any command can
   138   be undone using \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, excluding mere diagnostic
   139   elements.  Note that a theorem statement with a \emph{finished}
   140   proof is treated as a single unit by \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}.  In
   141   contrast, the variant \hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}} admits to step back
   142   into the middle of a proof.  The \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} command aborts
   143   the current history node altogether, discontinuing a proof or even
   144   the whole theory.  This operation is \emph{not} undo-able.
   145 
   146   \begin{warn}
   147     History commands should never be used with user interfaces such as
   148     Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes
   149     care of stepping forth and back itself.  Interfering by manual
   150     \hyperlink{command.undo}{\mbox{\isa{\isacommand{undo}}}}, \hyperlink{command.linear-undo}{\mbox{\isa{\isacommand{linear{\isacharunderscore}undo}}}}, or even \hyperlink{command.kill}{\mbox{\isa{\isacommand{kill}}}} commands would quickly result in utter confusion.
   151   \end{warn}%
   152 \end{isamarkuptext}%
   153 \isamarkuptrue%
   154 %
   155 \isamarkupsection{System commands%
   156 }
   157 \isamarkuptrue%
   158 %
   159 \begin{isamarkuptext}%
   160 \begin{matharray}{rcl}
   161     \indexdef{}{command}{cd}\hypertarget{command.cd}{\hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   162     \indexdef{}{command}{pwd}\hypertarget{command.pwd}{\hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   163     \indexdef{}{command}{use\_thy}\hypertarget{command.use-thy}{\hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
   164   \end{matharray}
   165 
   166   \begin{rail}
   167     ('cd' | 'use_thy') name
   168     ;
   169   \end{rail}
   170 
   171   \begin{description}
   172 
   173   \item \hyperlink{command.cd}{\mbox{\isa{\isacommand{cd}}}}~\isa{path} changes the current directory
   174   of the Isabelle process.
   175 
   176   \item \hyperlink{command.pwd}{\mbox{\isa{\isacommand{pwd}}}} prints the current working directory.
   177 
   178   \item \hyperlink{command.use-thy}{\mbox{\isa{\isacommand{use{\isacharunderscore}thy}}}}~\isa{A} preload theory \isa{A}.
   179   These system commands are scarcely used when working interactively,
   180   since loading of theories is done automatically as required.
   181 
   182   \end{description}
   183 
   184   %FIXME proper place (!?)
   185   Isabelle file specification may contain path variables (e.g.\
   186   \verb|$ISABELLE_HOME|) that are expanded accordingly.  Note
   187   that \verb|~| abbreviates \verb|$HOME|, and \verb|~~| abbreviates \verb|$ISABELLE_HOME|.  The general syntax
   188   for path specifications follows POSIX conventions.%
   189 \end{isamarkuptext}%
   190 \isamarkuptrue%
   191 %
   192 \isadelimtheory
   193 %
   194 \endisadelimtheory
   195 %
   196 \isatagtheory
   197 \isacommand{end}\isamarkupfalse%
   198 %
   199 \endisatagtheory
   200 {\isafoldtheory}%
   201 %
   202 \isadelimtheory
   203 %
   204 \endisadelimtheory
   205 \isanewline
   206 \end{isabellebody}%
   207 %%% Local Variables:
   208 %%% mode: latex
   209 %%% TeX-master: "root"
   210 %%% End: