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