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