doc-src/IsarRef/Thy/Outer_Syntax.thy
author wenzelm
Sun Oct 31 13:26:37 2010 +0100 (2010-10-31)
changeset 40296 ac4d75f86d97
parent 40291 012ed4426fda
child 42596 6c621a9d612a
permissions -rw-r--r--
syntax category "real" subsumes plain "int";
wenzelm@27037
     1
theory Outer_Syntax
wenzelm@27050
     2
imports Main
wenzelm@27037
     3
begin
wenzelm@27037
     4
wenzelm@27040
     5
chapter {* Outer syntax *}
wenzelm@27037
     6
wenzelm@27037
     7
text {*
wenzelm@27037
     8
  The rather generic framework of Isabelle/Isar syntax emerges from
wenzelm@27037
     9
  three main syntactic categories: \emph{commands} of the top-level
wenzelm@27037
    10
  Isar engine (covering theory and proof elements), \emph{methods} for
wenzelm@27037
    11
  general goal refinements (analogous to traditional ``tactics''), and
wenzelm@27037
    12
  \emph{attributes} for operations on facts (within a certain
wenzelm@27037
    13
  context).  Subsequently we give a reference of basic syntactic
wenzelm@27037
    14
  entities underlying Isabelle/Isar syntax in a bottom-up manner.
wenzelm@27037
    15
  Concrete theory and proof language elements will be introduced later
wenzelm@27037
    16
  on.
wenzelm@27037
    17
wenzelm@27037
    18
  \medskip In order to get started with writing well-formed
wenzelm@27037
    19
  Isabelle/Isar documents, the most important aspect to be noted is
wenzelm@27037
    20
  the difference of \emph{inner} versus \emph{outer} syntax.  Inner
wenzelm@27037
    21
  syntax is that of Isabelle types and terms of the logic, while outer
wenzelm@27037
    22
  syntax is that of Isabelle/Isar theory sources (specifications and
wenzelm@27037
    23
  proofs).  As a general rule, inner syntax entities may occur only as
wenzelm@27037
    24
  \emph{atomic entities} within outer syntax.  For example, the string
wenzelm@27037
    25
  @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term
wenzelm@27037
    26
  specifications within a theory, while @{verbatim "x + y"} without
wenzelm@27037
    27
  quotes is not.
wenzelm@27037
    28
wenzelm@27037
    29
  Printed theory documents usually omit quotes to gain readability
wenzelm@27037
    30
  (this is a matter of {\LaTeX} macro setup, say via @{verbatim
wenzelm@27037
    31
  "\\isabellestyle"}, see also \cite{isabelle-sys}).  Experienced
wenzelm@27037
    32
  users of Isabelle/Isar may easily reconstruct the lost technical
wenzelm@27037
    33
  information, while mere readers need not care about quotes at all.
wenzelm@27037
    34
wenzelm@27037
    35
  \medskip Isabelle/Isar input may contain any number of input
wenzelm@27037
    36
  termination characters ``@{verbatim ";"}'' (semicolon) to separate
wenzelm@27037
    37
  commands explicitly.  This is particularly useful in interactive
wenzelm@27037
    38
  shell sessions to make clear where the current command is intended
wenzelm@27037
    39
  to end.  Otherwise, the interpreter loop will continue to issue a
wenzelm@27037
    40
  secondary prompt ``@{verbatim "#"}'' until an end-of-command is
wenzelm@27037
    41
  clearly recognized from the input syntax, e.g.\ encounter of the
wenzelm@27037
    42
  next command keyword.
wenzelm@27037
    43
wenzelm@27037
    44
  More advanced interfaces such as Proof~General \cite{proofgeneral}
wenzelm@27037
    45
  do not require explicit semicolons, the amount of input text is
wenzelm@27037
    46
  determined automatically by inspecting the present content of the
wenzelm@27037
    47
  Emacs text buffer.  In the printed presentation of Isabelle/Isar
wenzelm@27037
    48
  documents semicolons are omitted altogether for readability.
wenzelm@27037
    49
wenzelm@27037
    50
  \begin{warn}
wenzelm@27037
    51
    Proof~General requires certain syntax classification tables in
wenzelm@27037
    52
    order to achieve properly synchronized interaction with the
wenzelm@27037
    53
    Isabelle/Isar process.  These tables need to be consistent with
wenzelm@27037
    54
    the Isabelle version and particular logic image to be used in a
wenzelm@27037
    55
    running session (common object-logics may well change the outer
wenzelm@27037
    56
    syntax).  The standard setup should work correctly with any of the
wenzelm@27037
    57
    ``official'' logic images derived from Isabelle/HOL (including
wenzelm@27037
    58
    HOLCF etc.).  Users of alternative logics may need to tell
wenzelm@27037
    59
    Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
wenzelm@27037
    60
    (in conjunction with @{verbatim "-l ZF"}, to specify the default
wenzelm@27037
    61
    logic image).  Note that option @{verbatim "-L"} does both
wenzelm@27037
    62
    of this at the same time.
wenzelm@27037
    63
  \end{warn}
wenzelm@27037
    64
*}
wenzelm@27037
    65
wenzelm@27037
    66
wenzelm@28774
    67
section {* Lexical matters \label{sec:outer-lex} *}
wenzelm@27037
    68
wenzelm@28775
    69
text {* The outer lexical syntax consists of three main categories of
wenzelm@28776
    70
  syntax tokens:
wenzelm@28775
    71
wenzelm@28775
    72
  \begin{enumerate}
wenzelm@28775
    73
wenzelm@28775
    74
  \item \emph{major keywords} --- the command names that are available
wenzelm@28775
    75
  in the present logic session;
wenzelm@28775
    76
wenzelm@28775
    77
  \item \emph{minor keywords} --- additional literal tokens required
wenzelm@28775
    78
  by the syntax of commands;
wenzelm@28775
    79
wenzelm@28776
    80
  \item \emph{named tokens} --- various categories of identifiers etc.
wenzelm@27037
    81
wenzelm@28775
    82
  \end{enumerate}
wenzelm@28775
    83
wenzelm@28776
    84
  Major keywords and minor keywords are guaranteed to be disjoint.
wenzelm@28775
    85
  This helps user-interfaces to determine the overall structure of a
wenzelm@28775
    86
  theory text, without knowing the full details of command syntax.
wenzelm@28776
    87
  Internally, there is some additional information about the kind of
wenzelm@28776
    88
  major keywords, which approximates the command type (theory command,
wenzelm@28776
    89
  proof command etc.).
wenzelm@28775
    90
wenzelm@28775
    91
  Keywords override named tokens.  For example, the presence of a
wenzelm@28775
    92
  command called @{verbatim term} inhibits the identifier @{verbatim
wenzelm@28775
    93
  term}, but the string @{verbatim "\"term\""} can be used instead.
wenzelm@28775
    94
  By convention, the outer syntax always allows quoted strings in
wenzelm@28775
    95
  addition to identifiers, wherever a named entity is expected.
wenzelm@28775
    96
wenzelm@28776
    97
  When tokenizing a given input sequence, the lexer repeatedly takes
wenzelm@28776
    98
  the longest prefix of the input that forms a valid token.  Spaces,
wenzelm@28776
    99
  tabs, newlines and formfeeds between tokens serve as explicit
wenzelm@28776
   100
  separators.
wenzelm@28776
   101
wenzelm@28775
   102
  \medskip The categories for named tokens are defined once and for
wenzelm@28775
   103
  all as follows.
wenzelm@27037
   104
wenzelm@28776
   105
  \begin{center}
wenzelm@28775
   106
  \begin{supertabular}{rcl}
wenzelm@28775
   107
    @{syntax_def ident} & = & @{text "letter quasiletter\<^sup>*"} \\
wenzelm@28775
   108
    @{syntax_def longident} & = & @{text "ident("}@{verbatim "."}@{text "ident)\<^sup>+"} \\
wenzelm@28775
   109
    @{syntax_def symident} & = & @{text "sym\<^sup>+  |  "}@{verbatim "\\"}@{verbatim "<"}@{text ident}@{verbatim ">"} \\
wenzelm@28775
   110
    @{syntax_def nat} & = & @{text "digit\<^sup>+"} \\
wenzelm@40290
   111
    @{syntax_def float} & = & @{syntax_ref nat}@{verbatim "."}@{syntax_ref nat}@{text "  |  "}@{verbatim "-"}@{syntax_ref nat}@{verbatim "."}@{syntax_ref nat} \\
wenzelm@28775
   112
    @{syntax_def var} & = & @{verbatim "?"}@{text "ident  |  "}@{verbatim "?"}@{text ident}@{verbatim "."}@{text nat} \\
wenzelm@28775
   113
    @{syntax_def typefree} & = & @{verbatim "'"}@{text ident} \\
wenzelm@28775
   114
    @{syntax_def typevar} & = & @{verbatim "?"}@{text "typefree  |  "}@{verbatim "?"}@{text typefree}@{verbatim "."}@{text nat} \\
wenzelm@28775
   115
    @{syntax_def string} & = & @{verbatim "\""} @{text "\<dots>"} @{verbatim "\""} \\
wenzelm@28775
   116
    @{syntax_def altstring} & = & @{verbatim "`"} @{text "\<dots>"} @{verbatim "`"} \\
wenzelm@28775
   117
    @{syntax_def verbatim} & = & @{verbatim "{*"} @{text "\<dots>"} @{verbatim "*"}@{verbatim "}"} \\[1ex]
wenzelm@28775
   118
wenzelm@28775
   119
    @{text letter} & = & @{text "latin  |  "}@{verbatim "\\"}@{verbatim "<"}@{text latin}@{verbatim ">"}@{text "  |  "}@{verbatim "\\"}@{verbatim "<"}@{text "latin latin"}@{verbatim ">"}@{text "  |  greek  |"} \\
wenzelm@28775
   120
          &   & @{verbatim "\<^isub>"}@{text "  |  "}@{verbatim "\<^isup>"} \\
wenzelm@28775
   121
    @{text quasiletter} & = & @{text "letter  |  digit  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "'"} \\
wenzelm@28775
   122
    @{text latin} & = & @{verbatim a}@{text "  | \<dots> |  "}@{verbatim z}@{text "  |  "}@{verbatim A}@{text "  |  \<dots> |  "}@{verbatim Z} \\
wenzelm@28775
   123
    @{text digit} & = & @{verbatim "0"}@{text "  |  \<dots> |  "}@{verbatim "9"} \\
wenzelm@28775
   124
    @{text sym} & = & @{verbatim "!"}@{text "  |  "}@{verbatim "#"}@{text "  |  "}@{verbatim "$"}@{text "  |  "}@{verbatim "%"}@{text "  |  "}@{verbatim "&"}@{text "  |  "}@{verbatim "*"}@{text "  |  "}@{verbatim "+"}@{text "  |  "}@{verbatim "-"}@{text "  |  "}@{verbatim "/"}@{text "  |"} \\
wenzelm@28775
   125
    & & @{verbatim "<"}@{text "  |  "}@{verbatim "="}@{text "  |  "}@{verbatim ">"}@{text "  |  "}@{verbatim "?"}@{text "  |  "}@{verbatim "@"}@{text "  |  "}@{verbatim "^"}@{text "  |  "}@{verbatim "_"}@{text "  |  "}@{verbatim "|"}@{text "  |  "}@{verbatim "~"} \\
wenzelm@28775
   126
    @{text greek} & = & @{verbatim "\<alpha>"}@{text "  |  "}@{verbatim "\<beta>"}@{text "  |  "}@{verbatim "\<gamma>"}@{text "  |  "}@{verbatim "\<delta>"}@{text "  |"} \\
wenzelm@28775
   127
          &   & @{verbatim "\<epsilon>"}@{text "  |  "}@{verbatim "\<zeta>"}@{text "  |  "}@{verbatim "\<eta>"}@{text "  |  "}@{verbatim "\<theta>"}@{text "  |"} \\
wenzelm@28775
   128
          &   & @{verbatim "\<iota>"}@{text "  |  "}@{verbatim "\<kappa>"}@{text "  |  "}@{verbatim "\<mu>"}@{text "  |  "}@{verbatim "\<nu>"}@{text "  |"} \\
wenzelm@28775
   129
          &   & @{verbatim "\<xi>"}@{text "  |  "}@{verbatim "\<pi>"}@{text "  |  "}@{verbatim "\<rho>"}@{text "  |  "}@{verbatim "\<sigma>"}@{text "  |  "}@{verbatim "\<tau>"}@{text "  |"} \\
wenzelm@28775
   130
          &   & @{verbatim "\<upsilon>"}@{text "  |  "}@{verbatim "\<phi>"}@{text "  |  "}@{verbatim "\<chi>"}@{text "  |  "}@{verbatim "\<psi>"}@{text "  |"} \\
wenzelm@28775
   131
          &   & @{verbatim "\<omega>"}@{text "  |  "}@{verbatim "\<Gamma>"}@{text "  |  "}@{verbatim "\<Delta>"}@{text "  |  "}@{verbatim "\<Theta>"}@{text "  |"} \\
wenzelm@28775
   132
          &   & @{verbatim "\<Lambda>"}@{text "  |  "}@{verbatim "\<Xi>"}@{text "  |  "}@{verbatim "\<Pi>"}@{text "  |  "}@{verbatim "\<Sigma>"}@{text "  |"} \\
wenzelm@28775
   133
          &   & @{verbatim "\<Upsilon>"}@{text "  |  "}@{verbatim "\<Phi>"}@{text "  |  "}@{verbatim "\<Psi>"}@{text "  |  "}@{verbatim "\<Omega>"} \\
wenzelm@28775
   134
  \end{supertabular}
wenzelm@28776
   135
  \end{center}
wenzelm@27037
   136
wenzelm@28778
   137
  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
wenzelm@28778
   138
  which is internally a pair of base name and index (ML type @{ML_type
wenzelm@28778
   139
  indexname}).  These components are either separated by a dot as in
wenzelm@28778
   140
  @{text "?x.1"} or @{text "?x7.3"} or run together as in @{text
wenzelm@28778
   141
  "?x1"}.  The latter form is possible if the base name does not end
wenzelm@28778
   142
  with digits.  If the index is 0, it may be dropped altogether:
wenzelm@28778
   143
  @{text "?x"} and @{text "?x0"} and @{text "?x.0"} all refer to the
wenzelm@28778
   144
  same unknown, with basename @{text "x"} and index 0.
wenzelm@28778
   145
wenzelm@28778
   146
  The syntax of @{syntax_ref string} admits any characters, including
wenzelm@27037
   147
  newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
wenzelm@27037
   148
  "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
wenzelm@27037
   149
  character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
wenzelm@27037
   150
  with three decimal digits.  Alternative strings according to
wenzelm@28778
   151
  @{syntax_ref altstring} are analogous, using single back-quotes
wenzelm@28778
   152
  instead.
wenzelm@28778
   153
wenzelm@28778
   154
  The body of @{syntax_ref verbatim} may consist of any text not
wenzelm@27037
   155
  containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
wenzelm@28778
   156
  convenient inclusion of quotes without further escapes.  There is no
wenzelm@28778
   157
  way to escape ``@{verbatim "*"}@{verbatim "}"}''.  If the quoted
wenzelm@28778
   158
  text is {\LaTeX} source, one may usually add some blank or comment
wenzelm@28778
   159
  to avoid the critical character sequence.
wenzelm@28778
   160
wenzelm@28778
   161
  Source comments take the form @{verbatim "(*"}~@{text
wenzelm@28778
   162
  "\<dots>"}~@{verbatim "*)"} and may be nested, although the user-interface
wenzelm@28778
   163
  might prevent this.  Note that this form indicates source comments
wenzelm@28778
   164
  only, which are stripped after lexical analysis of the input.  The
wenzelm@28778
   165
  Isar syntax also provides proper \emph{document comments} that are
wenzelm@28778
   166
  considered as part of the text (see \secref{sec:comments}).
wenzelm@27037
   167
wenzelm@27037
   168
  Common mathematical symbols such as @{text \<forall>} are represented in
wenzelm@27037
   169
  Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
wenzelm@27037
   170
  symbols like this, although proper presentation is left to front-end
wenzelm@27037
   171
  tools such as {\LaTeX} or Proof~General with the X-Symbol package.
wenzelm@29719
   172
  A list of predefined Isabelle symbols that work well with these
wenzelm@29719
   173
  tools is given in \appref{app:symbols}.  Note that @{verbatim "\<lambda>"}
wenzelm@29719
   174
  does not belong to the @{text letter} category, since it is already
wenzelm@29719
   175
  used differently in the Pure term language.
wenzelm@27037
   176
*}
wenzelm@27037
   177
wenzelm@27037
   178
wenzelm@27037
   179
section {* Common syntax entities *}
wenzelm@27037
   180
wenzelm@27037
   181
text {*
wenzelm@27037
   182
  We now introduce several basic syntactic entities, such as names,
wenzelm@27037
   183
  terms, and theorem specifications, which are factored out of the
wenzelm@27037
   184
  actual Isar language elements to be described later.
wenzelm@27037
   185
*}
wenzelm@27037
   186
wenzelm@27037
   187
wenzelm@27037
   188
subsection {* Names *}
wenzelm@27037
   189
wenzelm@27037
   190
text {*
wenzelm@27037
   191
  Entity \railqtok{name} usually refers to any name of types,
wenzelm@27037
   192
  constants, theorems etc.\ that are to be \emph{declared} or
wenzelm@27037
   193
  \emph{defined} (so qualified identifiers are excluded here).  Quoted
wenzelm@27037
   194
  strings provide an escape for non-identifier names or those ruled
wenzelm@27037
   195
  out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
wenzelm@27037
   196
  Already existing objects are usually referenced by
wenzelm@27037
   197
  \railqtok{nameref}.
wenzelm@27037
   198
wenzelm@27037
   199
  \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
wenzelm@27037
   200
  \begin{rail}
wenzelm@27037
   201
    name: ident | symident | string | nat
wenzelm@27037
   202
    ;
wenzelm@27037
   203
    parname: '(' name ')'
wenzelm@27037
   204
    ;
wenzelm@27037
   205
    nameref: name | longident
wenzelm@27037
   206
    ;
wenzelm@40296
   207
  \end{rail}
wenzelm@40296
   208
*}
wenzelm@40296
   209
wenzelm@40296
   210
wenzelm@40296
   211
subsection {* Numbers *}
wenzelm@40296
   212
wenzelm@40296
   213
text {* The outer lexical syntax (\secref{sec:outer-lex}) admits
wenzelm@40296
   214
  natural numbers and floating point numbers.  These are combined as
wenzelm@40296
   215
  @{syntax int} and @{syntax real} as follows.
wenzelm@40296
   216
wenzelm@40296
   217
  \indexoutertoken{int}\indexoutertoken{real}
wenzelm@40296
   218
  \begin{rail}
wenzelm@27037
   219
    int: nat | '-' nat
wenzelm@27037
   220
    ;
wenzelm@40296
   221
    real: float | int
wenzelm@40296
   222
    ;
wenzelm@27037
   223
  \end{rail}
wenzelm@40296
   224
wenzelm@40296
   225
  Note that there is an overlap with the category \railqtok{name},
wenzelm@40296
   226
  which also includes @{syntax nat}.
wenzelm@27037
   227
*}
wenzelm@27037
   228
wenzelm@27037
   229
wenzelm@27037
   230
subsection {* Comments \label{sec:comments} *}
wenzelm@27037
   231
wenzelm@27037
   232
text {*
wenzelm@27037
   233
  Large chunks of plain \railqtok{text} are usually given
wenzelm@27037
   234
  \railtok{verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
wenzelm@27037
   235
  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}.  For convenience,
wenzelm@27037
   236
  any of the smaller text units conforming to \railqtok{nameref} are
wenzelm@27037
   237
  admitted as well.  A marginal \railnonterm{comment} is of the form
wenzelm@27037
   238
  @{verbatim "--"} \railqtok{text}.  Any number of these may occur
wenzelm@27037
   239
  within Isabelle/Isar commands.
wenzelm@27037
   240
wenzelm@27037
   241
  \indexoutertoken{text}\indexouternonterm{comment}
wenzelm@27037
   242
  \begin{rail}
wenzelm@27037
   243
    text: verbatim | nameref
wenzelm@27037
   244
    ;
wenzelm@27037
   245
    comment: '--' text
wenzelm@27037
   246
    ;
wenzelm@27037
   247
  \end{rail}
wenzelm@27037
   248
*}
wenzelm@27037
   249
wenzelm@27037
   250
wenzelm@27037
   251
subsection {* Type classes, sorts and arities *}
wenzelm@27037
   252
wenzelm@27037
   253
text {*
wenzelm@27037
   254
  Classes are specified by plain names.  Sorts have a very simple
wenzelm@27037
   255
  inner syntax, which is either a single class name @{text c} or a
wenzelm@27037
   256
  list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
wenzelm@27037
   257
  intersection of these classes.  The syntax of type arities is given
wenzelm@27037
   258
  directly at the outer level.
wenzelm@27037
   259
wenzelm@27037
   260
  \indexouternonterm{sort}\indexouternonterm{arity}
wenzelm@27037
   261
  \indexouternonterm{classdecl}
wenzelm@27037
   262
  \begin{rail}
wenzelm@27037
   263
    classdecl: name (('<' | subseteq) (nameref + ','))?
wenzelm@27037
   264
    ;
wenzelm@27037
   265
    sort: nameref
wenzelm@27037
   266
    ;
wenzelm@27037
   267
    arity: ('(' (sort + ',') ')')? sort
wenzelm@27037
   268
    ;
wenzelm@27037
   269
  \end{rail}
wenzelm@27037
   270
*}
wenzelm@27037
   271
wenzelm@27037
   272
wenzelm@27037
   273
subsection {* Types and terms \label{sec:types-terms} *}
wenzelm@27037
   274
wenzelm@27037
   275
text {*
wenzelm@27037
   276
  The actual inner Isabelle syntax, that of types and terms of the
wenzelm@27037
   277
  logic, is far too sophisticated in order to be modelled explicitly
wenzelm@27037
   278
  at the outer theory level.  Basically, any such entity has to be
wenzelm@27037
   279
  quoted to turn it into a single token (the parsing and type-checking
wenzelm@27037
   280
  is performed internally later).  For convenience, a slightly more
wenzelm@27037
   281
  liberal convention is adopted: quotes may be omitted for any type or
wenzelm@27037
   282
  term that is already atomic at the outer level.  For example, one
wenzelm@27037
   283
  may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}.
wenzelm@27037
   284
  Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
wenzelm@27037
   285
  "\<forall>"} are available as well, provided these have not been superseded
wenzelm@27037
   286
  by commands or other keywords already (such as @{verbatim "="} or
wenzelm@27037
   287
  @{verbatim "+"}).
wenzelm@27037
   288
wenzelm@27037
   289
  \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
wenzelm@27037
   290
  \begin{rail}
wenzelm@27037
   291
    type: nameref | typefree | typevar
wenzelm@27037
   292
    ;
wenzelm@27037
   293
    term: nameref | var
wenzelm@27037
   294
    ;
wenzelm@27037
   295
    prop: term
wenzelm@27037
   296
    ;
wenzelm@27037
   297
  \end{rail}
wenzelm@27037
   298
wenzelm@27037
   299
  Positional instantiations are indicated by giving a sequence of
wenzelm@27037
   300
  terms, or the placeholder ``@{text _}'' (underscore), which means to
wenzelm@27037
   301
  skip a position.
wenzelm@27037
   302
wenzelm@27037
   303
  \indexoutertoken{inst}\indexoutertoken{insts}
wenzelm@27037
   304
  \begin{rail}
wenzelm@27037
   305
    inst: underscore | term
wenzelm@27037
   306
    ;
wenzelm@27037
   307
    insts: (inst *)
wenzelm@27037
   308
    ;
wenzelm@27037
   309
  \end{rail}
wenzelm@27037
   310
wenzelm@27037
   311
  Type declarations and definitions usually refer to
wenzelm@27037
   312
  \railnonterm{typespec} on the left-hand side.  This models basic
wenzelm@27037
   313
  type constructor application at the outer syntax level.  Note that
wenzelm@27037
   314
  only plain postfix notation is available here, but no infixes.
wenzelm@27037
   315
wenzelm@27037
   316
  \indexouternonterm{typespec}
wenzelm@35841
   317
  \indexouternonterm{typespecsorts}
wenzelm@27037
   318
  \begin{rail}
wenzelm@27037
   319
    typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
wenzelm@27037
   320
    ;
wenzelm@35841
   321
wenzelm@35841
   322
    typespecsorts: (() | (typefree ('::' sort)?) | '(' ( (typefree ('::' sort)?) + ',' ) ')') name
wenzelm@35841
   323
    ;
wenzelm@27037
   324
  \end{rail}
wenzelm@27037
   325
*}
wenzelm@27037
   326
wenzelm@27037
   327
wenzelm@28754
   328
subsection {* Term patterns and declarations \label{sec:term-decls} *}
wenzelm@28754
   329
wenzelm@28754
   330
text {*
wenzelm@28754
   331
  Wherever explicit propositions (or term fragments) occur in a proof
wenzelm@28754
   332
  text, casual binding of schematic term variables may be given
wenzelm@28754
   333
  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
wenzelm@28754
   334
  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
wenzelm@28754
   335
wenzelm@28754
   336
  \indexouternonterm{termpat}\indexouternonterm{proppat}
wenzelm@28754
   337
  \begin{rail}
wenzelm@28754
   338
    termpat: '(' ('is' term +) ')'
wenzelm@28754
   339
    ;
wenzelm@28754
   340
    proppat: '(' ('is' prop +) ')'
wenzelm@28754
   341
    ;
wenzelm@28754
   342
  \end{rail}
wenzelm@28754
   343
wenzelm@28754
   344
  \medskip Declarations of local variables @{text "x :: \<tau>"} and
wenzelm@28754
   345
  logical propositions @{text "a : \<phi>"} represent different views on
wenzelm@28754
   346
  the same principle of introducing a local scope.  In practice, one
wenzelm@28754
   347
  may usually omit the typing of \railnonterm{vars} (due to
wenzelm@28754
   348
  type-inference), and the naming of propositions (due to implicit
wenzelm@28754
   349
  references of current facts).  In any case, Isar proof elements
wenzelm@28754
   350
  usually admit to introduce multiple such items simultaneously.
wenzelm@28754
   351
wenzelm@28754
   352
  \indexouternonterm{vars}\indexouternonterm{props}
wenzelm@28754
   353
  \begin{rail}
wenzelm@28754
   354
    vars: (name+) ('::' type)?
wenzelm@28754
   355
    ;
wenzelm@28754
   356
    props: thmdecl? (prop proppat? +)
wenzelm@28754
   357
    ;
wenzelm@28754
   358
  \end{rail}
wenzelm@28754
   359
wenzelm@28754
   360
  The treatment of multiple declarations corresponds to the
wenzelm@28754
   361
  complementary focus of \railnonterm{vars} versus
wenzelm@28754
   362
  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
wenzelm@28754
   363
  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
wenzelm@28754
   364
  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
wenzelm@28754
   365
  Isar language elements that refer to \railnonterm{vars} or
wenzelm@28754
   366
  \railnonterm{props} typically admit separate typings or namings via
wenzelm@28754
   367
  another level of iteration, with explicit @{keyword_ref "and"}
wenzelm@28754
   368
  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
wenzelm@28754
   369
  \secref{sec:proof-context}.
wenzelm@28754
   370
*}
wenzelm@28754
   371
wenzelm@28754
   372
wenzelm@27037
   373
subsection {* Attributes and theorems \label{sec:syn-att} *}
wenzelm@27037
   374
wenzelm@28754
   375
text {* Attributes have their own ``semi-inner'' syntax, in the sense
wenzelm@28754
   376
  that input conforming to \railnonterm{args} below is parsed by the
wenzelm@28754
   377
  attribute a second time.  The attribute argument specifications may
wenzelm@28754
   378
  be any sequence of atomic entities (identifiers, strings etc.), or
wenzelm@28754
   379
  properly bracketed argument lists.  Below \railqtok{atom} refers to
wenzelm@28754
   380
  any atomic entity, including any \railtok{keyword} conforming to
wenzelm@28754
   381
  \railtok{symident}.
wenzelm@27037
   382
wenzelm@27037
   383
  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
wenzelm@27037
   384
  \begin{rail}
wenzelm@40291
   385
    atom: nameref | typefree | typevar | var | nat | float | keyword
wenzelm@27037
   386
    ;
wenzelm@27037
   387
    arg: atom | '(' args ')' | '[' args ']'
wenzelm@27037
   388
    ;
wenzelm@27037
   389
    args: arg *
wenzelm@27037
   390
    ;
wenzelm@27037
   391
    attributes: '[' (nameref args * ',') ']'
wenzelm@27037
   392
    ;
wenzelm@27037
   393
  \end{rail}
wenzelm@27037
   394
wenzelm@27037
   395
  Theorem specifications come in several flavors:
wenzelm@27037
   396
  \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
wenzelm@27037
   397
  axioms, assumptions or results of goal statements, while
wenzelm@27037
   398
  \railnonterm{thmdef} collects lists of existing theorems.  Existing
wenzelm@27037
   399
  theorems are given by \railnonterm{thmref} and
wenzelm@27037
   400
  \railnonterm{thmrefs}, the former requires an actual singleton
wenzelm@27037
   401
  result.
wenzelm@27037
   402
wenzelm@27037
   403
  There are three forms of theorem references:
wenzelm@27037
   404
  \begin{enumerate}
wenzelm@27037
   405
  
wenzelm@27037
   406
  \item named facts @{text "a"},
wenzelm@27037
   407
wenzelm@27037
   408
  \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
wenzelm@27037
   409
wenzelm@27037
   410
  \item literal fact propositions using @{syntax_ref altstring} syntax
wenzelm@27037
   411
  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
wenzelm@28754
   412
  @{method_ref fact}).
wenzelm@27037
   413
wenzelm@27037
   414
  \end{enumerate}
wenzelm@27037
   415
wenzelm@27037
   416
  Any kind of theorem specification may include lists of attributes
wenzelm@27037
   417
  both on the left and right hand sides; attributes are applied to any
wenzelm@27037
   418
  immediately preceding fact.  If names are omitted, the theorems are
wenzelm@27037
   419
  not stored within the theorem database of the theory or proof
wenzelm@27037
   420
  context, but any given attributes are applied nonetheless.
wenzelm@27037
   421
wenzelm@27037
   422
  An extra pair of brackets around attributes (like ``@{text
wenzelm@27037
   423
  "[[simproc a]]"}'') abbreviates a theorem reference involving an
wenzelm@27037
   424
  internal dummy fact, which will be ignored later on.  So only the
wenzelm@27037
   425
  effect of the attribute on the background context will persist.
wenzelm@27037
   426
  This form of in-place declarations is particularly useful with
wenzelm@27037
   427
  commands like @{command "declare"} and @{command "using"}.
wenzelm@27037
   428
wenzelm@27037
   429
  \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
wenzelm@27037
   430
  \indexouternonterm{thmdef}\indexouternonterm{thmref}
wenzelm@27037
   431
  \indexouternonterm{thmrefs}\indexouternonterm{selection}
wenzelm@27037
   432
  \begin{rail}
wenzelm@27037
   433
    axmdecl: name attributes? ':'
wenzelm@27037
   434
    ;
wenzelm@27037
   435
    thmdecl: thmbind ':'
wenzelm@27037
   436
    ;
wenzelm@27037
   437
    thmdef: thmbind '='
wenzelm@27037
   438
    ;
wenzelm@27037
   439
    thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
wenzelm@27037
   440
    ;
wenzelm@27037
   441
    thmrefs: thmref +
wenzelm@27037
   442
    ;
wenzelm@27037
   443
wenzelm@27037
   444
    thmbind: name attributes | name | attributes
wenzelm@27037
   445
    ;
wenzelm@27037
   446
    selection: '(' ((nat | nat '-' nat?) + ',') ')'
wenzelm@27037
   447
    ;
wenzelm@27037
   448
  \end{rail}
wenzelm@27037
   449
*}
wenzelm@27037
   450
wenzelm@27037
   451
end