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