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