doc-src/IsarRef/pure.tex
author wenzelm
Sat Oct 30 20:13:16 1999 +0200 (1999-10-30)
changeset 7981 5120a2a15d06
parent 7974 34245feb6e82
child 7987 d9aef93c0e32
permissions -rw-r--r--
tuned;
wenzelm@7046
     1
wenzelm@7895
     2
\chapter{Basic Isar Language Elements}\label{ch:pure-syntax}
wenzelm@7167
     3
wenzelm@7315
     4
Subsequently, we introduce the main part of the basic Isar theory and proof
wenzelm@7315
     5
commands as provided by Isabelle/Pure.  Chapter~\ref{ch:gen-tools} describes
wenzelm@7895
     6
further Isar elements provided by generic tools and packages (such as the
wenzelm@7895
     7
Simplifier) that are either part of Pure Isabelle or pre-loaded by most object
wenzelm@7895
     8
logics.  Chapter~\ref{ch:hol-tools} refers to actual object-logic specific
wenzelm@7895
     9
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@7981
    20
proving, which facilitates porting of legacy proof scripts.
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@7134
    30
  \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
wenzelm@7134
    31
  \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
wenzelm@7134
    32
  \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
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@7895
    48
last command in a 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@7895
    65
  the formal begin 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@7981
   131
    package to be included in {\LaTeX}.}
wenzelm@7167
   132
\end{descr}
wenzelm@7134
   133
wenzelm@7895
   134
Any markup command (except $\isarkeyword{text_raw}$) corresponds to a {\LaTeX}
wenzelm@7981
   135
macro with the name prefixed by \verb,\isamarkup, (e.g.\ 
wenzelm@7895
   136
\verb,\isamarkupchapter, for $\isarkeyword{chapter}$). The \railqtoken{text}
wenzelm@7981
   137
argument is passed to that macro unchanged, i.e.\ further {\LaTeX} commands
wenzelm@7981
   138
may be included here as well.
wenzelm@7895
   139
wenzelm@7981
   140
\medskip Additional markup commands are available for proofs (see
wenzelm@7895
   141
\S\ref{sec:markup-prf}).  Also note that the $\isarkeyword{header}$
wenzelm@7895
   142
declaration (see \S\ref{sec:begin-thy}) admits to insert document markup
wenzelm@7895
   143
elements just preceding the actual theory definition.
wenzelm@7895
   144
wenzelm@7134
   145
wenzelm@7135
   146
\subsection{Type classes and sorts}\label{sec:classes}
wenzelm@7134
   147
wenzelm@7134
   148
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
wenzelm@7134
   149
\begin{matharray}{rcl}
wenzelm@7134
   150
  \isarcmd{classes} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   151
  \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   152
  \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   153
\end{matharray}
wenzelm@7134
   154
wenzelm@7134
   155
\begin{rail}
wenzelm@7167
   156
  'classes' (classdecl comment? +)
wenzelm@7134
   157
  ;
wenzelm@7134
   158
  'classrel' nameref '<' nameref comment?
wenzelm@7134
   159
  ;
wenzelm@7134
   160
  'defaultsort' sort comment?
wenzelm@7134
   161
  ;
wenzelm@7134
   162
\end{rail}
wenzelm@7134
   163
wenzelm@7167
   164
\begin{descr}
wenzelm@7335
   165
\item [$\isarkeyword{classes}~c<\vec c$] declares class $c$ to be a subclass
wenzelm@7335
   166
  of existing classes $\vec c$.  Cyclic class structures are ruled out.
wenzelm@7134
   167
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
wenzelm@7134
   168
  existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
wenzelm@7895
   169
  $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way to
wenzelm@7175
   170
  introduce proven class relations.
wenzelm@7134
   171
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
wenzelm@7895
   172
  any type variables given without sort constraints.  Usually, the default
wenzelm@7134
   173
  sort would be only changed when defining new logics.
wenzelm@7167
   174
\end{descr}
wenzelm@7134
   175
wenzelm@7134
   176
wenzelm@7315
   177
\subsection{Primitive types and type abbreviations}\label{sec:types-pure}
wenzelm@7134
   178
wenzelm@7134
   179
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
wenzelm@7134
   180
\begin{matharray}{rcl}
wenzelm@7134
   181
  \isarcmd{types} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   182
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   183
  \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   184
  \isarcmd{arities} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   185
\end{matharray}
wenzelm@7134
   186
wenzelm@7134
   187
\begin{rail}
wenzelm@7134
   188
  'types' (typespec '=' type infix? comment? +)
wenzelm@7134
   189
  ;
wenzelm@7134
   190
  'typedecl' typespec infix? comment?
wenzelm@7134
   191
  ;
wenzelm@7134
   192
  'nonterminals' (name +) comment?
wenzelm@7134
   193
  ;
wenzelm@7134
   194
  'arities' (nameref '::' arity comment? +)
wenzelm@7134
   195
  ;
wenzelm@7134
   196
\end{rail}
wenzelm@7134
   197
wenzelm@7167
   198
\begin{descr}
wenzelm@7335
   199
\item [$\TYPES~(\vec\alpha)t = \tau$] introduces \emph{type synonym}
wenzelm@7134
   200
  $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
wenzelm@7134
   201
  as are available in Isabelle/HOL for example, type synonyms are just purely
wenzelm@7895
   202
  syntactic abbreviations without any logical significance.  Internally, type
wenzelm@7981
   203
  synonyms are fully expanded.
wenzelm@7134
   204
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
wenzelm@7895
   205
  $t$, intended as an actual logical type.  Note that object-logics such as
wenzelm@7895
   206
  Isabelle/HOL override $\isarkeyword{typedecl}$ by their own version.
wenzelm@7175
   207
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
wenzelm@7175
   208
  $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
wenzelm@7175
   209
  Isabelle's inner syntax of terms or types.
wenzelm@7335
   210
\item [$\isarkeyword{arities}~t::(\vec s)s$] augments Isabelle's order-sorted
wenzelm@7335
   211
  signature of types by new type constructor arities.  This is done
wenzelm@7335
   212
  axiomatically!  The $\isarkeyword{instance}$ command (see
wenzelm@7895
   213
  \S\ref{sec:axclass}) provides a way to introduce proven type arities.
wenzelm@7167
   214
\end{descr}
wenzelm@7134
   215
wenzelm@7134
   216
wenzelm@7981
   217
\subsection{Constants and simple definitions}\label{sec:consts}
wenzelm@7134
   218
wenzelm@7175
   219
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
wenzelm@7134
   220
\begin{matharray}{rcl}
wenzelm@7134
   221
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   222
  \isarcmd{defs} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   223
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   224
\end{matharray}
wenzelm@7134
   225
wenzelm@7134
   226
\begin{rail}
wenzelm@7134
   227
  'consts' (constdecl +)
wenzelm@7134
   228
  ;
wenzelm@7608
   229
  'defs' (axmdecl prop comment? +)
wenzelm@7134
   230
  ;
wenzelm@7134
   231
  'constdefs' (constdecl prop comment? +)
wenzelm@7134
   232
  ;
wenzelm@7134
   233
wenzelm@7134
   234
  constdecl: name '::' type mixfix? comment?
wenzelm@7134
   235
  ;
wenzelm@7134
   236
\end{rail}
wenzelm@7134
   237
wenzelm@7167
   238
\begin{descr}
wenzelm@7335
   239
\item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
wenzelm@7335
   240
  scheme $\sigma$.  The optional mixfix annotations may attach concrete syntax
wenzelm@7895
   241
  to the constants declared.
wenzelm@7335
   242
\item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
wenzelm@7335
   243
  existing constant.  See \cite[\S6]{isabelle-ref} for more details on the
wenzelm@7335
   244
  form of equations admitted as constant definitions.
wenzelm@7335
   245
\item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
wenzelm@7335
   246
  definitions of constants, using canonical name $c_def$ for the definitional
wenzelm@7335
   247
  axiom.
wenzelm@7167
   248
\end{descr}
wenzelm@7134
   249
wenzelm@7134
   250
wenzelm@7981
   251
\subsection{Syntax and translations}\label{sec:syn-trans}
wenzelm@7134
   252
wenzelm@7134
   253
\indexisarcmd{syntax}\indexisarcmd{translations}
wenzelm@7134
   254
\begin{matharray}{rcl}
wenzelm@7134
   255
  \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   256
  \isarcmd{translations} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   257
\end{matharray}
wenzelm@7134
   258
wenzelm@7134
   259
\begin{rail}
wenzelm@7134
   260
  'syntax' ('(' name 'output'? ')')? (constdecl +)
wenzelm@7134
   261
  ;
wenzelm@7134
   262
  'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
wenzelm@7134
   263
  ;
wenzelm@7134
   264
  transpat: ('(' nameref ')')? string
wenzelm@7134
   265
  ;
wenzelm@7134
   266
\end{rail}
wenzelm@7134
   267
wenzelm@7167
   268
\begin{descr}
wenzelm@7175
   269
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
wenzelm@7175
   270
  except that the actual logical signature extension is omitted.  Thus the
wenzelm@7175
   271
  context free grammar of Isabelle's inner syntax may be augmented in
wenzelm@7335
   272
  arbitrary ways, independently of the logic.  The $mode$ argument refers to
wenzelm@7335
   273
  the print mode that the grammar rules belong; unless there is the
wenzelm@7335
   274
  \texttt{output} flag given, all productions are added both to the input and
wenzelm@7335
   275
  output grammar.
wenzelm@7175
   276
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
wenzelm@7981
   277
  rules (i.e.\ \emph{macros}): parse~/ print rules (\texttt{==}), parse rules
wenzelm@7895
   278
  (\texttt{=>}), or print rules (\texttt{<=}).  Translation patterns may be
wenzelm@7895
   279
  prefixed by the syntactic category to be used for parsing; the default is
wenzelm@7134
   280
  \texttt{logic}.
wenzelm@7167
   281
\end{descr}
wenzelm@7134
   282
wenzelm@7134
   283
wenzelm@7134
   284
\subsection{Axioms and theorems}
wenzelm@7134
   285
wenzelm@7134
   286
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
wenzelm@7134
   287
\begin{matharray}{rcl}
wenzelm@7134
   288
  \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   289
  \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   290
  \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   291
\end{matharray}
wenzelm@7134
   292
wenzelm@7134
   293
\begin{rail}
wenzelm@7135
   294
  'axioms' (axmdecl prop comment? +)
wenzelm@7134
   295
  ;
wenzelm@7134
   296
  ('theorems' | 'lemmas') thmdef? thmrefs
wenzelm@7134
   297
  ;
wenzelm@7134
   298
\end{rail}
wenzelm@7134
   299
wenzelm@7167
   300
\begin{descr}
wenzelm@7335
   301
\item [$\isarkeyword{axioms}~a: \phi$] introduces arbitrary statements as
wenzelm@7895
   302
  axioms of the meta-logic.  In fact, axioms are ``axiomatic theorems'', and
wenzelm@7895
   303
  may be referred later just as any other theorem.
wenzelm@7134
   304
  
wenzelm@7134
   305
  Axioms are usually only introduced when declaring new logical systems.
wenzelm@7175
   306
  Everyday work is typically done the hard way, with proper definitions and
wenzelm@7134
   307
  actual theorems.
wenzelm@7335
   308
\item [$\isarkeyword{theorems}~a = \vec b$] stores lists of existing theorems.
wenzelm@7981
   309
  Typical applications would also involve attributes, to augment the
wenzelm@7335
   310
  Simplifier context, for example.
wenzelm@7134
   311
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
wenzelm@7134
   312
  tags the results as ``lemma''.
wenzelm@7167
   313
\end{descr}
wenzelm@7134
   314
wenzelm@7134
   315
wenzelm@7167
   316
\subsection{Name spaces}
wenzelm@7134
   317
wenzelm@7167
   318
\indexisarcmd{global}\indexisarcmd{local}
wenzelm@7134
   319
\begin{matharray}{rcl}
wenzelm@7134
   320
  \isarcmd{global} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   321
  \isarcmd{local} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   322
\end{matharray}
wenzelm@7134
   323
wenzelm@7895
   324
Isabelle organizes any kind of name declarations (of types, constants,
wenzelm@7895
   325
theorems etc.)  by hierarchically structured name spaces.  Normally the user
wenzelm@7895
   326
never has to control the behavior of name space entry by hand, yet the
wenzelm@7895
   327
following commands provide some way to do so.
wenzelm@7175
   328
wenzelm@7167
   329
\begin{descr}
wenzelm@7167
   330
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
wenzelm@7167
   331
  name declaration mode.  Initially, theories start in $\isarkeyword{local}$
wenzelm@7167
   332
  mode, causing all names to be automatically qualified by the theory name.
wenzelm@7895
   333
  Changing this to $\isarkeyword{global}$ causes all names to be declared
wenzelm@7895
   334
  without the theory prefix, until $\isarkeyword{local}$ is declared again.
wenzelm@7167
   335
\end{descr}
wenzelm@7134
   336
wenzelm@7134
   337
wenzelm@7167
   338
\subsection{Incorporating ML code}\label{sec:ML}
wenzelm@7134
   339
wenzelm@7895
   340
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{ML-setup}\indexisarcmd{setup}
wenzelm@7134
   341
\begin{matharray}{rcl}
wenzelm@7134
   342
  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134
   343
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7895
   344
  \isarcmd{ML_setup} & : & \isartrans{theory}{theory} \\
wenzelm@7175
   345
  \isarcmd{setup} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   346
\end{matharray}
wenzelm@7134
   347
wenzelm@7895
   348
\railalias{MLsetup}{ML\_setup}
wenzelm@7895
   349
\railterm{MLsetup}
wenzelm@7895
   350
wenzelm@7134
   351
\begin{rail}
wenzelm@7134
   352
  'use' name
wenzelm@7134
   353
  ;
wenzelm@7895
   354
  ('ML' | MLsetup | 'setup') text
wenzelm@7134
   355
  ;
wenzelm@7134
   356
\end{rail}
wenzelm@7134
   357
wenzelm@7167
   358
\begin{descr}
wenzelm@7175
   359
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
wenzelm@7466
   360
  The current theory context (if present) is passed down to the ML session,
wenzelm@7981
   361
  but may not be modified.  Furthermore, the file name is checked with the
wenzelm@7466
   362
  $\isarkeyword{files}$ dependency declaration given in the theory header (see
wenzelm@7466
   363
  also \S\ref{sec:begin-thy}).
wenzelm@7466
   364
  
wenzelm@7895
   365
\item [$\isarkeyword{ML}~text$] executes ML commands from $text$.  The theory
wenzelm@7895
   366
  context is passed in the same way as for $\isarkeyword{use}$.
wenzelm@7895
   367
  
wenzelm@7895
   368
\item [$\isarkeyword{ML_setup}~text$] executes ML commands from $text$.  The
wenzelm@7895
   369
  theory context is passed down to the ML session, and fetched back
wenzelm@7895
   370
  afterwards.  Thus $text$ may actually change the theory as a side effect.
wenzelm@7895
   371
  
wenzelm@7167
   372
\item [$\isarkeyword{setup}~text$] changes the current theory context by
wenzelm@7981
   373
  applying setup functions from $text$, which refers to an ML expression of
wenzelm@7981
   374
  type $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the
wenzelm@7981
   375
  canonical way to initialize object-logic specific tools and packages written
wenzelm@7981
   376
  in ML.
wenzelm@7167
   377
\end{descr}
wenzelm@7134
   378
wenzelm@7134
   379
wenzelm@7981
   380
%FIXME remove!?
wenzelm@7981
   381
%\subsection{Syntax translation functions}
wenzelm@7134
   382
wenzelm@7981
   383
%\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
wenzelm@7981
   384
%\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
wenzelm@7981
   385
%\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
wenzelm@7981
   386
%\begin{matharray}{rcl}
wenzelm@7981
   387
%  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7981
   388
%  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7981
   389
%  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7981
   390
%  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7981
   391
%  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7981
   392
%  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7981
   393
%\end{matharray}
wenzelm@7134
   394
wenzelm@7981
   395
%Syntax translation functions written in ML admit almost arbitrary
wenzelm@7981
   396
%manipulations of Isabelle's inner syntax.  Any of the above commands have a
wenzelm@7981
   397
%single \railqtoken{text} argument that refers to an ML expression of
wenzelm@7981
   398
%appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
wenzelm@7981
   399
%transformations.
wenzelm@7134
   400
wenzelm@7134
   401
wenzelm@7134
   402
\subsection{Oracles}
wenzelm@7134
   403
wenzelm@7134
   404
\indexisarcmd{oracle}
wenzelm@7134
   405
\begin{matharray}{rcl}
wenzelm@7134
   406
  \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   407
\end{matharray}
wenzelm@7134
   408
wenzelm@7175
   409
Oracles provide an interface to external reasoning systems, without giving up
wenzelm@7175
   410
control completely --- each theorem carries a derivation object recording any
wenzelm@7175
   411
oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
wenzelm@7175
   412
wenzelm@7134
   413
\begin{rail}
wenzelm@7134
   414
  'oracle' name '=' text comment?
wenzelm@7134
   415
  ;
wenzelm@7134
   416
\end{rail}
wenzelm@7134
   417
wenzelm@7167
   418
\begin{descr}
wenzelm@7175
   419
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
wenzelm@7315
   420
  function $text$, which has to be of type $Sign\mathord.sg \times
wenzelm@7335
   421
  Object\mathord.T \to term$.
wenzelm@7167
   422
\end{descr}
wenzelm@7134
   423
wenzelm@7134
   424
wenzelm@7134
   425
\section{Proof commands}
wenzelm@7134
   426
wenzelm@7315
   427
Proof commands provide transitions of Isar/VM machine configurations, which
wenzelm@7315
   428
are block-structured, consisting of a stack of nodes with three main
wenzelm@7335
   429
components: logical proof context, current facts, and open goals.  Isar/VM
wenzelm@7335
   430
transitions are \emph{typed} according to the following three three different
wenzelm@7335
   431
modes of operation:
wenzelm@7167
   432
\begin{descr}
wenzelm@7167
   433
\item [$proof(prove)$] means that a new goal has just been stated that is now
wenzelm@7167
   434
  to be \emph{proven}; the next command may refine it by some proof method
wenzelm@7895
   435
  (read: tactic), and enter a sub-proof to establish the actual result.
wenzelm@7167
   436
\item [$proof(state)$] is like an internal theory mode: the context may be
wenzelm@7175
   437
  augmented by \emph{stating} additional assumptions, intermediate result etc.
wenzelm@7895
   438
\item [$proof(chain)$] is intermediate between $proof(state)$ and
wenzelm@7458
   439
  $proof(prove)$: existing facts (i.e.\ the contents of $this$) have been just
wenzelm@7895
   440
  picked up in order to be used when refining the goal claimed next.
wenzelm@7167
   441
\end{descr}
wenzelm@7134
   442
wenzelm@7167
   443
wenzelm@7895
   444
\subsection{Proof markup commands}\label{sec:markup-prf}
wenzelm@7167
   445
wenzelm@7895
   446
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}
wenzelm@7895
   447
\indexisarcmd{txt}\indexisarcmd{txt-raw}
wenzelm@7134
   448
\begin{matharray}{rcl}
wenzelm@7167
   449
  \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   450
  \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   451
  \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   452
  \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7895
   453
  \isarcmd{txt_raw} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   454
\end{matharray}
wenzelm@7134
   455
wenzelm@7895
   456
These markup commands for proof mode closely correspond to the ones of theory
wenzelm@7895
   457
mode (see \S\ref{sec:markup-thy}).  Note that $\isarkeyword{txt_raw}$ is
wenzelm@7895
   458
special in the same way as $\isarkeyword{text_raw}$.
wenzelm@7895
   459
wenzelm@7895
   460
\railalias{txtraw}{txt\_raw}
wenzelm@7895
   461
\railterm{txtraw}
wenzelm@7175
   462
wenzelm@7134
   463
\begin{rail}
wenzelm@7895
   464
  ('sect' | 'subsect' | 'subsubsect' | 'txt' | txtraw) text
wenzelm@7134
   465
  ;
wenzelm@7134
   466
\end{rail}
wenzelm@7134
   467
wenzelm@7134
   468
wenzelm@7315
   469
\subsection{Proof context}\label{sec:proof-context}
wenzelm@7134
   470
wenzelm@7315
   471
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}
wenzelm@7134
   472
\begin{matharray}{rcl}
wenzelm@7134
   473
  \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   474
  \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   475
  \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   476
  \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   477
\end{matharray}
wenzelm@7134
   478
wenzelm@7315
   479
The logical proof context consists of fixed variables and assumptions.  The
wenzelm@7315
   480
former closely correspond to Skolem constants, or meta-level universal
wenzelm@7315
   481
quantification as provided by the Isabelle/Pure logical framework.
wenzelm@7315
   482
Introducing some \emph{arbitrary, but fixed} variable via $\FIX x$ results in
wenzelm@7319
   483
a local object that may be used in the subsequent proof as any other variable
wenzelm@7895
   484
or constant.  Furthermore, any result $\edrv \phi[x]$ exported from the
wenzelm@7895
   485
current context will be universally closed wrt.\ $x$ at the outermost level:
wenzelm@7895
   486
$\edrv \All x \phi$; this is expressed using Isabelle's meta-variables.
wenzelm@7315
   487
wenzelm@7315
   488
Similarly, introducing some assumption $\chi$ has two effects.  On the one
wenzelm@7315
   489
hand, a local theorem is created that may be used as a fact in subsequent
wenzelm@7895
   490
proof steps.  On the other hand, any result $\chi \drv \phi$ exported from the
wenzelm@7895
   491
context becomes conditional wrt.\ the assumption: $\edrv \chi \Imp \phi$.
wenzelm@7895
   492
Thus, solving an enclosing goal using such a result would basically introduce
wenzelm@7895
   493
a new subgoal stemming from the assumption.  How this situation is handled
wenzelm@7895
   494
depends on the actual version of assumption command used: while $\ASSUMENAME$
wenzelm@7895
   495
insists on solving the subgoal by unification with some premise of the goal,
wenzelm@7895
   496
$\PRESUMENAME$ leaves the subgoal unchanged in order to be proved later by the
wenzelm@7895
   497
user.
wenzelm@7315
   498
wenzelm@7319
   499
Local definitions, introduced by $\DEF{}{x \equiv t}$, are achieved by
wenzelm@7319
   500
combining $\FIX x$ with another kind of assumption that causes any
wenzelm@7895
   501
hypothetical equation $x \equiv t$ to be eliminated by reflexivity.  Thus,
wenzelm@7895
   502
exporting some result $x \equiv t \drv \phi[x]$ yields $\edrv \phi[t]$.
wenzelm@7175
   503
wenzelm@7134
   504
\begin{rail}
wenzelm@7431
   505
  'fix' (vars + 'and') comment?
wenzelm@7134
   506
  ;
wenzelm@7315
   507
  ('assume' | 'presume') (assm comment? + 'and')
wenzelm@7134
   508
  ;
wenzelm@7175
   509
  'def' thmdecl? \\ var '==' term termpat? comment?
wenzelm@7134
   510
  ;
wenzelm@7134
   511
wenzelm@7134
   512
  var: name ('::' type)?
wenzelm@7134
   513
  ;
wenzelm@7458
   514
  vars: (name+) ('::' type)?
wenzelm@7431
   515
  ;
wenzelm@7315
   516
  assm: thmdecl? (prop proppat? +)
wenzelm@7315
   517
  ;
wenzelm@7134
   518
\end{rail}
wenzelm@7134
   519
wenzelm@7167
   520
\begin{descr}
wenzelm@7315
   521
\item [$\FIX{x}$] introduces a local \emph{arbitrary, but fixed} variable $x$.
wenzelm@7315
   522
\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] introduce local theorems
wenzelm@7335
   523
  $\Phi$ by assumption.  Subsequent results applied to an enclosing goal
wenzelm@7895
   524
  (e.g.\ by $\SHOWNAME$) are handled as follows: $\ASSUMENAME$ expects to be
wenzelm@7335
   525
  able to unify with existing premises in the goal, while $\PRESUMENAME$
wenzelm@7335
   526
  leaves $\Phi$ as new subgoals.
wenzelm@7335
   527
  
wenzelm@7335
   528
  Several lists of assumptions may be given (separated by
wenzelm@7895
   529
  $\isarkeyword{and}$); the resulting list of current facts consists of all of
wenzelm@7895
   530
  these concatenated.
wenzelm@7315
   531
\item [$\DEF{a}{x \equiv t}$] introduces a local (non-polymorphic) definition.
wenzelm@7315
   532
  In results exported from the context, $x$ is replaced by $t$.  Basically,
wenzelm@7335
   533
  $\DEF{}{x \equiv t}$ abbreviates $\FIX{x}~\PRESUME{}{x \equiv t}$, with the
wenzelm@7335
   534
  resulting hypothetical equation solved by reflexivity.
wenzelm@7431
   535
  
wenzelm@7431
   536
  The default name for the definitional equation is $x_def$.
wenzelm@7167
   537
\end{descr}
wenzelm@7167
   538
wenzelm@7895
   539
The special name $prems$\indexisarthm{prems} refers to all assumptions of the
wenzelm@7895
   540
current context as a list of theorems.
wenzelm@7315
   541
wenzelm@7167
   542
wenzelm@7167
   543
\subsection{Facts and forward chaining}
wenzelm@7167
   544
wenzelm@7167
   545
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
wenzelm@7167
   546
\begin{matharray}{rcl}
wenzelm@7167
   547
  \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   548
  \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167
   549
  \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167
   550
  \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167
   551
\end{matharray}
wenzelm@7167
   552
wenzelm@7319
   553
New facts are established either by assumption or proof of local statements.
wenzelm@7335
   554
Any fact will usually be involved in further proofs, either as explicit
wenzelm@7335
   555
arguments of proof methods or when forward chaining towards the next goal via
wenzelm@7335
   556
$\THEN$ (and variants).  Note that the special theorem name
wenzelm@7458
   557
$this$.\indexisarthm{this} refers to the most recently established facts.
wenzelm@7167
   558
\begin{rail}
wenzelm@7167
   559
  'note' thmdef? thmrefs comment?
wenzelm@7167
   560
  ;
wenzelm@7167
   561
  'then' comment?
wenzelm@7167
   562
  ;
wenzelm@7167
   563
  ('from' | 'with') thmrefs comment?
wenzelm@7167
   564
  ;
wenzelm@7167
   565
\end{rail}
wenzelm@7167
   566
wenzelm@7167
   567
\begin{descr}
wenzelm@7175
   568
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
wenzelm@7175
   569
  as $a$.  Note that attributes may be involved as well, both on the left and
wenzelm@7175
   570
  right hand sides.
wenzelm@7167
   571
\item [$\THEN$] indicates forward chaining by the current facts in order to
wenzelm@7895
   572
  establish the goal to be claimed next.  The initial proof method invoked to
wenzelm@7895
   573
  refine that will be offered the facts to do ``anything appropriate'' (cf.\ 
wenzelm@7895
   574
  also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
wenzelm@7895
   575
  \S\ref{sec:pure-meth}) would typically do an elimination rather than an
wenzelm@7895
   576
  introduction.  Automatic methods usually insert the facts into the goal
wenzelm@7895
   577
  state before operation.
wenzelm@7335
   578
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; thus $\THEN$ is
wenzelm@7458
   579
  equivalent to $\FROM{this}$.
wenzelm@7175
   580
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
wenzelm@7175
   581
  chaining is from earlier facts together with the current ones.
wenzelm@7167
   582
\end{descr}
wenzelm@7167
   583
wenzelm@7389
   584
Basic proof methods (such as $rule$, see \S\ref{sec:pure-meth}) expect
wenzelm@7895
   585
multiple facts to be given in their proper order, corresponding to a prefix of
wenzelm@7895
   586
the premises of the rule involved.  Note that positions may be easily skipped
wenzelm@7458
   587
using a form like $\FROM{\text{\texttt{_}}~a~b}$, for example.  This involves
wenzelm@7895
   588
the trivial rule $\PROP\psi \Imp \PROP\psi$, which is bound in Isabelle/Pure
wenzelm@7895
   589
as ``\texttt{_}'' (underscore).\indexisarthm{_@\texttt{_}}
wenzelm@7389
   590
wenzelm@7167
   591
wenzelm@7167
   592
\subsection{Goal statements}
wenzelm@7167
   593
wenzelm@7167
   594
\indexisarcmd{theorem}\indexisarcmd{lemma}
wenzelm@7167
   595
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
wenzelm@7167
   596
\begin{matharray}{rcl}
wenzelm@7167
   597
  \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167
   598
  \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167
   599
  \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   600
  \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   601
  \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   602
  \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   603
\end{matharray}
wenzelm@7167
   604
wenzelm@7175
   605
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
wenzelm@7895
   606
and $\LEMMANAME$.  New local goals may be claimed within proof mode as well.
wenzelm@7895
   607
Four variants are available, indicating whether the result is meant to solve
wenzelm@7895
   608
some pending goal and whether forward chaining is employed.
wenzelm@7175
   609
wenzelm@7167
   610
\begin{rail}
wenzelm@7167
   611
  ('theorem' | 'lemma') goal
wenzelm@7167
   612
  ;
wenzelm@7167
   613
  ('have' | 'show' | 'hence' | 'thus') goal
wenzelm@7167
   614
  ;
wenzelm@7167
   615
wenzelm@7167
   616
  goal: thmdecl? proppat comment?
wenzelm@7167
   617
  ;
wenzelm@7167
   618
\end{rail}
wenzelm@7167
   619
wenzelm@7167
   620
\begin{descr}
wenzelm@7335
   621
\item [$\THEOREM{a}{\phi}$] enters proof mode with $\phi$ as main goal,
wenzelm@7895
   622
  eventually resulting in some theorem $\turn \phi$ put back into the theory.
wenzelm@7167
   623
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
wenzelm@7167
   624
  ``lemma''.
wenzelm@7335
   625
\item [$\HAVE{a}{\phi}$] claims a local goal, eventually resulting in a
wenzelm@7167
   626
  theorem with the current assumption context as hypotheses.
wenzelm@7335
   627
\item [$\SHOW{a}{\phi}$] is similar to $\HAVE{a}{\phi}$, but solves some
wenzelm@7895
   628
  pending goal with the result \emph{exported} into the corresponding context
wenzelm@7895
   629
  (cf.\ \S\ref{sec:proof-context}).
wenzelm@7895
   630
\item [$\HENCENAME$] abbreviates $\THEN~\HAVENAME$, i.e.\ claims a local goal
wenzelm@7895
   631
  to be proven by forward chaining the current facts.  Note that $\HENCENAME$
wenzelm@7895
   632
  is also equivalent to $\FROM{this}~\HAVENAME$.
wenzelm@7895
   633
\item [$\THUSNAME$] abbreviates $\THEN~\SHOWNAME$.  Note that $\THUSNAME$ is
wenzelm@7895
   634
  also equivalent to $\FROM{this}~\SHOWNAME$.
wenzelm@7167
   635
\end{descr}
wenzelm@7167
   636
wenzelm@7167
   637
wenzelm@7167
   638
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
wenzelm@7167
   639
wenzelm@7175
   640
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm@7175
   641
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm@7175
   642
\begin{matharray}{rcl}
wenzelm@7175
   643
  \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm@7175
   644
  \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm@7175
   645
  \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   646
  \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   647
  \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   648
  \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   649
\end{matharray}
wenzelm@7175
   650
wenzelm@7335
   651
Arbitrary goal refinement via tactics is considered harmful.  Consequently the
wenzelm@7335
   652
Isar framework admits proof methods to be invoked in two places only.
wenzelm@7167
   653
\begin{enumerate}
wenzelm@7175
   654
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
wenzelm@7335
   655
  goal to a number of sub-goals that are to be solved later.  Facts are passed
wenzelm@7895
   656
  to $m@1$ for forward chaining, if so indicated by $proof(chain)$ mode.
wenzelm@7167
   657
  
wenzelm@7335
   658
\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining goals
wenzelm@7335
   659
  completely.  No facts are passed to $m@2$.
wenzelm@7167
   660
\end{enumerate}
wenzelm@7167
   661
wenzelm@7335
   662
The only other proper way to affect pending goals is by $\SHOWNAME$ (or
wenzelm@7335
   663
$\THUSNAME$), which involves an explicit statement of what is to be solved.
wenzelm@7167
   664
wenzelm@7175
   665
\medskip
wenzelm@7175
   666
wenzelm@7167
   667
Also note that initial proof methods should either solve the goal completely,
wenzelm@7895
   668
or constitute some well-understood reduction to new sub-goals.  Arbitrary
wenzelm@7895
   669
automatic proof tools that are prone leave a large number of badly structured
wenzelm@7895
   670
sub-goals are no help in continuing the proof document in any intelligible
wenzelm@7895
   671
way.  A much better technique would be to $\SHOWNAME$ some non-trivial
wenzelm@7895
   672
reduction as an explicit rule, which is solved completely by some automated
wenzelm@7895
   673
method, and then applied to some pending goal.
wenzelm@7167
   674
wenzelm@7175
   675
\medskip
wenzelm@7175
   676
wenzelm@7175
   677
Unless given explicitly by the user, the default initial method is
wenzelm@7175
   678
``$default$'', which is usually set up to apply a single standard elimination
wenzelm@7458
   679
or introduction rule according to the topmost symbol involved.  There is no
wenzelm@7895
   680
separate default terminal method; in any case the final step is to solve all
wenzelm@7895
   681
remaining goals by assumption, though.
wenzelm@7167
   682
wenzelm@7167
   683
\begin{rail}
wenzelm@7167
   684
  'proof' interest? meth? comment?
wenzelm@7167
   685
  ;
wenzelm@7167
   686
  'qed' meth? comment?
wenzelm@7167
   687
  ;
wenzelm@7167
   688
  'by' meth meth? comment?
wenzelm@7167
   689
  ;
wenzelm@7167
   690
  ('.' | '..' | 'sorry') comment?
wenzelm@7167
   691
  ;
wenzelm@7167
   692
wenzelm@7167
   693
  meth: method interest?
wenzelm@7167
   694
  ;
wenzelm@7167
   695
\end{rail}
wenzelm@7167
   696
wenzelm@7167
   697
\begin{descr}
wenzelm@7335
   698
\item [$\PROOF{m@1}$] refines the goal by proof method $m@1$; facts for
wenzelm@7335
   699
  forward chaining are passed if so indicated by $proof(chain)$ mode.
wenzelm@7335
   700
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@2$ and
wenzelm@7895
   701
  concludes the sub-proof by assumption.  If the goal had been $\SHOWNAME$ (or
wenzelm@7895
   702
  $\THUSNAME$), some pending sub-goal is solved as well by the rule resulting
wenzelm@7895
   703
  from the result \emph{exported} into the enclosing goal context.  Thus
wenzelm@7895
   704
  $\QEDNAME$ may fail for two reasons: either $m@2$ fails, or the resulting
wenzelm@7895
   705
  rule does not fit to any pending goal\footnote{This includes any additional
wenzelm@7895
   706
    ``strong'' assumptions as introduced by $\ASSUMENAME$.} of the enclosing
wenzelm@7895
   707
  context.  Debugging such a situation might involve temporarily changing
wenzelm@7895
   708
  $\SHOWNAME$ into $\HAVENAME$, or weakening the local context by replacing
wenzelm@7895
   709
  some occurrences of $\ASSUMENAME$ by $\PRESUMENAME$.
wenzelm@7895
   710
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}\index{proof!terminal}; it
wenzelm@7895
   711
  abbreviates $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both
wenzelm@7895
   712
  methods.  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done
wenzelm@7895
   713
  by expanding its definition; in many cases $\PROOF{m@1}$ is already
wenzelm@7175
   714
  sufficient to see what is going wrong.
wenzelm@7895
   715
\item [``$\DDOT$''] is a \emph{default proof}\index{proof!default}; it
wenzelm@7895
   716
  abbreviates $\BY{default}$.
wenzelm@7895
   717
\item [``$\DOT$''] is a \emph{trivial proof}\index{proof!trivial}; it
wenzelm@7895
   718
  abbreviates $\BY{assumption}$.
wenzelm@7895
   719
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}\index{proof!fake};
wenzelm@7895
   720
  provided that \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$
wenzelm@7895
   721
  pretends to solve the goal without further ado.  Of course, the result is a
wenzelm@7895
   722
  fake theorem only, involving some oracle in its internal derivation object
wenzelm@7895
   723
  (this is indicated as ``$[!]$'' in the printed result).  The main
wenzelm@7895
   724
  application of $\isarkeyword{sorry}$ is to support experimentation and
wenzelm@7895
   725
  top-down proof development.
wenzelm@7167
   726
\end{descr}
wenzelm@7134
   727
wenzelm@7134
   728
wenzelm@7315
   729
\subsection{Improper proof steps}
wenzelm@7315
   730
wenzelm@7315
   731
The following commands emulate unstructured tactic scripts to some extent.
wenzelm@7315
   732
While these are anathema for writing proper Isar proof documents, they might
wenzelm@7895
   733
come in handy for interactive exploration and debugging.
wenzelm@7315
   734
wenzelm@7315
   735
\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
wenzelm@7315
   736
\begin{matharray}{rcl}
wenzelm@7315
   737
  \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7315
   738
  \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7315
   739
  \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
wenzelm@7315
   740
\end{matharray}
wenzelm@7315
   741
wenzelm@7315
   742
\railalias{thenapply}{then\_apply}
wenzelm@7315
   743
\railterm{thenapply}
wenzelm@7315
   744
wenzelm@7315
   745
\begin{rail}
wenzelm@7315
   746
  'apply' method
wenzelm@7315
   747
  ;
wenzelm@7315
   748
  thenapply method
wenzelm@7315
   749
  ;
wenzelm@7315
   750
  'back'
wenzelm@7315
   751
  ;
wenzelm@7315
   752
\end{rail}
wenzelm@7315
   753
wenzelm@7315
   754
\begin{descr}
wenzelm@7895
   755
\item [$\isarkeyword{apply}~(m)$] applies proof method $m$ in the plain old
wenzelm@7895
   756
  tactic sense.  Facts for forward chaining are reset.
wenzelm@7335
   757
\item [$\isarkeyword{then_apply}~(m)$] is similar to $\isarkeyword{apply}$,
wenzelm@7510
   758
  but keeps the goal's facts.
wenzelm@7315
   759
\item [$\isarkeyword{back}$] does back-tracking over the result sequence of
wenzelm@7389
   760
  the latest proof command.\footnote{Unlike the ML function \texttt{back}
wenzelm@7389
   761
    \cite{isabelle-ref}, the Isar command does not search upwards for further
wenzelm@7389
   762
    branch points.} Basically, any proof command may return multiple results.
wenzelm@7315
   763
\end{descr}
wenzelm@7315
   764
wenzelm@7315
   765
wenzelm@7315
   766
\subsection{Term abbreviations}\label{sec:term-abbrev}
wenzelm@7315
   767
wenzelm@7315
   768
\indexisarcmd{let}
wenzelm@7315
   769
\begin{matharray}{rcl}
wenzelm@7315
   770
  \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7315
   771
  \isarkeyword{is} & : & syntax \\
wenzelm@7315
   772
\end{matharray}
wenzelm@7315
   773
wenzelm@7315
   774
Abbreviations may be either bound by explicit $\LET{p \equiv t}$ statements,
wenzelm@7315
   775
or by annotating assumptions or goal statements ($\ASSUMENAME$, $\SHOWNAME$
wenzelm@7895
   776
etc.) with a list of patterns $\ISS{p@1 \dots}{p@n}$.  In both cases,
wenzelm@7895
   777
higher-order matching is invoked to bind extra-logical term variables, which
wenzelm@7466
   778
may be either named schematic variables of the form $\Var{x}$, or nameless
wenzelm@7466
   779
dummies ``\texttt{_}'' (underscore).\indexisarvar{_@\texttt{_}} Note that in
wenzelm@7466
   780
the $\LETNAME$ form the patterns occur on the left-hand side, while the
wenzelm@7466
   781
$\ISNAME$ patterns are in postfix position.
wenzelm@7315
   782
wenzelm@7319
   783
Term abbreviations are quite different from actual local definitions as
wenzelm@7319
   784
introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
wenzelm@7315
   785
visible within the logic as actual equations, while abbreviations disappear
wenzelm@7315
   786
during the input process just after type checking.
wenzelm@7315
   787
wenzelm@7315
   788
\begin{rail}
wenzelm@7315
   789
  'let' ((term + 'as') '=' term comment? + 'and')
wenzelm@7315
   790
  ;  
wenzelm@7315
   791
\end{rail}
wenzelm@7315
   792
wenzelm@7315
   793
The syntax of $\ISNAME$ patterns follows \railnonterm{termpat} or
wenzelm@7315
   794
\railnonterm{proppat} (see \S\ref{sec:term-pats}).
wenzelm@7315
   795
wenzelm@7315
   796
\begin{descr}
wenzelm@7315
   797
\item [$\LET{\vec p = \vec t}$] binds any text variables in patters $\vec p$
wenzelm@7315
   798
  by simultaneous higher-order matching against terms $\vec t$.
wenzelm@7315
   799
\item [$\IS{\vec p}$] resembles $\LETNAME$, but matches $\vec p$ against the
wenzelm@7315
   800
  preceding statement.  Also note that $\ISNAME$ is not a separate command,
wenzelm@7315
   801
  but part of others (such as $\ASSUMENAME$, $\HAVENAME$ etc.).
wenzelm@7315
   802
\end{descr}
wenzelm@7315
   803
wenzelm@7319
   804
A few \emph{automatic} term abbreviations\index{automatic abbreviation} for
wenzelm@7335
   805
goals and facts are available as well.  For any open goal,
wenzelm@7466
   806
$\Var{thesis_prop}$\indexisarvar{thesis-prop} refers to the full proposition
wenzelm@7466
   807
(which may be a rule), $\Var{thesis_concl}$\indexisarvar{thesis-concl} to its
wenzelm@7466
   808
(atomic) conclusion, and $\Var{thesis}$\indexisarvar{thesis} to its
wenzelm@7335
   809
object-logical statement.  The latter two abstract over any meta-level
wenzelm@7466
   810
parameters bound by $\Forall$.
wenzelm@7315
   811
wenzelm@7466
   812
Fact statements resulting from assumptions or finished goals are bound as
wenzelm@7466
   813
$\Var{this_prop}$\indexisarvar{this-prop},
wenzelm@7466
   814
$\Var{this_concl}$\indexisarvar{this-concl}, and
wenzelm@7466
   815
$\Var{this}$\indexisarvar{this}, similar to $\Var{thesis}$ above.  In case
wenzelm@7466
   816
$\Var{this}$ refers to an object-logic statement that is an application
wenzelm@7895
   817
$f(t)$, then $t$ is bound to the special text variable
wenzelm@7466
   818
``$\dots$''\indexisarvar{\dots} (three dots).  The canonical application of
wenzelm@7466
   819
this feature are calculational proofs (see \S\ref{sec:calculation}).
wenzelm@7315
   820
wenzelm@7315
   821
wenzelm@7134
   822
\subsection{Block structure}
wenzelm@7134
   823
wenzelm@7397
   824
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
wenzelm@7397
   825
\begin{matharray}{rcl}
wenzelm@7397
   826
  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7974
   827
  \BG & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7974
   828
  \EN & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7397
   829
\end{matharray}
wenzelm@7397
   830
wenzelm@7167
   831
While Isar is inherently block-structured, opening and closing blocks is
wenzelm@7167
   832
mostly handled rather casually, with little explicit user-intervention.  Any
wenzelm@7167
   833
local goal statement automatically opens \emph{two} blocks, which are closed
wenzelm@7167
   834
again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
wenzelm@7895
   835
different context within a sub-proof may be switched via $\isarkeyword{next}$,
wenzelm@7895
   836
which is just a single block-close followed by block-open again.  Thus the
wenzelm@7895
   837
effect of $\isarkeyword{next}$ is a local reset the proof
wenzelm@7895
   838
context.\footnote{There is no goal focus involved here!}
wenzelm@7167
   839
wenzelm@7175
   840
For slightly more advanced applications, there are explicit block parentheses
wenzelm@7895
   841
as well.  These typically achieve a stronger forward style of reasoning.
wenzelm@7167
   842
wenzelm@7167
   843
\begin{descr}
wenzelm@7167
   844
\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
wenzelm@7895
   845
  resetting the local context to the initial one.
wenzelm@7167
   846
\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
wenzelm@7895
   847
  close blocks.  Any current facts pass through ``$\isarkeyword{\{\{}$''
wenzelm@7895
   848
  unchanged, while ``$\isarkeyword{\}\}}$'' causes any result to be
wenzelm@7895
   849
  \emph{exported} into the enclosing context.  Thus fixed variables are
wenzelm@7895
   850
  generalized, assumptions discharged, and local definitions unfolded (cf.\ 
wenzelm@7895
   851
  \S\ref{sec:proof-context}).  There is no difference of $\ASSUMENAME$ and
wenzelm@7895
   852
  $\PRESUMENAME$ in this mode of forward reasoning --- in contrast to plain
wenzelm@7895
   853
  backward reasoning with the result exported at $\SHOWNAME$ time.
wenzelm@7167
   854
\end{descr}
wenzelm@7134
   855
wenzelm@7134
   856
wenzelm@7134
   857
\section{Other commands}
wenzelm@7134
   858
wenzelm@7134
   859
\subsection{Diagnostics}
wenzelm@7134
   860
wenzelm@7974
   861
\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
wenzelm@7134
   862
\begin{matharray}{rcl}
wenzelm@7974
   863
  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   864
  \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   865
  \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
wenzelm@7974
   866
  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   867
\end{matharray}
wenzelm@7134
   868
wenzelm@7335
   869
These commands are not part of the actual Isabelle/Isar syntax, but assist
wenzelm@7335
   870
interactive development.  Also note that $undo$ does not apply here, since the
wenzelm@7335
   871
theory or proof configuration is not changed.
wenzelm@7335
   872
wenzelm@7134
   873
\begin{rail}
wenzelm@7974
   874
  'thm' thmrefs
wenzelm@7134
   875
  ;
wenzelm@7134
   876
  'term' term
wenzelm@7134
   877
  ;
wenzelm@7134
   878
  'prop' prop
wenzelm@7134
   879
  ;
wenzelm@7974
   880
  'typ' type
wenzelm@7134
   881
  ;
wenzelm@7134
   882
\end{rail}
wenzelm@7134
   883
wenzelm@7167
   884
\begin{descr}
wenzelm@7974
   885
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
wenzelm@7974
   886
  theory or proof context.  Note that any attributes included in the theorem
wenzelm@7974
   887
  specifications are applied to a temporary context derived from the current
wenzelm@7974
   888
  theory or proof; the result is discarded, i.e.\ attributes involved in
wenzelm@7974
   889
  $thms$ do not have any permanent effect.
wenzelm@7895
   890
\item [$\isarkeyword{term}~t$, $\isarkeyword{prop}~\phi$] read, type-checks
wenzelm@7895
   891
  and print terms or propositions according to the current theory or proof
wenzelm@7895
   892
  context; the inferred type of $t$ is output as well.  Note that these
wenzelm@7895
   893
  commands are also useful in inspecting the current environment of term
wenzelm@7895
   894
  abbreviations.
wenzelm@7974
   895
\item [$\isarkeyword{typ}~\tau$] reads and prints types of the meta-logic
wenzelm@7974
   896
  according to the current theory or proof context.
wenzelm@7167
   897
\end{descr}
wenzelm@7134
   898
wenzelm@7134
   899
wenzelm@7134
   900
\subsection{System operations}
wenzelm@7134
   901
wenzelm@7167
   902
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
wenzelm@7167
   903
\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
wenzelm@7134
   904
\begin{matharray}{rcl}
wenzelm@7134
   905
  \isarcmd{cd} & : & \isarkeep{\cdot} \\
wenzelm@7134
   906
  \isarcmd{pwd} & : & \isarkeep{\cdot} \\
wenzelm@7134
   907
  \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134
   908
  \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134
   909
  \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134
   910
  \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134
   911
\end{matharray}
wenzelm@7134
   912
wenzelm@7167
   913
\begin{descr}
wenzelm@7134
   914
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
wenzelm@7134
   915
  process.
wenzelm@7134
   916
\item [$\isarkeyword{pwd}~$] prints the current working directory.
wenzelm@7175
   917
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
wenzelm@7175
   918
  $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
wenzelm@7895
   919
  theory given as $name$ argument.  These commands are basically the same as
wenzelm@7895
   920
  the corresponding ML functions\footnote{For historic reasons, the original
wenzelm@7895
   921
    ML versions also change the theory context to that of the theory loaded.}
wenzelm@7895
   922
  (see also \cite[\S1,\S6]{isabelle-ref}).  Note that both the ML and Isar
wenzelm@7895
   923
  versions may load new- and old-style theories alike.
wenzelm@7167
   924
\end{descr}
wenzelm@7134
   925
wenzelm@7895
   926
Note that these system commands are scarcely used when working with the
wenzelm@7895
   927
Proof~General interface, since loading of theories is done fully
wenzelm@7895
   928
transparently.
wenzelm@7134
   929
wenzelm@7046
   930
%%% Local Variables: 
wenzelm@7046
   931
%%% mode: latex
wenzelm@7046
   932
%%% TeX-master: "isar-ref"
wenzelm@7046
   933
%%% End: