doc-src/IsarRef/syntax.tex
author nipkow
Wed, 04 Aug 2004 11:25:08 +0200
changeset 15106 e8cef6993701
parent 14960 89cce4e95a22
child 15357 96698f16e3d9
permissions -rw-r--r--
aded comment
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
13048
wenzelm
parents: 13039
diff changeset
     2
\chapter{Syntax primitives}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     3
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
     4
The rather generic framework of Isabelle/Isar syntax emerges from three main
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
     5
syntactic categories: \emph{commands} of the top-level Isar engine (covering
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
     6
theory and proof elements), \emph{methods} for general goal refinements
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
     7
(analogous to traditional ``tactics''), and \emph{attributes} for operations
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
     8
on facts (within a certain context).  Here we give a reference of basic
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
     9
syntactic entities underlying Isabelle/Isar syntax in a bottom-up manner.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    10
Concrete theory and proof language elements will be introduced later on.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    11
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    12
\medskip
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    13
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    14
In order to get started with writing well-formed Isabelle/Isar documents, the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    15
most important aspect to be noted is the difference of \emph{inner} versus
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    16
\emph{outer} syntax.  Inner syntax is that of Isabelle types and terms of the
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    17
logic, while outer syntax is that of Isabelle/Isar theory sources (including
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    18
proofs).  As a general rule, inner syntax entities may occur only as
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    19
\emph{atomic entities} within outer syntax.  For example, the string
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    20
\texttt{"x + y"} and identifier \texttt{z} are legal term specifications
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    21
within a theory, while \texttt{x + y} is not.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    22
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    23
\begin{warn}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    24
  Old-style Isabelle theories used to fake parts of the inner syntax of types,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    25
  with rather complicated rules when quotes may be omitted.  Despite the minor
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    26
  drawback of requiring quotes more often, the syntax of Isabelle/Isar is
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    27
  somewhat simpler and more robust in that respect.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    28
\end{warn}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    29
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    30
Printed theory documents usually omit quotes to gain readability (this is a
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    31
matter of {\LaTeX} macro setup, say via \verb,\isabellestyle,, see also
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    32
\cite{isabelle-sys}).  Experienced users of Isabelle/Isar may easily
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    33
reconstruct the lost technical information, while mere readers need not care
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    34
about quotes at all.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    35
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
    36
\medskip
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
    37
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    38
Isabelle/Isar input may contain any number of input termination characters
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    39
``\texttt{;}'' (semicolon) to separate commands explicitly.  This is
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    40
particularly useful in interactive shell sessions to make clear where the
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    41
current command is intended to end.  Otherwise, the interpreter loop will
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    42
continue to issue a secondary prompt ``\verb,#,'' until an end-of-command is
13039
wenzelm
parents: 12976
diff changeset
    43
clearly recognized from the input syntax, e.g.\ encounter of the next command
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    44
keyword.
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    45
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    46
Advanced interfaces such as Proof~General \cite{proofgeneral} do not require
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    47
explicit semicolons, the amount of input text is determined automatically by
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    48
inspecting the present content of the Emacs text buffer.  In the printed
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    49
presentation of Isabelle/Isar documents semicolons are omitted altogether for
7981
wenzelm
parents: 7895
diff changeset
    50
readability.
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
    51
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    52
\begin{warn}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    53
  Proof~General requires certain syntax classification tables in order to
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    54
  achieve properly synchronized interaction with the Isabelle/Isar process.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    55
  These tables need to be consistent with the Isabelle version and particular
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    56
  logic image to be used in a running session (common object-logics may well
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    57
  change the outer syntax).  The standard setup should work correctly with any
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    58
  of the ``official'' logic images derived from Isabelle/HOL (including HOLCF
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    59
  etc.).  Users of alternative logics may need to tell Proof~General
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    60
  explicitly, e.g.\ by giving an option \verb,-k ZF, (in conjunction with
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    61
  \verb,-l ZF, to specify the default logic image).
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    62
\end{warn}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    63
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    64
\section{Lexical matters}\label{sec:lex-syntax}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    65
14955
wenzelm
parents: 14919
diff changeset
    66
The Isabelle/Isar outer syntax provides token classes as presented below; most
wenzelm
parents: 14919
diff changeset
    67
of these coincide with the inner lexical syntax as presented in
wenzelm
parents: 14919
diff changeset
    68
\cite{isabelle-ref}.
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    69
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
    70
\indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
    71
\indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
    72
\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{verbatim}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    73
\begin{matharray}{rcl}
14955
wenzelm
parents: 14919
diff changeset
    74
  ident & = & letter\,quasiletter^* \\
wenzelm
parents: 14919
diff changeset
    75
  longident & = & ident (\verb,.,ident)^+ \\
wenzelm
parents: 14919
diff changeset
    76
  symident & = & sym^+ ~|~ \verb,\<,ident\verb,>, \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    77
  nat & = & digit^+ \\
14212
cd05b503ca2d Improvements wrt rule_tac.
ballarin
parents: 13827
diff changeset
    78
  var & = & ident ~|~ \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    79
  typefree & = & \verb,',ident \\
14212
cd05b503ca2d Improvements wrt rule_tac.
ballarin
parents: 13827
diff changeset
    80
  typevar & = & typefree ~|~ \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    81
  string & = & \verb,", ~\dots~ \verb,", \\
14483
6eac487f9cfa documented new identifier syntax
kleing
parents: 14212
diff changeset
    82
  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\[1ex]
6eac487f9cfa documented new identifier syntax
kleing
parents: 14212
diff changeset
    83
14960
wenzelm
parents: 14955
diff changeset
    84
  letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~|~ \\
wenzelm
parents: 14955
diff changeset
    85
         &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
wenzelm
parents: 14955
diff changeset
    86
  quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
    87
  latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    88
  digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    89
  sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
10160
wenzelm
parents: 10152
diff changeset
    90
   \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
wenzelm
parents: 10152
diff changeset
    91
  & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
wenzelm
parents: 10152
diff changeset
    92
  \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
14955
wenzelm
parents: 14919
diff changeset
    93
greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
wenzelm
parents: 14919
diff changeset
    94
      &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
wenzelm
parents: 14919
diff changeset
    95
      &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
wenzelm
parents: 14919
diff changeset
    96
      &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
wenzelm
parents: 14919
diff changeset
    97
      &   & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
wenzelm
parents: 14919
diff changeset
    98
      &   & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
wenzelm
parents: 14919
diff changeset
    99
      &   & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
wenzelm
parents: 14919
diff changeset
   100
      &   & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   101
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   102
13039
wenzelm
parents: 12976
diff changeset
   103
The syntax of $string$ admits any characters, including newlines; ``\verb|"|''
wenzelm
parents: 12976
diff changeset
   104
(double-quote) and ``\verb|\|'' (backslash) need to be escaped by a backslash.
14955
wenzelm
parents: 14919
diff changeset
   105
The body of $verbatim$ may consist of any text not containing ``\verb|*}|'';
wenzelm
parents: 14919
diff changeset
   106
this allows convenient inclusion of quotes without further escapes.  The greek
wenzelm
parents: 14919
diff changeset
   107
letters do \emph{not} include \verb,\<lambda>,, which is already used
wenzelm
parents: 14919
diff changeset
   108
differently in the meta-logic.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   109
14955
wenzelm
parents: 14919
diff changeset
   110
Common mathematical symbols such as $\forall$ are represented in Isabelle as
wenzelm
parents: 14919
diff changeset
   111
\verb,\<forall>,.  There are infinitely many legal symbols like this, although
wenzelm
parents: 14919
diff changeset
   112
proper presentation is left to front-end tools such as {\LaTeX} or
wenzelm
parents: 14919
diff changeset
   113
Proof~General with the X-Symbol package.  A list of standard Isabelle symbols
wenzelm
parents: 14919
diff changeset
   114
that work well with these tools is given in \cite[appendix~A]{isabelle-sys}.
wenzelm
parents: 14919
diff changeset
   115
wenzelm
parents: 14919
diff changeset
   116
Comments take the form \texttt{(*~\dots~*)} and may be nested, although
wenzelm
parents: 14919
diff changeset
   117
user-interface tools may prevent this.  Note that \texttt{(*~\dots~*)}
wenzelm
parents: 14919
diff changeset
   118
indicate source comments only, which are stripped after lexical analysis of
wenzelm
parents: 14919
diff changeset
   119
the input.  The Isar document syntax also provides formal comments that are
wenzelm
parents: 14919
diff changeset
   120
considered as part of the text (see \S\ref{sec:comments}).
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   121
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   122
\begin{warn}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   123
  Proof~General does not handle nested comments properly; it is also unable to
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   124
  keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   125
  their rather different meaning.  These are inherent problems of Emacs
13039
wenzelm
parents: 12976
diff changeset
   126
  legacy.  Users should not be overly aggressive about nesting or alternating
wenzelm
parents: 12976
diff changeset
   127
  these delimiters.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   128
\end{warn}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   129
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   130
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   131
\section{Common syntax entities}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   132
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   133
Subsequently, we introduce several basic syntactic entities, such as names,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   134
terms, and theorem specifications, which have been factored out of the actual
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   135
Isar language elements to be described later.
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   136
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   137
Note that some of the basic syntactic entities introduced below (e.g.\
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   138
\railqtok{name}) act much like tokens rather than plain nonterminals (e.g.\
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   139
\railnonterm{sort}), especially for the sake of error messages.  E.g.\ syntax
13048
wenzelm
parents: 13039
diff changeset
   140
elements like $\CONSTS$ referring to \railqtok{name} or \railqtok{type} would
wenzelm
parents: 13039
diff changeset
   141
really report a missing name or type rather than any of the constituent
wenzelm
parents: 13039
diff changeset
   142
primitive tokens such as \railtok{ident} or \railtok{string}.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   143
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   144
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   145
\subsection{Names}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   146
13048
wenzelm
parents: 13039
diff changeset
   147
Entity \railqtok{name} usually refers to any name of types, constants,
7167
wenzelm
parents: 7141
diff changeset
   148
theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
8548
wenzelm
parents: 8532
diff changeset
   149
identifiers are excluded here).  Quoted strings provide an escape for
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   150
non-identifier names or those ruled out by outer syntax keywords (e.g.\
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   151
\verb|"let"|).  Already existing objects are usually referenced by
13048
wenzelm
parents: 13039
diff changeset
   152
\railqtok{nameref}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   153
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   154
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   155
\indexoutertoken{int}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   156
\begin{rail}
8145
cdd5386eb6fe 'name' syntax includes numbers;
wenzelm
parents: 8102
diff changeset
   157
  name: ident | symident | string | nat
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   158
  ;
7167
wenzelm
parents: 7141
diff changeset
   159
  parname: '(' name ')'
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   160
  ;
7167
wenzelm
parents: 7141
diff changeset
   161
  nameref: name | longident
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   162
  ;
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   163
  int: nat | '-' nat
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   164
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   165
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   166
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   167
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   168
\subsection{Comments}\label{sec:comments}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   169
13048
wenzelm
parents: 13039
diff changeset
   170
Large chunks of plain \railqtok{text} are usually given \railtok{verbatim},
wenzelm
parents: 13039
diff changeset
   171
i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For convenience, any of the
wenzelm
parents: 13039
diff changeset
   172
smaller text units conforming to \railqtok{nameref} are admitted as well.  A
wenzelm
parents: 13039
diff changeset
   173
marginal \railnonterm{comment} is of the form \texttt{--} \railqtok{text}.
wenzelm
parents: 13039
diff changeset
   174
Any number of these may occur within Isabelle/Isar commands.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   175
12879
wenzelm
parents: 12637
diff changeset
   176
\indexoutertoken{text}\indexouternonterm{comment}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   177
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   178
  text: verbatim | nameref
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   179
  ;
12879
wenzelm
parents: 12637
diff changeset
   180
  comment: '--' text
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   181
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   182
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   183
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   184
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   185
\subsection{Type classes, sorts and arities}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   186
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   187
Classes are specified by plain names.  Sorts have a very simple inner syntax,
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   188
which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   189
referring to the intersection of these classes.  The syntax of type arities is
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   190
given directly at the outer level.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   191
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   192
\railalias{subseteq}{\isasymsubseteq}
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   193
\railterm{subseteq}
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   194
14605
9de4d64eee3b 'instance' and intro_classes now handle general sorts;
wenzelm
parents: 14483
diff changeset
   195
\indexouternonterm{sort}\indexouternonterm{arity}
7135
wenzelm
parents: 7134
diff changeset
   196
\indexouternonterm{classdecl}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   197
\begin{rail}
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   198
  classdecl: name (('<' | subseteq) (nameref + ','))?
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   199
  ;
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   200
  sort: nameref
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   201
  ;
7167
wenzelm
parents: 7141
diff changeset
   202
  arity: ('(' (sort + ',') ')')? sort
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   203
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   204
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   205
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   206
7167
wenzelm
parents: 7141
diff changeset
   207
\subsection{Types and terms}\label{sec:types-terms}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   208
7167
wenzelm
parents: 7141
diff changeset
   209
The actual inner Isabelle syntax, that of types and terms of the logic, is far
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   210
too sophisticated in order to be modelled explicitly at the outer theory
8548
wenzelm
parents: 8532
diff changeset
   211
level.  Basically, any such entity has to be quoted to turn it into a single
wenzelm
parents: 8532
diff changeset
   212
token (the parsing and type-checking is performed internally later).  For
wenzelm
parents: 8532
diff changeset
   213
convenience, a slightly more liberal convention is adopted: quotes may be
13039
wenzelm
parents: 12976
diff changeset
   214
omitted for any type or term that is already atomic at the outer level.  For
wenzelm
parents: 12976
diff changeset
   215
example, one may just write \texttt{x} instead of \texttt{"x"}.  Note that
8548
wenzelm
parents: 8532
diff changeset
   216
symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   217
provided these have not been superseded by commands or other keywords already
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   218
(e.g.\ \texttt{=} or \texttt{+}).
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   219
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   220
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   221
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   222
  type: nameref | typefree | typevar
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   223
  ;
8593
68619606c5d1 fixed term syntax;
wenzelm
parents: 8548
diff changeset
   224
  term: nameref | var
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   225
  ;
7167
wenzelm
parents: 7141
diff changeset
   226
  prop: term
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   227
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   228
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   229
8690
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   230
Positional instantiations are indicated by giving a sequence of terms, or the
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   231
placeholder ``$\_$'' (underscore), which means to skip a position.
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   232
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   233
\indexoutertoken{inst}\indexoutertoken{insts}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   234
\begin{rail}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   235
  inst: underscore | term
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   236
  ;
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   237
  insts: (inst *)
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   238
  ;
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   239
\end{rail}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   240
7167
wenzelm
parents: 7141
diff changeset
   241
Type declarations and definitions usually refer to \railnonterm{typespec} on
wenzelm
parents: 7141
diff changeset
   242
the left-hand side.  This models basic type constructor application at the
wenzelm
parents: 7141
diff changeset
   243
outer syntax level.  Note that only plain postfix notation is available here,
wenzelm
parents: 7141
diff changeset
   244
but no infixes.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   245
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   246
\indexouternonterm{typespec}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   247
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   248
  typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   249
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   250
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   251
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   252
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   253
\subsection{Mixfix annotations}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   254
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   255
Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   256
terms.  Some commands such as $\TYPES$ (see \S\ref{sec:types-pure}) admit
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   257
infixes only, while $\CONSTS$ (see \S\ref{sec:consts}) and
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   258
$\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   259
general mixfixes and binders.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   260
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12879
diff changeset
   261
\indexouternonterm{infix}\indexouternonterm{mixfix}\indexouternonterm{structmixfix}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   262
\begin{rail}
11651
201b3f76c7b7 support non-oriented infix;
wenzelm
parents: 11100
diff changeset
   263
  infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
7167
wenzelm
parents: 7141
diff changeset
   264
  ;
7175
wenzelm
parents: 7167
diff changeset
   265
  mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   266
  ;
12976
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12879
diff changeset
   267
  structmixfix: mixfix | '(' 'structure' ')'
5cfe2941a5db contexts, locales, sym(metric);
wenzelm
parents: 12879
diff changeset
   268
  ;
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   269
7175
wenzelm
parents: 7167
diff changeset
   270
  prios: '[' (nat + ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   271
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   272
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   273
13048
wenzelm
parents: 13039
diff changeset
   274
Here the \railtok{string} specifications refer to the actual mixfix template
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   275
(see also \cite{isabelle-ref}), which may include literal text, spacing,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   276
blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   277
(printed as ``\i'') represents an index argument that specifies an implicit
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   278
structure reference (see also \S\ref{sec:locale}).  Infix and binder
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   279
declarations provide common abbreviations for particular mixfix declarations.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   280
So in practice, mixfix templates mostly degenerate to literal text for
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   281
concrete syntax, such as ``\verb,++,'' for an infix symbol, or ``\verb,++,\i''
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   282
for an infix of an implicit structure.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   283
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   284
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   285
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   286
\subsection{Proof methods}\label{sec:syn-meth}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   287
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   288
Proof methods are either basic ones, or expressions composed of methods via
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   289
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   290
``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once).  In practice,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   291
proof methods are usually just a comma separated list of
13048
wenzelm
parents: 13039
diff changeset
   292
\railqtok{nameref}~\railnonterm{args} specifications.  Note that parentheses
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   293
may be dropped for single method specifications (with no arguments).
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   294
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   295
\indexouternonterm{method}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   296
\begin{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   297
  method: (nameref | '(' methods ')') (() | '?' | '+')
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   298
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   299
  methods: (nameref args | method) + (',' | '|')
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   300
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   301
\end{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   302
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   303
Proper use of Isar proof methods does \emph{not} involve goal addressing.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   304
Nevertheless, specifying goal ranges may occasionally come in handy in
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   305
emulating tactic scripts.  Note that $[n-]$ refers to all goals, starting from
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   306
$n$.  All goals may be specified by $[!]$, which is the same as $[1-]$.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   307
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   308
\indexouternonterm{goalspec}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   309
\begin{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   310
  goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   311
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   312
\end{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   313
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   314
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   315
\subsection{Attributes and theorems}\label{sec:syn-att}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   316
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   317
Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   318
``semi-inner'' syntax, in the sense that input conforming to
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   319
\railnonterm{args} below is parsed by the attribute a second time.  The
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   320
attribute argument specifications may be any sequence of atomic entities
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   321
(identifiers, strings etc.), or properly bracketed argument lists.  Below
13048
wenzelm
parents: 13039
diff changeset
   322
\railqtok{atom} refers to any atomic entity, including any \railtok{keyword}
wenzelm
parents: 13039
diff changeset
   323
conforming to \railtok{symident}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   324
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   325
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   326
\begin{rail}
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   327
  atom: nameref | typefree | typevar | var | nat | keyword
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   328
  ;
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   329
  arg: atom | '(' args ')' | '[' args ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   330
  ;
7167
wenzelm
parents: 7141
diff changeset
   331
  args: arg *
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   332
  ;
7167
wenzelm
parents: 7141
diff changeset
   333
  attributes: '[' (nameref args * ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   334
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   335
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   336
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   337
Theorem specifications come in several flavors: \railnonterm{axmdecl} and
7175
wenzelm
parents: 7167
diff changeset
   338
\railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
7981
wenzelm
parents: 7895
diff changeset
   339
statements, while \railnonterm{thmdef} collects lists of existing theorems.
wenzelm
parents: 7895
diff changeset
   340
Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
wenzelm
parents: 7895
diff changeset
   341
the former requires an actual singleton result.  Any of these theorem
7175
wenzelm
parents: 7167
diff changeset
   342
specifications may include lists of attributes both on the left and right hand
13039
wenzelm
parents: 12976
diff changeset
   343
sides; attributes are applied to any immediately preceding fact.  If names are
wenzelm
parents: 12976
diff changeset
   344
omitted, the theorems are not stored within the theorem database of the theory
wenzelm
parents: 12976
diff changeset
   345
or proof context; any given attributes are still applied, though.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   346
7135
wenzelm
parents: 7134
diff changeset
   347
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
wenzelm
parents: 7134
diff changeset
   348
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   349
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   350
  axmdecl: name attributes? ':'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   351
  ;
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   352
  thmdecl: thmbind ':'
7135
wenzelm
parents: 7134
diff changeset
   353
  ;
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   354
  thmdef: thmbind '='
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   355
  ;
7175
wenzelm
parents: 7167
diff changeset
   356
  thmref: nameref attributes?
wenzelm
parents: 7167
diff changeset
   357
  ;
wenzelm
parents: 7167
diff changeset
   358
  thmrefs: thmref +
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   359
  ;
7167
wenzelm
parents: 7141
diff changeset
   360
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   361
  thmbind: name attributes | name | attributes
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   362
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   363
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   364
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   365
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   366
\subsection{Term patterns and declarations}\label{sec:term-decls}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   367
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   368
Wherever explicit propositions (or term fragments) occur in a proof text,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   369
casual binding of schematic term variables may be given specified via patterns
13039
wenzelm
parents: 12976
diff changeset
   370
of the form ``$\ISS{p@1\;\dots}{p@n}$''.  There are separate versions
13048
wenzelm
parents: 13039
diff changeset
   371
available for \railqtok{term}s and \railqtok{prop}s.  The latter provides a
wenzelm
parents: 13039
diff changeset
   372
$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   373
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   374
\indexouternonterm{termpat}\indexouternonterm{proppat}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   375
\begin{rail}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   376
  termpat: '(' ('is' term +) ')'
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   377
  ;
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   378
  proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   379
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   380
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   381
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   382
Declarations of local variables $x :: \tau$ and logical propositions $a :
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   383
\phi$ represent different views on the same principle of introducing a local
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   384
scope.  In practice, one may usually omit the typing of $vars$ (due to
13039
wenzelm
parents: 12976
diff changeset
   385
type-inference), and the naming of propositions (due to implicit references of
wenzelm
parents: 12976
diff changeset
   386
current facts).  In any case, Isar proof elements usually admit to introduce
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   387
multiple such items simultaneously.
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   388
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   389
\indexouternonterm{vars}\indexouternonterm{props}
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   390
\begin{rail}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   391
  vars: (name+) ('::' type)?
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   392
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   393
  props: thmdecl? (prop proppat? +)
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   394
  ;
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   395
\end{rail}
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   396
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   397
The treatment of multiple declarations corresponds to the complementary focus
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   398
of $vars$ versus $props$: in ``$x@1~\dots~x@n :: \tau$'' the typing refers to
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   399
all variables, while in $a\colon \phi@1~\dots~\phi@n$ the naming refers to all
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   400
propositions collectively.  Isar language elements that refer to $vars$ or
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   401
$props$ typically admit separate typings or namings via another level of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   402
iteration, with explicit $\AND$ separators; e.g.\ see $\FIXNAME$ and
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   403
$\ASSUMENAME$ in \S\ref{sec:proof-context}.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   404
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   405
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   406
\subsection{Antiquotations}\label{sec:antiq}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   407
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   408
\begin{matharray}{rcl}
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   409
  thm & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   410
  prop & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   411
  term & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   412
  typ & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   413
  text & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   414
  goals & : & \isarantiq \\
10351
770356c32ad9 added antiq. subgoals
nipkow
parents: 10336
diff changeset
   415
  subgoals & : & \isarantiq \\
13827
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   416
  prf & : & \isarantiq \\
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   417
  full_prf & : & \isarantiq \\
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   418
\end{matharray}
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   419
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   420
The text body of formal comments (see also \S\ref{sec:comments}) may contain
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   421
antiquotations of logical entities, such as theorems, terms and types, which
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   422
are to be presented in the final output produced by the Isabelle document
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   423
preparation system (see also \S\ref{sec:document-prep}).
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   424
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
   425
Thus embedding of
13039
wenzelm
parents: 12976
diff changeset
   426
``\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}}''
wenzelm
parents: 12976
diff changeset
   427
within a text block would cause
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   428
\isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
10160
wenzelm
parents: 10152
diff changeset
   429
to appear in the final {\LaTeX} document.  Also note that theorem
wenzelm
parents: 10152
diff changeset
   430
antiquotations may involve attributes as well.  For example,
wenzelm
parents: 10152
diff changeset
   431
\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
wenzelm
parents: 10152
diff changeset
   432
statement where all schematic variables have been replaced by fixed ones,
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   433
which are easier to read.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   434
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   435
\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   436
\indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   437
\begin{rail}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   438
  atsign lbrace antiquotation rbrace
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   439
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   440
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   441
  antiquotation:
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   442
    'thm' options thmrefs |
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   443
    'prop' options prop |
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   444
    'term' options term |
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   445
    'typ' options type |
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   446
    'text' options name |
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   447
    'goals' options |
13827
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   448
    'subgoals' options |
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   449
    'prf' options thmrefs |
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   450
    'full\_prf' options thmrefs
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   451
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   452
  options: '[' (option * ',') ']'
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   453
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   454
  option: name | name '=' name
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   455
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   456
\end{rail}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   457
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   458
Note that the syntax of antiquotations may \emph{not} include source comments
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   459
\texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   460
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   461
\begin{descr}
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   462
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   463
\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   464
  specifications may be included as well (see also \S\ref{sec:syn-att}); the
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   465
  $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   466
  useful to suppress printing of schematic variables.
13039
wenzelm
parents: 12976
diff changeset
   467
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   468
\item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
13039
wenzelm
parents: 12976
diff changeset
   469
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   470
\item [$\at\{term~t\}$] prints a well-typed term $t$.
13039
wenzelm
parents: 12976
diff changeset
   471
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   472
\item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   473
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   474
\item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   475
  particularly useful to print portions of text according to the Isabelle
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   476
  {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
13039
wenzelm
parents: 12976
diff changeset
   477
  of terms that should not be parsed or type-checked yet).
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   478
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   479
\item [$\at\{goals\}$] prints the current \emph{dynamic} goal state.  This is
13039
wenzelm
parents: 12976
diff changeset
   480
  mainly for support of tactic-emulation scripts within Isar --- presentation
wenzelm
parents: 12976
diff changeset
   481
  of goal states does not conform to actual human-readable proof documents.
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   482
  Please do not include goal states into document output unless you really
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   483
  know what you are doing!
13039
wenzelm
parents: 12976
diff changeset
   484
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   485
\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   486
  print the main goal.
13039
wenzelm
parents: 12976
diff changeset
   487
13827
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   488
\item [$\at\{prf~\vec a\}$] prints the (compact) proof terms corresponding to
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   489
  the theorems $\vec a$. Note that this
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   490
  requires proof terms to be switched on for the current object logic
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   491
  (see the ``Proof terms'' section of the Isabelle reference manual
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   492
  for information on how to do this).
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   493
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   494
\item [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   495
  the full proof terms, i.e.\ also displays information omitted in
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   496
  the compact proof term, which is denoted by ``$_$'' placeholders there.
c690cb885db4 Documented prf / full_prf commands and antiquotations.
berghofe
parents: 13048
diff changeset
   497
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   498
\end{descr}
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   499
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   500
\medskip
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   501
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   502
The following options are available to tune the output.  Note that most of
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   503
these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   504
\begin{descr}
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   505
\item[$show_types = bool$ and $show_sorts = bool$] control printing of
9234
0013b2aa98dd IGNORE last log message!
wenzelm
parents: 9233
diff changeset
   506
  explicit type and sort constraints.
14707
2d6350d7b9b7 show_structs option;
wenzelm
parents: 14689
diff changeset
   507
\item[$show_structs = bool$] controls printing of implicit structures.
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   508
\item[$long_names = bool$] forces names of types and constants etc.\ to be
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   509
  printed in their fully qualified internal form.
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   510
\item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   511
\item[$display = bool$] indicates if the text is to be output as multi-line
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   512
  ``display material'', rather than a small piece of text without line breaks
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   513
  (which is the default).
14689
eafb91eda9e8 breaks flag;
wenzelm
parents: 14605
diff changeset
   514
\item[$breaks = bool$] controls line breaks in non-display material.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   515
\item[$quotes = bool$] indicates if the output should be enclosed in double
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   516
  quotes.
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   517
\item[$mode = name$] adds $name$ to the print mode to be used for presentation
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   518
  (see also \cite{isabelle-ref}).  Note that the standard setup for {\LaTeX}
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   519
  output is already present by default, including the modes ``$latex$'',
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   520
  ``$xsymbols$'', ``$symbols$''.
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   521
\item[$margin = nat$ and $indent = nat$] change the margin or indentation for
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   522
  pretty printing of display material.
9752
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   523
\item[$source = bool$] prints the source text of the antiquotation arguments,
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   524
  rather than the actual value.  Note that this does not affect
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   525
  well-formedness checks of $thm$, $term$, etc. (only the $text$ antiquotation
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   526
  admits arbitrary output).
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   527
\item[$goals_limit = nat$] determines the maximum number of goals to be
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   528
  printed.
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   529
\item[$locale = name$] specifies an alternative context used for evaluating
14919
wenzelm
parents: 14895
diff changeset
   530
  and printing the subsequent argument.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   531
\end{descr}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   532
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   533
For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   534
the above flags are disabled by default, unless changed from ML.
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   535
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   536
\medskip Note that antiquotations do not only spare the author from tedious
13039
wenzelm
parents: 12976
diff changeset
   537
typing of logical entities, but also achieve some degree of
wenzelm
parents: 12976
diff changeset
   538
consistency-checking of informal explanations with formal developments:
wenzelm
parents: 12976
diff changeset
   539
well-formedness of terms and types with respect to the current theory or proof
wenzelm
parents: 12976
diff changeset
   540
context is ensured here.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   541
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   542
%%% Local Variables:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   543
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   544
%%% TeX-master: "isar-ref"
14895
b9cc12a91fd3 updated/tuned identifier syntax;
wenzelm
parents: 14707
diff changeset
   545
%%% End: