doc-src/IsarRef/pure.tex
author wenzelm
Wed Aug 04 18:20:24 1999 +0200 (1999-08-04)
changeset 7175 8263d0b50e12
parent 7167 0b2e3ef1d8f4
child 7315 76a39a3784b5
permissions -rw-r--r--
tuned;
wenzelm@7046
     1
wenzelm@7167
     2
\chapter{Basic Isar elements}
wenzelm@7167
     3
wenzelm@7167
     4
Subsequently, we introduce most of the basic Isar theory and proof commands as
wenzelm@7167
     5
provided by Isabelle/Pure.  Chapter~\ref{ch:gen-tools} describes further Isar
wenzelm@7167
     6
elements as provided by generic tools and packages that are either part of
wenzelm@7175
     7
Pure Isabelle, or preloaded by most object logics (such as the Simplifier).
wenzelm@7167
     8
See chapter~\ref{ch:hol-tools} for actual object-logic specific elements (for
wenzelm@7167
     9
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@7175
    14
\emph{improper commands} (indicated by $^*$).  Some proof methods and
wenzelm@7175
    15
attributes introduced later may be classified as improper as well.  Improper
wenzelm@7175
    16
Isar language elements might be helpful when developing proof documents, while
wenzelm@7175
    17
their use is strongly discouraged for the final version.  Typical examples are
wenzelm@7175
    18
diagnostic commands that print terms or theorems according to the current
wenzelm@7175
    19
context; other commands even emulate old-style tactical theorem proving, which
wenzelm@7175
    20
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@7134
    27
\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
wenzelm@7134
    28
\begin{matharray}{rcl}
wenzelm@7134
    29
  \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
wenzelm@7134
    30
  \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
wenzelm@7134
    31
  \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
wenzelm@7134
    32
\end{matharray}
wenzelm@7134
    33
wenzelm@7134
    34
Isabelle/Isar ``new-style'' theories are either defined via theory files or
wenzelm@7167
    35
interactively.  Both actual theory specifications and proofs are handled
wenzelm@7175
    36
uniformly --- occasionally definitional mechanisms even require some manual
wenzelm@7175
    37
proof.  In contrast, ``old-style'' Isabelle theories support batch processing
wenzelm@7175
    38
only, with the proof scripts collected in separate ML files.
wenzelm@7134
    39
wenzelm@7134
    40
The first command of any theory has to be $\THEORY$, starting a new theory
wenzelm@7175
    41
based on the merge of existing ones.  The theory context may be also changed
wenzelm@7175
    42
by $\CONTEXT$ without creating a new theory.  In both cases, $\END$ concludes
wenzelm@7175
    43
the theory development; it has to be the very last command of any proper
wenzelm@7175
    44
theory file.
wenzelm@7134
    45
wenzelm@7134
    46
\begin{rail}
wenzelm@7134
    47
  'theory' name '=' (name + '+') filespecs? ':'
wenzelm@7134
    48
  ;
wenzelm@7134
    49
  'context' name
wenzelm@7134
    50
  ;
wenzelm@7134
    51
  'end'
wenzelm@7134
    52
  ;;
wenzelm@7134
    53
wenzelm@7167
    54
  filespecs: 'files' ((name | parname) +);
wenzelm@7134
    55
\end{rail}
wenzelm@7134
    56
wenzelm@7167
    57
\begin{descr}
wenzelm@7134
    58
\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
wenzelm@7175
    59
  existing ones $B@1 + \cdots + B@n$.  Isabelle's theory loader system ensures
wenzelm@7175
    60
  that any of the base theories are properly loaded (and fully up-to-date when
wenzelm@7175
    61
  $\THEORY$ is executed interactively).  The optional $\isarkeyword{files}$
wenzelm@7175
    62
  specification declares additional dependencies on ML files.  Unless put in
wenzelm@7175
    63
  parentheses, any file will be loaded immediately via $\isarcmd{use}$ (see
wenzelm@7175
    64
  also \S\ref{sec:ML}).
wenzelm@7134
    65
  
wenzelm@7167
    66
\item [$\CONTEXT~B$] enters an existing theory context $B$, basically in
wenzelm@7134
    67
  read-only mode, so only a limited set of commands may be performed.  Just as
wenzelm@7134
    68
  for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
wenzelm@7175
    69
  
wenzelm@7167
    70
\item [$\END$] concludes the current theory definition or context switch.
wenzelm@7175
    71
  Note that this command cannot be undone, instead the theory definition
wenzelm@7175
    72
  itself has to be retracted.
wenzelm@7167
    73
\end{descr}
wenzelm@7134
    74
wenzelm@7134
    75
wenzelm@7167
    76
\subsection{Formal comments}\label{sec:formal-cmt-thy}
wenzelm@7134
    77
wenzelm@7167
    78
\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{section}\indexisarcmd{subsection}
wenzelm@7167
    79
\indexisarcmd{subsubsection}\indexisarcmd{text}
wenzelm@7134
    80
\begin{matharray}{rcl}
wenzelm@7134
    81
  \isarcmd{title} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    82
  \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
wenzelm@7167
    83
  \isarcmd{section} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    84
  \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    85
  \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    86
  \isarcmd{text} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    87
\end{matharray}
wenzelm@7134
    88
wenzelm@7167
    89
There are several commands to include \emph{formal comments} in theory
wenzelm@7167
    90
specification (a few more are available for proofs, see
wenzelm@7167
    91
\S\ref{sec:formal-cmt-prf}).  In contrast to source-level comments
wenzelm@7134
    92
\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
wenzelm@7134
    93
given as formal comment is meant to be part of the actual document.
wenzelm@7134
    94
Consequently, it would be included in the final printed version.
wenzelm@7134
    95
wenzelm@7134
    96
Apart from plain prose, formal comments may also refer to logical entities of
wenzelm@7175
    97
the theory context (types, terms, theorems etc.).  Proper processing of the
wenzelm@7175
    98
text would then include some further consistency checks with the items
wenzelm@7175
    99
declared in the current theory, e.g.\ type-checking of included
wenzelm@7175
   100
terms.\footnote{The current version of Isabelle/Isar does not process formal
wenzelm@7134
   101
  comments in any such way.  This will be available as part of the automatic
wenzelm@7175
   102
  theory and proof document preparation system (using (PDF){\LaTeX}) that is
wenzelm@7134
   103
  planned for the near future.}
wenzelm@7134
   104
wenzelm@7134
   105
\begin{rail}
wenzelm@7134
   106
  'title' text text? text?
wenzelm@7134
   107
  ;
wenzelm@7167
   108
  ('chapter' | 'section' | 'subsection' | 'subsubsection' | 'text') text
wenzelm@7134
   109
  ;
wenzelm@7134
   110
\end{rail}
wenzelm@7134
   111
wenzelm@7167
   112
\begin{descr}
wenzelm@7134
   113
\item [$\isarkeyword{title}~title~author~date$] specifies the document title
wenzelm@7175
   114
  just as in typical {\LaTeX} documents.
wenzelm@7167
   115
\item [$\isarkeyword{chapter}~text$, $\isarkeyword{section}~text$,
wenzelm@7175
   116
  $\isarkeyword{subsection}~text$, and $\isarkeyword{subsubsection}~text$]
wenzelm@7175
   117
  specify chapter and section headings.
wenzelm@7134
   118
\item [$\TEXT~text$] specifies an actual body of prose text, including
wenzelm@7175
   119
  references to formal entities (the latter feature is not yet exploited in
wenzelm@7175
   120
  any way).
wenzelm@7167
   121
\end{descr}
wenzelm@7134
   122
wenzelm@7134
   123
wenzelm@7135
   124
\subsection{Type classes and sorts}\label{sec:classes}
wenzelm@7134
   125
wenzelm@7134
   126
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
wenzelm@7134
   127
\begin{matharray}{rcl}
wenzelm@7134
   128
  \isarcmd{classes} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   129
  \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   130
  \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   131
\end{matharray}
wenzelm@7134
   132
wenzelm@7134
   133
\begin{rail}
wenzelm@7167
   134
  'classes' (classdecl comment? +)
wenzelm@7134
   135
  ;
wenzelm@7134
   136
  'classrel' nameref '<' nameref comment?
wenzelm@7134
   137
  ;
wenzelm@7134
   138
  'defaultsort' sort comment?
wenzelm@7134
   139
  ;
wenzelm@7134
   140
\end{rail}
wenzelm@7134
   141
wenzelm@7167
   142
\begin{descr}
wenzelm@7175
   143
\item [$\isarkeyword{classes}~c<\vec c ~\dots$] declares class $c$ to be a
wenzelm@7175
   144
  subclass of existing classes $\vec c$.  Cyclic class structures are ruled
wenzelm@7175
   145
  out.
wenzelm@7134
   146
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
wenzelm@7134
   147
  existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
wenzelm@7175
   148
  $\isarkeyword{instance}$ command (see \S\ref{sec:axclass}) provides a way
wenzelm@7175
   149
  introduce proven class relations.
wenzelm@7134
   150
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
wenzelm@7175
   151
  any type variables input without sort constraints.  Usually, the default
wenzelm@7134
   152
  sort would be only changed when defining new logics.
wenzelm@7167
   153
\end{descr}
wenzelm@7134
   154
wenzelm@7134
   155
wenzelm@7141
   156
\subsection{Types}\label{sec:types-pure}
wenzelm@7134
   157
wenzelm@7134
   158
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
wenzelm@7134
   159
\begin{matharray}{rcl}
wenzelm@7134
   160
  \isarcmd{types} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   161
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   162
  \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   163
  \isarcmd{arities} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   164
\end{matharray}
wenzelm@7134
   165
wenzelm@7134
   166
\begin{rail}
wenzelm@7134
   167
  'types' (typespec '=' type infix? comment? +)
wenzelm@7134
   168
  ;
wenzelm@7134
   169
  'typedecl' typespec infix? comment?
wenzelm@7134
   170
  ;
wenzelm@7134
   171
  'nonterminals' (name +) comment?
wenzelm@7134
   172
  ;
wenzelm@7134
   173
  'arities' (nameref '::' arity comment? +)
wenzelm@7134
   174
  ;
wenzelm@7134
   175
\end{rail}
wenzelm@7134
   176
wenzelm@7167
   177
\begin{descr}
wenzelm@7134
   178
\item [$\TYPES~(\vec\alpha)t = \tau~\dots$] introduces \emph{type synonym}
wenzelm@7134
   179
  $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
wenzelm@7134
   180
  as are available in Isabelle/HOL for example, type synonyms are just purely
wenzelm@7134
   181
  syntactic abbreviations, without any logical significance.  Internally, type
wenzelm@7134
   182
  synonyms are fully expanded, as may be observed when printing terms or
wenzelm@7134
   183
  theorems.
wenzelm@7134
   184
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
wenzelm@7134
   185
  $t$, intended as an actual logical type.  Note that some logics such as
wenzelm@7134
   186
  Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.
wenzelm@7175
   187
\item [$\isarkeyword{nonterminals}~\vec c$] declares $0$-ary type constructors
wenzelm@7175
   188
  $\vec c$ to act as purely syntactic types, i.e.\ nonterminal symbols of
wenzelm@7175
   189
  Isabelle's inner syntax of terms or types.
wenzelm@7134
   190
\item [$\isarkeyword{arities}~t::(\vec s)s~\dots$] augments Isabelle's
wenzelm@7134
   191
  order-sorted signature of types by new type constructor arities.  This is
wenzelm@7175
   192
  done axiomatically!  The $\isarkeyword{instance}$ command (see
wenzelm@7175
   193
  \S\ref{sec:axclass}) provides a way introduce proven type arities.
wenzelm@7167
   194
\end{descr}
wenzelm@7134
   195
wenzelm@7134
   196
wenzelm@7134
   197
\subsection{Constants and simple definitions}
wenzelm@7134
   198
wenzelm@7175
   199
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}\indexoutertoken{constdecl}
wenzelm@7134
   200
\begin{matharray}{rcl}
wenzelm@7134
   201
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   202
  \isarcmd{defs} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   203
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   204
\end{matharray}
wenzelm@7134
   205
wenzelm@7134
   206
\begin{rail}
wenzelm@7134
   207
  'consts' (constdecl +)
wenzelm@7134
   208
  ;
wenzelm@7134
   209
  'defs' (thmdecl? prop comment? +)
wenzelm@7134
   210
  ;
wenzelm@7134
   211
  'constdefs' (constdecl prop comment? +)
wenzelm@7134
   212
  ;
wenzelm@7134
   213
wenzelm@7134
   214
  constdecl: name '::' type mixfix? comment?
wenzelm@7134
   215
  ;
wenzelm@7134
   216
\end{rail}
wenzelm@7134
   217
wenzelm@7167
   218
\begin{descr}
wenzelm@7175
   219
\item [$\CONSTS~c::\sigma~\dots$] declares constant $c$ to have any instance
wenzelm@7175
   220
  of type scheme $\sigma$.  The optional mixfix annotations may attach
wenzelm@7175
   221
  concrete syntax constants.
wenzelm@7134
   222
\item [$\DEFS~name: eqn~\dots$] introduces $eqn$ as a definitional axiom for
wenzelm@7134
   223
  some existing constant.  See \cite[\S6]{isabelle-ref} for more details on
wenzelm@7134
   224
  the form of equations admitted as constant definitions.
wenzelm@7175
   225
\item [$\isarkeyword{constdefs}~c::\sigma~eqn~\dots$] combines constant
wenzelm@7134
   226
  declarations and definitions, using canonical name $c_def$ for the
wenzelm@7134
   227
  definitional axiom.
wenzelm@7167
   228
\end{descr}
wenzelm@7134
   229
wenzelm@7134
   230
wenzelm@7167
   231
\subsection{Syntax and translations}
wenzelm@7134
   232
wenzelm@7134
   233
\indexisarcmd{syntax}\indexisarcmd{translations}
wenzelm@7134
   234
\begin{matharray}{rcl}
wenzelm@7134
   235
  \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   236
  \isarcmd{translations} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   237
\end{matharray}
wenzelm@7134
   238
wenzelm@7134
   239
\begin{rail}
wenzelm@7134
   240
  'syntax' ('(' name 'output'? ')')? (constdecl +)
wenzelm@7134
   241
  ;
wenzelm@7134
   242
  'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
wenzelm@7134
   243
  ;
wenzelm@7134
   244
  transpat: ('(' nameref ')')? string
wenzelm@7134
   245
  ;
wenzelm@7134
   246
\end{rail}
wenzelm@7134
   247
wenzelm@7167
   248
\begin{descr}
wenzelm@7175
   249
\item [$\isarkeyword{syntax}~(mode)~decls$] is similar to $\CONSTS~decls$,
wenzelm@7175
   250
  except that the actual logical signature extension is omitted.  Thus the
wenzelm@7175
   251
  context free grammar of Isabelle's inner syntax may be augmented in
wenzelm@7175
   252
  arbitrary ways.  The $mode$ argument refers to the print mode that the
wenzelm@7175
   253
  grammar rules belong; unless there is the \texttt{output} flag given, all
wenzelm@7175
   254
  productions are added both to the input and output grammar.
wenzelm@7175
   255
\item [$\isarkeyword{translations}~rules$] specifies syntactic translation
wenzelm@7175
   256
  rules (also known as \emph{macros}): parse/print rules (\texttt{==}), parse
wenzelm@7175
   257
  rules (\texttt{=>}), print rules (\texttt{<=}).  Translation patterns may be
wenzelm@7134
   258
  prefixed by the syntactic category to be used for parsing; the default is
wenzelm@7134
   259
  \texttt{logic}.
wenzelm@7167
   260
\end{descr}
wenzelm@7134
   261
wenzelm@7134
   262
wenzelm@7134
   263
\subsection{Axioms and theorems}
wenzelm@7134
   264
wenzelm@7134
   265
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
wenzelm@7134
   266
\begin{matharray}{rcl}
wenzelm@7134
   267
  \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   268
  \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   269
  \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   270
\end{matharray}
wenzelm@7134
   271
wenzelm@7134
   272
\begin{rail}
wenzelm@7135
   273
  'axioms' (axmdecl prop comment? +)
wenzelm@7134
   274
  ;
wenzelm@7134
   275
  ('theorems' | 'lemmas') thmdef? thmrefs
wenzelm@7134
   276
  ;
wenzelm@7134
   277
\end{rail}
wenzelm@7134
   278
wenzelm@7167
   279
\begin{descr}
wenzelm@7134
   280
\item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary
wenzelm@7134
   281
  statements as logical axioms.  In fact, axioms are ``axiomatic theorems'',
wenzelm@7175
   282
  and may be referred just as any other theorem later.
wenzelm@7134
   283
  
wenzelm@7134
   284
  Axioms are usually only introduced when declaring new logical systems.
wenzelm@7175
   285
  Everyday work is typically done the hard way, with proper definitions and
wenzelm@7134
   286
  actual theorems.
wenzelm@7134
   287
\item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems
wenzelm@7175
   288
  as $name$.  Typical applications would also involve attributes (to augment
wenzelm@7175
   289
  the default simpset, for example).
wenzelm@7134
   290
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
wenzelm@7134
   291
  tags the results as ``lemma''.
wenzelm@7167
   292
\end{descr}
wenzelm@7134
   293
wenzelm@7134
   294
wenzelm@7167
   295
\subsection{Name spaces}
wenzelm@7134
   296
wenzelm@7167
   297
\indexisarcmd{global}\indexisarcmd{local}
wenzelm@7134
   298
\begin{matharray}{rcl}
wenzelm@7134
   299
  \isarcmd{global} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   300
  \isarcmd{local} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   301
\end{matharray}
wenzelm@7134
   302
wenzelm@7175
   303
Isabelle organizes any kind of names (of types, constants, theorems etc.)  by
wenzelm@7175
   304
hierarchically structured name spaces.  Normally the user never has to control
wenzelm@7175
   305
the behavior of name space entry by hand, yet the following commands provide
wenzelm@7175
   306
some way to do so.
wenzelm@7175
   307
wenzelm@7167
   308
\begin{descr}
wenzelm@7167
   309
\item [$\isarkeyword{global}$ and $\isarkeyword{local}$] change the current
wenzelm@7167
   310
  name declaration mode.  Initially, theories start in $\isarkeyword{local}$
wenzelm@7167
   311
  mode, causing all names to be automatically qualified by the theory name.
wenzelm@7167
   312
  Changing this to $\isarkeyword{global}$ causes all names to be declared as
wenzelm@7175
   313
  base names only, until $\isarkeyword{local}$ is declared again.
wenzelm@7167
   314
\end{descr}
wenzelm@7134
   315
wenzelm@7134
   316
wenzelm@7167
   317
\subsection{Incorporating ML code}\label{sec:ML}
wenzelm@7134
   318
wenzelm@7134
   319
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
wenzelm@7134
   320
\begin{matharray}{rcl}
wenzelm@7134
   321
  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134
   322
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7175
   323
  \isarcmd{setup} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   324
\end{matharray}
wenzelm@7134
   325
wenzelm@7134
   326
\begin{rail}
wenzelm@7134
   327
  'use' name
wenzelm@7134
   328
  ;
wenzelm@7134
   329
  'ML' text
wenzelm@7134
   330
  ;
wenzelm@7134
   331
  'setup' text
wenzelm@7134
   332
  ;
wenzelm@7134
   333
\end{rail}
wenzelm@7134
   334
wenzelm@7167
   335
\begin{descr}
wenzelm@7175
   336
\item [$\isarkeyword{use}~file$] reads and executes ML commands from $file$.
wenzelm@7175
   337
  The current theory context (if present) is passed down to the ML session.
wenzelm@7175
   338
  Furthermore, the file name is checked with the $\isarkeyword{files}$
wenzelm@7175
   339
  dependency declaration given in the theory header (see also
wenzelm@7175
   340
  \S\ref{sec:begin-thy}).
wenzelm@7175
   341
\item [$\isarkeyword{ML}~text$] reads and executes ML commands from $text$.
wenzelm@7175
   342
  The theory context is passed just as for $\isarkeyword{use}$.
wenzelm@7167
   343
\item [$\isarkeyword{setup}~text$] changes the current theory context by
wenzelm@7175
   344
  applying setup functions $text$, which has to be an ML expression of type
wenzelm@7175
   345
  $(theory \to theory)~list$.  The $\isarkeyword{setup}$ command is the usual
wenzelm@7175
   346
  way to initialize object-logic specific tools and packages written in ML.
wenzelm@7167
   347
\end{descr}
wenzelm@7134
   348
wenzelm@7134
   349
wenzelm@7167
   350
\subsection{Syntax translation functions}
wenzelm@7134
   351
wenzelm@7167
   352
\indexisarcmd{parse-ast-translation}\indexisarcmd{parse-translation}
wenzelm@7167
   353
\indexisarcmd{print-translation}\indexisarcmd{typed-print-translation}
wenzelm@7167
   354
\indexisarcmd{print-ast-translation}\indexisarcmd{token-translation}
wenzelm@7134
   355
\begin{matharray}{rcl}
wenzelm@7134
   356
  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   357
  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   358
  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   359
  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   360
  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   361
  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   362
\end{matharray}
wenzelm@7134
   363
wenzelm@7134
   364
Syntax translation functions written in ML admit almost arbitrary
wenzelm@7134
   365
manipulations of Isabelle's inner syntax.  Any of the above commands have a
wenzelm@7134
   366
single \railqtoken{text} argument that refers to an ML expression of
wenzelm@7134
   367
appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
wenzelm@7134
   368
transformations.
wenzelm@7134
   369
wenzelm@7134
   370
wenzelm@7134
   371
\subsection{Oracles}
wenzelm@7134
   372
wenzelm@7134
   373
\indexisarcmd{oracle}
wenzelm@7134
   374
\begin{matharray}{rcl}
wenzelm@7134
   375
  \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   376
\end{matharray}
wenzelm@7134
   377
wenzelm@7175
   378
Oracles provide an interface to external reasoning systems, without giving up
wenzelm@7175
   379
control completely --- each theorem carries a derivation object recording any
wenzelm@7175
   380
oracle invocation.  See \cite[\S6]{isabelle-ref} for more information.
wenzelm@7175
   381
wenzelm@7134
   382
\begin{rail}
wenzelm@7134
   383
  'oracle' name '=' text comment?
wenzelm@7134
   384
  ;
wenzelm@7134
   385
\end{rail}
wenzelm@7134
   386
wenzelm@7167
   387
\begin{descr}
wenzelm@7175
   388
\item [$\isarkeyword{oracle}~name=text$] declares oracle $name$ to be ML
wenzelm@7175
   389
  function $text$, which has to be of type $Sign\mathord.sg \times object \to
wenzelm@7175
   390
  term)$.
wenzelm@7167
   391
\end{descr}
wenzelm@7134
   392
wenzelm@7134
   393
wenzelm@7134
   394
\section{Proof commands}
wenzelm@7134
   395
wenzelm@7167
   396
Proof commands provide transitions of Isar/VM machine configurations.  There
wenzelm@7175
   397
are three different modes of operation.
wenzelm@7167
   398
\begin{descr}
wenzelm@7167
   399
\item [$proof(prove)$] means that a new goal has just been stated that is now
wenzelm@7167
   400
  to be \emph{proven}; the next command may refine it by some proof method
wenzelm@7175
   401
  ($\approx$ tactic), and enter a sub-proof to establish the final result.
wenzelm@7167
   402
\item [$proof(state)$] is like an internal theory mode: the context may be
wenzelm@7175
   403
  augmented by \emph{stating} additional assumptions, intermediate result etc.
wenzelm@7175
   404
\item [$proof(chain)$] is an intermediate mode between $proof(state)$ and
wenzelm@7175
   405
  $proof(prove)$: some existing facts have been just picked up in order to use
wenzelm@7175
   406
  them when refining the goal to be claimed next.
wenzelm@7167
   407
\end{descr}
wenzelm@7134
   408
wenzelm@7167
   409
wenzelm@7167
   410
\subsection{Formal comments}\label{sec:formal-cmt-prf}
wenzelm@7167
   411
wenzelm@7167
   412
\indexisarcmd{sect}\indexisarcmd{subsect}\indexisarcmd{subsect}\indexisarcmd{txt}
wenzelm@7134
   413
\begin{matharray}{rcl}
wenzelm@7167
   414
  \isarcmd{sect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   415
  \isarcmd{subsect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   416
  \isarcmd{subsubsect} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   417
  \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   418
\end{matharray}
wenzelm@7134
   419
wenzelm@7175
   420
These formal comments in proof mode closely correspond to the ones of theory
wenzelm@7175
   421
mode (see \S\ref{sec:formal-cmt-thy}).
wenzelm@7175
   422
wenzelm@7134
   423
\begin{rail}
wenzelm@7167
   424
  ('sect' | 'subsect' | 'subsubsect' | 'txt') text
wenzelm@7134
   425
  ;
wenzelm@7134
   426
\end{rail}
wenzelm@7134
   427
wenzelm@7134
   428
wenzelm@7134
   429
\subsection{Proof context}
wenzelm@7134
   430
wenzelm@7134
   431
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}
wenzelm@7134
   432
\begin{matharray}{rcl}
wenzelm@7134
   433
  \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   434
  \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   435
  \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   436
  \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   437
  \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   438
\end{matharray}
wenzelm@7134
   439
wenzelm@7175
   440
FIXME
wenzelm@7175
   441
wenzelm@7134
   442
\begin{rail}
wenzelm@7134
   443
  'fix' (var +) comment?
wenzelm@7134
   444
  ;
wenzelm@7175
   445
  ('assume' | 'presume') thmdecl? \\ (prop proppat? +) comment?
wenzelm@7134
   446
  ;
wenzelm@7175
   447
  'def' thmdecl? \\ var '==' term termpat? comment?
wenzelm@7134
   448
  ;
wenzelm@7134
   449
  'let' ((term + 'as') '=' term comment? + 'and')
wenzelm@7134
   450
  ;
wenzelm@7134
   451
wenzelm@7134
   452
  var: name ('::' type)?
wenzelm@7134
   453
  ;
wenzelm@7134
   454
\end{rail}
wenzelm@7134
   455
wenzelm@7167
   456
\begin{descr}
wenzelm@7167
   457
\item [$\FIX{x}$] FIXME
wenzelm@7167
   458
\item [$\ASSUME{a}{\Phi}$ and $\PRESUME{a}{\Phi}$] FIXME
wenzelm@7167
   459
\item [$\DEF{a}{x \equiv t}$] FIXME
wenzelm@7167
   460
\item [$\LET{\vec p = \vec t}$] FIXME
wenzelm@7167
   461
\end{descr}
wenzelm@7167
   462
wenzelm@7167
   463
wenzelm@7167
   464
\subsection{Facts and forward chaining}
wenzelm@7167
   465
wenzelm@7167
   466
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
wenzelm@7167
   467
\begin{matharray}{rcl}
wenzelm@7167
   468
  \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7167
   469
  \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167
   470
  \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167
   471
  \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7167
   472
\end{matharray}
wenzelm@7167
   473
wenzelm@7175
   474
FIXME
wenzelm@7175
   475
wenzelm@7167
   476
\begin{rail}
wenzelm@7167
   477
  'note' thmdef? thmrefs comment?
wenzelm@7167
   478
  ;
wenzelm@7167
   479
  'then' comment?
wenzelm@7167
   480
  ;
wenzelm@7167
   481
  ('from' | 'with') thmrefs comment?
wenzelm@7167
   482
  ;
wenzelm@7167
   483
\end{rail}
wenzelm@7167
   484
wenzelm@7167
   485
\begin{descr}
wenzelm@7175
   486
\item [$\NOTE{a}{\vec b}$] recalls existing facts $\vec b$, binding the result
wenzelm@7175
   487
  as $a$.  Note that attributes may be involved as well, both on the left and
wenzelm@7175
   488
  right hand sides.
wenzelm@7167
   489
\item [$\THEN$] indicates forward chaining by the current facts in order to
wenzelm@7175
   490
  establish the goal to be claimed next.  The initial proof method invoked to
wenzelm@7175
   491
  solve that will be offered these facts to do ``anything appropriate'' (see
wenzelm@7175
   492
  also \S\ref{sec:proof-steps}).  For example, method $rule$ (see
wenzelm@7167
   493
  \S\ref{sec:pure-meth}) would do an elimination rather than an introduction.
wenzelm@7175
   494
\item [$\FROM{\vec b}$] abbreviates $\NOTE{}{\vec b}~\THEN$; also note that
wenzelm@7167
   495
  $\THEN$ is equivalent to $\FROM{facts}$.
wenzelm@7175
   496
\item [$\WITH{\vec b}$] abbreviates $\FROM{\vec b~facts}$; thus the forward
wenzelm@7175
   497
  chaining is from earlier facts together with the current ones.
wenzelm@7167
   498
\end{descr}
wenzelm@7167
   499
wenzelm@7167
   500
wenzelm@7167
   501
\subsection{Goal statements}
wenzelm@7167
   502
wenzelm@7167
   503
\indexisarcmd{theorem}\indexisarcmd{lemma}
wenzelm@7167
   504
\indexisarcmd{have}\indexisarcmd{show}\indexisarcmd{hence}\indexisarcmd{thus}
wenzelm@7167
   505
\begin{matharray}{rcl}
wenzelm@7167
   506
  \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167
   507
  \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7167
   508
  \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   509
  \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   510
  \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   511
  \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7167
   512
\end{matharray}
wenzelm@7167
   513
wenzelm@7175
   514
Proof mode is entered from theory mode by initial goal commands $\THEOREMNAME$
wenzelm@7175
   515
and $\LEMMANAME$.  New local goals may be claimed within proof mode: four
wenzelm@7175
   516
variants are available, indicating whether the result is meant to solve some
wenzelm@7175
   517
pending goal and whether forward chaining is employed.
wenzelm@7175
   518
wenzelm@7167
   519
\begin{rail}
wenzelm@7167
   520
  ('theorem' | 'lemma') goal
wenzelm@7167
   521
  ;
wenzelm@7167
   522
  ('have' | 'show' | 'hence' | 'thus') goal
wenzelm@7167
   523
  ;
wenzelm@7167
   524
wenzelm@7167
   525
  goal: thmdecl? proppat comment?
wenzelm@7167
   526
  ;
wenzelm@7167
   527
\end{rail}
wenzelm@7167
   528
wenzelm@7167
   529
\begin{descr}
wenzelm@7167
   530
\item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,
wenzelm@7175
   531
  eventually resulting in some theorem $\turn \phi$, which will be stored in
wenzelm@7175
   532
  the theory.
wenzelm@7167
   533
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
wenzelm@7167
   534
  ``lemma''.
wenzelm@7167
   535
\item [$\HAVE{name}{\phi}$] claims a local goal, eventually resulting in a
wenzelm@7167
   536
  theorem with the current assumption context as hypotheses.
wenzelm@7175
   537
\item [$\SHOW{name}{\phi}$] is similar to $\HAVE{name}{\phi}$, but solves some
wenzelm@7175
   538
  pending goal with the result \emph{exported} into the corresponding context.
wenzelm@7167
   539
\item [$\HENCE{name}{\phi}$] abbreviates $\THEN~\HAVE{name}{\phi}$, i.e.\ 
wenzelm@7167
   540
  claims a local goal to be proven by forward chaining the current facts.
wenzelm@7167
   541
\item [$\THUS{name}{\phi}$] abbreviates $\THEN~\SHOW{name}{\phi}$.
wenzelm@7167
   542
\end{descr}
wenzelm@7167
   543
wenzelm@7167
   544
wenzelm@7167
   545
\subsection{Initial and terminal proof steps}\label{sec:proof-steps}
wenzelm@7167
   546
wenzelm@7175
   547
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm@7175
   548
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm@7175
   549
\begin{matharray}{rcl}
wenzelm@7175
   550
  \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm@7175
   551
  \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm@7175
   552
  \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   553
  \isarcmd{.\,.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   554
  \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   555
  \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7175
   556
\end{matharray}
wenzelm@7175
   557
wenzelm@7167
   558
Arbitrary goal refinements via tactics is considered harmful.  Consequently
wenzelm@7167
   559
the Isar framework admits proof methods to be invoked in two places only.
wenzelm@7167
   560
\begin{enumerate}
wenzelm@7175
   561
\item An \emph{initial} refinement step $\PROOF{m@1}$ reduces a newly stated
wenzelm@7175
   562
  intermediate goal to a number of sub-goals that are to be solved later.
wenzelm@7175
   563
  Facts are passed to $m@1$ for forward chaining if so indicated by
wenzelm@7175
   564
  $proof(chain)$ mode.
wenzelm@7167
   565
  
wenzelm@7175
   566
\item A \emph{terminal} conclusion step $\QED{m@2}$ solves any remaining
wenzelm@7167
   567
  pending goals completely.  No facts are passed to $m@2$.
wenzelm@7167
   568
\end{enumerate}
wenzelm@7167
   569
wenzelm@7167
   570
The only other proper way to affect pending goals is by $\SHOWNAME$, which
wenzelm@7167
   571
involves an explicit statement of what is solved.
wenzelm@7167
   572
wenzelm@7175
   573
\medskip
wenzelm@7175
   574
wenzelm@7167
   575
Also note that initial proof methods should either solve the goal completely,
wenzelm@7167
   576
or constitute some well-understood deterministic reduction to new sub-goals.
wenzelm@7167
   577
Arbitrary automatic proof tools that are prone leave a large number of badly
wenzelm@7167
   578
structured sub-goals are no help in continuing the proof document in any
wenzelm@7175
   579
intelligible way.  A much better technique would be to $\SHOWNAME$ some
wenzelm@7175
   580
non-trivial reduction as an explicit rule, which is solved completely by some
wenzelm@7175
   581
automated method, and then applied to some pending goal.
wenzelm@7167
   582
wenzelm@7175
   583
\medskip
wenzelm@7175
   584
wenzelm@7175
   585
Unless given explicitly by the user, the default initial method is
wenzelm@7175
   586
``$default$'', which is usually set up to apply a single standard elimination
wenzelm@7175
   587
or introduction rule according to the topmost symbol involved.  The default
wenzelm@7175
   588
terminal method is ``$finish$''; it solves all goals by assumption.
wenzelm@7167
   589
wenzelm@7167
   590
\begin{rail}
wenzelm@7167
   591
  'proof' interest? meth? comment?
wenzelm@7167
   592
  ;
wenzelm@7167
   593
  'qed' meth? comment?
wenzelm@7167
   594
  ;
wenzelm@7167
   595
  'by' meth meth? comment?
wenzelm@7167
   596
  ;
wenzelm@7167
   597
  ('.' | '..' | 'sorry') comment?
wenzelm@7167
   598
  ;
wenzelm@7167
   599
wenzelm@7167
   600
  meth: method interest?
wenzelm@7167
   601
  ;
wenzelm@7167
   602
\end{rail}
wenzelm@7167
   603
wenzelm@7167
   604
\begin{descr}
wenzelm@7175
   605
\item [$\PROOF{m@1}$] refines the pending goal by proof method $m@1$; facts
wenzelm@7175
   606
  for forward chaining are passed if so indicated by $proof(chain)$.
wenzelm@7175
   607
\item [$\QED{m@2}$] refines any remaining goals by proof method $m@1$ and
wenzelm@7167
   608
  concludes the sub-proof.  If the goal had been $\SHOWNAME$, some pending
wenzelm@7167
   609
  sub-goal is solved as well by the rule resulting from the result exported to
wenzelm@7175
   610
  the enclosing goal context.  Thus $\QEDNAME$ may fail for two reasons:
wenzelm@7175
   611
  either $m@2$ fails to solve all remaining goals completely, or the resulting
wenzelm@7175
   612
  rule does not resolve with any enclosing goal.  Debugging such a situation
wenzelm@7175
   613
  might involve temporarily changing $\SHOWNAME$ into $\HAVENAME$, or
wenzelm@7175
   614
  weakening the local context by replacing $\ASSUMENAME$ by $\PRESUMENAME$.
wenzelm@7175
   615
\item [$\BYY{m@1}{m@2}$] is a \emph{terminal proof}; it abbreviates
wenzelm@7175
   616
  $\PROOF{m@1}~\QED{m@2}$, with automatic backtracking across both methods.
wenzelm@7175
   617
  Debugging an unsuccessful $\BYY{m@1}{m@2}$ commands might be done by simply
wenzelm@7175
   618
  expanding the abbreviation by hand; note that $\PROOF{m@1}$ is usually
wenzelm@7175
   619
  sufficient to see what is going wrong.
wenzelm@7175
   620
\item [$\DDOT$] is a \emph{default proof}; it abbreviates $\BY{default}$.
wenzelm@7175
   621
\item [$\DOT$] is a \emph{trivial proof}, it abbreviates $\BY{-}$, where
wenzelm@7175
   622
  method ``$-$'' does nothing except inserting any facts into the proof state.
wenzelm@7167
   623
\item [$\isarkeyword{sorry}$] is a \emph{fake proof}; provided that
wenzelm@7167
   624
  \texttt{quick_and_dirty} is enabled, $\isarkeyword{sorry}$ pretends to solve
wenzelm@7167
   625
  the goal without much ado.  Of course, the result is a fake theorem only,
wenzelm@7175
   626
  involving some oracle in its internal derivation object (this is indicated
wenzelm@7175
   627
  as $[!]$ in the printed result.  The main application of
wenzelm@7167
   628
  $\isarkeyword{sorry}$ is to support top-down proof development.
wenzelm@7167
   629
\end{descr}
wenzelm@7134
   630
wenzelm@7134
   631
wenzelm@7134
   632
\subsection{Block structure}
wenzelm@7134
   633
wenzelm@7167
   634
While Isar is inherently block-structured, opening and closing blocks is
wenzelm@7167
   635
mostly handled rather casually, with little explicit user-intervention.  Any
wenzelm@7167
   636
local goal statement automatically opens \emph{two} blocks, which are closed
wenzelm@7167
   637
again when concluding the sub-proof (by $\QEDNAME$ etc.).  Sections of
wenzelm@7167
   638
different context within a sub-proof are typically switched via
wenzelm@7167
   639
$\isarkeyword{next}$, which is just a single block-close followed by
wenzelm@7167
   640
block-open again.  Thus the effect of $\isarkeyword{next}$ is to reset the
wenzelm@7167
   641
proof context to that of the head of the sub-proof.  Note that there is no
wenzelm@7175
   642
goal focus involved here!
wenzelm@7167
   643
wenzelm@7175
   644
For slightly more advanced applications, there are explicit block parentheses
wenzelm@7175
   645
as well.  These typically achieve a strong forward style of reasoning.
wenzelm@7167
   646
wenzelm@7134
   647
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
wenzelm@7134
   648
\begin{matharray}{rcl}
wenzelm@7134
   649
  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   650
  \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   651
  \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   652
\end{matharray}
wenzelm@7134
   653
wenzelm@7167
   654
\begin{descr}
wenzelm@7167
   655
\item [$\isarkeyword{next}$] switches to a fresh block within a sub-proof,
wenzelm@7167
   656
  resetting the context to the initial one.
wenzelm@7167
   657
\item [$\isarkeyword{\{\{}$ and $\isarkeyword{\}\}}$] explicitly open and
wenzelm@7167
   658
  close blocks.  Any current facts pass through $\isarkeyword{\{\{}$
wenzelm@7167
   659
  unchanged, while $\isarkeyword{\}\}}$ causes them to be \emph{exported} into
wenzelm@7167
   660
  the enclosing context.  Thus fixed variables are generalized, assumptions
wenzelm@7167
   661
  discharged, and local definitions eliminated.
wenzelm@7167
   662
\end{descr}
wenzelm@7134
   663
wenzelm@7134
   664
\subsection{Calculational proof}
wenzelm@7134
   665
wenzelm@7134
   666
\indexisarcmd{also}\indexisarcmd{finally}
wenzelm@7134
   667
\begin{matharray}{rcl}
wenzelm@7134
   668
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   669
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7134
   670
\end{matharray}
wenzelm@7134
   671
wenzelm@7175
   672
FIXME
wenzelm@7175
   673
wenzelm@7134
   674
\begin{rail}
wenzelm@7134
   675
  ('also' | 'finally') transrules? comment?
wenzelm@7134
   676
  ;
wenzelm@7134
   677
wenzelm@7134
   678
  transrules: '(' thmrefs ')' interest?
wenzelm@7134
   679
  ;
wenzelm@7134
   680
\end{rail}
wenzelm@7134
   681
wenzelm@7167
   682
\begin{descr}
wenzelm@7175
   683
\item [$\ALSO~(thms)$] FIXME
wenzelm@7175
   684
\item [$\FINALLY~(thms)$] FIXME
wenzelm@7167
   685
\end{descr}
wenzelm@7134
   686
wenzelm@7134
   687
wenzelm@7134
   688
wenzelm@7134
   689
\subsection{Improper proof steps}
wenzelm@7134
   690
wenzelm@7175
   691
The following commands emulate unstructured tactic scripts to some extent.
wenzelm@7175
   692
While these are anathema for writing proper Isar proof documents, they might
wenzelm@7175
   693
come in handy for exploring and debugging.
wenzelm@7167
   694
wenzelm@7167
   695
\indexisarcmd{apply}\indexisarcmd{then-apply}\indexisarcmd{back}
wenzelm@7134
   696
\begin{matharray}{rcl}
wenzelm@7134
   697
  \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7134
   698
  \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7134
   699
  \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
wenzelm@7134
   700
\end{matharray}
wenzelm@7134
   701
wenzelm@7134
   702
\railalias{thenapply}{then\_apply}
wenzelm@7134
   703
\railterm{thenapply}
wenzelm@7134
   704
wenzelm@7134
   705
\begin{rail}
wenzelm@7134
   706
  'apply' method
wenzelm@7134
   707
  ;
wenzelm@7134
   708
  thenapply method
wenzelm@7134
   709
  ;
wenzelm@7134
   710
  'back'
wenzelm@7134
   711
  ;
wenzelm@7134
   712
\end{rail}
wenzelm@7134
   713
wenzelm@7167
   714
\begin{descr}
wenzelm@7134
   715
\item [$ $] FIXME
wenzelm@7167
   716
\end{descr}
wenzelm@7134
   717
wenzelm@7134
   718
wenzelm@7134
   719
\section{Other commands}
wenzelm@7134
   720
wenzelm@7134
   721
\subsection{Diagnostics}
wenzelm@7134
   722
wenzelm@7134
   723
\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
wenzelm@7134
   724
\begin{matharray}{rcl}
wenzelm@7134
   725
  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   726
  \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   727
  \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   728
  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   729
\end{matharray}
wenzelm@7134
   730
wenzelm@7134
   731
\begin{rail}
wenzelm@7134
   732
  'typ' type
wenzelm@7134
   733
  ;
wenzelm@7134
   734
  'term' term
wenzelm@7134
   735
  ;
wenzelm@7134
   736
  'prop' prop
wenzelm@7134
   737
  ;
wenzelm@7134
   738
  'thm' thmrefs
wenzelm@7134
   739
  ;
wenzelm@7134
   740
\end{rail}
wenzelm@7134
   741
wenzelm@7167
   742
\begin{descr}
wenzelm@7134
   743
\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
wenzelm@7134
   744
  $\isarkeyword{prop}~\phi$] read and print types / terms / propositions
wenzelm@7134
   745
  according to the current theory or proof context.
wenzelm@7134
   746
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
wenzelm@7134
   747
  theory or proof context.  Note that any attributes included in the theorem
wenzelm@7175
   748
  specifications are applied to a temporary context derived from the current
wenzelm@7175
   749
  theory or proof; the result is discarded.
wenzelm@7167
   750
\end{descr}
wenzelm@7134
   751
wenzelm@7134
   752
wenzelm@7134
   753
\subsection{System operations}
wenzelm@7134
   754
wenzelm@7167
   755
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use-thy}\indexisarcmd{use-thy-only}
wenzelm@7167
   756
\indexisarcmd{update-thy}\indexisarcmd{update-thy-only}
wenzelm@7134
   757
\begin{matharray}{rcl}
wenzelm@7134
   758
  \isarcmd{cd} & : & \isarkeep{\cdot} \\
wenzelm@7134
   759
  \isarcmd{pwd} & : & \isarkeep{\cdot} \\
wenzelm@7134
   760
  \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134
   761
  \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134
   762
  \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134
   763
  \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134
   764
\end{matharray}
wenzelm@7134
   765
wenzelm@7167
   766
\begin{descr}
wenzelm@7134
   767
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
wenzelm@7134
   768
  process.
wenzelm@7134
   769
\item [$\isarkeyword{pwd}~$] prints the current working directory.
wenzelm@7175
   770
\item [$\isarkeyword{use_thy}$, $\isarkeyword{use_thy_only}$,
wenzelm@7175
   771
  $\isarkeyword{update_thy}$, and $\isarkeyword{update_thy_only}$] load some
wenzelm@7175
   772
  theory given as $name$ argument.  These commands are exactly the same as the
wenzelm@7175
   773
  corresponding ML functions (see also \cite[\S1 and \S6]{isabelle-ref}).
wenzelm@7175
   774
  Note that both the ML and Isar versions of these commands may load new- and
wenzelm@7175
   775
  old-style theories alike.
wenzelm@7167
   776
\end{descr}
wenzelm@7134
   777
wenzelm@7134
   778
wenzelm@7046
   779
%%% Local Variables: 
wenzelm@7046
   780
%%% mode: latex
wenzelm@7046
   781
%%% TeX-master: "isar-ref"
wenzelm@7046
   782
%%% End: