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