doc-src/IsarRef/syntax.tex
author wenzelm
Wed, 02 Jan 2002 21:53:50 +0100
changeset 12618 43a97a2155d0
parent 11651 201b3f76c7b7
child 12637 4d43b06a81e1
permissions -rw-r--r--
first stage of major update;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
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
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    43
clearly indicated from the input syntax, e.g.\ encounter of the next command
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
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    66
The Isabelle/Isar outer syntax provides token classes as presented below.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    67
Note that some of these coincide (by full intention) with the inner lexical
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    68
syntax as presented in \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}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    74
  ident & = & letter~quasiletter^* \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    75
  longident & = & ident\verb,.,ident~\dots~ident \\
8548
wenzelm
parents: 8532
diff changeset
    76
  symident & = & sym^+ ~|~ symbol \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    77
  nat & = & digit^+ \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    78
  var & = & \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    79
  typefree & = & \verb,',ident \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    80
  typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    81
  string & = & \verb,", ~\dots~ \verb,", \\
7319
wenzelm
parents: 7315
diff changeset
    82
  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
wenzelm
parents: 7315
diff changeset
    83
\end{matharray}
wenzelm
parents: 7315
diff changeset
    84
\begin{matharray}{rcl}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    85
  letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    86
  digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    87
  quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    88
  sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
10160
wenzelm
parents: 10152
diff changeset
    89
   \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
wenzelm
parents: 10152
diff changeset
    90
  & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
wenzelm
parents: 10152
diff changeset
    91
  \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    92
  symbol & = & {\forall} ~|~ {\exists} ~|~ {\land} ~|~ {\lor} ~|~ \dots
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    93
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    94
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    95
The syntax of \railtoken{string} admits any characters, including newlines;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    96
``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) need to be escaped by
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    97
a backslash.  Note that ML-style control characters are \emph{not} supported.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    98
The body of \railtoken{verbatim} may consist of any text not containing
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
    99
``\verb|*}|''; this allows handsome inclusion of quotes without further
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   100
escapes.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   101
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   102
Comments take the form \texttt{(*~\dots~*)} and may in principle be nested,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   103
just as in ML.  Note that these are \emph{source} comments only, which are
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   104
stripped after lexical analysis of the input.  The Isar document syntax also
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   105
provides \emph{formal comments} that are actually part of the text (see
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   106
\S\ref{sec:comments}).
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   107
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   108
\begin{warn}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   109
  Proof~General does not handle nested comments properly; it is also unable to
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   110
  keep \verb,(*,\,/\,\verb,{*, and \verb,*),\,/\,\verb,*}, apart, despite
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   111
  their rather different meaning.  These are inherent problems of Emacs
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   112
  legacy.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   113
\end{warn}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   114
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   115
\medskip
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   116
10160
wenzelm
parents: 10152
diff changeset
   117
Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   118
``\verb,\<forall>,''.  Concerning Isabelle itself, any sequence of the form
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   119
\verb,\<,$ident$\verb,>, (or \verb,\\<,$ident$\verb,>,) is a legal symbol.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   120
Display of appropriate glyphs is a matter of front-end tools, say the
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   121
user-interface of Proof~General plus the X-Symbol package, or the {\LaTeX}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   122
macro setup of document output.  A list of predefined Isabelle symbols is
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   123
given in \cite[Appendix~A]{isabelle-sys}.
10160
wenzelm
parents: 10152
diff changeset
   124
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   125
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   126
\section{Common syntax entities}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   127
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   128
Subsequently, we introduce several basic syntactic entities, such as names,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   129
terms, and theorem specifications, which have been factored out of the actual
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   130
Isar language elements to be described later.
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   131
7981
wenzelm
parents: 7895
diff changeset
   132
Note that some of the basic syntactic entities introduced below (e.g.\ 
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   133
\railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\ 
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   134
\railnonterm{sort}), especially for the sake of error messages.  E.g.\ syntax
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   135
elements like $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   136
would really report a missing name or type rather than any of the constituent
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   137
primitive tokens such as \railtoken{ident} or \railtoken{string}.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   138
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   139
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   140
\subsection{Names}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   141
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   142
Entity \railqtoken{name} usually refers to any name of types, constants,
7167
wenzelm
parents: 7141
diff changeset
   143
theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
8548
wenzelm
parents: 8532
diff changeset
   144
identifiers are excluded here).  Quoted strings provide an escape for
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   145
non-identifier names or those ruled out by outer syntax keywords (e.g.\ 
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   146
\verb|"let"|).  Already existing objects are usually referenced by
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   147
\railqtoken{nameref}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   148
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   149
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   150
\indexoutertoken{int}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   151
\begin{rail}
8145
cdd5386eb6fe 'name' syntax includes numbers;
wenzelm
parents: 8102
diff changeset
   152
  name: ident | symident | string | nat
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   153
  ;
7167
wenzelm
parents: 7141
diff changeset
   154
  parname: '(' name ')'
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   155
  ;
7167
wenzelm
parents: 7141
diff changeset
   156
  nameref: name | longident
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   157
  ;
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   158
  int: nat | '-' nat
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   159
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   160
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   161
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   162
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   163
\subsection{Comments}\label{sec:comments}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   164
7167
wenzelm
parents: 7141
diff changeset
   165
Large chunks of plain \railqtoken{text} are usually given
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   166
\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For
7175
wenzelm
parents: 7167
diff changeset
   167
convenience, any of the smaller text units conforming to \railqtoken{nameref}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   168
are admitted as well.  Almost any of the Isar commands may be annotated by a
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   169
marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   170
Note that the latter kind of comment is actually part of the language, while
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   171
source level comments \verb|(*|~\dots~\verb|*)| are stripped at the lexical
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   172
level.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   173
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   174
A few commands such as $\PROOFNAME$ admit additional markup with a ``level of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   175
interest'': \texttt{\%} followed by an optional number $n$ (default $n = 1$)
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   176
indicates that the respective part of the document becomes $n$ levels more
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   177
obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon every
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   178
hope, who enter here.  So far the Isabelle tool-chain (for document output
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   179
etc.) does not yet treat interest levels specifically.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   180
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   181
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   182
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   183
  text: verbatim | nameref
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   184
  ;
8102
424f6e663977 comment: any number of texts;
wenzelm
parents: 7981
diff changeset
   185
  comment: ('--' text +)
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   186
  ;
7167
wenzelm
parents: 7141
diff changeset
   187
  interest: percent nat? | ppercent
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   188
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   189
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   190
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   191
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   192
\subsection{Type classes, sorts and arities}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   193
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   194
Classes are specified by plain names.  Sorts have a very simple inner syntax,
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   195
which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   196
referring to the intersection of these classes.  The syntax of type arities is
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   197
given directly at the outer level.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   198
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   199
\railalias{subseteq}{\isasymsubseteq}
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   200
\railterm{subseteq}
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   201
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   202
\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
7135
wenzelm
parents: 7134
diff changeset
   203
\indexouternonterm{classdecl}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   204
\begin{rail}
11100
34d58b1818f4 \<subseteq> syntax for classes/classrel/axclass/instance;
wenzelm
parents: 10858
diff changeset
   205
  classdecl: name (('<' | subseteq) (nameref + ','))?
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   206
  ;
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   207
  sort: nameref
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   208
  ;
7167
wenzelm
parents: 7141
diff changeset
   209
  arity: ('(' (sort + ',') ')')? sort
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   210
  ;
7167
wenzelm
parents: 7141
diff changeset
   211
  simplearity: ('(' (sort + ',') ')')? nameref
wenzelm
parents: 7141
diff changeset
   212
  ;
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   213
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   214
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   215
7167
wenzelm
parents: 7141
diff changeset
   216
\subsection{Types and terms}\label{sec:types-terms}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   217
7167
wenzelm
parents: 7141
diff changeset
   218
The actual inner Isabelle syntax, that of types and terms of the logic, is far
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   219
too sophisticated in order to be modelled explicitly at the outer theory
8548
wenzelm
parents: 8532
diff changeset
   220
level.  Basically, any such entity has to be quoted to turn it into a single
wenzelm
parents: 8532
diff changeset
   221
token (the parsing and type-checking is performed internally later).  For
wenzelm
parents: 8532
diff changeset
   222
convenience, a slightly more liberal convention is adopted: quotes may be
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   223
omitted for any type or term that is already \emph{atomic} at the outer level.
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   224
For example, one may just write \texttt{x} instead of \texttt{"x"}.  Note that
8548
wenzelm
parents: 8532
diff changeset
   225
symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   226
provided these have not been superseded by commands or other keywords already
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   227
(e.g.\ \texttt{=} or \texttt{+}).
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   228
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   229
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   230
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   231
  type: nameref | typefree | typevar
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   232
  ;
8593
68619606c5d1 fixed term syntax;
wenzelm
parents: 8548
diff changeset
   233
  term: nameref | var
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   234
  ;
7167
wenzelm
parents: 7141
diff changeset
   235
  prop: term
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   236
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   237
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   238
8690
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   239
Positional instantiations are indicated by giving a sequence of terms, or the
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   240
placeholder ``$\_$'' (underscore), which means to skip a position.
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   241
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   242
\indexoutertoken{inst}\indexoutertoken{insts}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   243
\begin{rail}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   244
  inst: underscore | term
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   245
  ;
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   246
  insts: (inst *)
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   247
  ;
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   248
\end{rail}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   249
7167
wenzelm
parents: 7141
diff changeset
   250
Type declarations and definitions usually refer to \railnonterm{typespec} on
wenzelm
parents: 7141
diff changeset
   251
the left-hand side.  This models basic type constructor application at the
wenzelm
parents: 7141
diff changeset
   252
outer syntax level.  Note that only plain postfix notation is available here,
wenzelm
parents: 7141
diff changeset
   253
but no infixes.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   254
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   255
\indexouternonterm{typespec}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   256
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   257
  typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   258
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   259
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   260
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   261
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   262
\subsection{Mixfix annotations}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   263
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   264
Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   265
terms.  Some commands such as $\TYPES$ (see \S\ref{sec:types-pure}) admit
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   266
infixes only, while $\CONSTS$ (see \S\ref{sec:consts}) and
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   267
$\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans}) support the full range of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   268
general mixfixes and binders.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   269
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   270
\indexouternonterm{infix}\indexouternonterm{mixfix}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   271
\begin{rail}
11651
201b3f76c7b7 support non-oriented infix;
wenzelm
parents: 11100
diff changeset
   272
  infix: '(' ('infix' | 'infixl' | 'infixr') string? nat ')'
7167
wenzelm
parents: 7141
diff changeset
   273
  ;
7175
wenzelm
parents: 7167
diff changeset
   274
  mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   275
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   276
7175
wenzelm
parents: 7167
diff changeset
   277
  prios: '[' (nat + ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   278
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   279
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   280
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   281
Here the \railtoken{string} specifications refer to the actual mixfix template
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   282
(see also \cite{isabelle-ref}), which may include literal text, spacing,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   283
blocks, and arguments (denoted by ``$_$''); the special symbol \verb,\<index>,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   284
(printed as ``\i'') represents an index argument that specifies an implicit
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   285
structure reference (see also \S\ref{sec:locale}).  Infix and binder
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   286
declarations provide common abbreviations for particular mixfix declarations.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   287
So in practice, mixfix templates mostly degenerate to literal text for
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   288
concrete syntax, such as ``\verb,++,'' for an infix symbol, or ``\verb,++,\i''
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   289
for an infix of an implicit structure.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   290
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   291
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   292
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   293
\subsection{Proof methods}\label{sec:syn-meth}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   294
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   295
Proof methods are either basic ones, or expressions composed of methods via
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   296
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   297
``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once).  In practice,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   298
proof methods are usually just a comma separated list of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   299
\railqtoken{nameref}~\railnonterm{args} specifications.  Note that parentheses
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   300
may be dropped for single method specifications (with no arguments).
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   301
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   302
\indexouternonterm{method}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   303
\begin{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   304
  method: (nameref | '(' methods ')') (() | '?' | '+')
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   305
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   306
  methods: (nameref args | method) + (',' | '|')
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   307
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   308
\end{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   309
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   310
Proper use of Isar proof methods does \emph{not} involve goal addressing.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   311
Nevertheless, specifying goal ranges may occasionally come in handy in
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   312
emulating tactic scripts.  Note that $[n-]$ refers to all goals, starting from
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   313
$n$.  All goals may be specified by $[!]$, which is the same as $[1-]$.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   314
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   315
\indexouternonterm{goalspec}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   316
\begin{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   317
  goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   318
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   319
\end{rail}
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   320
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   321
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   322
\subsection{Attributes and theorems}\label{sec:syn-att}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   323
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   324
Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   325
``semi-inner'' syntax, in the sense that input conforming to
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   326
\railnonterm{args} below is parsed by the attribute a second time.  The
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   327
attribute argument specifications may be any sequence of atomic entities
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   328
(identifiers, strings etc.), or properly bracketed argument lists.  Below
7981
wenzelm
parents: 7895
diff changeset
   329
\railqtoken{atom} refers to any atomic entity, including any
wenzelm
parents: 7895
diff changeset
   330
\railtoken{keyword} conforming to \railtoken{symident}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   331
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   332
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   333
\begin{rail}
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   334
  atom: nameref | typefree | typevar | var | nat | keyword
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   335
  ;
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   336
  arg: atom | '(' args ')' | '[' args ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   337
  ;
7167
wenzelm
parents: 7141
diff changeset
   338
  args: arg *
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   339
  ;
7167
wenzelm
parents: 7141
diff changeset
   340
  attributes: '[' (nameref args * ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   341
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   342
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   343
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   344
Theorem specifications come in several flavors: \railnonterm{axmdecl} and
7175
wenzelm
parents: 7167
diff changeset
   345
\railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
7981
wenzelm
parents: 7895
diff changeset
   346
statements, while \railnonterm{thmdef} collects lists of existing theorems.
wenzelm
parents: 7895
diff changeset
   347
Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
wenzelm
parents: 7895
diff changeset
   348
the former requires an actual singleton result.  Any of these theorem
7175
wenzelm
parents: 7167
diff changeset
   349
specifications may include lists of attributes both on the left and right hand
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   350
sides; attributes are applied to any immediately preceding theorem.  If names
7981
wenzelm
parents: 7895
diff changeset
   351
are omitted, the theorems are not stored within the theorem database of the
wenzelm
parents: 7895
diff changeset
   352
theory or proof context; any given attributes are still applied, though.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   353
7135
wenzelm
parents: 7134
diff changeset
   354
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
wenzelm
parents: 7134
diff changeset
   355
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   356
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   357
  axmdecl: name attributes? ':'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   358
  ;
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   359
  thmdecl: thmbind ':'
7135
wenzelm
parents: 7134
diff changeset
   360
  ;
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   361
  thmdef: thmbind '='
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   362
  ;
7175
wenzelm
parents: 7167
diff changeset
   363
  thmref: nameref attributes?
wenzelm
parents: 7167
diff changeset
   364
  ;
wenzelm
parents: 7167
diff changeset
   365
  thmrefs: thmref +
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   366
  ;
7167
wenzelm
parents: 7141
diff changeset
   367
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   368
  thmbind: name attributes | name | attributes
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   369
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   370
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   371
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   372
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   373
\subsection{Term patterns and declarations}\label{sec:term-decls}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   374
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   375
Wherever explicit propositions (or term fragments) occur in a proof text,
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   376
casual binding of schematic term variables may be given specified via patterns
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   377
of the form $\ISS{p@1\;\dots}{p@n}$.  There are separate versions available
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   378
for \railqtoken{term}s and \railqtoken{prop}s.  The latter provides a
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   379
$\CONCLNAME$ part with patterns referring the (atomic) conclusion of a rule.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   380
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   381
\indexouternonterm{termpat}\indexouternonterm{proppat}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   382
\begin{rail}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   383
  termpat: '(' ('is' term +) ')'
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   384
  ;
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   385
  proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   386
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   387
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   388
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   389
Declarations of local variables $x :: \tau$ and logical propositions $a :
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   390
\phi$ represent different views on the same principle of introducing a local
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   391
scope.  In practice, one may usually omit the typing of $vars$ (due to
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   392
type-inference), and the naming of propositions (due to implicit chaining of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   393
emerging facts).  In any case, Isar proof elements usually admit to introduce
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   394
multiple such items simultaneously.
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   395
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   396
\indexouternonterm{vars}\indexouternonterm{props}
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   397
\begin{rail}
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   398
  vars: (name+) ('::' type)?
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   399
  ;
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   400
  props: thmdecl? (prop proppat? +)
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   401
  ;
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   402
\end{rail}
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   403
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   404
The treatment of multiple declarations corresponds to the complementary focus
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   405
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
   406
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
   407
propositions collectively.  Isar language elements that refer to $vars$ or
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   408
$props$ typically admit separate typings or namings via another level of
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   409
iteration, with explicit $\AND$ separators; e.g.\ see $\FIXNAME$ and
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   410
$\ASSUMENAME$ in \S\ref{sec:proof-context}.
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   411
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   412
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   413
\subsection{Antiquotations}\label{sec:antiq}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   414
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   415
\begin{matharray}{rcl}
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   416
  thm & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   417
  prop & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   418
  term & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   419
  typ & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   420
  text & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   421
  goals & : & \isarantiq \\
10351
770356c32ad9 added antiq. subgoals
nipkow
parents: 10336
diff changeset
   422
  subgoals & : & \isarantiq \\
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   423
\end{matharray}
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   424
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   425
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
   426
antiquotations of logical entities, such as theorems, terms and types, which
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   427
are to be presented in the final output produced by the Isabelle document
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   428
preparation system (see also \S\ref{sec:document-prep}).
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   429
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
   430
Thus embedding of
10160
wenzelm
parents: 10152
diff changeset
   431
\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
   432
text block would cause
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   433
\isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
10160
wenzelm
parents: 10152
diff changeset
   434
to appear in the final {\LaTeX} document.  Also note that theorem
wenzelm
parents: 10152
diff changeset
   435
antiquotations may involve attributes as well.  For example,
wenzelm
parents: 10152
diff changeset
   436
\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
wenzelm
parents: 10152
diff changeset
   437
statement where all schematic variables have been replaced by fixed ones,
12618
43a97a2155d0 first stage of major update;
wenzelm
parents: 11651
diff changeset
   438
which are easier to read.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   439
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   440
\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   441
\indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   442
\begin{rail}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   443
  atsign lbrace antiquotation rbrace
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   444
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   445
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   446
  antiquotation:
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   447
    'thm' options thmrefs |
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   448
    'prop' options prop |
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   449
    'term' options term |
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   450
    'typ' options type |
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   451
    'text' options name |
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   452
    'goals' options |
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   453
    'subgoals' options
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   454
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   455
  options: '[' (option * ',') ']'
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   456
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   457
  option: name | name '=' name
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   458
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   459
\end{rail}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   460
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   461
Note that the syntax of antiquotations may \emph{not} include source comments
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   462
\texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   463
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   464
\begin{descr}
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   465
\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   466
  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
   467
  $no_vars$ operation (see \S\ref{sec:misc-meth-att}) would be particularly
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   468
  useful to suppress printing of schematic variables.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   469
\item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   470
\item [$\at\{term~t\}$] prints a well-typed term $t$.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   471
\item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   472
\item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   473
  particularly useful to print portions of text according to the Isabelle
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   474
  {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   475
  of terms that cannot be parsed or type-checked yet).
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   476
\item [$\at\{goals\}$] prints the current \emph{dynamic} goal state.  This is
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   477
  only for support of tactic-emulation scripts within Isar --- presentation of
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   478
  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
   479
  
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   480
  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
   481
  know what you are doing!
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   482
\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   483
  print the main goal.
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   484
\end{descr}
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   485
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   486
\medskip
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   487
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   488
The following options are available to tune the output.  Note that most of
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   489
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
   490
\begin{descr}
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   491
\item[$show_types = bool$ and $show_sorts = bool$] control printing of
9234
0013b2aa98dd IGNORE last log message!
wenzelm
parents: 9233
diff changeset
   492
  explicit type and sort constraints.
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   493
\item[$long_names = bool$] forces names of types and constants etc.\ to be
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   494
  printed in their fully qualified internal form.
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   495
\item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   496
\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
   497
  ``display material'', rather than a small piece of text without line breaks
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   498
  (which is the default).
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   499
\item[$quotes = bool$] indicates if the output should be enclosed in double
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   500
  quotes.
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   501
\item[$mode = name$] adds $name$ to the print mode to be used for presentation
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   502
  (see also \cite{isabelle-ref}).  Note that the standard setup for {\LaTeX}
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   503
  output is already present by default, including the modes ``$latex$'',
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   504
  ``$xsymbols$'', ``$symbols$''.
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   505
\item[$margin = nat$ and $indent = nat$] change the margin or indentation for
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   506
  pretty printing of display material.
9752
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   507
\item[$source = bool$] prints the source text of the antiquotation arguments,
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   508
  rather than the actual value.  Note that this does not affect
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   509
  well-formedness checks of $thm$, $term$, etc. (only the $text$ antiquotation
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   510
  admits arbitrary output).
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   511
\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
   512
  printed.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   513
\end{descr}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   514
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   515
For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   516
the above flags are disabled by default, unless changed from ML.
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   517
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   518
\medskip Note that antiquotations do not only spare the author from tedious
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   519
typing, but also achieve some degree of consistency-checking of informal
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   520
explanations with formal developments, since well-formedness of terms and
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   521
types with respect to the current theory or proof context can be ensured.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   522
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   523
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   524
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   525
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   526
%%% End: