doc-src/IsarRef/pure.tex
author wenzelm
Fri Jul 30 14:59:32 1999 +0200 (1999-07-30)
changeset 7134 320b412e5800
parent 7046 9f755ff43cff
child 7135 8eabfd7e6b9b
permissions -rw-r--r--
more stuff;
wenzelm@7046
     1
wenzelm@7046
     2
\chapter{Common Isar elements}
wenzelm@7046
     3
wenzelm@7134
     4
FIXME $*$ indicates \emph{improper commands}
wenzelm@7134
     5
wenzelm@7134
     6
\section{Theory commands}
wenzelm@7134
     7
wenzelm@7134
     8
\subsection{Defining theories}
wenzelm@7134
     9
wenzelm@7134
    10
\indexisarcmd{theory}\indexisarcmd{end}\indexisarcmd{context}
wenzelm@7134
    11
\begin{matharray}{rcl}
wenzelm@7134
    12
  \isarcmd{theory} & : & \isartrans{\cdot}{theory} \\
wenzelm@7134
    13
  \isarcmd{context}^* & : & \isartrans{\cdot}{theory} \\
wenzelm@7134
    14
  \isarcmd{end} & : & \isartrans{theory}{\cdot} \\
wenzelm@7134
    15
\end{matharray}
wenzelm@7134
    16
wenzelm@7134
    17
Isabelle/Isar ``new-style'' theories are either defined via theory files or
wenzelm@7134
    18
interactively.\footnote{In contrast, ``old-style'' Isabelle theories support
wenzelm@7134
    19
  batch processing only, with only the ML proof script part suitable for
wenzelm@7134
    20
  interaction.}
wenzelm@7134
    21
wenzelm@7134
    22
The first command of any theory has to be $\THEORY$, starting a new theory
wenzelm@7134
    23
based on the merge of existing ones.  In interactive experiments, the theory
wenzelm@7134
    24
context may be changed by $\CONTEXT$ without creating a new theory.  In both
wenzelm@7134
    25
cases the concluding command is $\END$, which has to be the very last one of
wenzelm@7134
    26
any proper theory file.
wenzelm@7134
    27
wenzelm@7134
    28
\begin{rail}
wenzelm@7134
    29
  'theory' name '=' (name + '+') filespecs? ':'
wenzelm@7134
    30
  ;
wenzelm@7134
    31
  'context' name
wenzelm@7134
    32
  ;
wenzelm@7134
    33
  'end'
wenzelm@7134
    34
  ;;
wenzelm@7134
    35
wenzelm@7134
    36
  filespecs : 'files' ((name | '(' name ')') +);
wenzelm@7134
    37
\end{rail}
wenzelm@7134
    38
wenzelm@7134
    39
\begin{description}
wenzelm@7134
    40
\item [$\THEORY~A = B@1 + \cdots + B@n$] commences a new theory $A$ based on
wenzelm@7134
    41
  existing ones $B@1 + \cdots + B@n$.  Note that Isabelle's theory loader
wenzelm@7134
    42
  system ensures that any of the base theories are properly loaded (and fully
wenzelm@7134
    43
  up-to-date when $\THEORY$ is executed interactively).
wenzelm@7134
    44
  
wenzelm@7134
    45
\item [$\CONTEXT~B$] enters existing theory context $B$, basically in
wenzelm@7134
    46
  read-only mode, so only a limited set of commands may be performed.  Just as
wenzelm@7134
    47
  for $\THEORY$, the theory loader ensures that $B$ is loaded and up-to-date.
wenzelm@7134
    48
wenzelm@7134
    49
\item [$\END$] concludes the current theory definition of context switch.
wenzelm@7134
    50
\end{description}
wenzelm@7134
    51
wenzelm@7134
    52
wenzelm@7134
    53
\subsection{Formal comments}
wenzelm@7134
    54
wenzelm@7134
    55
\indexisarcmd{title}\indexisarcmd{chapter}\indexisarcmd{subsection}\indexisarcmd{subsubsection}
wenzelm@7134
    56
\indexisarcmd{text}\indexisarcmd{txt}
wenzelm@7134
    57
\begin{matharray}{rcl}
wenzelm@7134
    58
  \isarcmd{title} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    59
  \isarcmd{chapter} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    60
  \isarcmd{subsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    61
  \isarcmd{subsubsection} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    62
  \isarcmd{text} & : & \isartrans{theory}{theory} \\
wenzelm@7134
    63
  \isarcmd{txt} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
    64
\end{matharray}
wenzelm@7134
    65
wenzelm@7134
    66
There are several commands to include \emph{formal comments} in theory and
wenzelm@7134
    67
proof specification.  In contrast to source-level comments
wenzelm@7134
    68
\verb|(*|\dots\verb|*)|, which are stripped at the lexical level, any text
wenzelm@7134
    69
given as formal comment is meant to be part of the actual document.
wenzelm@7134
    70
Consequently, it would be included in the final printed version.
wenzelm@7134
    71
wenzelm@7134
    72
Apart from plain prose, formal comments may also refer to logical entities of
wenzelm@7134
    73
the current theory context (types, terms, theorems etc.).  Proper processing
wenzelm@7134
    74
of the text would then include some further consistency checks with the items
wenzelm@7134
    75
declared in the current theory, e.g.\ type-checking of included terms.
wenzelm@7134
    76
\footnote{The current version of Isabelle/Isar does not process formal
wenzelm@7134
    77
  comments in any such way.  This will be available as part of the automatic
wenzelm@7134
    78
  theory and proof document preparation system (via (PDF)LaTeX) that is
wenzelm@7134
    79
  planned for the near future.}
wenzelm@7134
    80
wenzelm@7134
    81
\begin{rail}
wenzelm@7134
    82
  'title' text text? text?
wenzelm@7134
    83
  ;
wenzelm@7134
    84
  'chapter' text
wenzelm@7134
    85
  ;
wenzelm@7134
    86
  'subsection' text
wenzelm@7134
    87
  ;
wenzelm@7134
    88
  'subsubsection' text
wenzelm@7134
    89
  ;
wenzelm@7134
    90
  'text' text
wenzelm@7134
    91
  ;
wenzelm@7134
    92
  'txt' text
wenzelm@7134
    93
  ;
wenzelm@7134
    94
\end{rail}
wenzelm@7134
    95
wenzelm@7134
    96
\begin{description}
wenzelm@7134
    97
\item [$\isarkeyword{title}~title~author~date$] specifies the document title
wenzelm@7134
    98
  just as in typical LaTeX documents.
wenzelm@7134
    99
\item [$\isarkeyword{chapter}~text$, $\isarkeyword{subsection}~text$,
wenzelm@7134
   100
  $\isarkeyword{subsubsection}~text$] specify chapter and subsection headings.
wenzelm@7134
   101
\item [$\TEXT~text$] specifies an actual body of prose text, including
wenzelm@7134
   102
  references to formal entities.\footnote{The latter feature is not yet
wenzelm@7134
   103
    exploited in any way.}
wenzelm@7134
   104
\item [$\TXT~text$] is similar to $\TEXT$, but may appear within proofs.
wenzelm@7134
   105
\end{description}
wenzelm@7134
   106
wenzelm@7134
   107
wenzelm@7134
   108
\subsection{Type classes and sorts}
wenzelm@7134
   109
wenzelm@7134
   110
\indexisarcmd{classes}\indexisarcmd{classrel}\indexisarcmd{defaultsort}
wenzelm@7134
   111
\begin{matharray}{rcl}
wenzelm@7134
   112
  \isarcmd{classes} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   113
  \isarcmd{classrel} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   114
  \isarcmd{defaultsort} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   115
\end{matharray}
wenzelm@7134
   116
wenzelm@7134
   117
\begin{rail}
wenzelm@7134
   118
  'classes' (name ('<' (nameref ',' +))? comment? +)
wenzelm@7134
   119
  ;
wenzelm@7134
   120
  'classrel' nameref '<' nameref comment?
wenzelm@7134
   121
  ;
wenzelm@7134
   122
  'defaultsort' sort comment?
wenzelm@7134
   123
  ;
wenzelm@7134
   124
\end{rail}
wenzelm@7134
   125
wenzelm@7134
   126
\begin{description}
wenzelm@7134
   127
\item [$\isarkeyword{classes}~c<cs ~\dots$] declares class $c$ to be a
wenzelm@7134
   128
  subclass of existing classes $cs$.  Cyclic class structures are ruled out.
wenzelm@7134
   129
\item [$\isarkeyword{classrel}~c@1<c@2$] states a subclass relation between
wenzelm@7134
   130
  existing classes $c@1$ and $c@2$.  This is done axiomatically!  The
wenzelm@7134
   131
  $\isarkeyword{instance}$ command provides a way introduce proven class
wenzelm@7134
   132
  relations (see \S\ref{sec:axclass}).
wenzelm@7134
   133
\item [$\isarkeyword{defaultsort}~s$] makes sort $s$ the new default sort for
wenzelm@7134
   134
  any type variables input without sort constraints.  Typically, the default
wenzelm@7134
   135
  sort would be only changed when defining new logics.
wenzelm@7134
   136
\end{description}
wenzelm@7134
   137
wenzelm@7134
   138
wenzelm@7134
   139
\subsection{Types}
wenzelm@7134
   140
wenzelm@7134
   141
\indexisarcmd{typedecl}\indexisarcmd{types}\indexisarcmd{nonterminals}\indexisarcmd{arities}
wenzelm@7134
   142
\begin{matharray}{rcl}
wenzelm@7134
   143
  \isarcmd{types} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   144
  \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   145
  \isarcmd{nonterminals} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   146
  \isarcmd{arities} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   147
\end{matharray}
wenzelm@7134
   148
wenzelm@7134
   149
\begin{rail}
wenzelm@7134
   150
  'types' (typespec '=' type infix? comment? +)
wenzelm@7134
   151
  ;
wenzelm@7134
   152
  'typedecl' typespec infix? comment?
wenzelm@7134
   153
  ;
wenzelm@7134
   154
  'nonterminals' (name +) comment?
wenzelm@7134
   155
  ;
wenzelm@7134
   156
  'arities' (nameref '::' arity comment? +)
wenzelm@7134
   157
  ;
wenzelm@7134
   158
\end{rail}
wenzelm@7134
   159
wenzelm@7134
   160
\begin{description}
wenzelm@7134
   161
\item [$\TYPES~(\vec\alpha)t = \tau~\dots$] introduces \emph{type synonym}
wenzelm@7134
   162
  $(\vec\alpha)t$ for existing type $\tau$.  Unlike actual type definitions,
wenzelm@7134
   163
  as are available in Isabelle/HOL for example, type synonyms are just purely
wenzelm@7134
   164
  syntactic abbreviations, without any logical significance.  Internally, type
wenzelm@7134
   165
  synonyms are fully expanded, as may be observed when printing terms or
wenzelm@7134
   166
  theorems.
wenzelm@7134
   167
\item [$\isarkeyword{typedecl}~(\vec\alpha)t$] declares a new type constructor
wenzelm@7134
   168
  $t$, intended as an actual logical type.  Note that some logics such as
wenzelm@7134
   169
  Isabelle/HOL provide their own version of $\isarkeyword{typedecl}$.
wenzelm@7134
   170
\item [$\isarkeyword{nonterminals}~c~\dots$] declares $0$-ary type
wenzelm@7134
   171
  constructors $c$ to act as purely syntactic types, i.e.\ nonterminal symbols
wenzelm@7134
   172
  of Isabelle's inner syntax of terms or types.
wenzelm@7134
   173
\item [$\isarkeyword{arities}~t::(\vec s)s~\dots$] augments Isabelle's
wenzelm@7134
   174
  order-sorted signature of types by new type constructor arities.  This is
wenzelm@7134
   175
  done axiomatically!  The $\isarkeyword{instance}$ command provides a way
wenzelm@7134
   176
  introduce proven type arities (see \S\ref{sec:axclass}).
wenzelm@7134
   177
\end{description}
wenzelm@7134
   178
wenzelm@7134
   179
wenzelm@7134
   180
\subsection{Constants and simple definitions}
wenzelm@7134
   181
wenzelm@7134
   182
\indexisarcmd{consts}\indexisarcmd{defs}\indexisarcmd{constdefs}
wenzelm@7134
   183
\begin{matharray}{rcl}
wenzelm@7134
   184
  \isarcmd{consts} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   185
  \isarcmd{defs} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   186
  \isarcmd{constdefs} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   187
\end{matharray}
wenzelm@7134
   188
wenzelm@7134
   189
\begin{rail}
wenzelm@7134
   190
  'consts' (constdecl +)
wenzelm@7134
   191
  ;
wenzelm@7134
   192
  'defs' (thmdecl? prop comment? +)
wenzelm@7134
   193
  ;
wenzelm@7134
   194
  'constdefs' (constdecl prop comment? +)
wenzelm@7134
   195
  ;
wenzelm@7134
   196
wenzelm@7134
   197
  constdecl: name '::' type mixfix? comment?
wenzelm@7134
   198
  ;
wenzelm@7134
   199
\end{rail}
wenzelm@7134
   200
wenzelm@7134
   201
\begin{description}
wenzelm@7134
   202
\item [$\CONSTS~c::\tau~\dots$] declares constant $c$ to have any instance of
wenzelm@7134
   203
  type scheme $\tau$.  The optional mixfix annotations may attach concrete
wenzelm@7134
   204
  syntax to the constant.
wenzelm@7134
   205
\item [$\DEFS~name: eqn~\dots$] introduces $eqn$ as a definitional axiom for
wenzelm@7134
   206
  some existing constant.  See \cite[\S6]{isabelle-ref} for more details on
wenzelm@7134
   207
  the form of equations admitted as constant definitions.
wenzelm@7134
   208
\item [$\isarkeyword{constdefs}~c::\tau~eqn~\dots$] combines constant
wenzelm@7134
   209
  declarations and definitions, using canonical name $c_def$ for the
wenzelm@7134
   210
  definitional axiom.
wenzelm@7134
   211
\end{description}
wenzelm@7134
   212
wenzelm@7134
   213
wenzelm@7134
   214
\subsection{Concrete syntax}
wenzelm@7134
   215
wenzelm@7134
   216
\indexisarcmd{syntax}\indexisarcmd{translations}
wenzelm@7134
   217
\begin{matharray}{rcl}
wenzelm@7134
   218
  \isarcmd{syntax} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   219
  \isarcmd{translations} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   220
\end{matharray}
wenzelm@7134
   221
wenzelm@7134
   222
\begin{rail}
wenzelm@7134
   223
  'syntax' ('(' name 'output'? ')')? (constdecl +)
wenzelm@7134
   224
  ;
wenzelm@7134
   225
  'translations' (transpat ('==' | '=>' | '<=') transpat comment? +)
wenzelm@7134
   226
  ;
wenzelm@7134
   227
  transpat: ('(' nameref ')')? string
wenzelm@7134
   228
  ;
wenzelm@7134
   229
\end{rail}
wenzelm@7134
   230
wenzelm@7134
   231
\begin{description}
wenzelm@7134
   232
\item [$\isarkeyword{syntax}~mode~decls$] is similar to $\CONSTS~decls$,
wenzelm@7134
   233
  except the actual logical signature extension.  Thus the context free
wenzelm@7134
   234
  grammar of Isabelle's inner syntax may be augmented in arbitrary ways.  The
wenzelm@7134
   235
  $mode$ argument refers to the print mode that the grammar rules belong;
wenzelm@7134
   236
  unless there is the \texttt{output} flag given, all productions are added
wenzelm@7134
   237
  both to the input and output grammar.
wenzelm@7134
   238
\item [$\isarkeyword{translations}~rule~\dots$] specifies syntactic
wenzelm@7134
   239
  translation rules (macros): parse/print rules (\texttt{==}), parse rules
wenzelm@7134
   240
  (\texttt{=>}), print rules (\texttt{<=}).  Translation patterns may be
wenzelm@7134
   241
  prefixed by the syntactic category to be used for parsing; the default is
wenzelm@7134
   242
  \texttt{logic}.
wenzelm@7134
   243
\end{description}
wenzelm@7134
   244
wenzelm@7134
   245
wenzelm@7134
   246
\subsection{Axioms and theorems}
wenzelm@7134
   247
wenzelm@7134
   248
\indexisarcmd{axioms}\indexisarcmd{theorems}\indexisarcmd{lemmas}
wenzelm@7134
   249
\begin{matharray}{rcl}
wenzelm@7134
   250
  \isarcmd{axioms} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   251
  \isarcmd{theorems} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   252
  \isarcmd{lemmas} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   253
\end{matharray}
wenzelm@7134
   254
wenzelm@7134
   255
\begin{rail}
wenzelm@7134
   256
  'axioms' (name attributes? ':' prop comment? +)
wenzelm@7134
   257
  ;
wenzelm@7134
   258
  ('theorems' | 'lemmas') thmdef? thmrefs
wenzelm@7134
   259
  ;
wenzelm@7134
   260
\end{rail}
wenzelm@7134
   261
wenzelm@7134
   262
\begin{description}
wenzelm@7134
   263
\item [$\isarkeyword{axioms}~name: \phi~\dots$] introduces arbitrary
wenzelm@7134
   264
  statements as logical axioms.  In fact, axioms are ``axiomatic theorems'',
wenzelm@7134
   265
  and may be referred as any other theorems later.
wenzelm@7134
   266
  
wenzelm@7134
   267
  Axioms are usually only introduced when declaring new logical systems.
wenzelm@7134
   268
  Everyday work is normally done the hard way, with proper definitions and
wenzelm@7134
   269
  actual theorems.
wenzelm@7134
   270
\item [$\isarkeyword{theorems}~name = thms$] stores lists of existing theorems
wenzelm@7134
   271
  as $name$.  Typical applications would also involve attributes to augment
wenzelm@7134
   272
  the default simpset, for example.
wenzelm@7134
   273
\item [$\isarkeyword{lemmas}$] is similar to $\isarkeyword{theorems}$, but
wenzelm@7134
   274
  tags the results as ``lemma''.
wenzelm@7134
   275
\end{description}
wenzelm@7134
   276
wenzelm@7134
   277
wenzelm@7134
   278
\subsection{Manipulating name spaces}
wenzelm@7134
   279
wenzelm@7134
   280
\indexisarcmd{global}\indexisarcmd{local}\indexisarcmd{path}
wenzelm@7134
   281
\begin{matharray}{rcl}
wenzelm@7134
   282
  \isarcmd{global} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   283
  \isarcmd{local} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   284
  \isarcmd{path} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   285
\end{matharray}
wenzelm@7134
   286
wenzelm@7134
   287
\begin{rail}
wenzelm@7134
   288
  'global'
wenzelm@7134
   289
  ;
wenzelm@7134
   290
  'local'
wenzelm@7134
   291
  ;
wenzelm@7134
   292
  'path' nameref
wenzelm@7134
   293
  ;
wenzelm@7134
   294
\end{rail}
wenzelm@7134
   295
wenzelm@7134
   296
\begin{description}
wenzelm@7134
   297
\item [$\isarkeyword{global}$] FIXME
wenzelm@7134
   298
\item [$\isarkeyword{local}$] FIXME
wenzelm@7134
   299
\item [$\isarkeyword{path}~name$] FIXME
wenzelm@7134
   300
\end{description}
wenzelm@7134
   301
wenzelm@7134
   302
wenzelm@7134
   303
\subsection{Incorporating ML code}
wenzelm@7134
   304
wenzelm@7134
   305
\indexisarcmd{use}\indexisarcmd{ML}\indexisarcmd{setup}
wenzelm@7134
   306
\begin{matharray}{rcl}
wenzelm@7134
   307
  \isarcmd{use} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134
   308
  \isarcmd{ML} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134
   309
  \isarcmd{setup} & : & \isartrans{\cdot}{\cdot} \\
wenzelm@7134
   310
\end{matharray}
wenzelm@7134
   311
wenzelm@7134
   312
\begin{rail}
wenzelm@7134
   313
  'use' name
wenzelm@7134
   314
  ;
wenzelm@7134
   315
  'ML' text
wenzelm@7134
   316
  ;
wenzelm@7134
   317
  'setup' text
wenzelm@7134
   318
  ;
wenzelm@7134
   319
\end{rail}
wenzelm@7134
   320
wenzelm@7134
   321
\begin{description}
wenzelm@7134
   322
\item [$\isarkeyword{use}~file$] FIXME
wenzelm@7134
   323
\item [$\isarkeyword{ML}~text$] FIXME
wenzelm@7134
   324
\item [$\isarkeyword{setup}~text$] FIXME
wenzelm@7134
   325
\end{description}
wenzelm@7134
   326
wenzelm@7134
   327
wenzelm@7134
   328
\subsection{ML translation functions}
wenzelm@7134
   329
wenzelm@7134
   330
\indexisarcmd{parse_ast_translation}\indexisarcmd{parse_translation}
wenzelm@7134
   331
\indexisarcmd{print_translation}\indexisarcmd{typed_print_translation}
wenzelm@7134
   332
\indexisarcmd{print_ast_translation}\indexisarcmd{token_translation}
wenzelm@7134
   333
\begin{matharray}{rcl}
wenzelm@7134
   334
  \isarcmd{parse_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   335
  \isarcmd{parse_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   336
  \isarcmd{print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   337
  \isarcmd{typed_print_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   338
  \isarcmd{print_ast_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   339
  \isarcmd{token_translation} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   340
\end{matharray}
wenzelm@7134
   341
wenzelm@7134
   342
Syntax translation functions written in ML admit almost arbitrary
wenzelm@7134
   343
manipulations of Isabelle's inner syntax.  Any of the above commands have a
wenzelm@7134
   344
single \railqtoken{text} argument that refers to an ML expression of
wenzelm@7134
   345
appropriate type.  See \cite[\S8]{isabelle-ref} for more information on syntax
wenzelm@7134
   346
transformations.
wenzelm@7134
   347
wenzelm@7134
   348
wenzelm@7134
   349
\subsection{Oracles}
wenzelm@7134
   350
wenzelm@7134
   351
\indexisarcmd{oracle}
wenzelm@7134
   352
\begin{matharray}{rcl}
wenzelm@7134
   353
  \isarcmd{oracle} & : & \isartrans{theory}{theory} \\
wenzelm@7134
   354
\end{matharray}
wenzelm@7134
   355
wenzelm@7134
   356
\begin{rail}
wenzelm@7134
   357
  'oracle' name '=' text comment?
wenzelm@7134
   358
  ;
wenzelm@7134
   359
\end{rail}
wenzelm@7134
   360
wenzelm@7134
   361
\begin{description}
wenzelm@7134
   362
\item [$\isarkeyword{oracle}~name=text$] FIXME
wenzelm@7134
   363
\end{description}
wenzelm@7134
   364
wenzelm@7134
   365
wenzelm@7134
   366
\section{Proof commands}
wenzelm@7134
   367
wenzelm@7134
   368
\subsection{Goal statements}
wenzelm@7134
   369
wenzelm@7134
   370
\indexisarcmd{}
wenzelm@7134
   371
\begin{matharray}{rcl}
wenzelm@7134
   372
  \isarcmd{theorem} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7134
   373
  \isarcmd{lemma} & : & \isartrans{theory}{proof(prove)} \\
wenzelm@7134
   374
  \isarcmd{have} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7134
   375
  \isarcmd{show} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7134
   376
  \isarcmd{hence} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7134
   377
  \isarcmd{thus} & : & \isartrans{proof(state)}{proof(prove)} \\
wenzelm@7134
   378
\end{matharray}
wenzelm@7134
   379
wenzelm@7134
   380
\begin{rail}
wenzelm@7134
   381
  ('theorem' | 'lemma') goal
wenzelm@7134
   382
  ;
wenzelm@7134
   383
  ('have' | 'show' | 'hence' | 'thus') goal
wenzelm@7134
   384
  ;
wenzelm@7134
   385
wenzelm@7134
   386
  goal: thmdecl? proppat comment?
wenzelm@7134
   387
  ;
wenzelm@7134
   388
\end{rail}
wenzelm@7134
   389
wenzelm@7134
   390
\begin{description}
wenzelm@7134
   391
\item [$\THEOREM{name}{\phi}$] enters proof mode with $\phi$ as main goal,
wenzelm@7134
   392
  eventually resulting in some theorem $\turn \phi$, which stored in the
wenzelm@7134
   393
  theory.
wenzelm@7134
   394
\item [$\LEMMANAME$] is similar to $\THEOREMNAME$, but tags the result as
wenzelm@7134
   395
  ``lemma''.
wenzelm@7134
   396
\item [$\HAVE{name}{\phi}$] FIXME
wenzelm@7134
   397
\item [$\SHOW{name}{\phi}$] FIXME
wenzelm@7134
   398
\item [$\HENCE{name}{\phi}$] FIXME
wenzelm@7134
   399
\item [$\THUS{name}{\phi}$] FIXME
wenzelm@7134
   400
\end{description}
wenzelm@7134
   401
wenzelm@7134
   402
wenzelm@7134
   403
\subsection{Initial and terminal proof steps}
wenzelm@7134
   404
wenzelm@7134
   405
\indexisarcmd{proof}\indexisarcmd{qed}\indexisarcmd{by}
wenzelm@7134
   406
\indexisarcmd{.}\indexisarcmd{..}\indexisarcmd{sorry}
wenzelm@7134
   407
\begin{matharray}{rcl}
wenzelm@7134
   408
  \isarcmd{proof} & : & \isartrans{proof(prove)}{proof(state)} \\
wenzelm@7134
   409
  \isarcmd{qed} & : & \isartrans{proof(state)}{proof(state) ~|~ theory} \\
wenzelm@7134
   410
  \isarcmd{by} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7134
   411
  \isarcmd{.} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7134
   412
  \isarcmd{..} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7134
   413
  \isarcmd{sorry} & : & \isartrans{proof(prove)}{proof(state) ~|~ theory} \\
wenzelm@7134
   414
\end{matharray}
wenzelm@7134
   415
wenzelm@7134
   416
\begin{rail}
wenzelm@7134
   417
  'proof' interest? meth? comment?
wenzelm@7134
   418
  ;
wenzelm@7134
   419
  'qed' meth? comment?
wenzelm@7134
   420
  ;
wenzelm@7134
   421
  'by' meth meth? comment?
wenzelm@7134
   422
  ;
wenzelm@7134
   423
  ('.' | '..' | 'sorry') comment?
wenzelm@7134
   424
  ;
wenzelm@7134
   425
wenzelm@7134
   426
  meth: method interest?
wenzelm@7134
   427
  ;
wenzelm@7134
   428
\end{rail}
wenzelm@7134
   429
wenzelm@7134
   430
\begin{description}
wenzelm@7134
   431
\item [$ $] FIXME
wenzelm@7134
   432
\end{description}
wenzelm@7134
   433
wenzelm@7134
   434
wenzelm@7134
   435
\subsection{Facts and forward chaining}
wenzelm@7134
   436
wenzelm@7134
   437
\indexisarcmd{note}\indexisarcmd{then}\indexisarcmd{from}\indexisarcmd{with}
wenzelm@7134
   438
\begin{matharray}{rcl}
wenzelm@7134
   439
  \isarcmd{note} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   440
  \isarcmd{then} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7134
   441
  \isarcmd{from} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7134
   442
  \isarcmd{with} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7134
   443
\end{matharray}
wenzelm@7134
   444
wenzelm@7134
   445
\begin{rail}
wenzelm@7134
   446
  'note' thmdef? thmrefs comment?
wenzelm@7134
   447
  ;
wenzelm@7134
   448
  'then' comment?
wenzelm@7134
   449
  ;
wenzelm@7134
   450
  ('from' | 'with') thmrefs comment?
wenzelm@7134
   451
  ;
wenzelm@7134
   452
\end{rail}
wenzelm@7134
   453
wenzelm@7134
   454
\begin{description}
wenzelm@7134
   455
\item [$ $] FIXME
wenzelm@7134
   456
\end{description}
wenzelm@7134
   457
wenzelm@7134
   458
wenzelm@7134
   459
\subsection{Proof context}
wenzelm@7134
   460
wenzelm@7134
   461
\indexisarcmd{fix}\indexisarcmd{assume}\indexisarcmd{presume}\indexisarcmd{def}\indexisarcmd{let}
wenzelm@7134
   462
\begin{matharray}{rcl}
wenzelm@7134
   463
  \isarcmd{fix} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   464
  \isarcmd{assume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   465
  \isarcmd{presume} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   466
  \isarcmd{def} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   467
  \isarcmd{let} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   468
\end{matharray}
wenzelm@7134
   469
wenzelm@7134
   470
\begin{rail}
wenzelm@7134
   471
  'fix' (var +) comment?
wenzelm@7134
   472
  ;
wenzelm@7134
   473
  ('assume' | 'presume') thmdecl? (proppat +) comment?
wenzelm@7134
   474
  ;
wenzelm@7134
   475
  'def' thmdecl? var '==' termpat comment?
wenzelm@7134
   476
  ;
wenzelm@7134
   477
  'let' ((term + 'as') '=' term comment? + 'and')
wenzelm@7134
   478
  ;
wenzelm@7134
   479
wenzelm@7134
   480
  var: name ('::' type)?
wenzelm@7134
   481
  ;
wenzelm@7134
   482
\end{rail}
wenzelm@7134
   483
wenzelm@7134
   484
\begin{description}
wenzelm@7134
   485
\item [$ $] FIXME
wenzelm@7134
   486
\end{description}
wenzelm@7134
   487
wenzelm@7134
   488
wenzelm@7134
   489
\subsection{Block structure}
wenzelm@7134
   490
wenzelm@7134
   491
\indexisarcmd{next}\indexisarcmd{\{\{}\indexisarcmd{\}\}}
wenzelm@7134
   492
\begin{matharray}{rcl}
wenzelm@7134
   493
  \isarcmd{next} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   494
  \isarcmd{\{\{} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   495
  \isarcmd{\}\}} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   496
\end{matharray}
wenzelm@7134
   497
wenzelm@7134
   498
\begin{rail}
wenzelm@7134
   499
  llbrace
wenzelm@7134
   500
  ;
wenzelm@7134
   501
  rrbrace
wenzelm@7134
   502
  ;
wenzelm@7134
   503
  'next'
wenzelm@7134
   504
  ;
wenzelm@7134
   505
\end{rail}
wenzelm@7134
   506
wenzelm@7134
   507
\begin{description}
wenzelm@7134
   508
\item [$ $] FIXME
wenzelm@7134
   509
\end{description}
wenzelm@7134
   510
wenzelm@7134
   511
wenzelm@7134
   512
\subsection{Calculational proof}
wenzelm@7134
   513
wenzelm@7134
   514
\indexisarcmd{also}\indexisarcmd{finally}
wenzelm@7134
   515
\begin{matharray}{rcl}
wenzelm@7134
   516
  \isarcmd{also} & : & \isartrans{proof(state)}{proof(state)} \\
wenzelm@7134
   517
  \isarcmd{finally} & : & \isartrans{proof(state)}{proof(chain)} \\
wenzelm@7134
   518
\end{matharray}
wenzelm@7134
   519
wenzelm@7134
   520
\begin{rail}
wenzelm@7134
   521
  ('also' | 'finally') transrules? comment?
wenzelm@7134
   522
  ;
wenzelm@7134
   523
wenzelm@7134
   524
  transrules: '(' thmrefs ')' interest?
wenzelm@7134
   525
  ;
wenzelm@7134
   526
\end{rail}
wenzelm@7134
   527
wenzelm@7134
   528
\begin{description}
wenzelm@7134
   529
\item [$ $] FIXME
wenzelm@7134
   530
\end{description}
wenzelm@7134
   531
wenzelm@7134
   532
wenzelm@7134
   533
wenzelm@7134
   534
\subsection{Improper proof steps}
wenzelm@7134
   535
wenzelm@7134
   536
\indexisarcmd{apply}\indexisarcmd{then_apply}\indexisarcmd{back}
wenzelm@7134
   537
\begin{matharray}{rcl}
wenzelm@7134
   538
  \isarcmd{apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7134
   539
  \isarcmd{then_apply}^* & : & \isartrans{proof}{proof} \\
wenzelm@7134
   540
  \isarcmd{back}^* & : & \isartrans{proof}{proof} \\
wenzelm@7134
   541
\end{matharray}
wenzelm@7134
   542
wenzelm@7134
   543
\railalias{thenapply}{then\_apply}
wenzelm@7134
   544
\railterm{thenapply}
wenzelm@7134
   545
wenzelm@7134
   546
\begin{rail}
wenzelm@7134
   547
  'apply' method
wenzelm@7134
   548
  ;
wenzelm@7134
   549
  thenapply method
wenzelm@7134
   550
  ;
wenzelm@7134
   551
  'back'
wenzelm@7134
   552
  ;
wenzelm@7134
   553
\end{rail}
wenzelm@7134
   554
wenzelm@7134
   555
\begin{description}
wenzelm@7134
   556
\item [$ $] FIXME
wenzelm@7134
   557
\end{description}
wenzelm@7134
   558
wenzelm@7134
   559
wenzelm@7134
   560
\section{Other commands}
wenzelm@7134
   561
wenzelm@7134
   562
\subsection{Diagnostics}
wenzelm@7134
   563
wenzelm@7134
   564
\indexisarcmd{typ}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{thm}
wenzelm@7134
   565
\begin{matharray}{rcl}
wenzelm@7134
   566
  \isarcmd{typ} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   567
  \isarcmd{term} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   568
  \isarcmd{prop} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   569
  \isarcmd{thm} & : & \isarkeep{theory~|~proof} \\
wenzelm@7134
   570
\end{matharray}
wenzelm@7134
   571
wenzelm@7134
   572
\begin{rail}
wenzelm@7134
   573
  'typ' type
wenzelm@7134
   574
  ;
wenzelm@7134
   575
  'term' term
wenzelm@7134
   576
  ;
wenzelm@7134
   577
  'prop' prop
wenzelm@7134
   578
  ;
wenzelm@7134
   579
  'thm' thmrefs
wenzelm@7134
   580
  ;
wenzelm@7134
   581
\end{rail}
wenzelm@7134
   582
wenzelm@7134
   583
\begin{description}
wenzelm@7134
   584
\item [$\isarkeyword{typ}~\tau$, $\isarkeyword{term}~t$,
wenzelm@7134
   585
  $\isarkeyword{prop}~\phi$] read and print types / terms / propositions
wenzelm@7134
   586
  according to the current theory or proof context.
wenzelm@7134
   587
\item [$\isarkeyword{thm}~thms$] retrieves lists of theorems from the current
wenzelm@7134
   588
  theory or proof context.  Note that any attributes included in the theorem
wenzelm@7134
   589
  specifications are applied to a temporary proof context derived from the
wenzelm@7134
   590
  current theory or proof; the resulting context is discarded.
wenzelm@7134
   591
\end{description}
wenzelm@7134
   592
wenzelm@7134
   593
wenzelm@7134
   594
\subsection{System operations}
wenzelm@7134
   595
wenzelm@7134
   596
\indexisarcmd{cd}\indexisarcmd{pwd}\indexisarcmd{use_thy}\indexisarcmd{use_thy_only}
wenzelm@7134
   597
\indexisarcmd{update_thy}\indexisarcmd{update_thy_only}
wenzelm@7134
   598
\begin{matharray}{rcl}
wenzelm@7134
   599
  \isarcmd{cd} & : & \isarkeep{\cdot} \\
wenzelm@7134
   600
  \isarcmd{pwd} & : & \isarkeep{\cdot} \\
wenzelm@7134
   601
  \isarcmd{use_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134
   602
  \isarcmd{use_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134
   603
  \isarcmd{update_thy} & : & \isarkeep{\cdot} \\
wenzelm@7134
   604
  \isarcmd{update_thy_only} & : & \isarkeep{\cdot} \\
wenzelm@7134
   605
\end{matharray}
wenzelm@7134
   606
wenzelm@7134
   607
\begin{description}
wenzelm@7134
   608
\item [$\isarkeyword{cd}~name$] changes the current directory of the Isabelle
wenzelm@7134
   609
  process.
wenzelm@7134
   610
\item [$\isarkeyword{pwd}~$] prints the current working directory.
wenzelm@7134
   611
\item [$\isarkeyword{use_thy}~name$, $\isarkeyword{use_thy_only}~name$,
wenzelm@7134
   612
  $\isarkeyword{update_thy}~name$, $\isarkeyword{update_thy_only}~name$] load
wenzelm@7134
   613
  theory files.  These commands are exactly the same as the corresponding ML
wenzelm@7134
   614
  functions (see also \cite[\S1 and \S6]{isabelle-ref}).
wenzelm@7134
   615
\end{description}
wenzelm@7134
   616
wenzelm@7134
   617
wenzelm@7046
   618
%%% Local Variables: 
wenzelm@7046
   619
%%% mode: latex
wenzelm@7046
   620
%%% TeX-master: "isar-ref"
wenzelm@7046
   621
%%% End: