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