doc-src/IsarRef/syntax.tex
author wenzelm
Fri, 30 Jul 1999 15:40:54 +0200
changeset 7135 8eabfd7e6b9b
parent 7134 320b412e5800
child 7141 a67dde8820c0
permissions -rw-r--r--
more;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
     1
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
     2
%FIXME
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
     3
% - examples (!?)
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
     4
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     5
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     6
\chapter{Isar document syntax}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     7
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
     8
FIXME shortcut
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
     9
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    10
FIXME important note: inner versus outer syntax
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    11
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    12
\section{Lexical matters}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    13
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    14
\section{Common syntax entities}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    15
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    16
The Isar proof and theory language syntax has been carefully designed with
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    17
orthogonality in mind.  Subsequently, we introduce several basic syntactic
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    18
entities, such as names, terms, theorem specifications, which have been
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    19
factored out of the actual Isar language elements described later.
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    20
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    21
Some of the basic syntactic entities introduced below act much like tokens
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    22
rather than nonterminals, in particular for error messages are concerned.
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    23
E.g.\ syntax elements such as $\CONSTS$ referring to \railqtoken{name} or
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    24
\railqtoken{type} would really report a missing \railqtoken{name} or
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    25
\railqtoken{type} rather than any of its constituent primitive tokens
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    26
(\railtoken{ident}, \railtoken{string} etc.).
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    27
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    28
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    29
\subsection{Names}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    30
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    31
Entity \railqtoken{name} usually refers to any name of types, constants,
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    32
theorems, etc.\ to be \emph{declared} or \emph{defined} (so qualified
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    33
identifiers are excluded).  Quoted strings provide an escape for
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    34
non-identifier names or those ruled out by outer syntax keywords (e.g.\ 
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    35
\verb|"let"|).  Already existing objects are usually referenced by
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    36
\railqtoken{nameref}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    37
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    38
\indexoutertoken{name}\indexoutertoken{nameref}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    39
\begin{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    40
  name : ident | symident | string
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    41
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    42
  nameref : name | longident
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    43
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    44
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    45
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    46
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    47
\subsection{Comments}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    48
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    49
Large chunks of plain \railqtoken{text} are usually given \railtoken{verbatim},
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    50
i.e.\ enclosed in \verb|{*|\dots\verb|*}|.  For convenience, any of the
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    51
smaller text entities (\railtoken{ident}, \railtoken{string} etc.)  are
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    52
admitted as well.  Almost any of the Isar commands may be annotated by a
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    53
marginal \railnonterm{comment}: \texttt{--} \railqtoken{text}.  Note that this
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    54
kind of comment is actually part of the language, while source level comments
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    55
\verb|(*|\dots\verb|*)| are already stripped at the lexical level.  A few
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    56
commands such as $\PROOFNAME$ admit additional markup with a ``level of
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    57
interest'', currently only \texttt{\%} for ``boring, don't read this''.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    58
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    59
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    60
\begin{rail}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    61
  text : verbatim | nameref
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    62
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    63
  comment : '--' text
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    64
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    65
  interest : '\%'
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    66
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    67
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    68
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    69
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    70
\subsection{Sorts and arities}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    71
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    72
The syntax of sorts and arities is given directly at the outer level.  Note
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    73
that this in contrast to that types and terms (see below).  Only few commands
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    74
ever refer to sorts or arities explicitly.
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    75
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    76
\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
7135
wenzelm
parents: 7134
diff changeset
    77
\indexouternonterm{classdecl}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    78
\begin{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    79
  sort : nameref | lbrace (nameref * ',') rbrace
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    80
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    81
  arity : ( () | '(' (sort + ',') ')' ) sort
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    82
  ;
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    83
  simplearity : ( () | '(' (sort + ',') ')' ) nameref
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    84
  ;
7135
wenzelm
parents: 7134
diff changeset
    85
  classdecl: name ('<' (nameref ',' +))? comment?
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    86
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    87
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    88
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    89
\subsection{Types and terms}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    90
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    91
The actual inner Isabelle syntax, i.e.\ that of types and terms, is far too
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    92
flexible in order to be modeled explicitly at the outer theory level.
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    93
Basically, any such entity would have to be quoted at the outer level to turn
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    94
it into a single token, with the actual parsing deferred to some functions
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    95
that read and type-check terms etc.\ (note that \railqtoken{prop}s will be
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    96
handled differently from plain \railqtoken{term}s here).  For convenience, the
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    97
quotes may be omitted for any \emph{atomic} term or type (e.g.\ a single
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    98
variable).
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
    99
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   100
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   101
\begin{rail}
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   102
  type : nameref | typefree | typevar
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   103
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   104
  term : nameref | var | textvar | nat
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   105
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   106
  prop : term
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   107
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   108
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   109
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   110
Type definitions etc.\ usually refer to \railnonterm{typespec} on the
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   111
left-hand side.  This models basic type constructor application at the outer
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   112
syntax level.  Note that only plain postfix notation is available here, but no
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   113
infixes.
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   114
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   115
\indexouternonterm{typespec}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   116
\begin{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   117
  typespec : (() | typefree | '(' ( typefree + ',' ) ')') name
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   118
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   119
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   120
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   121
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   122
\subsection{Term patterns}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   123
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   124
Statements like $\SHOWNAME$ involve propositions, some others like $\DEFNAME$
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   125
plain terms.  Any of these usually admit automatic binding of schematic text
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   126
variables by giving (optional) patterns $\IS{p@1 \dots p@n}$.  For
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   127
\railqtoken{prop}s the $\CONCLNAME$ part refers to the conclusion only, in case
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   128
actual rules are involved, rather than atomic propositions.
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   129
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   130
\indexouternonterm{termpat}\indexouternonterm{proppat}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   131
\begin{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   132
  termpat : '(' (term + 'is' ) ')'
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   133
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   134
  proppat : '(' (() | (prop + 'is' )) (() | 'concl' (prop + 'is' )) ')'
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   135
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   136
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   137
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   138
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   139
\subsection{Mixfix annotations}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   140
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   141
Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   142
terms.  Some commands such as $\TYPES$ admit infixes only, while $\CONSTS$
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   143
etc.\ support the full range of general mixfixes and binders.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   144
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   145
\indexouternonterm{infix}\indexouternonterm{mixfix}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   146
\begin{rail}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   147
  infix : '(' ('infixl' | 'infixr') (() | string) nat ')'
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   148
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   149
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   150
  mixfix : infix | string (() | '[' (nat + ',') ']') (() | nat) |
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   151
  'binder' string (() | '[' (nat + ',') ']') nat
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   152
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   153
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   154
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   155
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   156
\subsection{Attributes and theorems}\label{sec:syn-att}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   157
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   158
Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   159
``semi-inner'' syntax, which does not have to be atomic at the outer level
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   160
unlike that of types and terms.  Instead, the attribute argument
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   161
specifications may be any sequence of atomic entities (identifiers, strings
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   162
etc.), or properly bracketed argument lists.  Below \railqtoken{atom} refers to
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   163
any atomic entity (\railtoken{ident}, \railtoken{longident},
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   164
\railtoken{symident} etc.), including keywords that conform to
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   165
\railtoken{symident}, but do not coincide with actual command names.
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   166
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   167
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   168
\begin{rail}
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   169
  atom : nameref | typefree | typevar | var | textvar | nat
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   170
  ;
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   171
  arg : atom | '(' args ')' | '[' args ']' | lbrace args rbrace
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   172
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   173
  args : arg *
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   174
  ;
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   175
  attributes : '[' (nameref args * ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   176
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   177
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   178
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   179
Theorem specifications come in three flavors: \railnonterm{thmdecl} usually
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   180
refers to the result of an assumption or goal statement (e.g.\ $\SHOWNAME$),
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   181
\railnonterm{thmdef} collects lists of existing theorems (as in $\NOTENAME$),
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   182
\railnonterm{thmrefs} refers to any list of existing theorems (e.g.\ occurring
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   183
as proof method arguments).  Any of these may include lists of attributes,
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   184
which are applied to the preceding theorem or list of theorems.
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   185
7135
wenzelm
parents: 7134
diff changeset
   186
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
wenzelm
parents: 7134
diff changeset
   187
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   188
\begin{rail}
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   189
  thmname : name attributes | name | attributes
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   190
  ;
7135
wenzelm
parents: 7134
diff changeset
   191
  axmdecl : name attributes? ':'
wenzelm
parents: 7134
diff changeset
   192
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   193
  thmdecl : thmname ':'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   194
  ;
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   195
  thmdef : thmname '='
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   196
  ;
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   197
  thmrefs : nameref (() | attributes) +
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   198
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   199
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   200
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   201
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   202
\subsection{Proof methods}\label{sec:syn-meth}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   203
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   204
Proof methods are either basic ones, or expressions composed of methods via
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   205
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternatives),
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   206
``\texttt{?}'' (try), ``\texttt{*}'' (repeat, ${} \ge 0$ times),
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   207
``\texttt{+}'' (repeat, ${} > 0$ times).  In practice, proof methods are very
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   208
often just a comma separated list of \railqtoken{nameref}~\railnonterm{args}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   209
specifications.  Thus the syntax is similar to that of attributes, with plain
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   210
parentheses instead of square brackets (see also \S\ref{sec:syn-att}).  Note
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   211
that parentheses may be dropped for single method specifications without
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   212
arguments.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   213
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   214
\indexouternonterm{method}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   215
\begin{rail}
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   216
  method : (nameref | '(' methods ')') (() | '?' | '*' | '+')
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   217
  ;
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   218
  methods : (nameref args | method) + (',' | '|')
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   219
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   220
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   221
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   222
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   223
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   224
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   225
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   226
%%% End: