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