doc-src/IsarRef/Thy/Outer_Syntax.thy
author wenzelm
Thu, 13 Nov 2008 21:34:55 +0100
changeset 28753 b5926a48c943
parent 28752 754f10154d73
child 28754 6f2e67a3dfaa
permissions -rw-r--r--
more on mixfix annotations (updated material from old ref manual);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     1
(* $Id$ *)
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     2
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     3
theory Outer_Syntax
27050
cd8d99b9ef09 tuned structure;
wenzelm
parents: 27040
diff changeset
     4
imports Main
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     5
begin
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     6
27040
3d3e6e07b931 major reorganization of document structure;
wenzelm
parents: 27037
diff changeset
     7
chapter {* Outer syntax *}
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     8
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
     9
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    10
  The rather generic framework of Isabelle/Isar syntax emerges from
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    11
  three main syntactic categories: \emph{commands} of the top-level
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    12
  Isar engine (covering theory and proof elements), \emph{methods} for
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    13
  general goal refinements (analogous to traditional ``tactics''), and
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    14
  \emph{attributes} for operations on facts (within a certain
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    15
  context).  Subsequently we give a reference of basic syntactic
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    16
  entities underlying Isabelle/Isar syntax in a bottom-up manner.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    17
  Concrete theory and proof language elements will be introduced later
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    18
  on.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    19
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    20
  \medskip In order to get started with writing well-formed
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    21
  Isabelle/Isar documents, the most important aspect to be noted is
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    22
  the difference of \emph{inner} versus \emph{outer} syntax.  Inner
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    23
  syntax is that of Isabelle types and terms of the logic, while outer
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    24
  syntax is that of Isabelle/Isar theory sources (specifications and
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    25
  proofs).  As a general rule, inner syntax entities may occur only as
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    26
  \emph{atomic entities} within outer syntax.  For example, the string
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    27
  @{verbatim "\"x + y\""} and identifier @{verbatim z} are legal term
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    28
  specifications within a theory, while @{verbatim "x + y"} without
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    29
  quotes is not.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    30
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    31
  Printed theory documents usually omit quotes to gain readability
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    32
  (this is a matter of {\LaTeX} macro setup, say via @{verbatim
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    33
  "\\isabellestyle"}, see also \cite{isabelle-sys}).  Experienced
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    34
  users of Isabelle/Isar may easily reconstruct the lost technical
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    35
  information, while mere readers need not care about quotes at all.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    36
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    37
  \medskip Isabelle/Isar input may contain any number of input
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    38
  termination characters ``@{verbatim ";"}'' (semicolon) to separate
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    39
  commands explicitly.  This is particularly useful in interactive
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    40
  shell sessions to make clear where the current command is intended
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    41
  to end.  Otherwise, the interpreter loop will continue to issue a
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    42
  secondary prompt ``@{verbatim "#"}'' until an end-of-command is
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    43
  clearly recognized from the input syntax, e.g.\ encounter of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    44
  next command keyword.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    45
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    46
  More advanced interfaces such as Proof~General \cite{proofgeneral}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    47
  do not require explicit semicolons, the amount of input text is
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    48
  determined automatically by inspecting the present content of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    49
  Emacs text buffer.  In the printed presentation of Isabelle/Isar
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    50
  documents semicolons are omitted altogether for readability.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    51
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    52
  \begin{warn}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    53
    Proof~General requires certain syntax classification tables in
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    54
    order to achieve properly synchronized interaction with the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    55
    Isabelle/Isar process.  These tables need to be consistent with
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    56
    the Isabelle version and particular logic image to be used in a
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    57
    running session (common object-logics may well change the outer
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    58
    syntax).  The standard setup should work correctly with any of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    59
    ``official'' logic images derived from Isabelle/HOL (including
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    60
    HOLCF etc.).  Users of alternative logics may need to tell
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    61
    Proof~General explicitly, e.g.\ by giving an option @{verbatim "-k ZF"}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    62
    (in conjunction with @{verbatim "-l ZF"}, to specify the default
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    63
    logic image).  Note that option @{verbatim "-L"} does both
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    64
    of this at the same time.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    65
  \end{warn}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    66
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    67
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    68
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    69
section {* Lexical matters \label{sec:lex-syntax} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    70
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    71
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    72
  The Isabelle/Isar outer syntax provides token classes as presented
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    73
  below; most of these coincide with the inner lexical syntax as
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    74
  presented in \cite{isabelle-ref}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    75
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    76
  \begin{matharray}{rcl}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    77
    @{syntax_def ident} & = & letter\,quasiletter^* \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    78
    @{syntax_def longident} & = & ident (\verb,.,ident)^+ \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    79
    @{syntax_def symident} & = & sym^+ ~|~ \verb,\,\verb,<,ident\verb,>, \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    80
    @{syntax_def nat} & = & digit^+ \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    81
    @{syntax_def var} & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    82
    @{syntax_def typefree} & = & \verb,',ident \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    83
    @{syntax_def typevar} & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    84
    @{syntax_def string} & = & \verb,", ~\dots~ \verb,", \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    85
    @{syntax_def altstring} & = & \backquote ~\dots~ \backquote \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    86
    @{syntax_def verbatim} & = & \verb,{*, ~\dots~ \verb,*,\verb,}, \\[1ex]
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    87
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    88
    letter & = & latin ~|~ \verb,\,\verb,<,latin\verb,>, ~|~ \verb,\,\verb,<,latin\,latin\verb,>, ~|~ greek ~|~ \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    89
           &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    90
    quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    91
    latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    92
    digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    93
    sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    94
     \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    95
    & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    96
    \verb,^, ~|~ \verb,_, ~|~ \verb,|, ~|~ \verb,~, \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    97
    greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    98
          &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
    99
          &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   100
          &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~|~ \verb,\<tau>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   101
          &   & \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<chi>, ~|~ \verb,\<psi>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   102
          &   & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   103
          &   & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   104
          &   & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   105
  \end{matharray}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   106
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   107
  The syntax of @{syntax string} admits any characters, including
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   108
  newlines; ``@{verbatim "\""}'' (double-quote) and ``@{verbatim
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   109
  "\\"}'' (backslash) need to be escaped by a backslash; arbitrary
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   110
  character codes may be specified as ``@{verbatim "\\"}@{text ddd}'',
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   111
  with three decimal digits.  Alternative strings according to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   112
  @{syntax altstring} are analogous, using single back-quotes instead.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   113
  The body of @{syntax verbatim} may consist of any text not
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   114
  containing ``@{verbatim "*"}@{verbatim "}"}''; this allows
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   115
  convenient inclusion of quotes without further escapes.  The greek
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   116
  letters do \emph{not} include @{verbatim "\<lambda>"}, which is already used
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   117
  differently in the meta-logic.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   118
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   119
  Common mathematical symbols such as @{text \<forall>} are represented in
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   120
  Isabelle as @{verbatim \<forall>}.  There are infinitely many Isabelle
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   121
  symbols like this, although proper presentation is left to front-end
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   122
  tools such as {\LaTeX} or Proof~General with the X-Symbol package.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   123
  A list of standard Isabelle symbols that work well with these tools
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   124
  is given in \cite[appendix~A]{isabelle-sys}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   125
  
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   126
  Source comments take the form @{verbatim "(*"}~@{text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   127
  "\<dots>"}~@{verbatim "*)"} and may be nested, although user-interface
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   128
  tools might prevent this.  Note that this form indicates source
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   129
  comments only, which are stripped after lexical analysis of the
28748
69268a097405 renamed "formal comments" to "document comments";
wenzelm
parents: 27050
diff changeset
   130
  input.  The Isar syntax also provides proper \emph{document
69268a097405 renamed "formal comments" to "document comments";
wenzelm
parents: 27050
diff changeset
   131
  comments} that are considered as part of the text (see
69268a097405 renamed "formal comments" to "document comments";
wenzelm
parents: 27050
diff changeset
   132
  \secref{sec:comments}).
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   133
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   134
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   135
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   136
section {* Common syntax entities *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   137
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   138
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   139
  We now introduce several basic syntactic entities, such as names,
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   140
  terms, and theorem specifications, which are factored out of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   141
  actual Isar language elements to be described later.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   142
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   143
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   144
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   145
subsection {* Names *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   146
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   147
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   148
  Entity \railqtok{name} usually refers to any name of types,
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   149
  constants, theorems etc.\ that are to be \emph{declared} or
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   150
  \emph{defined} (so qualified identifiers are excluded here).  Quoted
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   151
  strings provide an escape for non-identifier names or those ruled
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   152
  out by outer syntax keywords (e.g.\ quoted @{verbatim "\"let\""}).
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   153
  Already existing objects are usually referenced by
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   154
  \railqtok{nameref}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   155
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   156
  \indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   157
  \indexoutertoken{int}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   158
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   159
    name: ident | symident | string | nat
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   160
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   161
    parname: '(' name ')'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   162
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   163
    nameref: name | longident
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   164
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   165
    int: nat | '-' nat
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   166
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   167
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   168
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   169
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   170
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   171
subsection {* Comments \label{sec:comments} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   172
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   173
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   174
  Large chunks of plain \railqtok{text} are usually given
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   175
  \railtok{verbatim}, i.e.\ enclosed in @{verbatim "{"}@{verbatim
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   176
  "*"}~@{text "\<dots>"}~@{verbatim "*"}@{verbatim "}"}.  For convenience,
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   177
  any of the smaller text units conforming to \railqtok{nameref} are
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   178
  admitted as well.  A marginal \railnonterm{comment} is of the form
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   179
  @{verbatim "--"} \railqtok{text}.  Any number of these may occur
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   180
  within Isabelle/Isar commands.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   181
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   182
  \indexoutertoken{text}\indexouternonterm{comment}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   183
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   184
    text: verbatim | nameref
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   185
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   186
    comment: '--' text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   187
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   188
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   189
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   190
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   191
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   192
subsection {* Type classes, sorts and arities *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   193
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   194
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   195
  Classes are specified by plain names.  Sorts have a very simple
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   196
  inner syntax, which is either a single class name @{text c} or a
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   197
  list @{text "{c\<^sub>1, \<dots>, c\<^sub>n}"} referring to the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   198
  intersection of these classes.  The syntax of type arities is given
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   199
  directly at the outer level.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   200
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   201
  \indexouternonterm{sort}\indexouternonterm{arity}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   202
  \indexouternonterm{classdecl}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   203
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   204
    classdecl: name (('<' | subseteq) (nameref + ','))?
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   205
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   206
    sort: nameref
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   207
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   208
    arity: ('(' (sort + ',') ')')? sort
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   209
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   210
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   211
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   212
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   213
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   214
subsection {* Types and terms \label{sec:types-terms} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   215
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   216
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   217
  The actual inner Isabelle syntax, that of types and terms of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   218
  logic, is far too sophisticated in order to be modelled explicitly
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   219
  at the outer theory level.  Basically, any such entity has to be
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   220
  quoted to turn it into a single token (the parsing and type-checking
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   221
  is performed internally later).  For convenience, a slightly more
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   222
  liberal convention is adopted: quotes may be omitted for any type or
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   223
  term that is already atomic at the outer level.  For example, one
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   224
  may just write @{verbatim x} instead of quoted @{verbatim "\"x\""}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   225
  Note that symbolic identifiers (e.g.\ @{verbatim "++"} or @{text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   226
  "\<forall>"} are available as well, provided these have not been superseded
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   227
  by commands or other keywords already (such as @{verbatim "="} or
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   228
  @{verbatim "+"}).
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   229
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   230
  \indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   231
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   232
    type: nameref | typefree | typevar
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   233
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   234
    term: nameref | var
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   235
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   236
    prop: term
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   237
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   238
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   239
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   240
  Positional instantiations are indicated by giving a sequence of
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   241
  terms, or the placeholder ``@{text _}'' (underscore), which means to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   242
  skip a position.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   243
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   244
  \indexoutertoken{inst}\indexoutertoken{insts}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   245
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   246
    inst: underscore | term
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   247
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   248
    insts: (inst *)
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   249
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   250
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   251
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   252
  Type declarations and definitions usually refer to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   253
  \railnonterm{typespec} on the left-hand side.  This models basic
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   254
  type constructor application at the outer syntax level.  Note that
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   255
  only plain postfix notation is available here, but no infixes.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   256
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   257
  \indexouternonterm{typespec}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   258
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   259
    typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   260
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   261
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   262
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   263
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   264
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   265
subsection {* Mixfix annotations *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   266
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   267
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   268
  Mixfix annotations specify concrete \emph{inner} syntax of Isabelle
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   269
  types and terms.  Some commands such as @{command "types"} (see
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   270
  \secref{sec:types-pure}) admit infixes only, while @{command
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   271
  "consts"} (see \secref{sec:consts}) and @{command "syntax"} (see
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   272
  \secref{sec:syn-trans}) support the full range of general mixfixes
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   273
  and binders.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   274
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   275
  \indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   276
  \begin{rail}
28752
wenzelm
parents: 28748
diff changeset
   277
    infix: '(' ('infix' | 'infixl' | 'infixr') string nat ')'
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   278
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   279
    mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   280
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   281
    structmixfix: mixfix | '(' 'structure' ')'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   282
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   283
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   284
    prios: '[' (nat + ',') ']'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   285
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   286
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   287
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   288
  Here the \railtok{string} specifications refer to the actual mixfix
28752
wenzelm
parents: 28748
diff changeset
   289
  template, which may include literal text, spacing, blocks, and
wenzelm
parents: 28748
diff changeset
   290
  arguments (denoted by ``@{text _}''); the special symbol
wenzelm
parents: 28748
diff changeset
   291
  ``@{verbatim "\<index>"}'' (printed as ``@{text "\<index>"}'') represents an index
wenzelm
parents: 28748
diff changeset
   292
  argument that specifies an implicit structure reference (see also
wenzelm
parents: 28748
diff changeset
   293
  \secref{sec:locale}).  Infix and binder declarations provide common
wenzelm
parents: 28748
diff changeset
   294
  abbreviations for particular mixfix declarations.  So in practice,
wenzelm
parents: 28748
diff changeset
   295
  mixfix templates mostly degenerate to literal text for concrete
wenzelm
parents: 28748
diff changeset
   296
  syntax, such as ``@{verbatim "++"}'' for an infix symbol.
wenzelm
parents: 28748
diff changeset
   297
wenzelm
parents: 28748
diff changeset
   298
  \medskip In full generality, mixfix declarations work as follows.
wenzelm
parents: 28748
diff changeset
   299
  Suppose a constant @{text "c :: \<tau>\<^sub>1 \<Rightarrow> \<dots> \<tau>\<^sub>n \<Rightarrow> \<tau>"} is
wenzelm
parents: 28748
diff changeset
   300
  annotated by @{text "(mixfix [p\<^sub>1, \<dots>, p\<^sub>n] p)"}, where @{text
wenzelm
parents: 28748
diff changeset
   301
  "mixfix"} is a string @{text "d\<^sub>0 _ d\<^sub>1 _ \<dots> _ d\<^sub>n"} consisting of
wenzelm
parents: 28748
diff changeset
   302
  delimiters that surround argument positions as indicated by
wenzelm
parents: 28748
diff changeset
   303
  underscores.
wenzelm
parents: 28748
diff changeset
   304
wenzelm
parents: 28748
diff changeset
   305
  Altogether this determines a production for a context-free priority
wenzelm
parents: 28748
diff changeset
   306
  grammar, where for each argument @{text "i"} the syntactic category
wenzelm
parents: 28748
diff changeset
   307
  is determined by @{text "\<tau>\<^sub>i"} (with priority @{text "p\<^sub>i"}), and
wenzelm
parents: 28748
diff changeset
   308
  the result category is determined from @{text "\<tau>"} (with
wenzelm
parents: 28748
diff changeset
   309
  priority @{text "p"}).  Priority specifications are optional, with
wenzelm
parents: 28748
diff changeset
   310
  default 0 for arguments and 1000 for the result.
wenzelm
parents: 28748
diff changeset
   311
wenzelm
parents: 28748
diff changeset
   312
  Since @{text "\<tau>"} may be again a function type, the constant
wenzelm
parents: 28748
diff changeset
   313
  type scheme may have more argument positions than the mixfix
wenzelm
parents: 28748
diff changeset
   314
  pattern.  Printing a nested application @{text "c t\<^sub>1 \<dots> t\<^sub>m"} for
wenzelm
parents: 28748
diff changeset
   315
  @{text "m > n"} works by attaching concrete notation only to the
wenzelm
parents: 28748
diff changeset
   316
  innermost part, essentially by printing @{text "(c t\<^sub>1 \<dots> t\<^sub>n) \<dots> t\<^sub>m"}
28753
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   317
  instead.  If a term has fewer argument than specified in the mixfix
28752
wenzelm
parents: 28748
diff changeset
   318
  template, the concrete syntax is ignored.
wenzelm
parents: 28748
diff changeset
   319
wenzelm
parents: 28748
diff changeset
   320
  \medskip A mixfix template may also contain additional directives
wenzelm
parents: 28748
diff changeset
   321
  for pretty printing, notably spaces, blocks, and breaks.  The
wenzelm
parents: 28748
diff changeset
   322
  general template format is a sequence over any of the following
wenzelm
parents: 28748
diff changeset
   323
  entities.
wenzelm
parents: 28748
diff changeset
   324
wenzelm
parents: 28748
diff changeset
   325
  \begin{itemize}
wenzelm
parents: 28748
diff changeset
   326
wenzelm
parents: 28748
diff changeset
   327
  \item @{text "\<^bold>d"} is a delimiter, namely a non-empty
wenzelm
parents: 28748
diff changeset
   328
  sequence of characters other than the special characters @{text "'"}
wenzelm
parents: 28748
diff changeset
   329
  (single quote), @{text "_"} (underscore), @{text "\<index>"} (index
wenzelm
parents: 28748
diff changeset
   330
  symbol), @{text "/"} (slash), @{text "("} and @{text ")"}
wenzelm
parents: 28748
diff changeset
   331
  (parentheses).
wenzelm
parents: 28748
diff changeset
   332
wenzelm
parents: 28748
diff changeset
   333
  A single quote escapes the special meaning of these meta-characters,
wenzelm
parents: 28748
diff changeset
   334
  producing a literal version of the following character, unless that
wenzelm
parents: 28748
diff changeset
   335
  is a blank.  A single quote followed by a blank separates
wenzelm
parents: 28748
diff changeset
   336
  delimiters, without affecting printing, but input tokens may have
wenzelm
parents: 28748
diff changeset
   337
  additional white space here.
wenzelm
parents: 28748
diff changeset
   338
wenzelm
parents: 28748
diff changeset
   339
  \item @{text "_"} is an argument position, which stands for a
wenzelm
parents: 28748
diff changeset
   340
  certain syntactic category in the underlying grammar.
wenzelm
parents: 28748
diff changeset
   341
wenzelm
parents: 28748
diff changeset
   342
  \item @{text "\<index>"} is an indexed argument position; this is
wenzelm
parents: 28748
diff changeset
   343
  the place where implicit structure arguments can be attached.
wenzelm
parents: 28748
diff changeset
   344
wenzelm
parents: 28748
diff changeset
   345
  \item @{text "\<^bold>s"} is a non-empty sequence of spaces for
wenzelm
parents: 28748
diff changeset
   346
  printing.  This and the following specifications do not affect
wenzelm
parents: 28748
diff changeset
   347
  parsing at all.
wenzelm
parents: 28748
diff changeset
   348
wenzelm
parents: 28748
diff changeset
   349
  \item @{text "(\<^bold>n"} opens a pretty printing block.  The
wenzelm
parents: 28748
diff changeset
   350
  optional number specifies how much indentation to add when a line
wenzelm
parents: 28748
diff changeset
   351
  break occurs within the block.  If the parenthesis is not followed
wenzelm
parents: 28748
diff changeset
   352
  by digits, the indentation defaults to 0.  A block specified via
wenzelm
parents: 28748
diff changeset
   353
  @{text "(00"} is unbreakable.
wenzelm
parents: 28748
diff changeset
   354
wenzelm
parents: 28748
diff changeset
   355
  \item @{text ")"} closes a pretty printing block.
wenzelm
parents: 28748
diff changeset
   356
wenzelm
parents: 28748
diff changeset
   357
  \item @{text "//"} forces a line break.
wenzelm
parents: 28748
diff changeset
   358
wenzelm
parents: 28748
diff changeset
   359
  \item @{text "/\<^bold>s"} allows a line break.  Here @{text
wenzelm
parents: 28748
diff changeset
   360
  "\<^bold>s"} stands for the string of spaces (zero or more) right
wenzelm
parents: 28748
diff changeset
   361
  after the slash.  These spaces are printed if the break is
wenzelm
parents: 28748
diff changeset
   362
  \emph{not} taken.
wenzelm
parents: 28748
diff changeset
   363
wenzelm
parents: 28748
diff changeset
   364
  \end{itemize}
wenzelm
parents: 28748
diff changeset
   365
wenzelm
parents: 28748
diff changeset
   366
  For example, the template @{text "(_ +/ _)"} specifies an infix
wenzelm
parents: 28748
diff changeset
   367
  operator.  There are two argument positions; the delimiter @{text
wenzelm
parents: 28748
diff changeset
   368
  "+"} is preceded by a space and followed by a space or line break;
28753
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   369
  the entire phrase is a pretty printing block.  
28752
wenzelm
parents: 28748
diff changeset
   370
wenzelm
parents: 28748
diff changeset
   371
  The general idea of pretty printing with blocks and breaks is also
wenzelm
parents: 28748
diff changeset
   372
  described in \cite{paulson-ml2}.
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   373
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   374
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   375
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   376
subsection {* Proof methods \label{sec:syn-meth} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   377
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   378
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   379
  Proof methods are either basic ones, or expressions composed of
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   380
  methods via ``@{verbatim ","}'' (sequential composition),
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   381
  ``@{verbatim "|"}'' (alternative choices), ``@{verbatim "?"}'' 
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   382
  (try), ``@{verbatim "+"}'' (repeat at least once), ``@{verbatim
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   383
  "["}@{text n}@{verbatim "]"}'' (restriction to first @{text n}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   384
  sub-goals, with default @{text "n = 1"}).  In practice, proof
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   385
  methods are usually just a comma separated list of
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   386
  \railqtok{nameref}~\railnonterm{args} specifications.  Note that
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   387
  parentheses may be dropped for single method specifications (with no
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   388
  arguments).
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   389
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   390
  \indexouternonterm{method}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   391
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   392
    method: (nameref | '(' methods ')') (() | '?' | '+' | '[' nat? ']')
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   393
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   394
    methods: (nameref args | method) + (',' | '|')
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   395
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   396
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   397
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   398
  Proper Isar proof methods do \emph{not} admit arbitrary goal
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   399
  addressing, but refer either to the first sub-goal or all sub-goals
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   400
  uniformly.  The goal restriction operator ``@{text "[n]"}''
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   401
  evaluates a method expression within a sandbox consisting of the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   402
  first @{text n} sub-goals (which need to exist).  For example, the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   403
  method ``@{text "simp_all[3]"}'' simplifies the first three
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   404
  sub-goals, while ``@{text "(rule foo, simp_all)[]"}'' simplifies all
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   405
  new goals that emerge from applying rule @{text "foo"} to the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   406
  originally first one.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   407
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   408
  Improper methods, notably tactic emulations, offer a separate
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   409
  low-level goal addressing scheme as explicit argument to the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   410
  individual tactic being involved.  Here ``@{text "[!]"}'' refers to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   411
  all goals, and ``@{text "[n-]"}'' to all goals starting from @{text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   412
  "n"}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   413
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   414
  \indexouternonterm{goalspec}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   415
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   416
    goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   417
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   418
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   419
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   420
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   421
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   422
subsection {* Attributes and theorems \label{sec:syn-att} *}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   423
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   424
text {*
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   425
  Attributes (and proof methods, see \secref{sec:syn-meth}) have their
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   426
  own ``semi-inner'' syntax, in the sense that input conforming to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   427
  \railnonterm{args} below is parsed by the attribute a second time.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   428
  The attribute argument specifications may be any sequence of atomic
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   429
  entities (identifiers, strings etc.), or properly bracketed argument
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   430
  lists.  Below \railqtok{atom} refers to any atomic entity, including
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   431
  any \railtok{keyword} conforming to \railtok{symident}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   432
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   433
  \indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   434
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   435
    atom: nameref | typefree | typevar | var | nat | keyword
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   436
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   437
    arg: atom | '(' args ')' | '[' args ']'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   438
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   439
    args: arg *
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   440
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   441
    attributes: '[' (nameref args * ',') ']'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   442
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   443
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   444
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   445
  Theorem specifications come in several flavors:
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   446
  \railnonterm{axmdecl} and \railnonterm{thmdecl} usually refer to
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   447
  axioms, assumptions or results of goal statements, while
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   448
  \railnonterm{thmdef} collects lists of existing theorems.  Existing
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   449
  theorems are given by \railnonterm{thmref} and
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   450
  \railnonterm{thmrefs}, the former requires an actual singleton
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   451
  result.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   452
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   453
  There are three forms of theorem references:
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   454
  \begin{enumerate}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   455
  
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   456
  \item named facts @{text "a"},
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   457
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   458
  \item selections from named facts @{text "a(i)"} or @{text "a(j - k)"},
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   459
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   460
  \item literal fact propositions using @{syntax_ref altstring} syntax
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   461
  @{verbatim "`"}@{text "\<phi>"}@{verbatim "`"} (see also method
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   462
  @{method_ref fact} in \secref{sec:pure-meth-att}).
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   463
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   464
  \end{enumerate}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   465
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   466
  Any kind of theorem specification may include lists of attributes
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   467
  both on the left and right hand sides; attributes are applied to any
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   468
  immediately preceding fact.  If names are omitted, the theorems are
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   469
  not stored within the theorem database of the theory or proof
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   470
  context, but any given attributes are applied nonetheless.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   471
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   472
  An extra pair of brackets around attributes (like ``@{text
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   473
  "[[simproc a]]"}'') abbreviates a theorem reference involving an
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   474
  internal dummy fact, which will be ignored later on.  So only the
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   475
  effect of the attribute on the background context will persist.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   476
  This form of in-place declarations is particularly useful with
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   477
  commands like @{command "declare"} and @{command "using"}.
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   478
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   479
  \indexouternonterm{axmdecl}\indexouternonterm{thmdecl}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   480
  \indexouternonterm{thmdef}\indexouternonterm{thmref}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   481
  \indexouternonterm{thmrefs}\indexouternonterm{selection}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   482
  \begin{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   483
    axmdecl: name attributes? ':'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   484
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   485
    thmdecl: thmbind ':'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   486
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   487
    thmdef: thmbind '='
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   488
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   489
    thmref: (nameref selection? | altstring) attributes? | '[' attributes ']'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   490
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   491
    thmrefs: thmref +
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   492
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   493
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   494
    thmbind: name attributes | name | attributes
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   495
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   496
    selection: '(' ((nat | nat '-' nat?) + ',') ')'
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   497
    ;
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   498
  \end{rail}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   499
*}
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   500
28753
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   501
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   502
subsection {* Term patterns and declarations \label{sec:term-decls} *}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   503
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   504
text {*
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   505
  Wherever explicit propositions (or term fragments) occur in a proof
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   506
  text, casual binding of schematic term variables may be given
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   507
  specified via patterns of the form ``@{text "(\<IS> p\<^sub>1 \<dots>
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   508
  p\<^sub>n)"}''.  This works both for \railqtok{term} and \railqtok{prop}.
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   509
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   510
  \indexouternonterm{termpat}\indexouternonterm{proppat}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   511
  \begin{rail}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   512
    termpat: '(' ('is' term +) ')'
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   513
    ;
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   514
    proppat: '(' ('is' prop +) ')'
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   515
    ;
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   516
  \end{rail}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   517
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   518
  \medskip Declarations of local variables @{text "x :: \<tau>"} and
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   519
  logical propositions @{text "a : \<phi>"} represent different views on
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   520
  the same principle of introducing a local scope.  In practice, one
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   521
  may usually omit the typing of \railnonterm{vars} (due to
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   522
  type-inference), and the naming of propositions (due to implicit
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   523
  references of current facts).  In any case, Isar proof elements
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   524
  usually admit to introduce multiple such items simultaneously.
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   525
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   526
  \indexouternonterm{vars}\indexouternonterm{props}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   527
  \begin{rail}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   528
    vars: (name+) ('::' type)?
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   529
    ;
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   530
    props: thmdecl? (prop proppat? +)
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   531
    ;
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   532
  \end{rail}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   533
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   534
  The treatment of multiple declarations corresponds to the
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   535
  complementary focus of \railnonterm{vars} versus
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   536
  \railnonterm{props}.  In ``@{text "x\<^sub>1 \<dots> x\<^sub>n :: \<tau>"}''
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   537
  the typing refers to all variables, while in @{text "a: \<phi>\<^sub>1 \<dots>
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   538
  \<phi>\<^sub>n"} the naming refers to all propositions collectively.
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   539
  Isar language elements that refer to \railnonterm{vars} or
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   540
  \railnonterm{props} typically admit separate typings or namings via
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   541
  another level of iteration, with explicit @{keyword_ref "and"}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   542
  separators; e.g.\ see @{command "fix"} and @{command "assume"} in
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   543
  \secref{sec:proof-context}.
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   544
*}
b5926a48c943 more on mixfix annotations (updated material from old ref manual);
wenzelm
parents: 28752
diff changeset
   545
27037
33d95687514e renamed theory "syntax" to "Outer_Syntax";
wenzelm
parents:
diff changeset
   546
end