doc-src/IsarRef/pure.tex
author ballarin
Wed Dec 10 14:27:50 2003 +0100 (2003-12-10)
changeset 14285 92ed032e83a1
parent 14212 cd05b503ca2d
child 14642 2bfe5de2d1fa
permissions -rw-r--r--
Isar: where attribute supports instantiation of type vars.
     1 
     2 \chapter{Basic language elements}\label{ch:pure-syntax}
     3 
     4 Subsequently, we introduce the main part of Pure theory and proof commands,
     5 together with fundamental proof methods and attributes.
     6 Chapter~\ref{ch:gen-tools} describes further Isar elements provided by generic
     7 tools and packages (such as the Simplifier) that are either part of Pure
     8 Isabelle or pre-installed in most object logics.  Chapter~\ref{ch:logics}
     9 refers to object-logic specific elements (mainly for HOL and ZF).
    10 
    11 \medskip
    12 
    13 Isar commands may be either \emph{proper} document constructors, or
    14 \emph{improper commands}.  Some proof methods and attributes introduced later
    15 are classified as improper as well.  Improper Isar language elements, which
    16 are subsequently marked by ``$^*$'', are often helpful when developing proof
    17 documents, while their use is discouraged for the final human-readable
    18 outcome.  Typical examples are diagnostic commands that print terms or
    19 theorems according to the current context; other commands emulate old-style
    20 tactical theorem proving.
    21 
    22 
    23 \section{Theory commands}
    24 
    25 \subsection{Defining theories}\label{sec:begin-thy}
    26 
    27 \indexisarcmd{header}\indexisarcmd{theory}\indexisarcmd{context}\indexisarcmd{end}
    28 \begin{matharray}{rcl}
    29   \isarcmd{header} & : & \isarkeep{toplevel} \\
    30   \isarcmd{theory} & : & \isartrans{toplevel}{theory} \\
    31   \isarcmd{context}^* & : & \isartrans{toplevel}{theory} \\
    32   \isarcmd{end} & : & \isartrans{theory}{toplevel} \\
    33 \end{matharray}
    34 
    35 Isabelle/Isar ``new-style'' theories are either defined via theory files or
    36 interactively.  Both theory-level specifications and proofs are handled
    37 uniformly --- occasionally definitional mechanisms even require some explicit
    38 proof as well.  In contrast, ``old-style'' Isabelle theories support batch
    39 processing only, with the proof scripts collected in separate ML files.
    40 
    41 The first ``real'' command of any theory has to be $\THEORY$, which starts a
    42 new theory based on the merge of existing ones.  Just preceding $\THEORY$,
    43 there may be an optional $\isarkeyword{header}$ declaration, which is relevant
    44 to document preparation only; it acts very much like a special pre-theory
    45 markup command (cf.\ \S\ref{sec:markup-thy} and \S\ref{sec:markup-thy}).  The
    46 $\END$ command concludes a theory development; it has to be the very last
    47 command of any theory file loaded in batch-mode.  The theory context may be
    48 also changed interactively by $\CONTEXT$ without creating a new theory.
    49 
    50 \begin{rail}
    51   'header' text
    52   ;
    53   'theory' name '=' (name + '+') filespecs? ':'
    54   ;
    55   'context' name
    56   ;
    57 
    58   filespecs: 'files' ((name | parname) +);
    59 \end{rail}
    60 
    61 \begin{descr}
    62 \item [$\isarkeyword{header}~text$] provides plain text markup just preceding
    63   the formal beginning of a theory.  In actual document preparation the
    64   corresponding {\LaTeX} macro \verb,\isamarkupheader, may be redefined to
    65   produce chapter or section headings.  See also \S\ref{sec:markup-thy} and
    66   \S\ref{sec:markup-prf} for further markup commands.
    67   
    68 \item [$\THEORY~A = B@1 + \cdots + B@n\colon$] starts a new theory $A$ based
    69   on the merge of existing theories $B@1, \dots, B@n$.
    70   
    71   Due to inclusion of several ancestors, the overall theory structure emerging
    72   in an Isabelle session forms a directed acyclic graph (DAG).  Isabelle's
    73   theory loader ensures that the sources contributing to the development graph
    74   are always up-to-date.  Changed files are automatically reloaded when
    75   processing theory headers interactively; batch-mode explicitly distinguishes
    76   \verb,update_thy, from \verb,use_thy,, see also \cite{isabelle-ref}.
    77   
    78   The optional $\isarkeyword{files}$ specification declares additional
    79   dependencies on ML files.  Files will be loaded immediately, unless the name
    80   is put in parentheses, which merely documents the dependency to be resolved
    81   later in the text (typically via explicit $\isarcmd{use}$ in the body text,
    82   see \S\ref{sec:ML}).  In reminiscence of the old-style theory system of
    83   Isabelle, \texttt{$A$.thy} may be also accompanied by an additional file
    84   \texttt{$A$.ML} consisting of ML code that is executed in the context of the
    85   \emph{finished} theory $A$.  That file should not be included in the
    86   $\isarkeyword{files}$ dependency declaration, though.
    87   
    88 \item [$\CONTEXT~B$] enters an existing theory context, basically in read-only
    89   mode, so only a limited set of commands may be performed without destroying
    90   the theory.  Just as for $\THEORY$, the theory loader ensures that $B$ is
    91   loaded and up-to-date.
    92   
    93   This command is occasionally useful for quick interactive experiments;
    94   normally one should always commence a new context via $\THEORY$.
    95   
    96 \item [$\END$] concludes the current theory definition or context switch.
    97   Note that this command cannot be undone, but the whole theory definition has
    98   to be retracted.
    99 
   100 \end{descr}
   101 
   102 
   103 \subsection{Markup commands}\label{sec:markup-thy}
   104 
   105 \indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
   106 \indexisarcmd{subsubsection}\indexisarcmd{text}\indexisarcmd{text-raw}
   107 \begin{matharray}{rcl}
   108   \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
   109   \isarcmd{section} & : & \isartrans{theory}{theory} \\
   110   \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
   111   \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
   112   \isarcmd{text} & : & \isartrans{theory}{theory} \\
   113   \isarcmd{text_raw} & : & \isartrans{theory}{theory} \\
   114 \end{matharray}
   115 
   116 Apart from formal comments (see \S\ref{sec:comments}), markup commands provide
   117 a structured way to insert text into the document generated from a theory (see
   118 \cite{isabelle-sys} for more information on Isabelle's document preparation
   119 tools).
   120 
   121 \railalias{textraw}{text\_raw}
   122 \railterm{textraw}
   123 
   124 \begin{rail}
   125   ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text' | textraw) text
   126   ;
   127 \end{rail}
   128 
   129 \begin{descr}
   130 \item [$\isarkeyword{chapter}$, $\isarkeyword{section}$,
   131   $\isarkeyword{subsection}$, and $\isarkeyword{subsubsection}$] mark chapter
   132   and section headings.
   133 \item [$\TEXT$] specifies paragraphs of plain text, including references to
   134   formal entities (see also \S\ref{sec:antiq} on ``antiquotations'').
   135 \item [$\isarkeyword{text_raw}$] inserts {\LaTeX} source into the output,
   136   without additional markup.  Thus the full range of document manipulations
   137   becomes available.
   138 \end{descr}
   139 
   140 Any of these markup elements corresponds to a {\LaTeX} command with the name
   141 prefixed by \verb,\isamarkup,.  For the sectioning commands this is a plain
   142 macro with a single argument, e.g.\ \verb,\isamarkupchapter{,\dots\verb,}, for
   143 $\isarkeyword{chapter}$.  The $\isarkeyword{text}$ markup results in a
   144 {\LaTeX} environment \verb,\begin{isamarkuptext}, {\dots}
   145   \verb,\end{isamarkuptext},, while $\isarkeyword{text_raw}$ causes the text
   146 to be inserted directly into the {\LaTeX} source.
   147 
   148 \medskip
   149 
   150 Additional markup commands are available for proofs (see
   151 \S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
   152 declaration (see \S\ref{sec:begin-thy}) admits to insert section markup just
   153 preceding the actual theory definition.
   154 
   155 
   156 \subsection{Type classes and sorts}\label{sec:classes}
   157 
   158 \indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
   159 \begin{matharray}{rcll}
   160   \isarcmd{classes} & : & \isartrans{theory}{theory} \\
   161   \isarcmd{classrel} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   162   \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
   163 \end{matharray}
   164 
   165 \begin{rail}
   166   'classes' (classdecl +)
   167   ;
   168   'classrel' nameref ('<' | subseteq) nameref
   169   ;
   170   'defaultsort' sort
   171   ;
   172 \end{rail}
   173 
   174 \begin{descr}
   175 \item [$\isarkeyword{classes}~c \subseteq \vec c$] declares class $c$ to be a
   176   subclass of existing classes $\vec c$.  Cyclic class structures are ruled
   177   out.
   178 \item [$\isarkeyword{classrel}~c@1 \subseteq c@2$] states a subclass relation
   179   between existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
   180   $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a way to introduce
   181   proven class relations.
   182 \item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
   183   any type variables given without sort constraints.  Usually, the default
   184   sort would be only changed when defining a new object-logic.
   185 \end{descr}
   186 
   187 
   188 \subsection{Primitive types and type abbreviations}\label{sec:types-pure}
   189 
   190 \indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
   191 \begin{matharray}{rcll}
   192   \isarcmd{types} & : & \isartrans{theory}{theory} \\
   193   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
   194   \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
   195   \isarcmd{arities} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   196 \end{matharray}
   197 
   198 \begin{rail}
   199   'types' (typespec '=' type infix? +)
   200   ;
   201   'typedecl' typespec infix?
   202   ;
   203   'nonterminals' (name +)
   204   ;
   205   'arities' (nameref '::' arity +)
   206   ;
   207 \end{rail}
   208 
   209 \begin{descr}
   210 
   211 \item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
   212   $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
   213   as are available in Isabelle/HOL for example, type synonyms are just purely
   214   syntactic abbreviations without any logical significance.  Internally, type
   215   synonyms are fully expanded.
   216   
   217 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
   218   $t$, intended as an actual logical type.  Note that the Isabelle/HOL
   219   object-logic overrides $\isarkeyword{typedecl}$ by its own version
   220   (\S\ref{sec:hol-typedef}).
   221 
   222 \item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
   223   $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
   224   Isabelle's inner syntax of terms or types.
   225 
   226 \item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
   227   signature of types by new type constructor arities.  This is done
   228   axiomatically!  The $\INSTANCE$ command (see \S\ref{sec:axclass}) provides a
   229   way to introduce proven type arities.
   230 
   231 \end{descr}
   232 
   233 
   234 \subsection{Constants and simple definitions}\label{sec:consts}
   235 
   236 \indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
   237 \begin{matharray}{rcl}
   238   \isarcmd{consts} & : & \isartrans{theory}{theory} \\
   239   \isarcmd{defs} & : & \isartrans{theory}{theory} \\
   240   \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
   241 \end{matharray}
   242 
   243 \begin{rail}
   244   'consts' (constdecl +)
   245   ;
   246   'defs' ('(overloaded)')? (axmdecl prop +)
   247   ;
   248   'constdefs' (constdecl prop +)
   249   ;
   250 
   251   constdecl: name '::' type mixfix?
   252   ;
   253 \end{rail}
   254 
   255 \begin{descr}
   256 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
   257   scheme $\sigma$.  The optional mixfix annotations may attach concrete syntax
   258   to the constants declared.
   259 
   260 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
   261   existing constant.  See \cite[\S6]{isabelle-ref} for more details on the
   262   form of equations admitted as constant definitions.
   263   
   264   The $overloaded$ option declares definitions to be potentially overloaded.
   265   Unless this option is given, a warning message would be issued for any
   266   definitional equation with a more special type than that of the
   267   corresponding constant declaration.
   268   
   269 \item [$\CONSTDEFS~c::\sigma~eqn$] combines declarations and definitions of
   270   constants, using the canonical name $c_def$ for the definitional axiom.
   271 \end{descr}
   272 
   273 
   274 \subsection{Syntax and translations}\label{sec:syn-trans}
   275 
   276 \indexisarcmd{syntax}\indexisarcmd{translations}
   277 \begin{matharray}{rcl}
   278   \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
   279   \isarcmd{translations} & : & \isartrans{theory}{theory} \\
   280 \end{matharray}
   281 
   282 \railalias{rightleftharpoons}{\isasymrightleftharpoons}
   283 \railterm{rightleftharpoons}
   284 
   285 \railalias{rightharpoonup}{\isasymrightharpoonup}
   286 \railterm{rightharpoonup}
   287 
   288 \railalias{leftharpoondown}{\isasymleftharpoondown}
   289 \railterm{leftharpoondown}
   290 
   291 \begin{rail}
   292   'syntax' ('(' ( name | 'output' | name 'output' ) ')')? (constdecl +)
   293   ;
   294   'translations' (transpat ('==' | '=>' | '<=' | rightleftharpoons | rightharpoonup | leftharpoondown) transpat +)
   295   ;
   296   transpat: ('(' nameref ')')? string
   297   ;
   298 \end{rail}
   299 
   300 \begin{descr}
   301   
   302 \item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
   303   except that the actual logical signature extension is omitted.  Thus the
   304   context free grammar of Isabelle's inner syntax may be augmented in
   305   arbitrary ways, independently of the logic.  The $mode$ argument refers to
   306   the print mode that the grammar rules belong; unless the
   307   $\isarkeyword{output}$ indicator is given, all productions are added both to
   308   the input and output grammar.
   309   
   310 \item [$\isarkeyword{translations}~rules$] specifies syntactic translation
   311   rules (i.e.\ macros): parse~/ print rules (\isasymrightleftharpoons), parse
   312   rules (\isasymrightharpoonup), or print rules (\isasymleftharpoondown).
   313   Translation patterns may be prefixed by the syntactic category to be used
   314   for parsing; the default is $logic$.
   315 \end{descr}
   316 
   317 
   318 \subsection{Axioms and theorems}\label{sec:axms-thms}
   319 
   320 \indexisarcmd{axioms}\indexisarcmd{lemmas}\indexisarcmd{theorems}
   321 \begin{matharray}{rcll}
   322   \isarcmd{axioms} & : & \isartrans{theory}{theory} & (axiomatic!) \\
   323   \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
   324   \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
   325 \end{matharray}
   326 
   327 \begin{rail}
   328   'axioms' (axmdecl prop +)
   329   ;
   330   ('lemmas' | 'theorems') locale? (thmdef? thmrefs + 'and')
   331   ;
   332 \end{rail}
   333 
   334 \begin{descr}
   335   
   336 \item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
   337   axioms of the meta-logic.  In fact, axioms are ``axiomatic theorems'', and
   338   may be referred later just as any other theorem.
   339   
   340   Axioms are usually only introduced when declaring new logical systems.
   341   Everyday work is typically done the hard way, with proper definitions and
   342   proven theorems.
   343   
   344 \item [$\isarkeyword{lemmas}~a = \vec b$] retrieves and stores existing facts
   345   in the theory context, or the specified locale (see also
   346   \S\ref{sec:locale}).  Typical applications would also involve attributes, to
   347   declare Simplifier rules, for example.
   348   
   349 \item [$\isarkeyword{theorems}$] is essentially the same as
   350   $\isarkeyword{lemmas}$, but marks the result as a different kind of facts.
   351 
   352 \end{descr}
   353 
   354 
   355 \subsection{Name spaces}
   356 
   357 \indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{hide}
   358 \begin{matharray}{rcl}
   359   \isarcmd{global} & : & \isartrans{theory}{theory} \\
   360   \isarcmd{local} & : & \isartrans{theory}{theory} \\
   361   \isarcmd{hide} & : & \isartrans{theory}{theory} \\
   362 \end{matharray}
   363 
   364 \begin{rail}
   365   'hide' name (nameref + )
   366   ;
   367 \end{rail}
   368 
   369 Isabelle organizes any kind of name declarations (of types, constants,
   370 theorems etc.) by separate hierarchically structured name spaces.  Normally
   371 the user does not have to control the behavior of name spaces by hand, yet the
   372 following commands provide some way to do so.
   373 
   374 \begin{descr}
   375 \item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
   376   name declaration mode.  Initially, theories start in $\isarkeyword{local}$
   377   mode, causing all names to be automatically qualified by the theory name.
   378   Changing this to $\isarkeyword{global}$ causes all names to be declared
   379   without the theory prefix, until $\isarkeyword{local}$ is declared again.
   380   
   381   Note that global names are prone to get hidden accidently later, when
   382   qualified names of the same base name are introduced.
   383   
   384 \item [$\isarkeyword{hide}~space~names$] removes declarations from a given
   385   name space (which may be $class$, $type$, or $const$).  Hidden objects
   386   remain valid within the logic, but are inaccessible from user input.  In
   387   output, the special qualifier ``$\mathord?\mathord?$'' is prefixed to the
   388   full internal name.  Unqualified (global) names may not be hidden.
   389 \end{descr}
   390 
   391 
   392 \subsection{Incorporating ML code}\label{sec:ML}
   393 
   394 \indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-command}
   395 \indexisarcmd{ML-setup}\indexisarcmd{setup}
   396 \indexisarcmd{method-setup}
   397 \begin{matharray}{rcl}
   398   \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
   399   \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
   400   \isarcmd{ML_command} & : & \isartrans{\cdot}{\cdot} \\
   401   \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
   402   \isarcmd{setup} & : & \isartrans{theory}{theory} \\
   403   \isarcmd{method_setup} & : & \isartrans{theory}{theory} \\
   404 \end{matharray}
   405 
   406 \railalias{MLsetup}{ML\_setup}
   407 \railterm{MLsetup}
   408 
   409 \railalias{methodsetup}{method\_setup}
   410 \railterm{methodsetup}
   411 
   412 \railalias{MLcommand}{ML\_command}
   413 \railterm{MLcommand}
   414 
   415 \begin{rail}
   416   'use' name
   417   ;
   418   ('ML' | MLcommand | MLsetup | 'setup') text
   419   ;
   420   methodsetup name '=' text text
   421   ;
   422 \end{rail}
   423 
   424 \begin{descr}
   425 \item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
   426   The current theory context (if present) is passed down to the ML session,
   427   but may not be modified.  Furthermore, the file name is checked with the
   428   $\isarkeyword{files}$ dependency declaration given in the theory header (see
   429   also \S\ref{sec:begin-thy}).
   430   
   431 \item [$\isarkeyword{ML}~text$ and $\isarkeyword{ML_command}~text$] execute ML
   432   commands from $text$.  The theory context is passed in the same way as for
   433   $\isarkeyword{use}$, but may not be changed.  Note that the output of
   434   $\isarkeyword{ML_command}$ is less verbose than plain $\isarkeyword{ML}$.
   435   
   436 \item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
   437   theory context is passed down to the ML session, and fetched back
   438   afterwards.  Thus $text$ may actually change the theory as a side effect.
   439   
   440 \item [$\isarkeyword{setup}~text$] changes the current theory context by
   441   applying $text$, which refers to an ML expression of type
   442   \texttt{(theory~->~theory)~list}.  The $\isarkeyword{setup}$ command is the
   443   canonical way to initialize any object-logic specific tools and packages
   444   written in ML.
   445   
   446 \item [$\isarkeyword{method_setup}~name = text~description$] defines a proof
   447   method in the current theory.  The given $text$ has to be an ML expression
   448   of type \texttt{Args.src -> Proof.context -> Proof.method}.  Parsing
   449   concrete method syntax from \texttt{Args.src} input can be quite tedious in
   450   general.  The following simple examples are for methods without any explicit
   451   arguments, or a list of theorems, respectively.
   452 
   453 {\footnotesize
   454 \begin{verbatim}
   455  Method.no_args (Method.METHOD (fn facts => foobar_tac))
   456  Method.thms_args (fn thms => Method.METHOD (fn facts => foobar_tac))
   457  Method.ctxt_args (fn ctxt => Method.METHOD (fn facts => foobar_tac))
   458  Method.thms_ctxt_args (fn thms => fn ctxt =>
   459     Method.METHOD (fn facts => foobar_tac))
   460 \end{verbatim}
   461 }
   462 
   463 Note that mere tactic emulations may ignore the \texttt{facts} parameter
   464 above.  Proper proof methods would do something appropriate with the list of
   465 current facts, though.  Single-rule methods usually do strict forward-chaining
   466 (e.g.\ by using \texttt{Method.multi_resolves}), while automatic ones just
   467 insert the facts using \texttt{Method.insert_tac} before applying the main
   468 tactic.
   469 \end{descr}
   470 
   471 
   472 \subsection{Syntax translation functions}
   473 
   474 \indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
   475 \indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
   476 \indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
   477 \begin{matharray}{rcl}
   478   \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
   479   \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
   480   \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
   481   \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
   482   \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
   483   \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
   484 \end{matharray}
   485 
   486 \railalias{parseasttranslation}{parse\_ast\_translation}
   487 \railterm{parseasttranslation}
   488 
   489 \railalias{parsetranslation}{parse\_translation}
   490 \railterm{parsetranslation}
   491 
   492 \railalias{printtranslation}{print\_translation}
   493 \railterm{printtranslation}
   494 
   495 \railalias{typedprinttranslation}{typed\_print\_translation}
   496 \railterm{typedprinttranslation}
   497 
   498 \railalias{printasttranslation}{print\_ast\_translation}
   499 \railterm{printasttranslation}
   500 
   501 \railalias{tokentranslation}{token\_translation}
   502 \railterm{tokentranslation}
   503 
   504 \begin{rail}
   505   ( parseasttranslation | parsetranslation | printtranslation | typedprinttranslation |
   506   printasttranslation | tokentranslation ) text
   507 \end{rail}
   508 
   509 Syntax translation functions written in ML admit almost arbitrary
   510 manipulations of Isabelle's inner syntax.  Any of the above commands have a
   511 single \railqtok{text} argument that refers to an ML expression of appropriate
   512 type.
   513 
   514 \begin{ttbox}
   515 val parse_ast_translation   : (string * (ast list -> ast)) list
   516 val parse_translation       : (string * (term list -> term)) list
   517 val print_translation       : (string * (term list -> term)) list
   518 val typed_print_translation :
   519   (string * (bool -> typ -> term list -> term)) list
   520 val print_ast_translation   : (string * (ast list -> ast)) list
   521 val token_translation       :
   522   (string * string * (string -> string * real)) list
   523 \end{ttbox}
   524 See \cite[\S8]{isabelle-ref} for more information on syntax transformations.
   525 
   526 
   527 \subsection{Oracles}
   528 
   529 \indexisarcmd{oracle}
   530 \begin{matharray}{rcl}
   531   \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
   532 \end{matharray}
   533 
   534 Oracles provide an interface to external reasoning systems, without giving up
   535 control completely --- each theorem carries a derivation object recording any
   536 oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
   537 
   538 \begin{rail}
   539   'oracle' name '=' text
   540   ;
   541 \end{rail}
   542 
   543 \begin{descr}
   544 \item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
   545   function $text$, which has to be of type
   546   \texttt{Sign.sg~*~Object.T~->~term}.
   547 \end{descr}
   548 
   549 
   550 \section{Proof commands}
   551 
   552 Proof commands perform transitions of Isar/VM machine configurations, which
   553 are block-structured, consisting of a stack of nodes with three main
   554 components: logical proof context, current facts, and open goals.  Isar/VM
   555 transitions are \emph{typed} according to the following three different modes
   556 of operation:
   557 \begin{descr}
   558 \item [$proof(prove)$] means that a new goal has just been stated that is now
   559   to be \emph{proven}; the next command may refine it by some proof method,
   560   and enter a sub-proof to establish the actual result.
   561 \item [$proof(state)$] is like a nested theory mode: the context may be
   562   augmented by \emph{stating} additional assumptions, intermediate results
   563   etc.
   564 \item [$proof(chain)$] is intermediate between $proof(state)$ and
   565   $proof(prove)$: existing facts (i.e.\ the contents of the special ``$this$''
   566   register) have been just picked up in order to be used when refining the
   567   goal claimed next.
   568 \end{descr}
   569 
   570 The proof mode indicator may be read as a verb telling the writer what kind of
   571 operation may be performed next.  The corresponding typings of proof commands
   572 restricts the shape of well-formed proof texts to particular command
   573 sequences.  So dynamic arrangements of commands eventually turn out as static
   574 texts of a certain structure.  Appendix~\ref{ap:refcard} gives a simplified
   575 grammar of the overall (extensible) language emerging that way.
   576 
   577 
   578 \subsection{Markup commands}\label{sec:markup-prf}
   579 
   580 \indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsubsect}
   581 \indexisarcmd{txt}\indexisarcmd{txt-raw}
   582 \begin{matharray}{rcl}
   583   \isarcmd{sect} & : & \isartrans{proof}{proof} \\
   584   \isarcmd{subsect} & : & \isartrans{proof}{proof} \\
   585   \isarcmd{subsubsect} & : & \isartrans{proof}{proof} \\
   586   \isarcmd{txt} & : & \isartrans{proof}{proof} \\
   587   \isarcmd{txt_raw} & : & \isartrans{proof}{proof} \\
   588 \end{matharray}
   589 
   590 These markup commands for proof mode closely correspond to the ones of theory
   591 mode (see \S\ref{sec:markup-thy}).
   592 
   593 \railalias{txtraw}{txt\_raw}
   594 \railterm{txtraw}
   595 
   596 \begin{rail}
   597   ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
   598   ;
   599 \end{rail}
   600 
   601 
   602 \subsection{Context elements}\label{sec:proof-context}
   603 
   604 \indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
   605 \begin{matharray}{rcl}
   606   \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
   607   \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
   608   \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
   609   \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
   610 \end{matharray}
   611 
   612 The logical proof context consists of fixed variables and assumptions.  The
   613 former closely correspond to Skolem constants, or meta-level universal
   614 quantification as provided by the Isabelle/Pure logical framework.
   615 Introducing some \emph{arbitrary, but fixed} variable via ``$\FIX x$'' results
   616 in a local value that may be used in the subsequent proof as any other
   617 variable or constant.  Furthermore, any result $\edrv \phi[x]$ exported from
   618 the context will be universally closed wrt.\ $x$ at the outermost level:
   619 $\edrv \All x \phi$ (this is expressed using Isabelle's meta-variables).
   620 
   621 Similarly, introducing some assumption $\chi$ has two effects.  On the one
   622 hand, a local theorem is created that may be used as a fact in subsequent
   623 proof steps.  On the other hand, any result $\chi \drv \phi$ exported from the
   624 context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
   625 Thus, solving an enclosing goal using such a result would basically introduce
   626 a new subgoal stemming from the assumption.  How this situation is handled
   627 depends on the actual version of assumption command used: while $\ASSUMENAME$
   628 insists on solving the subgoal by unification with some premise of the goal,
   629 $\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
   630 user.
   631 
   632 Local definitions, introduced by ``$\DEF{}{x \equiv t}$'', are achieved by
   633 combining ``$\FIX x$'' with another version of assumption that causes any
   634 hypothetical equation $x \equiv t$ to be eliminated by the reflexivity rule.
   635 Thus, exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
   636 
   637 \railalias{equiv}{\isasymequiv}
   638 \railterm{equiv}
   639 
   640 \begin{rail}
   641   'fix' (vars + 'and')
   642   ;
   643   ('assume' | 'presume') (props + 'and')
   644   ;
   645   'def' thmdecl? \\ name ('==' | equiv) term termpat?
   646   ;
   647 \end{rail}
   648 
   649 \begin{descr}
   650   
   651 \item [$\FIX{\vec x}$] introduces local \emph{arbitrary, but fixed} variables
   652   $\vec x$.
   653   
   654 \item [$\ASSUME{a}{\vec\phi}$ and $\PRESUME{a}{\vec\phi}$] introduce local
   655   theorems $\vec\phi$ by assumption.  Subsequent results applied to an
   656   enclosing goal (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$
   657   expects to be able to unify with existing premises in the goal, while
   658   $\PRESUMENAME$ leaves $\vec\phi$ as new subgoals.
   659   
   660   Several lists of assumptions may be given (separated by
   661   $\isarkeyword{and}$); the resulting list of current facts consists of all of
   662   these concatenated.
   663   
   664 \item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
   665   In results exported from the context, $x$ is replaced by $t$.  Basically,
   666   ``$\DEF{}{x \equiv t}$'' abbreviates ``$\FIX{x}~\ASSUME{}{x \equiv t}$'',
   667   with the resulting hypothetical equation solved by reflexivity.
   668   
   669   The default name for the definitional equation is $x_def$.
   670 
   671 \end{descr}
   672 
   673 The special name $prems$\indexisarthm{prems} refers to all assumptions of the
   674 current context as a list of theorems.
   675 
   676 
   677 \subsection{Facts and forward chaining}
   678 
   679 \indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
   680 \indexisarcmd{using}
   681 \begin{matharray}{rcl}
   682   \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
   683   \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
   684   \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
   685   \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
   686   \isarcmd{using} & : & \isartrans{proof(prove)}{proof(prove)} \\
   687 \end{matharray}
   688 
   689 New facts are established either by assumption or proof of local statements.
   690 Any fact will usually be involved in further proofs, either as explicit
   691 arguments of proof methods, or when forward chaining towards the next goal via
   692 $\THEN$ (and variants); $\FROMNAME$ and $\WITHNAME$ are composite forms
   693 involving $\NOTENAME$.  The $\USINGNAME$ elements augments the collection of
   694 used facts \emph{after} a goal has been stated.  Note that the special theorem
   695 name $this$\indexisarthm{this} refers to the most recently established facts,
   696 but only \emph{before} issuing a follow-up claim.
   697 
   698 \begin{rail}
   699   'note' (thmdef? thmrefs + 'and')
   700   ;
   701   ('from' | 'with' | 'using') (thmrefs + 'and')
   702   ;
   703 \end{rail}
   704 
   705 \begin{descr}
   706 
   707 \item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
   708   as $a$.  Note that attributes may be involved as well, both on the left and
   709   right hand sides.
   710 
   711 \item [$\THEN$] indicates forward chaining by the current facts in order to
   712   establish the goal to be claimed next.  The initial proof method invoked to
   713   refine that will be offered the facts to do ``anything appropriate'' (see
   714   also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
   715   \S\ref{sec:pure-meth-att}) would typically do an elimination rather than an
   716   introduction.  Automatic methods usually insert the facts into the goal
   717   state before operation.  This provides a simple scheme to control relevance
   718   of facts in automated proof search.
   719   
   720 \item [$\FROM{\vec b}$] abbreviates ``$\NOTE{}{\vec b}~\THEN$''; thus $\THEN$
   721   is equivalent to ``$\FROM{this}$''.
   722   
   723 \item [$\WITH{\vec b}$] abbreviates ``$\FROM{\vec b~\AND~this}$''; thus the
   724   forward chaining is from earlier facts together with the current ones.
   725   
   726 \item [$\USING{\vec b}$] augments the facts being currently indicated for use
   727   by a subsequent refinement step (such as $\APPLYNAME$ or $\PROOFNAME$).
   728 
   729 \end{descr}
   730 
   731 Forward chaining with an empty list of theorems is the same as not chaining at
   732 all.  Thus ``$\FROM{nothing}$'' has no effect apart from entering
   733 $prove(chain)$ mode, since $nothing$\indexisarthm{nothing} is bound to the
   734 empty list of theorems.
   735 
   736 Basic proof methods (such as $rule$) expect multiple facts to be given in
   737 their proper order, corresponding to a prefix of the premises of the rule
   738 involved.  Note that positions may be easily skipped using something like
   739 $\FROM{\Text{\texttt{_}}~a~b}$, for example.  This involves the trivial rule
   740 $\PROP\psi \Imp \PROP\psi$, which happens to be bound in Isabelle/Pure as
   741 ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
   742 
   743 Automated methods (such as $simp$ or $auto$) just insert any given facts
   744 before their usual operation.  Depending on the kind of procedure involved,
   745 the order of facts is less significant here.
   746 
   747 
   748 \subsection{Goal statements}\label{sec:goals}
   749 
   750 \indexisarcmd{lemma}\indexisarcmd{theorem}\indexisarcmd{corollary}
   751 \indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
   752 \begin{matharray}{rcl}
   753   \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
   754   \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
   755   \isarcmd{corollary} & : & \isartrans{theory}{proof(prove)} \\
   756   \isarcmd{have} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   757   \isarcmd{show} & : & \isartrans{proof(state) ~|~ proof(chain)}{proof(prove)} \\
   758   \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
   759   \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
   760 \end{matharray}
   761 
   762 From a theory context, proof mode is entered by an initial goal command such
   763 as $\LEMMANAME$, $\THEOREMNAME$, or $\COROLLARYNAME$.  Within a proof, new
   764 claims may be introduced locally as well; four variants are available here to
   765 indicate whether forward chaining of facts should be performed initially (via
   766 $\THEN$), and whether the final result is meant to solve some pending goal.
   767 
   768 Goals may consist of multiple statements, resulting in a list of facts
   769 eventually.  A pending multi-goal is internally represented as a meta-level
   770 conjunction (printed as \verb,&&,), which is usually split into the
   771 corresponding number of sub-goals prior to an initial method application, via
   772 $\PROOFNAME$ (\S\ref{sec:proof-steps}) or $\APPLYNAME$
   773 (\S\ref{sec:tactic-commands}).  The $induct$ method covered in
   774 \S\ref{sec:cases-induct-meth} acts on multiple claims simultaneously.
   775 
   776 Claims at the theory level may be either in short or long form.  A short goal
   777 merely consists of several simultaneous propositions (often just one).  A long
   778 goal includes an explicit context specification for the subsequent
   779 conclusions, involving local parameters; here the role of each part of the
   780 statement is explicitly marked by separate keywords (see also
   781 \S\ref{sec:locale}).
   782 
   783 \begin{rail}
   784   ('lemma' | 'theorem' | 'corollary') locale? (goal | longgoal)
   785   ;
   786   ('have' | 'show' | 'hence' | 'thus') goal
   787   ;
   788   
   789   goal: (props + 'and')
   790   ;
   791   longgoal: thmdecl? (contextelem *) 'shows' goal
   792   ;
   793 \end{rail}
   794 
   795 \begin{descr}
   796   
   797 \item [$\LEMMA{a}{\vec\phi}$] enters proof mode with $\vec\phi$ as main goal,
   798   eventually resulting in some fact $\turn \vec\phi$ to be put back into the
   799   theory context, or into the specified locale (cf.\ \S\ref{sec:locale}).  An
   800   additional \railnonterm{context} specification may build up an initial proof
   801   context for the subsequent claim; this includes local definitions and syntax
   802   as well, see the definition of $contextelem$ in \S\ref{sec:locale}.
   803   
   804 \item [$\THEOREM{a}{\vec\phi}$ and $\COROLLARY{a}{\vec\phi}$] are essentially
   805   the same as $\LEMMA{a}{\vec\phi}$, but the facts are internally marked as
   806   being of a different kind.  This discrimination acts like a formal comment.
   807   
   808 \item [$\HAVE{a}{\vec\phi}$] claims a local goal, eventually resulting in a
   809   fact within the current logical context.  This operation is completely
   810   independent of any pending sub-goals of an enclosing goal statements, so
   811   $\HAVENAME$ may be freely used for experimental exploration of potential
   812   results within a proof body.
   813   
   814 \item [$\SHOW{a}{\vec\phi}$] is like $\HAVE{a}{\vec\phi}$ plus a second stage
   815   to refine some pending sub-goal for each one of the finished result, after
   816   having been exported into the corresponding context (at the head of the
   817   sub-proof of this $\SHOWNAME$ command).
   818   
   819   To accommodate interactive debugging, resulting rules are printed before
   820   being applied internally.  Even more, interactive execution of $\SHOWNAME$
   821   predicts potential failure and displays the resulting error as a warning
   822   beforehand.  Watch out for the following message:
   823 
   824   \begin{ttbox}
   825   Problem! Local statement will fail to solve any pending goal
   826   \end{ttbox}
   827   
   828 \item [$\HENCENAME$] abbreviates ``$\THEN~\HAVENAME$'', i.e.\ claims a local
   829   goal to be proven by forward chaining the current facts.  Note that
   830   $\HENCENAME$ is also equivalent to ``$\FROM{this}~\HAVENAME$''.
   831   
   832 \item [$\THUSNAME$] abbreviates ``$\THEN~\SHOWNAME$''.  Note that $\THUSNAME$
   833   is also equivalent to ``$\FROM{this}~\SHOWNAME$''.
   834 
   835 \end{descr}
   836 
   837 Any goal statement causes some term abbreviations (such as $\Var{thesis}$) to
   838 be bound automatically, see also \S\ref{sec:term-abbrev}.  Furthermore, the
   839 local context of a (non-atomic) goal is provided via the
   840 $rule_context$\indexisarcase{rule-context} case.
   841 
   842 \medskip
   843 
   844 \begin{warn}
   845   Isabelle/Isar suffers theory-level goal statements to contain \emph{unbound
   846     schematic variables}, although this does not conform to the aim of
   847   human-readable proof documents!  The main problem with schematic goals is
   848   that the actual outcome is usually hard to predict, depending on the
   849   behavior of the proof methods applied during the course of reasoning.  Note
   850   that most semi-automated methods heavily depend on several kinds of implicit
   851   rule declarations within the current theory context.  As this would also
   852   result in non-compositional checking of sub-proofs, \emph{local goals} are
   853   not allowed to be schematic at all.  Nevertheless, schematic goals do have
   854   their use in Prolog-style interactive synthesis of proven results, usually
   855   by stepwise refinement via emulation of traditional Isabelle tactic scripts
   856   (see also \S\ref{sec:tactic-commands}).  In any case, users should know what
   857   they are doing.
   858 \end{warn}
   859 
   860 
   861 \subsection{Initial and terminal proof steps}\label{sec:proof-steps}
   862 
   863 \indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
   864 \indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
   865 \begin{matharray}{rcl}
   866   \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
   867   \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
   868   \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
   869   \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
   870   \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
   871   \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
   872 \end{matharray}
   873 
   874 Arbitrary goal refinement via tactics is considered harmful.  Properly, the
   875 Isar framework admits proof methods to be invoked in two places only.
   876 \begin{enumerate}
   877 \item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
   878   goal to a number of sub-goals that are to be solved later.  Facts are passed
   879   to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
   880   
   881 \item A \emph{terminal} conclusion step $\QED{m@2}$ is intended to solve
   882   remaining goals.  No facts are passed to $m@2$.
   883 \end{enumerate}
   884 
   885 The only other (proper) way to affect pending goals in a proof body is by
   886 $\SHOWNAME$, which involves an explicit statement of what is to be solved
   887 eventually.  Thus we avoid the fundamental problem of unstructured tactic
   888 scripts that consist of numerous consecutive goal transformations, with
   889 invisible effects.
   890 
   891 \medskip
   892 
   893 As a general rule of thumb for good proof style, initial proof methods should
   894 either solve the goal completely, or constitute some well-understood reduction
   895 to new sub-goals.  Arbitrary automatic proof tools that are prone leave a
   896 large number of badly structured sub-goals are no help in continuing the proof
   897 document in an intelligible manner.
   898 
   899 Unless given explicitly by the user, the default initial method is ``$rule$'',
   900 which applies a single standard elimination or introduction rule according to
   901 the topmost symbol involved.  There is no separate default terminal method.
   902 Any remaining goals are always solved by assumption in the very last step.
   903 
   904 \begin{rail}
   905   'proof' method?
   906   ;
   907   'qed' method?
   908   ;
   909   'by' method method?
   910   ;
   911   ('.' | '..' | 'sorry')
   912   ;
   913 \end{rail}
   914 
   915 \begin{descr}
   916   
   917 \item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
   918   forward chaining are passed if so indicated by $proof(chain)$ mode.
   919   
   920 \item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
   921   concludes the sub-proof by assumption.  If the goal had been $\SHOWNAME$ (or
   922   $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
   923   from the result \emph{exported} into the enclosing goal context.  Thus
   924   $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
   925   rule does not fit to any pending goal\footnote{This includes any additional
   926     ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
   927   context.  Debugging such a situation might involve temporarily changing
   928   $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
   929   occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
   930   
   931 \item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
   932   abbreviates $\PROOF{m@1}~\QED{m@2}$, but with backtracking across both
   933   methods.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
   934   by expanding its definition; in many cases $\PROOF{m@1}$ (or even
   935   $\APPLY{m@1}$) is already sufficient to see the problem.
   936 
   937 \item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
   938   abbreviates $\BY{rule}$.
   939 
   940 \item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
   941   abbreviates $\BY{this}$.
   942   
   943 \item [$\SORRY$] is a \emph{fake proof}\index{proof!fake} pretending to solve
   944   the pending claim without further ado.  This only works in interactive
   945   development, or if the \texttt{quick_and_dirty} flag is enabled.  Facts
   946   emerging from fake proofs are not the real thing.  Internally, each theorem
   947   container is tainted by an oracle invocation, which is indicated as
   948   ``$[!]$'' in the printed result.
   949   
   950   The most important application of $\SORRY$ is to support experimentation and
   951   top-down proof development.
   952 \end{descr}
   953 
   954 
   955 \subsection{Fundamental methods and attributes}\label{sec:pure-meth-att}
   956 
   957 The following proof methods and attributes refer to basic logical operations
   958 of Isar.  Further methods and attributes are provided by several generic and
   959 object-logic specific tools and packages (see chapters \ref{ch:gen-tools} and
   960 \ref{ch:logics}).
   961 
   962 \indexisarmeth{$-$}\indexisarmeth{assumption}
   963 \indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
   964 \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
   965 \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
   966 \indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
   967 \begin{matharray}{rcl}
   968   - & : & \isarmeth \\
   969   assumption & : & \isarmeth \\
   970   this & : & \isarmeth \\
   971   rule & : & \isarmeth \\
   972   rules & : & \isarmeth \\[0.5ex]
   973   intro & : & \isaratt \\
   974   elim & : & \isaratt \\
   975   dest & : & \isaratt \\
   976   rule & : & \isaratt \\[0.5ex]
   977   OF & : & \isaratt \\
   978   of & : & \isaratt \\
   979   where & : & \isaratt \\
   980 \end{matharray}
   981 
   982 \begin{rail}
   983   'rule' thmrefs?
   984   ;
   985   'rules' ('!' ?) (rulemod *)
   986   ;
   987   rulemod: ('intro' | 'elim' | 'dest') ((('!' | () | '?') nat?) | 'del') ':' thmrefs
   988   ;
   989   ('intro' | 'elim' | 'dest') ('!' | () | '?') nat?
   990   ;
   991   'rule' 'del'
   992   ;
   993   'OF' thmrefs
   994   ;
   995   'of' insts ('concl' ':' insts)?
   996   ;
   997   'where' (name '=' term * 'and')
   998   ;
   999 \end{rail}
  1000 
  1001 \begin{descr}
  1002   
  1003 \item [``$-$''] does nothing but insert the forward chaining facts as premises
  1004   into the goal.  Note that command $\PROOFNAME$ without any method actually
  1005   performs a single reduction step using the $rule$ method; thus a plain
  1006   \emph{do-nothing} proof step would be ``$\PROOF{-}$'' rather than
  1007   $\PROOFNAME$ alone.
  1008   
  1009 \item [$assumption$] solves some goal by a single assumption step.  All given
  1010   facts are guaranteed to participate in the refinement; this means there may
  1011   be only $0$ or $1$ in the first place.  Recall that $\QEDNAME$ (see
  1012   \S\ref{sec:proof-steps}) already concludes any remaining sub-goals by
  1013   assumption, so structured proofs usually need not quote the $assumption$
  1014   method at all.
  1015   
  1016 \item [$this$] applies all of the current facts directly as rules.  Recall
  1017   that ``$\DOT$'' (dot) abbreviates ``$\BY{this}$''.
  1018   
  1019 \item [$rule~\vec a$] applies some rule given as argument in backward manner;
  1020   facts are used to reduce the rule before applying it to the goal.  Thus
  1021   $rule$ without facts is plain introduction, while with facts it becomes
  1022   elimination.
  1023   
  1024   When no arguments are given, the $rule$ method tries to pick appropriate
  1025   rules automatically, as declared in the current context using the $intro$,
  1026   $elim$, $dest$ attributes (see below).  This is the default behavior of
  1027   $\PROOFNAME$ and ``$\DDOT$'' (double-dot) steps (see
  1028   \S\ref{sec:proof-steps}).
  1029   
  1030 \item [$rules$] performs intuitionistic proof search, depending on
  1031   specifically declared rules from the context, or given as explicit
  1032   arguments.  Chained facts are inserted into the goal before commencing proof
  1033   search; ``$rules!$'' means to include the current $prems$ as well.
  1034   
  1035   Rules need to be classified as $intro$, $elim$, or $dest$; here the ``$!$''
  1036   indicator refers to ``safe'' rules, which may be applied aggressively
  1037   (without considering back-tracking later).  Rules declared with ``$?$'' are
  1038   ignored in proof search (the single-step $rule$ method still observes
  1039   these).  An explicit weight annotation may be given as well; otherwise the
  1040   number of rule premises will be taken into account here.
  1041   
  1042 \item [$intro$, $elim$, and $dest$] declare introduction, elimination, and
  1043   destruct rules, to be used with the $rule$ and $rules$ methods.  Note that
  1044   the latter will ignore rules declared with ``$?$'', while ``$!$'' are used
  1045   most aggressively.
  1046   
  1047   The classical reasoner (see \S\ref{sec:classical}) introduces its own
  1048   variants of these attributes; use qualified names to access the present
  1049   versions of Isabelle/Pure, i.e.\ $Pure{\dtt}intro$ or $CPure{\dtt}intro$.
  1050   
  1051 \item [$rule~del$] undeclares introduction, elimination, or destruct rules.
  1052   
  1053 \item [$OF~\vec a$] applies some theorem to given rules $\vec a$ (in
  1054   parallel).  This corresponds to the \texttt{MRS} operator in ML
  1055   \cite[\S5]{isabelle-ref}, but note the reversed order.  Positions may be
  1056   effectively skipped by including ``$\_$'' (underscore) as argument.
  1057   
  1058 \item [$of~\vec t$] performs positional instantiation of term
  1059   variables.  The terms $\vec t$ are substituted for any schematic
  1060   variables occurring in a theorem from left to right; ``\texttt{_}''
  1061   (underscore) indicates to skip a position.  Arguments following a
  1062   ``$concl\colon$'' specification refer to positions of the conclusion
  1063   of a rule.
  1064   
  1065 \item [$where~\vec x = \vec t$] performs named instantiation of
  1066   schematic type and term variables occurring in a theorem.  Schematic
  1067   variables have to be specified on the left-hand side (e.g.\
  1068   $?x1\!.\!3$).  The question mark may be omitted if the variable name
  1069   is neither a keyword nor contains a dot.  Types are instantiated
  1070   before terms, and instantiations have to be written in that order.
  1071   Because type instantiations are inferred from term instantiations,
  1072   explicit type instantiations are seldom necessary.
  1073 
  1074 \end{descr}
  1075 
  1076 
  1077 \subsection{Term abbreviations}\label{sec:term-abbrev}
  1078 
  1079 \indexisarcmd{let}
  1080 \begin{matharray}{rcl}
  1081   \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
  1082   \isarkeyword{is} & : & syntax \\
  1083 \end{matharray}
  1084 
  1085 Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
  1086 or by annotating assumptions or goal statements with a list of patterns
  1087 ``$\ISS{p@1\;\dots}{p@n}$''.  In both cases, higher-order matching is invoked
  1088 to bind extra-logical term variables, which may be either named schematic
  1089 variables of the form $\Var{x}$, or nameless dummies ``\texttt{_}''
  1090 (underscore).\indexisarvar{_@\texttt{_}} Note that in the $\LETNAME$ form the
  1091 patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
  1092 postfix position.
  1093 
  1094 Polymorphism of term bindings is handled in Hindley-Milner style, similar to
  1095 ML.  Type variables referring to local assumptions or open goal statements are
  1096 \emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
  1097 in \emph{arbitrary} instances later.  Even though actual polymorphism should
  1098 be rarely used in practice, this mechanism is essential to achieve proper
  1099 incremental type-inference, as the user proceeds to build up the Isar proof
  1100 text from left to right.
  1101 
  1102 \medskip
  1103 
  1104 Term abbreviations are quite different from local definitions as introduced
  1105 via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are visible within
  1106 the logic as actual equations, while abbreviations disappear during the input
  1107 process just after type checking.  Also note that $\DEFNAME$ does not support
  1108 polymorphism.
  1109 
  1110 \begin{rail}
  1111   'let' ((term + 'and') '=' term + 'and')
  1112   ;  
  1113 \end{rail}
  1114 
  1115 The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
  1116 \railnonterm{proppat} (see \S\ref{sec:term-decls}).
  1117 
  1118 \begin{descr}
  1119 \item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
  1120   by simultaneous higher-order matching against terms $\vec t$.
  1121 \item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
  1122   preceding statement.  Also note that $\ISNAME$ is not a separate command,
  1123   but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
  1124 \end{descr}
  1125 
  1126 Some \emph{automatic} term abbreviations\index{term abbreviations} for goals
  1127 and facts are available as well.  For any open goal,
  1128 $\Var{thesis}$\indexisarvar{thesis} refers to its object-level statement,
  1129 abstracted over any meta-level parameters (if present).  Likewise,
  1130 $\Var{this}$\indexisarvar{this} is bound for fact statements resulting from
  1131 assumptions or finished goals.  In case $\Var{this}$ refers to an object-logic
  1132 statement that is an application $f(t)$, then $t$ is bound to the special text
  1133 variable ``$\dots$''\indexisarvar{\dots} (three dots).  The canonical
  1134 application of the latter are calculational proofs (see
  1135 \S\ref{sec:calculation}).
  1136 
  1137 
  1138 \subsection{Block structure}
  1139 
  1140 \indexisarcmd{next}\indexisarcmd{\{}\indexisarcmd{\}}
  1141 \begin{matharray}{rcl}
  1142   \NEXT & : & \isartrans{proof(state)}{proof(state)} \\
  1143   \BG & : & \isartrans{proof(state)}{proof(state)} \\
  1144   \EN & : & \isartrans{proof(state)}{proof(state)} \\
  1145 \end{matharray}
  1146 
  1147 While Isar is inherently block-structured, opening and closing blocks is
  1148 mostly handled rather casually, with little explicit user-intervention.  Any
  1149 local goal statement automatically opens \emph{two} blocks, which are closed
  1150 again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
  1151 different context within a sub-proof may be switched via $\NEXT$, which is
  1152 just a single block-close followed by block-open again.  The effect of $\NEXT$
  1153 is to reset the local proof context; there is no goal focus involved here!
  1154 
  1155 For slightly more advanced applications, there are explicit block parentheses
  1156 as well.  These typically achieve a stronger forward style of reasoning.
  1157 
  1158 \begin{descr}
  1159 \item [$\NEXT$] switches to a fresh block within a sub-proof, resetting the
  1160   local context to the initial one.
  1161 \item [$\BG$ and $\EN$] explicitly open and close blocks.  Any current facts
  1162   pass through ``$\BG$'' unchanged, while ``$\EN$'' causes any result to be
  1163   \emph{exported} into the enclosing context.  Thus fixed variables are
  1164   generalized, assumptions discharged, and local definitions unfolded (cf.\ 
  1165   \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and
  1166   $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
  1167   backward reasoning with the result exported at $\SHOWNAME$ time.
  1168 \end{descr}
  1169 
  1170 
  1171 \subsection{Emulating tactic scripts}\label{sec:tactic-commands}
  1172 
  1173 The Isar provides separate commands to accommodate tactic-style proof scripts
  1174 within the same system.  While being outside the orthodox Isar proof language,
  1175 these might come in handy for interactive exploration and debugging, or even
  1176 actual tactical proof within new-style theories (to benefit from document
  1177 preparation, for example).  See also \S\ref{sec:tactics} for actual tactics,
  1178 that have been encapsulated as proof methods.  Proper proof methods may be
  1179 used in scripts, too.
  1180 
  1181 \indexisarcmd{apply}\indexisarcmd{apply-end}\indexisarcmd{done}
  1182 \indexisarcmd{defer}\indexisarcmd{prefer}\indexisarcmd{back}
  1183 \indexisarcmd{declare}
  1184 \begin{matharray}{rcl}
  1185   \isarcmd{apply}^* & : & \isartrans{proof(prove)}{proof(prove)} \\
  1186   \isarcmd{apply_end}^* & : & \isartrans{proof(state)}{proof(state)} \\
  1187   \isarcmd{done}^* & : & \isartrans{proof(prove)}{proof(state)} \\
  1188   \isarcmd{defer}^* & : & \isartrans{proof}{proof} \\
  1189   \isarcmd{prefer}^* & : & \isartrans{proof}{proof} \\
  1190   \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
  1191   \isarcmd{declare}^* & : & \isartrans{theory}{theory} \\
  1192 \end{matharray}
  1193 
  1194 \railalias{applyend}{apply\_end}
  1195 \railterm{applyend}
  1196 
  1197 \begin{rail}
  1198   ( 'apply' | applyend ) method
  1199   ;
  1200   'defer' nat?
  1201   ;
  1202   'prefer' nat
  1203   ;
  1204   'declare' locale? (thmrefs + 'and')
  1205   ;
  1206 \end{rail}
  1207 
  1208 \begin{descr}
  1209 
  1210 \item [$\APPLY{m}$] applies proof method $m$ in initial position, but unlike
  1211   $\PROOFNAME$ it retains ``$proof(prove)$'' mode.  Thus consecutive method
  1212   applications may be given just as in tactic scripts.
  1213   
  1214   Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
  1215   are \emph{consumed} afterwards.  Thus any further $\APPLYNAME$ command would
  1216   always work in a purely backward manner.
  1217   
  1218 \item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
  1219   terminal position.  Basically, this simulates a multi-step tactic script for
  1220   $\QEDNAME$, but may be given anywhere within the proof body.
  1221   
  1222   No facts are passed to $m$.  Furthermore, the static context is that of the
  1223   enclosing goal (as for actual $\QEDNAME$).  Thus the proof method may not
  1224   refer to any assumptions introduced in the current body, for example.
  1225   
  1226 \item [$\isarkeyword{done}$] completes a proof script, provided that the
  1227   current goal state is solved completely.  Note that actual structured proof
  1228   commands (e.g.\ ``$\DOT$'' or $\SORRY$) may be used to conclude proof
  1229   scripts as well.
  1230 
  1231 \item [$\isarkeyword{defer}~n$ and $\isarkeyword{prefer}~n$] shuffle the list
  1232   of pending goals: $defer$ puts off goal $n$ to the end of the list ($n = 1$
  1233   by default), while $prefer$ brings goal $n$ to the top.
  1234   
  1235 \item [$\isarkeyword{back}$] does back-tracking over the result sequence of
  1236   the latest proof command.  Basically, any proof command may return multiple
  1237   results.
  1238   
  1239 \item [$\isarkeyword{declare}~thms$] declares theorems to the current theory
  1240   context (or the specified locale, see also \S\ref{sec:locale}).  No theorem
  1241   binding is involved here, unlike $\isarkeyword{theorems}$ or
  1242   $\isarkeyword{lemmas}$ (cf.\ \S\ref{sec:axms-thms}), so
  1243   $\isarkeyword{declare}$ only has the effect of applying attributes as
  1244   included in the theorem specification.
  1245 
  1246 \end{descr}
  1247 
  1248 Any proper Isar proof method may be used with tactic script commands such as
  1249 $\APPLYNAME$.  A few additional emulations of actual tactics are provided as
  1250 well; these would be never used in actual structured proofs, of course.
  1251 
  1252 
  1253 \subsection{Meta-linguistic features}
  1254 
  1255 \indexisarcmd{oops}
  1256 \begin{matharray}{rcl}
  1257   \isarcmd{oops} & : & \isartrans{proof}{theory} \\
  1258 \end{matharray}
  1259 
  1260 The $\OOPS$ command discontinues the current proof attempt, while considering
  1261 the partial proof text as properly processed.  This is conceptually quite
  1262 different from ``faking'' actual proofs via $\SORRY$ (see
  1263 \S\ref{sec:proof-steps}): $\OOPS$ does not observe the proof structure at all,
  1264 but goes back right to the theory level.  Furthermore, $\OOPS$ does not
  1265 produce any result theorem --- there is no intended claim to be able to
  1266 complete the proof anyhow.
  1267 
  1268 A typical application of $\OOPS$ is to explain Isar proofs \emph{within} the
  1269 system itself, in conjunction with the document preparation tools of Isabelle
  1270 described in \cite{isabelle-sys}.  Thus partial or even wrong proof attempts
  1271 can be discussed in a logically sound manner.  Note that the Isabelle {\LaTeX}
  1272 macros can be easily adapted to print something like ``$\dots$'' instead of an
  1273 ``$\OOPS$'' keyword.
  1274 
  1275 \medskip The $\OOPS$ command is undo-able, unlike $\isarkeyword{kill}$ (see
  1276 \S\ref{sec:history}).  The effect is to get back to the theory just before the
  1277 opening of the proof.
  1278 
  1279 
  1280 \section{Other commands}
  1281 
  1282 \subsection{Diagnostics}
  1283 
  1284 \indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}
  1285 \indexisarcmd{prop}\indexisarcmd{typ}
  1286 \begin{matharray}{rcl}
  1287   \isarcmd{pr}^* & : & \isarkeep{\cdot} \\
  1288   \isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
  1289   \isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
  1290   \isarcmd{prop}^* & : & \isarkeep{theory~|~proof} \\
  1291   \isarcmd{typ}^* & : & \isarkeep{theory~|~proof} \\
  1292   \isarcmd{prf}^* & : & \isarkeep{theory~|~proof} \\
  1293   \isarcmd{full_prf}^* & : & \isarkeep{theory~|~proof} \\
  1294 \end{matharray}
  1295 
  1296 These diagnostic commands assist interactive development.  Note that $undo$
  1297 does not apply here, the theory or proof configuration is not changed.
  1298 
  1299 \begin{rail}
  1300   'pr' modes? nat? (',' nat)?
  1301   ;
  1302   'thm' modes? thmrefs
  1303   ;
  1304   'term' modes? term
  1305   ;
  1306   'prop' modes? prop
  1307   ;
  1308   'typ' modes? type
  1309   ;
  1310   'prf' modes? thmrefs?
  1311   ;
  1312   'full\_prf' modes? thmrefs?
  1313   ;
  1314 
  1315   modes: '(' (name + ) ')'
  1316   ;
  1317 \end{rail}
  1318 
  1319 \begin{descr}
  1320 \item [$\isarkeyword{pr}~goals, prems$] prints the current proof state (if
  1321   present), including the proof context, current facts and goals.  The
  1322   optional limit arguments affect the number of goals and premises to be
  1323   displayed, which is initially 10 for both.  Omitting limit values leaves the
  1324   current setting unchanged.
  1325 \item [$\isarkeyword{thm}~\vec a$] retrieves theorems from the current theory
  1326   or proof context.  Note that any attributes included in the theorem
  1327   specifications are applied to a temporary context derived from the current
  1328   theory or proof; the result is discarded, i.e.\ attributes involved in $\vec
  1329   a$ do not have any permanent effect.
  1330 \item [$\isarkeyword{term}~t$ and $\isarkeyword{prop}~\phi$] read, type-check
  1331   and print terms or propositions according to the current theory or proof
  1332   context; the inferred type of $t$ is output as well.  Note that these
  1333   commands are also useful in inspecting the current environment of term
  1334   abbreviations.
  1335 \item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
  1336   according to the current theory or proof context.
  1337 \item [$\isarkeyword{prf}$] displays the (compact) proof term of the current
  1338   proof state (if present), or of the given theorems. Note that this
  1339   requires proof terms to be switched on for the current object logic
  1340   (see the ``Proof terms'' section of the Isabelle reference manual
  1341   for information on how to do this).
  1342 \item [$\isarkeyword{full_prf}$] is like $\isarkeyword{prf}$, but displays
  1343   the full proof term, i.e.\ also displays information omitted in
  1344   the compact proof term, which is denoted by ``$_$'' placeholders there.
  1345 \end{descr}
  1346 
  1347 All of the diagnostic commands above admit a list of $modes$ to be specified,
  1348 which is appended to the current print mode (see also \cite{isabelle-ref}).
  1349 Thus the output behavior may be modified according particular print mode
  1350 features.  For example, $\isarkeyword{pr}~(latex~xsymbols~symbols)$ would
  1351 print the current proof state with mathematical symbols and special characters
  1352 represented in {\LaTeX} source, according to the Isabelle style
  1353 \cite{isabelle-sys}.
  1354 
  1355 Note that antiquotations (cf.\ \S\ref{sec:antiq}) provide a more systematic
  1356 way to include formal items into the printed text document.
  1357 
  1358 
  1359 \subsection{Inspecting the context}
  1360 
  1361 \indexisarcmd{print-facts}\indexisarcmd{print-binds}
  1362 \indexisarcmd{print-commands}\indexisarcmd{print-syntax}
  1363 \indexisarcmd{print-methods}\indexisarcmd{print-attributes}
  1364 \indexisarcmd{thms-containing}\indexisarcmd{thm-deps}
  1365 \indexisarcmd{print-theorems}
  1366 \begin{matharray}{rcl}
  1367   \isarcmd{print_commands}^* & : & \isarkeep{\cdot} \\
  1368   \isarcmd{print_syntax}^* & : & \isarkeep{theory~|~proof} \\
  1369   \isarcmd{print_methods}^* & : & \isarkeep{theory~|~proof} \\
  1370   \isarcmd{print_attributes}^* & : & \isarkeep{theory~|~proof} \\
  1371   \isarcmd{print_theorems}^* & : & \isarkeep{theory~|~proof} \\
  1372   \isarcmd{thms_containing}^* & : & \isarkeep{theory~|~proof} \\
  1373   \isarcmd{thms_deps}^* & : & \isarkeep{theory~|~proof} \\
  1374   \isarcmd{print_facts}^* & : & \isarkeep{proof} \\
  1375   \isarcmd{print_binds}^* & : & \isarkeep{proof} \\
  1376 \end{matharray}
  1377 
  1378 \railalias{thmscontaining}{thms\_containing}
  1379 \railterm{thmscontaining}
  1380 
  1381 \railalias{thmdeps}{thm\_deps}
  1382 \railterm{thmdeps}
  1383 
  1384 \begin{rail}
  1385   thmscontaining ('(' nat ')')? (term * )
  1386   ;
  1387   thmdeps thmrefs
  1388   ;
  1389 \end{rail}
  1390 
  1391 These commands print certain parts of the theory and proof context.  Note that
  1392 there are some further ones available, such as for the set of rules declared
  1393 for simplifications.
  1394 
  1395 \begin{descr}
  1396   
  1397 \item [$\isarkeyword{print_commands}$] prints Isabelle's outer theory syntax,
  1398   including keywords and command.
  1399   
  1400 \item [$\isarkeyword{print_syntax}$] prints the inner syntax of types and
  1401   terms, depending on the current context.  The output can be very verbose,
  1402   including grammar tables and syntax translation rules.  See \cite[\S7,
  1403   \S8]{isabelle-ref} for further information on Isabelle's inner syntax.
  1404   
  1405 \item [$\isarkeyword{print_methods}$] prints all proof methods available in
  1406   the current theory context.
  1407   
  1408 \item [$\isarkeyword{print_attributes}$] prints all attributes available in
  1409   the current theory context.
  1410   
  1411 \item [$\isarkeyword{print_theorems}$] prints theorems available in the
  1412   current theory context.
  1413   
  1414   In interactive mode this actually refers to the theorems left by the last
  1415   transaction; this allows to inspect the result of advanced definitional
  1416   packages, such as $\isarkeyword{datatype}$.
  1417   
  1418 \item [$\isarkeyword{thms_containing}~\vec t$] retrieves facts from the theory
  1419   or proof context containing all of the constants or variables occurring in
  1420   terms $\vec t$ (which may contain occurrences of ``$\_$'').  Note that
  1421   giving the empty list yields \emph{all} currently known facts.  An optional
  1422   limit for the number printed facts may be given; the default is 40.
  1423   
  1424 \item [$\isarkeyword{thm_deps}~\vec a$] visualizes dependencies of facts,
  1425   using Isabelle's graph browser tool (see also \cite{isabelle-sys}).
  1426   
  1427 \item [$\isarkeyword{print_facts}$] prints any named facts of the current
  1428   context, including assumptions and local results.
  1429   
  1430 \item [$\isarkeyword{print_binds}$] prints all term abbreviations present in
  1431   the context.
  1432 
  1433 \end{descr}
  1434 
  1435 
  1436 \subsection{History commands}\label{sec:history}
  1437 
  1438 \indexisarcmd{undo}\indexisarcmd{redo}\indexisarcmd{kill}
  1439 \begin{matharray}{rcl}
  1440   \isarcmd{undo}^{{*}{*}} & : & \isarkeep{\cdot} \\
  1441   \isarcmd{redo}^{{*}{*}} & : & \isarkeep{\cdot} \\
  1442   \isarcmd{kill}^{{*}{*}} & : & \isarkeep{\cdot} \\
  1443 \end{matharray}
  1444 
  1445 The Isabelle/Isar top-level maintains a two-stage history, for theory and
  1446 proof state transformation.  Basically, any command can be undone using
  1447 $\isarkeyword{undo}$, excluding mere diagnostic elements.  Its effect may be
  1448 revoked via $\isarkeyword{redo}$, unless the corresponding
  1449 $\isarkeyword{undo}$ step has crossed the beginning of a proof or theory.  The
  1450 $\isarkeyword{kill}$ command aborts the current history node altogether,
  1451 discontinuing a proof or even the whole theory.  This operation is \emph{not}
  1452 undo-able.
  1453 
  1454 \begin{warn}
  1455   History commands should never be used with user interfaces such as
  1456   Proof~General \cite{proofgeneral,Aspinall:TACAS:2000}, which takes care of
  1457   stepping forth and back itself.  Interfering by manual $\isarkeyword{undo}$,
  1458   $\isarkeyword{redo}$, or even $\isarkeyword{kill}$ commands would quickly
  1459   result in utter confusion.
  1460 \end{warn}
  1461 
  1462 
  1463 \subsection{System operations}
  1464 
  1465 \indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
  1466 \indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
  1467 \begin{matharray}{rcl}
  1468   \isarcmd{cd}^* & : & \isarkeep{\cdot} \\
  1469   \isarcmd{pwd}^* & : & \isarkeep{\cdot} \\
  1470   \isarcmd{use_thy}^* & : & \isarkeep{\cdot} \\
  1471   \isarcmd{use_thy_only}^* & : & \isarkeep{\cdot} \\
  1472   \isarcmd{update_thy}^* & : & \isarkeep{\cdot} \\
  1473   \isarcmd{update_thy_only}^* & : & \isarkeep{\cdot} \\
  1474 \end{matharray}
  1475 
  1476 \begin{descr}
  1477 \item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
  1478   process.
  1479 \item [$\isarkeyword{pwd}~$] prints the current working directory.
  1480 \item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
  1481   $\isarkeyword{update_thy}$, $\isarkeyword{update_thy_only}$] load some
  1482   theory given as $name$ argument.  These commands are basically the same as
  1483   the corresponding ML functions\footnote{The ML versions also change the
  1484     implicit theory context to that of the theory loaded.}  (see also
  1485   \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar versions may
  1486   load new- and old-style theories alike.
  1487 \end{descr}
  1488 
  1489 These system commands are scarcely used when working with the Proof~General
  1490 interface, since loading of theories is done transparently.
  1491 
  1492 %%% Local Variables: 
  1493 %%% mode: latex
  1494 %%% TeX-master: "isar-ref"
  1495 %%% End: