src/Doc/Isar_Ref/Outer_Syntax.thy
author wenzelm
Thu Nov 05 00:02:30 2015 +0100 (2015-11-05)
changeset 61579 634cd44bb1d3
parent 61503 28e788ca2c5d
child 61656 cfabbc083977
permissions -rw-r--r--
symbolic syntax "\<comment> text";
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@61477
     9
  three main syntactic categories: \<^emph>\<open>commands\<close> of the top-level
wenzelm@61477
    10
  Isar engine (covering theory and proof elements), \<^emph>\<open>methods\<close> for
wenzelm@27037
    11
  general goal refinements (analogous to traditional ``tactics''), and
wenzelm@61477
    12
  \<^emph>\<open>attributes\<close> 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@61421
    18
  \<^medskip>
wenzelm@61421
    19
  In order to get started with writing well-formed
wenzelm@27037
    20
  Isabelle/Isar documents, the most important aspect to be noted is
wenzelm@61477
    21
  the difference of \<^emph>\<open>inner\<close> versus \<^emph>\<open>outer\<close> syntax.  Inner
wenzelm@27037
    22
  syntax is that of Isabelle types and terms of the logic, while outer
wenzelm@27037
    23
  syntax is that of Isabelle/Isar theory sources (specifications and
wenzelm@27037
    24
  proofs).  As a general rule, inner syntax entities may occur only as
wenzelm@61477
    25
  \<^emph>\<open>atomic entities\<close> within outer syntax.  For example, the string
wenzelm@61503
    26
  \<^verbatim>\<open>"x + y"\<close> and identifier \<^verbatim>\<open>z\<close> are legal term
wenzelm@61503
    27
  specifications within a theory, while \<^verbatim>\<open>x + y\<close> without
wenzelm@27037
    28
  quotes is not.
wenzelm@27037
    29
wenzelm@27037
    30
  Printed theory documents usually omit quotes to gain readability
wenzelm@61503
    31
  (this is a matter of {\LaTeX} macro setup, say via \<^verbatim>\<open>\isabellestyle\<close>,
wenzelm@61503
    32
  see also @{cite "isabelle-system"}).  Experienced
wenzelm@27037
    33
  users of Isabelle/Isar may easily reconstruct the lost technical
wenzelm@27037
    34
  information, while mere readers need not care about quotes at all.
wenzelm@58618
    35
\<close>
wenzelm@27037
    36
wenzelm@27037
    37
wenzelm@58618
    38
section \<open>Commands\<close>
wenzelm@50213
    39
wenzelm@58618
    40
text \<open>
wenzelm@50213
    41
  \begin{matharray}{rcl}
wenzelm@61493
    42
    @{command_def "print_commands"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
wenzelm@61493
    43
    @{command_def "help"}\<open>\<^sup>*\<close> & : & \<open>any \<rightarrow>\<close> \\
wenzelm@50213
    44
  \end{matharray}
wenzelm@50213
    45
wenzelm@55112
    46
  @{rail \<open>
wenzelm@50213
    47
    @@{command help} (@{syntax name} * )
wenzelm@55112
    48
  \<close>}
wenzelm@50213
    49
wenzelm@61439
    50
  \<^descr> @{command "print_commands"} prints all outer syntax keywords
wenzelm@50213
    51
  and commands.
wenzelm@50213
    52
wenzelm@61493
    53
  \<^descr> @{command "help"}~\<open>pats\<close> retrieves outer syntax
wenzelm@50213
    54
  commands according to the specified name patterns.
wenzelm@58618
    55
\<close>
wenzelm@50213
    56
wenzelm@50213
    57
wenzelm@58618
    58
subsubsection \<open>Examples\<close>
wenzelm@50213
    59
wenzelm@58618
    60
text \<open>Some common diagnostic commands are retrieved like this
wenzelm@58618
    61
  (according to usual naming conventions):\<close>
wenzelm@50213
    62
wenzelm@50213
    63
help "print"
wenzelm@50213
    64
help "find"
wenzelm@50213
    65
wenzelm@50213
    66
wenzelm@58618
    67
section \<open>Lexical matters \label{sec:outer-lex}\<close>
wenzelm@27037
    68
wenzelm@58618
    69
text \<open>The outer lexical syntax consists of three main categories of
wenzelm@28776
    70
  syntax tokens:
wenzelm@28775
    71
wenzelm@61477
    72
  \<^enum> \<^emph>\<open>major keywords\<close> --- the command names that are available
wenzelm@28775
    73
  in the present logic session;
wenzelm@28775
    74
wenzelm@61477
    75
  \<^enum> \<^emph>\<open>minor keywords\<close> --- additional literal tokens required
wenzelm@28775
    76
  by the syntax of commands;
wenzelm@28775
    77
wenzelm@61477
    78
  \<^enum> \<^emph>\<open>named tokens\<close> --- various categories of identifiers etc.
wenzelm@27037
    79
wenzelm@28775
    80
wenzelm@28776
    81
  Major keywords and minor keywords are guaranteed to be disjoint.
wenzelm@28775
    82
  This helps user-interfaces to determine the overall structure of a
wenzelm@28775
    83
  theory text, without knowing the full details of command syntax.
wenzelm@28776
    84
  Internally, there is some additional information about the kind of
wenzelm@28776
    85
  major keywords, which approximates the command type (theory command,
wenzelm@28776
    86
  proof command etc.).
wenzelm@28775
    87
wenzelm@28775
    88
  Keywords override named tokens.  For example, the presence of a
wenzelm@61503
    89
  command called \<^verbatim>\<open>term\<close> inhibits the identifier \<^verbatim>\<open>term\<close>, but the
wenzelm@61503
    90
  string \<^verbatim>\<open>"term"\<close> can be used instead.
wenzelm@28775
    91
  By convention, the outer syntax always allows quoted strings in
wenzelm@28775
    92
  addition to identifiers, wherever a named entity is expected.
wenzelm@28775
    93
wenzelm@28776
    94
  When tokenizing a given input sequence, the lexer repeatedly takes
wenzelm@28776
    95
  the longest prefix of the input that forms a valid token.  Spaces,
wenzelm@28776
    96
  tabs, newlines and formfeeds between tokens serve as explicit
wenzelm@28776
    97
  separators.
wenzelm@28776
    98
wenzelm@61421
    99
  \<^medskip>
wenzelm@61421
   100
  The categories for named tokens are defined once and for all as follows.
wenzelm@27037
   101
wenzelm@28776
   102
  \begin{center}
wenzelm@28775
   103
  \begin{supertabular}{rcl}
wenzelm@61493
   104
    @{syntax_def ident} & = & \<open>letter (subscript\<^sup>? quasiletter)\<^sup>*\<close> \\
wenzelm@61503
   105
    @{syntax_def longident} & = & \<open>ident(\<close>\<^verbatim>\<open>.\<close>\<open>ident)\<^sup>+\<close> \\
wenzelm@61503
   106
    @{syntax_def symident} & = & \<open>sym\<^sup>+  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>ident\<close>\<^verbatim>\<open>>\<close> \\
wenzelm@61493
   107
    @{syntax_def nat} & = & \<open>digit\<^sup>+\<close> \\
wenzelm@61503
   108
    @{syntax_def float} & = & @{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat}~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>@{syntax_ref nat}\<^verbatim>\<open>.\<close>@{syntax_ref nat} \\
wenzelm@61503
   109
    @{syntax_def var} & = & \<^verbatim>\<open>?\<close>\<open>ident  |\<close>~~\<^verbatim>\<open>?\<close>\<open>ident\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
wenzelm@61503
   110
    @{syntax_def typefree} & = & \<^verbatim>\<open>'\<close>\<open>ident\<close> \\
wenzelm@61503
   111
    @{syntax_def typevar} & = & \<^verbatim>\<open>?\<close>\<open>typefree  |\<close>~~\<^verbatim>\<open>?\<close>\<open>typefree\<close>\<^verbatim>\<open>.\<close>\<open>nat\<close> \\
wenzelm@61503
   112
    @{syntax_def string} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
wenzelm@61503
   113
    @{syntax_def altstring} & = & \<^verbatim>\<open>`\<close> \<open>\<dots>\<close> \<^verbatim>\<open>`\<close> \\
wenzelm@61493
   114
    @{syntax_def cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
wenzelm@61503
   115
    @{syntax_def verbatim} & = & \<^verbatim>\<open>{*\<close> \<open>\<dots>\<close> \<^verbatim>\<open>*}\<close> \\[1ex]
wenzelm@28775
   116
wenzelm@61503
   117
    \<open>letter\<close> & = & \<open>latin  |\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\\<close>\<^verbatim>\<open><\<close>\<open>latin latin\<close>\<^verbatim>\<open>>\<close>~~\<open>|  greek  |\<close> \\
wenzelm@61503
   118
    \<open>subscript\<close> & = & \<^verbatim>\<open>\<^sub>\<close> \\
wenzelm@61503
   119
    \<open>quasiletter\<close> & = & \<open>letter  |  digit  |\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>'\<close> \\
wenzelm@61503
   120
    \<open>latin\<close> & = & \<^verbatim>\<open>a\<close>~~\<open>| \<dots> |\<close>~~\<^verbatim>\<open>z\<close>~~\<open>|\<close>~~\<^verbatim>\<open>A\<close>~~\<open>|  \<dots> |\<close>~~\<^verbatim>\<open>Z\<close> \\
wenzelm@61503
   121
    \<open>digit\<close> & = & \<^verbatim>\<open>0\<close>~~\<open>|  \<dots> |\<close>~~\<^verbatim>\<open>9\<close> \\
wenzelm@61503
   122
    \<open>sym\<close> & = & \<^verbatim>\<open>!\<close>~~\<open>|\<close>~~\<^verbatim>\<open>#\<close>~~\<open>|\<close>~~\<^verbatim>\<open>$\<close>~~\<open>|\<close>~~\<^verbatim>\<open>%\<close>~~\<open>|\<close>~~\<^verbatim>\<open>&\<close>~~\<open>|\<close>~~\<^verbatim>\<open>*\<close>~~\<open>|\<close>~~\<^verbatim>\<open>+\<close>~~\<open>|\<close>~~\<^verbatim>\<open>-\<close>~~\<open>|\<close>~~\<^verbatim>\<open>/\<close>~~\<open>|\<close> \\
wenzelm@61503
   123
    & & \<^verbatim>\<open><\<close>~~\<open>|\<close>~~\<^verbatim>\<open>=\<close>~~\<open>|\<close>~~\<^verbatim>\<open>>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>?\<close>~~\<open>|\<close>~~\<^verbatim>\<open>@\<close>~~\<open>|\<close>~~\<^verbatim>\<open>^\<close>~~\<open>|\<close>~~\<^verbatim>\<open>_\<close>~~\<open>|\<close>~~\<^verbatim>\<open>|\<close>~~\<open>|\<close>~~\<^verbatim>\<open>~\<close> \\
wenzelm@61503
   124
    \<open>greek\<close> & = & \<^verbatim>\<open>\<alpha>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<beta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<delta>\<close>~~\<open>|\<close> \\
wenzelm@61503
   125
          &   & \<^verbatim>\<open>\<epsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<zeta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<eta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<theta>\<close>~~\<open>|\<close> \\
wenzelm@61503
   126
          &   & \<^verbatim>\<open>\<iota>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<kappa>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<mu>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<nu>\<close>~~\<open>|\<close> \\
wenzelm@61503
   127
          &   & \<^verbatim>\<open>\<xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<rho>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<sigma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<tau>\<close>~~\<open>|\<close> \\
wenzelm@61503
   128
          &   & \<^verbatim>\<open>\<upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<chi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<psi>\<close>~~\<open>|\<close> \\
wenzelm@61503
   129
          &   & \<^verbatim>\<open>\<omega>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Gamma>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Delta>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Theta>\<close>~~\<open>|\<close> \\
wenzelm@61503
   130
          &   & \<^verbatim>\<open>\<Lambda>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Xi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Pi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Sigma>\<close>~~\<open>|\<close> \\
wenzelm@61503
   131
          &   & \<^verbatim>\<open>\<Upsilon>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Phi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Psi>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>\<Omega>\<close> \\
wenzelm@28775
   132
  \end{supertabular}
wenzelm@28776
   133
  \end{center}
wenzelm@27037
   134
wenzelm@28778
   135
  A @{syntax_ref var} or @{syntax_ref typevar} describes an unknown,
wenzelm@28778
   136
  which is internally a pair of base name and index (ML type @{ML_type
wenzelm@28778
   137
  indexname}).  These components are either separated by a dot as in
wenzelm@61503
   138
  \<open>?x.1\<close> or \<open>?x7.3\<close> or run together as in \<open>?x1\<close>.  The latter form is possible
wenzelm@61503
   139
  if the base name does not end with digits.  If the index is 0, it may be
wenzelm@61503
   140
  dropped altogether: \<open>?x\<close> and \<open>?x0\<close> and \<open>?x.0\<close> all refer to the
wenzelm@61493
   141
  same unknown, with basename \<open>x\<close> and index 0.
wenzelm@28778
   142
wenzelm@28778
   143
  The syntax of @{syntax_ref string} admits any characters, including
wenzelm@61503
   144
  newlines; ``\<^verbatim>\<open>"\<close>'' (double-quote) and ``\<^verbatim>\<open>\\<close>''
wenzelm@58724
   145
  (backslash) need to be escaped by a backslash; arbitrary
wenzelm@61503
   146
  character codes may be specified as ``\<^verbatim>\<open>\\<close>\<open>ddd\<close>'',
wenzelm@27037
   147
  with three decimal digits.  Alternative strings according to
wenzelm@28778
   148
  @{syntax_ref altstring} are analogous, using single back-quotes
wenzelm@28778
   149
  instead.
wenzelm@28778
   150
wenzelm@58725
   151
  The body of @{syntax_ref verbatim} may consist of any text not containing
wenzelm@61503
   152
  ``\<^verbatim>\<open>*}\<close>''; this allows to include quotes without further
wenzelm@61503
   153
  escapes, but there is no way to escape ``\<^verbatim>\<open>*}\<close>''. Cartouches
wenzelm@58725
   154
  do not have this limitation.
wenzelm@28778
   155
wenzelm@55033
   156
  A @{syntax_ref cartouche} consists of arbitrary text, with properly
wenzelm@61493
   157
  balanced blocks of ``@{verbatim "\<open>"}~\<open>\<dots>\<close>~@{verbatim
wenzelm@55033
   158
  "\<close>"}''.  Note that the rendering of cartouche delimiters is
wenzelm@61493
   159
  usually like this: ``\<open>\<open> \<dots> \<close>\<close>''.
wenzelm@55033
   160
wenzelm@61503
   161
  Source comments take the form \<^verbatim>\<open>(*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*)\<close> and may be nested, although the user-interface
wenzelm@28778
   162
  might prevent this.  Note that this form indicates source comments
wenzelm@28778
   163
  only, which are stripped after lexical analysis of the input.  The
wenzelm@61477
   164
  Isar syntax also provides proper \<^emph>\<open>document comments\<close> that are
wenzelm@28778
   165
  considered as part of the text (see \secref{sec:comments}).
wenzelm@27037
   166
wenzelm@61493
   167
  Common mathematical symbols such as \<open>\<forall>\<close> are represented in
wenzelm@61503
   168
  Isabelle as \<^verbatim>\<open>\<forall>\<close>.  There are infinitely many Isabelle
wenzelm@27037
   169
  symbols like this, although proper presentation is left to front-end
wenzelm@58842
   170
  tools such as {\LaTeX} or Isabelle/jEdit.  A list of
wenzelm@47822
   171
  predefined Isabelle symbols that work well with these tools is given
wenzelm@61503
   172
  in \appref{app:symbols}.  Note that \<^verbatim>\<open>\<lambda>\<close> does not belong
wenzelm@61493
   173
  to the \<open>letter\<close> category, since it is already used differently
wenzelm@58618
   174
  in the Pure term language.\<close>
wenzelm@27037
   175
wenzelm@27037
   176
wenzelm@58618
   177
section \<open>Common syntax entities\<close>
wenzelm@27037
   178
wenzelm@58618
   179
text \<open>
wenzelm@27037
   180
  We now introduce several basic syntactic entities, such as names,
wenzelm@27037
   181
  terms, and theorem specifications, which are factored out of the
wenzelm@27037
   182
  actual Isar language elements to be described later.
wenzelm@58618
   183
\<close>
wenzelm@27037
   184
wenzelm@27037
   185
wenzelm@58618
   186
subsection \<open>Names\<close>
wenzelm@27037
   187
wenzelm@58618
   188
text \<open>Entity @{syntax name} usually refers to any name of types,
wenzelm@61477
   189
  constants, theorems etc.\ that are to be \<^emph>\<open>declared\<close> or
wenzelm@61477
   190
  \<^emph>\<open>defined\<close> (so qualified identifiers are excluded here).  Quoted
wenzelm@27037
   191
  strings provide an escape for non-identifier names or those ruled
wenzelm@61503
   192
  out by outer syntax keywords (e.g.\ quoted \<^verbatim>\<open>"let"\<close>).
wenzelm@42596
   193
  Already existing objects are usually referenced by @{syntax
wenzelm@42596
   194
  nameref}.
wenzelm@27037
   195
wenzelm@55112
   196
  @{rail \<open>
wenzelm@42596
   197
    @{syntax_def name}: @{syntax ident} | @{syntax symident} |
wenzelm@42596
   198
      @{syntax string} | @{syntax nat}
wenzelm@27037
   199
    ;
wenzelm@60131
   200
    @{syntax_def par_name}: '(' @{syntax name} ')'
wenzelm@27037
   201
    ;
wenzelm@42596
   202
    @{syntax_def nameref}: @{syntax name} | @{syntax longident}
wenzelm@55112
   203
  \<close>}
wenzelm@58618
   204
\<close>
wenzelm@40296
   205
wenzelm@40296
   206
wenzelm@58618
   207
subsection \<open>Numbers\<close>
wenzelm@40296
   208
wenzelm@58618
   209
text \<open>The outer lexical syntax (\secref{sec:outer-lex}) admits
wenzelm@40296
   210
  natural numbers and floating point numbers.  These are combined as
wenzelm@40296
   211
  @{syntax int} and @{syntax real} as follows.
wenzelm@40296
   212
wenzelm@55112
   213
  @{rail \<open>
wenzelm@42596
   214
    @{syntax_def int}: @{syntax nat} | '-' @{syntax nat}
wenzelm@27037
   215
    ;
wenzelm@42596
   216
    @{syntax_def real}: @{syntax float} | @{syntax int}
wenzelm@55112
   217
  \<close>}
wenzelm@40296
   218
wenzelm@42596
   219
  Note that there is an overlap with the category @{syntax name},
wenzelm@40296
   220
  which also includes @{syntax nat}.
wenzelm@58618
   221
\<close>
wenzelm@27037
   222
wenzelm@27037
   223
wenzelm@58618
   224
subsection \<open>Comments \label{sec:comments}\<close>
wenzelm@27037
   225
wenzelm@61579
   226
text \<open>
wenzelm@61579
   227
  Large chunks of plain @{syntax text} are usually given @{syntax verbatim},
wenzelm@61579
   228
  i.e.\ enclosed in \<^verbatim>\<open>{*\<close>~\<open>\<dots>\<close>~\<^verbatim>\<open>*}\<close>, or as @{syntax cartouche} \<open>\<open>\<dots>\<close>\<close>. For
wenzelm@61579
   229
  convenience, any of the smaller text units conforming to @{syntax nameref}
wenzelm@61579
   230
  are admitted as well. A marginal @{syntax comment} is of the form
wenzelm@61579
   231
  \<^verbatim>\<open>--\<close>~@{syntax text} or \<^verbatim>\<open>\<comment>\<close>~@{syntax text}. Any number of these may occur
wenzelm@61579
   232
  within Isabelle/Isar commands.
wenzelm@27037
   233
wenzelm@55112
   234
  @{rail \<open>
wenzelm@56499
   235
    @{syntax_def text}: @{syntax verbatim} | @{syntax cartouche} | @{syntax nameref}
wenzelm@27037
   236
    ;
wenzelm@61579
   237
    @{syntax_def comment}: ('--' | @'\<comment>') @{syntax text}
wenzelm@55112
   238
  \<close>}
wenzelm@58618
   239
\<close>
wenzelm@27037
   240
wenzelm@27037
   241
wenzelm@58618
   242
subsection \<open>Type classes, sorts and arities\<close>
wenzelm@27037
   243
wenzelm@58618
   244
text \<open>
wenzelm@27037
   245
  Classes are specified by plain names.  Sorts have a very simple
wenzelm@61493
   246
  inner syntax, which is either a single class name \<open>c\<close> or a
wenzelm@61493
   247
  list \<open>{c\<^sub>1, \<dots>, c\<^sub>n}\<close> referring to the
wenzelm@27037
   248
  intersection of these classes.  The syntax of type arities is given
wenzelm@27037
   249
  directly at the outer level.
wenzelm@27037
   250
wenzelm@55112
   251
  @{rail \<open>
wenzelm@42596
   252
    @{syntax_def classdecl}: @{syntax name} (('<' | '\<subseteq>') (@{syntax nameref} + ','))?
wenzelm@27037
   253
    ;
wenzelm@42596
   254
    @{syntax_def sort}: @{syntax nameref}
wenzelm@27037
   255
    ;
wenzelm@42596
   256
    @{syntax_def arity}: ('(' (@{syntax sort} + ',') ')')? @{syntax sort}
wenzelm@55112
   257
  \<close>}
wenzelm@58618
   258
\<close>
wenzelm@27037
   259
wenzelm@27037
   260
wenzelm@58618
   261
subsection \<open>Types and terms \label{sec:types-terms}\<close>
wenzelm@27037
   262
wenzelm@58618
   263
text \<open>
wenzelm@27037
   264
  The actual inner Isabelle syntax, that of types and terms of the
wenzelm@27037
   265
  logic, is far too sophisticated in order to be modelled explicitly
wenzelm@27037
   266
  at the outer theory level.  Basically, any such entity has to be
wenzelm@27037
   267
  quoted to turn it into a single token (the parsing and type-checking
wenzelm@27037
   268
  is performed internally later).  For convenience, a slightly more
wenzelm@27037
   269
  liberal convention is adopted: quotes may be omitted for any type or
wenzelm@27037
   270
  term that is already atomic at the outer level.  For example, one
wenzelm@61503
   271
  may just write \<^verbatim>\<open>x\<close> instead of quoted \<^verbatim>\<open>"x"\<close>.
wenzelm@61503
   272
  Note that symbolic identifiers (e.g.\ \<^verbatim>\<open>++\<close> or \<open>\<forall>\<close> are available as well,
wenzelm@61503
   273
  provided these have not been superseded
wenzelm@61503
   274
  by commands or other keywords already (such as \<^verbatim>\<open>=\<close> or
wenzelm@61503
   275
  \<^verbatim>\<open>+\<close>).
wenzelm@27037
   276
wenzelm@55112
   277
  @{rail \<open>
wenzelm@42596
   278
    @{syntax_def type}: @{syntax nameref} | @{syntax typefree} |
wenzelm@42596
   279
      @{syntax typevar}
wenzelm@27037
   280
    ;
wenzelm@42596
   281
    @{syntax_def term}: @{syntax nameref} | @{syntax var}
wenzelm@27037
   282
    ;
wenzelm@42596
   283
    @{syntax_def prop}: @{syntax term}
wenzelm@55112
   284
  \<close>}
wenzelm@27037
   285
wenzelm@59853
   286
  Positional instantiations are specified as a sequence of terms, or the
wenzelm@61493
   287
  placeholder ``\<open>_\<close>'' (underscore), which means to skip a position.
wenzelm@27037
   288
wenzelm@55112
   289
  @{rail \<open>
wenzelm@42596
   290
    @{syntax_def inst}: '_' | @{syntax term}
wenzelm@27037
   291
    ;
wenzelm@42596
   292
    @{syntax_def insts}: (@{syntax inst} *)
wenzelm@55112
   293
  \<close>}
wenzelm@27037
   294
wenzelm@61493
   295
  Named instantiations are specified as pairs of assignments \<open>v =
wenzelm@61493
   296
  t\<close>, which refer to schematic variables in some theorem that is
wenzelm@59853
   297
  instantiated. Both type and terms instantiations are admitted, and
wenzelm@59853
   298
  distinguished by the usual syntax of variable names.
wenzelm@59853
   299
wenzelm@59853
   300
  @{rail \<open>
wenzelm@59853
   301
    @{syntax_def named_inst}: variable '=' (type | term)
wenzelm@59853
   302
    ;
wenzelm@59853
   303
    @{syntax_def named_insts}: (named_inst @'and' +)
wenzelm@59853
   304
    ;
wenzelm@59853
   305
    variable: @{syntax name} | @{syntax var} | @{syntax typefree} | @{syntax typevar}
wenzelm@59853
   306
  \<close>}
wenzelm@59853
   307
wenzelm@42596
   308
  Type declarations and definitions usually refer to @{syntax
wenzelm@42596
   309
  typespec} on the left-hand side.  This models basic type constructor
wenzelm@42596
   310
  application at the outer syntax level.  Note that only plain postfix
wenzelm@42596
   311
  notation is available here, but no infixes.
wenzelm@27037
   312
wenzelm@55112
   313
  @{rail \<open>
wenzelm@42596
   314
    @{syntax_def typespec}:
wenzelm@42596
   315
      (() | @{syntax typefree} | '(' ( @{syntax typefree} + ',' ) ')') @{syntax name}
wenzelm@27037
   316
    ;
wenzelm@42705
   317
    @{syntax_def typespec_sorts}:
wenzelm@42596
   318
      (() | (@{syntax typefree} ('::' @{syntax sort})?) |
wenzelm@42596
   319
        '(' ( (@{syntax typefree} ('::' @{syntax sort})?) + ',' ) ')') @{syntax name}
wenzelm@55112
   320
  \<close>}
wenzelm@58618
   321
\<close>
wenzelm@27037
   322
wenzelm@27037
   323
wenzelm@58618
   324
subsection \<open>Term patterns and declarations \label{sec:term-decls}\<close>
wenzelm@28754
   325
wenzelm@58618
   326
text \<open>Wherever explicit propositions (or term fragments) occur in a
wenzelm@42596
   327
  proof text, casual binding of schematic term variables may be given
wenzelm@61493
   328
  specified via patterns of the form ``\<open>(\<IS> p\<^sub>1 \<dots> p\<^sub>n)\<close>''.
wenzelm@42596
   329
  This works both for @{syntax term} and @{syntax prop}.
wenzelm@28754
   330
wenzelm@55112
   331
  @{rail \<open>
wenzelm@42705
   332
    @{syntax_def term_pat}: '(' (@'is' @{syntax term} +) ')'
wenzelm@28754
   333
    ;
wenzelm@42705
   334
    @{syntax_def prop_pat}: '(' (@'is' @{syntax prop} +) ')'
wenzelm@55112
   335
  \<close>}
wenzelm@28754
   336
wenzelm@61421
   337
  \<^medskip>
wenzelm@61493
   338
  Declarations of local variables \<open>x :: \<tau>\<close> and
wenzelm@61493
   339
  logical propositions \<open>a : \<phi>\<close> represent different views on
wenzelm@28754
   340
  the same principle of introducing a local scope.  In practice, one
wenzelm@42596
   341
  may usually omit the typing of @{syntax vars} (due to
wenzelm@28754
   342
  type-inference), and the naming of propositions (due to implicit
wenzelm@28754
   343
  references of current facts).  In any case, Isar proof elements
wenzelm@28754
   344
  usually admit to introduce multiple such items simultaneously.
wenzelm@28754
   345
wenzelm@55112
   346
  @{rail \<open>
wenzelm@42596
   347
    @{syntax_def vars}: (@{syntax name} +) ('::' @{syntax type})?
wenzelm@28754
   348
    ;
wenzelm@42705
   349
    @{syntax_def props}: @{syntax thmdecl}? (@{syntax prop} @{syntax prop_pat}? +)
wenzelm@55112
   350
  \<close>}
wenzelm@28754
   351
wenzelm@28754
   352
  The treatment of multiple declarations corresponds to the
wenzelm@42596
   353
  complementary focus of @{syntax vars} versus @{syntax props}.  In
wenzelm@61493
   354
  ``\<open>x\<^sub>1 \<dots> x\<^sub>n :: \<tau>\<close>'' the typing refers to all variables, while
wenzelm@61493
   355
  in \<open>a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n\<close> the naming refers to all propositions
wenzelm@42596
   356
  collectively.  Isar language elements that refer to @{syntax vars}
wenzelm@42596
   357
  or @{syntax props} typically admit separate typings or namings via
wenzelm@28754
   358
  another level of iteration, with explicit @{keyword_ref "and"}
wenzelm@28754
   359
  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
wenzelm@28754
   360
  \secref{sec:proof-context}.
wenzelm@59785
   361
wenzelm@59785
   362
  @{rail \<open>
wenzelm@59785
   363
    @{syntax_def "fixes"}:
wenzelm@59785
   364
      ((@{syntax name} ('::' @{syntax type})? @{syntax mixfix}? | @{syntax vars}) + @'and')
wenzelm@59785
   365
    ;
wenzelm@59785
   366
    @{syntax_def "for_fixes"}: (@'for' @{syntax "fixes"})?
wenzelm@59785
   367
  \<close>}
wenzelm@59785
   368
wenzelm@59785
   369
  The category @{syntax "fixes"} is a richer variant of @{syntax vars}: it
wenzelm@59785
   370
  admits specification of mixfix syntax for the entities that are introduced
wenzelm@61493
   371
  into the context. An optional suffix ``@{keyword "for"}~\<open>fixes\<close>''
wenzelm@59785
   372
  is admitted in many situations to indicate a so-called ``eigen-context''
wenzelm@59785
   373
  of a formal element: the result will be exported and thus generalized over
wenzelm@59785
   374
  the given variables.\<close>
wenzelm@28754
   375
wenzelm@28754
   376
wenzelm@58618
   377
subsection \<open>Attributes and theorems \label{sec:syn-att}\<close>
wenzelm@27037
   378
wenzelm@58618
   379
text \<open>Attributes have their own ``semi-inner'' syntax, in the sense
wenzelm@42596
   380
  that input conforming to @{syntax args} below is parsed by the
wenzelm@28754
   381
  attribute a second time.  The attribute argument specifications may
wenzelm@28754
   382
  be any sequence of atomic entities (identifiers, strings etc.), or
wenzelm@42596
   383
  properly bracketed argument lists.  Below @{syntax atom} refers to
wenzelm@42596
   384
  any atomic entity, including any @{syntax keyword} conforming to
wenzelm@42596
   385
  @{syntax symident}.
wenzelm@27037
   386
wenzelm@55112
   387
  @{rail \<open>
wenzelm@42596
   388
    @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
wenzelm@42596
   389
      @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
wenzelm@55045
   390
      @{syntax keyword} | @{syntax cartouche}
wenzelm@27037
   391
    ;
wenzelm@42596
   392
    arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
wenzelm@27037
   393
    ;
wenzelm@42596
   394
    @{syntax_def args}: arg *
wenzelm@27037
   395
    ;
wenzelm@42596
   396
    @{syntax_def attributes}: '[' (@{syntax nameref} @{syntax args} * ',') ']'
wenzelm@55112
   397
  \<close>}
wenzelm@27037
   398
wenzelm@42596
   399
  Theorem specifications come in several flavors: @{syntax axmdecl}
wenzelm@42596
   400
  and @{syntax thmdecl} usually refer to axioms, assumptions or
wenzelm@42596
   401
  results of goal statements, while @{syntax thmdef} collects lists of
wenzelm@42596
   402
  existing theorems.  Existing theorems are given by @{syntax thmref}
wenzelm@42596
   403
  and @{syntax thmrefs}, the former requires an actual singleton
wenzelm@27037
   404
  result.
wenzelm@27037
   405
wenzelm@27037
   406
  There are three forms of theorem references:
wenzelm@60674
   407
wenzelm@61493
   408
  \<^enum> named facts \<open>a\<close>,
wenzelm@27037
   409
wenzelm@61493
   410
  \<^enum> selections from named facts \<open>a(i)\<close> or \<open>a(j - k)\<close>,
wenzelm@27037
   411
wenzelm@61421
   412
  \<^enum> literal fact propositions using token syntax @{syntax_ref altstring}
wenzelm@61503
   413
  \<^verbatim>\<open>`\<close>\<open>\<phi>\<close>\<^verbatim>\<open>`\<close> or @{syntax_ref cartouche}
wenzelm@61493
   414
  \<open>\<open>\<phi>\<close>\<close> (see also method @{method_ref fact}).
wenzelm@27037
   415
wenzelm@27037
   416
wenzelm@27037
   417
  Any kind of theorem specification may include lists of attributes
wenzelm@27037
   418
  both on the left and right hand sides; attributes are applied to any
wenzelm@27037
   419
  immediately preceding fact.  If names are omitted, the theorems are
wenzelm@27037
   420
  not stored within the theorem database of the theory or proof
wenzelm@27037
   421
  context, but any given attributes are applied nonetheless.
wenzelm@27037
   422
wenzelm@61493
   423
  An extra pair of brackets around attributes (like ``\<open>[[simproc a]]\<close>'') 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@55112
   429
  @{rail \<open>
wenzelm@42596
   430
    @{syntax_def axmdecl}: @{syntax name} @{syntax attributes}? ':'
wenzelm@42596
   431
    ;
wenzelm@60631
   432
    @{syntax_def thmbind}:
wenzelm@60631
   433
      @{syntax name} @{syntax attributes} | @{syntax name} | @{syntax attributes}
wenzelm@60631
   434
    ;
wenzelm@42596
   435
    @{syntax_def thmdecl}: thmbind ':'
wenzelm@27037
   436
    ;
wenzelm@42596
   437
    @{syntax_def thmdef}: thmbind '='
wenzelm@27037
   438
    ;
wenzelm@42596
   439
    @{syntax_def thmref}:
wenzelm@56499
   440
      (@{syntax nameref} selection? | @{syntax altstring} | @{syntax cartouche})
wenzelm@56499
   441
        @{syntax attributes}? |
wenzelm@42596
   442
      '[' @{syntax attributes} ']'
wenzelm@27037
   443
    ;
wenzelm@42596
   444
    @{syntax_def thmrefs}: @{syntax thmref} +
wenzelm@27037
   445
    ;
wenzelm@42596
   446
    selection: '(' ((@{syntax nat} | @{syntax nat} '-' @{syntax nat}?) + ',') ')'
wenzelm@55112
   447
  \<close>}
wenzelm@58618
   448
\<close>
wenzelm@27037
   449
wenzelm@60674
   450
wenzelm@60674
   451
section \<open>Diagnostic commands\<close>
wenzelm@60674
   452
wenzelm@60674
   453
text \<open>
wenzelm@60674
   454
  \begin{matharray}{rcl}
wenzelm@61493
   455
    @{command_def "print_theory"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   456
    @{command_def "print_definitions"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   457
    @{command_def "print_methods"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   458
    @{command_def "print_attributes"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   459
    @{command_def "print_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   460
    @{command_def "find_theorems"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   461
    @{command_def "find_consts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   462
    @{command_def "thm_deps"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   463
    @{command_def "unused_thms"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   464
    @{command_def "print_facts"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@61493
   465
    @{command_def "print_term_bindings"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
wenzelm@60674
   466
  \end{matharray}
wenzelm@60674
   467
wenzelm@60674
   468
  @{rail \<open>
wenzelm@60674
   469
    (@@{command print_theory} |
wenzelm@61252
   470
      @@{command print_definitions} |
wenzelm@60674
   471
      @@{command print_methods} |
wenzelm@60674
   472
      @@{command print_attributes} |
wenzelm@60674
   473
      @@{command print_theorems} |
wenzelm@60674
   474
      @@{command print_facts}) ('!'?)
wenzelm@60674
   475
    ;
wenzelm@60674
   476
    @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thm_criterion*)
wenzelm@60674
   477
    ;
wenzelm@60674
   478
    thm_criterion: ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
wenzelm@60674
   479
      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
wenzelm@60674
   480
    ;
wenzelm@60674
   481
    @@{command find_consts} (const_criterion*)
wenzelm@60674
   482
    ;
wenzelm@60674
   483
    const_criterion: ('-'?)
wenzelm@60674
   484
      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
wenzelm@60674
   485
    ;
wenzelm@60674
   486
    @@{command thm_deps} @{syntax thmrefs}
wenzelm@60674
   487
    ;
wenzelm@60674
   488
    @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
wenzelm@60674
   489
  \<close>}
wenzelm@60674
   490
wenzelm@60674
   491
  These commands print certain parts of the theory and proof context.
wenzelm@60674
   492
  Note that there are some further ones available, such as for the set
wenzelm@60674
   493
  of rules declared for simplifications.
wenzelm@60674
   494
wenzelm@61439
   495
  \<^descr> @{command "print_theory"} prints the main logical content of the
wenzelm@61493
   496
  background theory; the ``\<open>!\<close>'' option indicates extra verbosity.
wenzelm@60674
   497
wenzelm@61439
   498
  \<^descr> @{command "print_definitions"} prints dependencies of definitional
wenzelm@61252
   499
  specifications within the background theory, which may be constants
wenzelm@61252
   500
  \secref{sec:consts} or types (\secref{sec:types-pure},
wenzelm@61493
   501
  \secref{sec:hol-typedef}); the ``\<open>!\<close>'' option indicates extra
wenzelm@61252
   502
  verbosity.
wenzelm@61252
   503
wenzelm@61439
   504
  \<^descr> @{command "print_methods"} prints all proof methods available in the
wenzelm@61493
   505
  current theory context; the ``\<open>!\<close>'' option indicates extra
wenzelm@60674
   506
  verbosity.
wenzelm@60674
   507
wenzelm@61439
   508
  \<^descr> @{command "print_attributes"} prints all attributes available in the
wenzelm@61493
   509
  current theory context; the ``\<open>!\<close>'' option indicates extra
wenzelm@60674
   510
  verbosity.
wenzelm@60674
   511
wenzelm@61439
   512
  \<^descr> @{command "print_theorems"} prints theorems of the background theory
wenzelm@61493
   513
  resulting from the last command; the ``\<open>!\<close>'' option indicates
wenzelm@60674
   514
  extra verbosity.
wenzelm@60674
   515
wenzelm@61439
   516
  \<^descr> @{command "print_facts"} prints all local facts of the current
wenzelm@61493
   517
  context, both named and unnamed ones; the ``\<open>!\<close>'' option indicates
wenzelm@60674
   518
  extra verbosity.
wenzelm@60674
   519
wenzelm@61439
   520
  \<^descr> @{command "print_term_bindings"} prints all term bindings that
wenzelm@60674
   521
  are present in the context.
wenzelm@60674
   522
wenzelm@61493
   523
  \<^descr> @{command "find_theorems"}~\<open>criteria\<close> retrieves facts
wenzelm@60674
   524
  from the theory or proof context matching all of given search
wenzelm@61493
   525
  criteria.  The criterion \<open>name: p\<close> selects all theorems
wenzelm@61493
   526
  whose fully qualified name matches pattern \<open>p\<close>, which may
wenzelm@61493
   527
  contain ``\<open>*\<close>'' wildcards.  The criteria \<open>intro\<close>,
wenzelm@61493
   528
  \<open>elim\<close>, and \<open>dest\<close> select theorems that match the
wenzelm@60674
   529
  current goal as introduction, elimination or destruction rules,
wenzelm@61493
   530
  respectively.  The criterion \<open>solves\<close> returns all rules
wenzelm@60674
   531
  that would directly solve the current goal.  The criterion
wenzelm@61493
   532
  \<open>simp: t\<close> selects all rewrite rules whose left-hand side
wenzelm@61493
   533
  matches the given term.  The criterion term \<open>t\<close> selects all
wenzelm@61493
   534
  theorems that contain the pattern \<open>t\<close> -- as usual, patterns
wenzelm@61493
   535
  may contain occurrences of the dummy ``\<open>_\<close>'', schematic
wenzelm@60674
   536
  variables, and type constraints.
wenzelm@60674
   537
wenzelm@61493
   538
  Criteria can be preceded by ``\<open>-\<close>'' to select theorems that
wenzelm@61477
   539
  do \<^emph>\<open>not\<close> match. Note that giving the empty list of criteria
wenzelm@61477
   540
  yields \<^emph>\<open>all\<close> currently known facts.  An optional limit for the
wenzelm@60674
   541
  number of printed facts may be given; the default is 40.  By
wenzelm@60674
   542
  default, duplicates are removed from the search result. Use
wenzelm@61493
   543
  \<open>with_dups\<close> to display duplicates.
wenzelm@60674
   544
wenzelm@61493
   545
  \<^descr> @{command "find_consts"}~\<open>criteria\<close> prints all constants
wenzelm@61493
   546
  whose type meets all of the given criteria. The criterion \<open>strict: ty\<close> is met by any type that matches the type pattern
wenzelm@61493
   547
  \<open>ty\<close>.  Patterns may contain both the dummy type ``\<open>_\<close>''
wenzelm@61493
   548
  and sort constraints. The criterion \<open>ty\<close> is similar, but it
wenzelm@61493
   549
  also matches against subtypes. The criterion \<open>name: p\<close> and
wenzelm@61493
   550
  the prefix ``\<open>-\<close>'' function as described for @{command
wenzelm@60674
   551
  "find_theorems"}.
wenzelm@60674
   552
wenzelm@61493
   553
  \<^descr> @{command "thm_deps"}~\<open>a\<^sub>1 \<dots> a\<^sub>n\<close>
wenzelm@60674
   554
  visualizes dependencies of facts, using Isabelle's graph browser
wenzelm@60674
   555
  tool (see also @{cite "isabelle-system"}).
wenzelm@60674
   556
wenzelm@61493
   557
  \<^descr> @{command "unused_thms"}~\<open>A\<^sub>1 \<dots> A\<^sub>m - B\<^sub>1 \<dots> B\<^sub>n\<close>
wenzelm@61493
   558
  displays all theorems that are proved in theories \<open>B\<^sub>1 \<dots> B\<^sub>n\<close>
wenzelm@61493
   559
  or their parents but not in \<open>A\<^sub>1 \<dots> A\<^sub>m\<close> or their parents and
wenzelm@60674
   560
  that are never used.
wenzelm@61493
   561
  If \<open>n\<close> is \<open>0\<close>, the end of the range of theories
wenzelm@60674
   562
  defaults to the current theory. If no range is specified,
wenzelm@60674
   563
  only the unused theorems in the current theory are displayed.
wenzelm@60674
   564
\<close>
wenzelm@60674
   565
wenzelm@27037
   566
end