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