doc-src/IsarRef/syntax.tex
author wenzelm
Fri, 10 Nov 2000 19:02:37 +0100
changeset 10432 3dfbc913d184
parent 10355 aef4f587a0e4
child 10858 479dad7b3b41
permissions -rw-r--r--
added axclass inverse and consts inverse, divide (infix "/"); moved axclass power to Nat.thy;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     1
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
     2
\chapter{Isar Syntax Primitives}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
     3
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     4
We give a complete reference of all basic syntactic entities underlying the
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
     5
Isabelle/Isar document syntax.  Actual theory and proof commands will be
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
     6
introduced later on.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     7
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     8
\medskip
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
     9
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    10
In order to get started with writing well-formed Isabelle/Isar documents, the
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    11
most important aspect to be noted is the difference of \emph{inner} versus
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    12
\emph{outer} syntax.  Inner syntax is that of Isabelle types and terms of the
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    13
logic, while outer syntax is that of Isabelle/Isar theories (including
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    14
proofs).  As a general rule, inner syntax entities may occur only as
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    15
\emph{atomic entities} within outer syntax.  For example, the string
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    16
\texttt{"x + y"} and identifier \texttt{z} are legal term specifications
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    17
within a theory, while \texttt{x + y} is not.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    18
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    19
\begin{warn}
8378
wenzelm
parents: 8145
diff changeset
    20
  Note that classic Isabelle theories used to fake parts of the inner syntax
wenzelm
parents: 8145
diff changeset
    21
  of types, with rather complicated rules when quotes may be omitted.  Despite
7981
wenzelm
parents: 7895
diff changeset
    22
  the minor drawback of requiring quotes more often, the syntax of
8548
wenzelm
parents: 8532
diff changeset
    23
  Isabelle/Isar is much simpler and more robust in that respect.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    24
\end{warn}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    25
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
    26
\medskip
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
    27
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    28
Isabelle/Isar input may contain any number of input termination characters
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    29
``\texttt{;}'' (semicolon) to separate commands explicitly.  This may be
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    30
particularly useful in interactive shell sessions to make clear where the
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    31
current command is intended to end.  Otherwise, the interactive loop will
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    32
continue until end-of-command in clearly indicated from the input syntax,
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    33
e.g.\ encounter of the next command keyword.
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    34
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    35
Advanced interfaces such as Proof~General \cite{proofgeneral} do not require
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    36
explicit semicolons, the amount of input text is determined automatically by
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    37
inspecting the Emacs text buffer.  Also note that in the presentation of
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
    38
Isabelle/Isar documents, semicolons are omitted in any case to gain
7981
wenzelm
parents: 7895
diff changeset
    39
readability.
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
    40
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    41
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    42
\section{Lexical matters}\label{sec:lex-syntax}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    43
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    44
The Isabelle/Isar outer syntax provides token classes as presented below.
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    45
Note that some of these coincide (by full intention) with the inner lexical
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    46
syntax as presented in \cite{isabelle-ref}.  These different levels of syntax
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    47
should not be confused, though.
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    48
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
    49
%FIXME keyword, command
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
    50
\indexoutertoken{ident}\indexoutertoken{longident}\indexoutertoken{symident}
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
    51
\indexoutertoken{nat}\indexoutertoken{var}\indexoutertoken{typefree}
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
    52
\indexoutertoken{typevar}\indexoutertoken{string}\indexoutertoken{verbatim}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    53
\begin{matharray}{rcl}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    54
  ident & = & letter~quasiletter^* \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    55
  longident & = & ident\verb,.,ident~\dots~ident \\
8548
wenzelm
parents: 8532
diff changeset
    56
  symident & = & sym^+ ~|~ symbol \\
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    57
  nat & = & digit^+ \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    58
  var & = & \verb,?,ident ~|~ \verb,?,ident\verb,.,nat \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    59
  typefree & = & \verb,',ident \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    60
  typevar & = & \verb,?,typefree ~|~ \verb,?,typefree\verb,.,nat \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    61
  string & = & \verb,", ~\dots~ \verb,", \\
7319
wenzelm
parents: 7315
diff changeset
    62
  verbatim & = & \verb,{*, ~\dots~ \verb,*}, \\
wenzelm
parents: 7315
diff changeset
    63
\end{matharray}
wenzelm
parents: 7315
diff changeset
    64
\begin{matharray}{rcl}
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    65
  letter & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    66
  digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    67
  quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    68
  sym & = & \verb,!, ~|~ \verb,#, ~|~ \verb,$, ~|~ \verb,%, ~|~ \verb,&, ~|~  %$
10160
wenzelm
parents: 10152
diff changeset
    69
   \verb,*, ~|~ \verb,+, ~|~ \verb,-, ~|~ \verb,/, ~|~ \verb,:, ~|~ \\
wenzelm
parents: 10152
diff changeset
    70
  & & \verb,<, ~|~ \verb,=, ~|~ \verb,>, ~|~ \verb,?, ~|~ \texttt{\at} ~|~
wenzelm
parents: 10152
diff changeset
    71
  \verb,^, ~|~ \verb,_, ~|~ \verb,`, ~|~ \verb,|, ~|~ \verb,~, \\
8548
wenzelm
parents: 8532
diff changeset
    72
  symbol & = & {\forall} ~|~ {\exists} ~|~ \dots
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    73
\end{matharray}
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    74
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    75
The syntax of \texttt{string} admits any characters, including newlines;
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    76
``\verb|"|'' (double-quote) and ``\verb|\|'' (backslash) have to be escaped by
9051
887a15590f0e string syntax: allow \\ \" \\n only;
wenzelm
parents: 8896
diff changeset
    77
a backslash; newlines need not be escaped.  Note that ML-style control
887a15590f0e string syntax: allow \\ \" \\n only;
wenzelm
parents: 8896
diff changeset
    78
characters are \emph{not} supported.  The body of \texttt{verbatim} may
887a15590f0e string syntax: allow \\ \" \\n only;
wenzelm
parents: 8896
diff changeset
    79
consist of any text not containing ``\verb|*}|''.
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    80
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    81
Comments take the form \texttt{(*~\dots~*)} and may be
8378
wenzelm
parents: 8145
diff changeset
    82
nested\footnote{Proof~General may occasionally get confused by nested
wenzelm
parents: 8145
diff changeset
    83
  comments.}, just as in ML. Note that these are \emph{source} comments only,
wenzelm
parents: 8145
diff changeset
    84
which are stripped after lexical analysis of the input.  The Isar document
wenzelm
parents: 8145
diff changeset
    85
syntax also provides \emph{formal comments} that are actually part of the text
wenzelm
parents: 8145
diff changeset
    86
(see \S\ref{sec:comments}).
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
    87
10160
wenzelm
parents: 10152
diff changeset
    88
Mathematical symbols such as ``$\forall$'' are represented in plain ASCII as
wenzelm
parents: 10152
diff changeset
    89
``\verb,\<forall>,''.
wenzelm
parents: 10152
diff changeset
    90
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    91
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    92
\section{Common syntax entities}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
    93
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
    94
Subsequently, we introduce several basic syntactic entities, such as names,
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    95
terms, and theorem specifications, which have been factored out of the actual
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    96
Isar language elements to be described later.
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
    97
7981
wenzelm
parents: 7895
diff changeset
    98
Note that some of the basic syntactic entities introduced below (e.g.\ 
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
    99
\railqtoken{name}) act much like tokens rather than plain nonterminals (e.g.\ 
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   100
\railnonterm{sort}), especially for the sake of error messages.  E.g.\ syntax
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   101
elements such as $\CONSTS$ referring to \railqtoken{name} or \railqtoken{type}
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   102
would really report a missing name or type rather than any of the constituent
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   103
primitive tokens such as \railtoken{ident} or \railtoken{string}.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   104
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   105
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   106
\subsection{Names}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   107
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   108
Entity \railqtoken{name} usually refers to any name of types, constants,
7167
wenzelm
parents: 7141
diff changeset
   109
theorems etc.\ that are to be \emph{declared} or \emph{defined} (so qualified
8548
wenzelm
parents: 8532
diff changeset
   110
identifiers are excluded here).  Quoted strings provide an escape for
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   111
non-identifier names or those ruled out by outer syntax keywords (e.g.\ 
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   112
\verb|"let"|).  Already existing objects are usually referenced by
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   113
\railqtoken{nameref}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   114
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   115
\indexoutertoken{name}\indexoutertoken{parname}\indexoutertoken{nameref}
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   116
\indexoutertoken{int}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   117
\begin{rail}
8145
cdd5386eb6fe 'name' syntax includes numbers;
wenzelm
parents: 8102
diff changeset
   118
  name: ident | symident | string | nat
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   119
  ;
7167
wenzelm
parents: 7141
diff changeset
   120
  parname: '(' name ')'
7141
a67dde8820c0 even more stuff;
wenzelm
parents: 7135
diff changeset
   121
  ;
7167
wenzelm
parents: 7141
diff changeset
   122
  nameref: name | longident
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   123
  ;
9617
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   124
  int: nat | '-' nat
574ab125a03b index tokens;
wenzelm
parents: 9601
diff changeset
   125
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   126
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   127
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   128
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   129
\subsection{Comments}\label{sec:comments}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   130
7167
wenzelm
parents: 7141
diff changeset
   131
Large chunks of plain \railqtoken{text} are usually given
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   132
\railtoken{verbatim}, i.e.\ enclosed in \verb|{*|~\dots~\verb|*}|.  For
7175
wenzelm
parents: 7167
diff changeset
   133
convenience, any of the smaller text units conforming to \railqtoken{nameref}
8102
424f6e663977 comment: any number of texts;
wenzelm
parents: 7981
diff changeset
   134
are admitted as well.  Almost any of the Isar commands may be annotated by
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   135
marginal \railnonterm{comment} of the form \texttt{--} \railqtoken{text}.
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   136
Note that the latter kind of comment is actually part of the language, while
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   137
source level comments \verb|(*|~\dots~\verb|*)| are stripped at the lexical
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   138
level.  A few commands such as $\PROOFNAME$ admit additional markup with a
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   139
``level of interest'': \texttt{\%} followed by an optional number $n$ (default
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   140
$n = 1$) indicates that the respective part of the document becomes $n$ levels
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   141
more obscure; \texttt{\%\%} means that interest drops by $\infty$ --- abandon
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   142
every hope, who enter here.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   143
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   144
\indexoutertoken{text}\indexouternonterm{comment}\indexouternonterm{interest}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   145
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   146
  text: verbatim | nameref
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   147
  ;
8102
424f6e663977 comment: any number of texts;
wenzelm
parents: 7981
diff changeset
   148
  comment: ('--' text +)
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   149
  ;
7167
wenzelm
parents: 7141
diff changeset
   150
  interest: percent nat? | ppercent
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   151
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   152
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   153
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   154
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   155
\subsection{Type classes, sorts and arities}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   156
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   157
Classes are specified by plain names.  Sorts have a very simple inner syntax,
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   158
which is either a single class name $c$ or a list $\{c@1, \dots, c@n\}$
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   159
referring to the intersection of these classes.  The syntax of type arities is
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   160
given directly at the outer level.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   161
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   162
\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
7135
wenzelm
parents: 7134
diff changeset
   163
\indexouternonterm{classdecl}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   164
\begin{rail}
7321
wenzelm
parents: 7319
diff changeset
   165
  classdecl: name ('<' (nameref + ','))?
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   166
  ;
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   167
  sort: nameref
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   168
  ;
7167
wenzelm
parents: 7141
diff changeset
   169
  arity: ('(' (sort + ',') ')')? sort
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   170
  ;
7167
wenzelm
parents: 7141
diff changeset
   171
  simplearity: ('(' (sort + ',') ')')? nameref
wenzelm
parents: 7141
diff changeset
   172
  ;
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   173
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   174
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   175
7167
wenzelm
parents: 7141
diff changeset
   176
\subsection{Types and terms}\label{sec:types-terms}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   177
7167
wenzelm
parents: 7141
diff changeset
   178
The actual inner Isabelle syntax, that of types and terms of the logic, is far
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   179
too sophisticated in order to be modelled explicitly at the outer theory
8548
wenzelm
parents: 8532
diff changeset
   180
level.  Basically, any such entity has to be quoted to turn it into a single
wenzelm
parents: 8532
diff changeset
   181
token (the parsing and type-checking is performed internally later).  For
wenzelm
parents: 8532
diff changeset
   182
convenience, a slightly more liberal convention is adopted: quotes may be
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   183
omitted for any type or term that is already \emph{atomic} at the outer level.
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   184
For example, one may write just \texttt{x} instead of \texttt{"x"}.  Note that
8548
wenzelm
parents: 8532
diff changeset
   185
symbolic identifiers (e.g.\ \texttt{++} or $\forall$) are available as well,
wenzelm
parents: 8532
diff changeset
   186
provided these are not superseded by commands or keywords (e.g.\ \texttt{+}).
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   187
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   188
\indexoutertoken{type}\indexoutertoken{term}\indexoutertoken{prop}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   189
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   190
  type: nameref | typefree | typevar
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   191
  ;
8593
68619606c5d1 fixed term syntax;
wenzelm
parents: 8548
diff changeset
   192
  term: nameref | var
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   193
  ;
7167
wenzelm
parents: 7141
diff changeset
   194
  prop: term
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   195
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   196
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   197
8690
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   198
Positional instantiations are indicated by giving a sequence of terms, or the
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   199
placeholder ``$\_$'' (underscore), which means to skip a position.
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   200
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   201
\indexoutertoken{inst}\indexoutertoken{insts}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   202
\begin{rail}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   203
  inst: underscore | term
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   204
  ;
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   205
  insts: (inst *)
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   206
  ;
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   207
\end{rail}
48786b52c8d8 added inst, insts;
wenzelm
parents: 8593
diff changeset
   208
7167
wenzelm
parents: 7141
diff changeset
   209
Type declarations and definitions usually refer to \railnonterm{typespec} on
wenzelm
parents: 7141
diff changeset
   210
the left-hand side.  This models basic type constructor application at the
wenzelm
parents: 7141
diff changeset
   211
outer syntax level.  Note that only plain postfix notation is available here,
wenzelm
parents: 7141
diff changeset
   212
but no infixes.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   213
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   214
\indexouternonterm{typespec}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   215
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   216
  typespec: (() | typefree | '(' ( typefree + ',' ) ')') name
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   217
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   218
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   219
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   220
7315
76a39a3784b5 checkpoint;
wenzelm
parents: 7175
diff changeset
   221
\subsection{Term patterns}\label{sec:term-pats}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   222
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   223
Assumptions and goal statements usually admit casual binding of schematic term
7981
wenzelm
parents: 7895
diff changeset
   224
variables by giving (optional) patterns of the form $\ISS{p@1\;\dots}{p@n}$.
7167
wenzelm
parents: 7141
diff changeset
   225
There are separate versions available for \railqtoken{term}s and
wenzelm
parents: 7141
diff changeset
   226
\railqtoken{prop}s.  The latter provides a $\CONCLNAME$ part with patterns
wenzelm
parents: 7141
diff changeset
   227
referring the (atomic) conclusion of a rule.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   228
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   229
\indexouternonterm{termpat}\indexouternonterm{proppat}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   230
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   231
  termpat: '(' ('is' term +) ')'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   232
  ;
7167
wenzelm
parents: 7141
diff changeset
   233
  proppat: '(' (('is' prop +) | 'concl' ('is' prop +) | ('is' prop +) 'concl' ('is' prop +)) ')'
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   234
  ;
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   235
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   236
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   237
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   238
\subsection{Mixfix annotations}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   239
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   240
Mixfix annotations specify concrete \emph{inner} syntax of Isabelle types and
8548
wenzelm
parents: 8532
diff changeset
   241
terms (see also \cite{isabelle-ref}).  Some commands such as $\TYPES$ (see
wenzelm
parents: 8532
diff changeset
   242
\S\ref{sec:types-pure}) admit infixes only, while $\CONSTS$ (see
wenzelm
parents: 8532
diff changeset
   243
\S\ref{sec:consts}) and $\isarkeyword{syntax}$ (see \S\ref{sec:syn-trans})
wenzelm
parents: 8532
diff changeset
   244
support the full range of general mixfixes and binders.
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   245
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   246
\indexouternonterm{infix}\indexouternonterm{mixfix}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   247
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   248
  infix: '(' ('infixl' | 'infixr') string? nat ')'
wenzelm
parents: 7141
diff changeset
   249
  ;
7175
wenzelm
parents: 7167
diff changeset
   250
  mixfix: infix | '(' string prios? nat? ')' | '(' 'binder' string prios? nat ')'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   251
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   252
7175
wenzelm
parents: 7167
diff changeset
   253
  prios: '[' (nat + ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   254
  ;
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   255
\end{rail}
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   256
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   257
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   258
\subsection{Attributes and theorems}\label{sec:syn-att}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   259
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   260
Attributes (and proof methods, see \S\ref{sec:syn-meth}) have their own
7335
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   261
``semi-inner'' syntax, in the sense that input conforming to
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   262
\railnonterm{args} below is parsed by the attribute a second time.  The
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   263
attribute argument specifications may be any sequence of atomic entities
abba35b98892 draft release;
wenzelm
parents: 7321
diff changeset
   264
(identifiers, strings etc.), or properly bracketed argument lists.  Below
7981
wenzelm
parents: 7895
diff changeset
   265
\railqtoken{atom} refers to any atomic entity, including any
wenzelm
parents: 7895
diff changeset
   266
\railtoken{keyword} conforming to \railtoken{symident}.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   267
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   268
\indexoutertoken{atom}\indexouternonterm{args}\indexouternonterm{attributes}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   269
\begin{rail}
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   270
  atom: nameref | typefree | typevar | var | nat | keyword
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   271
  ;
8896
c80aba8c1d5e replaced {{ }} by { };
wenzelm
parents: 8690
diff changeset
   272
  arg: atom | '(' args ')' | '[' args ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   273
  ;
7167
wenzelm
parents: 7141
diff changeset
   274
  args: arg *
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   275
  ;
7167
wenzelm
parents: 7141
diff changeset
   276
  attributes: '[' (nameref args * ',') ']'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   277
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   278
\end{rail}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   279
7895
7c492d8bc8e3 updated;
wenzelm
parents: 7466
diff changeset
   280
Theorem specifications come in several flavors: \railnonterm{axmdecl} and
7175
wenzelm
parents: 7167
diff changeset
   281
\railnonterm{thmdecl} usually refer to axioms, assumptions or results of goal
7981
wenzelm
parents: 7895
diff changeset
   282
statements, while \railnonterm{thmdef} collects lists of existing theorems.
wenzelm
parents: 7895
diff changeset
   283
Existing theorems are given by \railnonterm{thmref} and \railnonterm{thmrefs},
wenzelm
parents: 7895
diff changeset
   284
the former requires an actual singleton result.  Any of these theorem
7175
wenzelm
parents: 7167
diff changeset
   285
specifications may include lists of attributes both on the left and right hand
7466
7df66ce6508a updated;
wenzelm
parents: 7430
diff changeset
   286
sides; attributes are applied to any immediately preceding theorem.  If names
7981
wenzelm
parents: 7895
diff changeset
   287
are omitted, the theorems are not stored within the theorem database of the
wenzelm
parents: 7895
diff changeset
   288
theory or proof context; any given attributes are still applied, though.
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   289
7135
wenzelm
parents: 7134
diff changeset
   290
\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
wenzelm
parents: 7134
diff changeset
   291
\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   292
\begin{rail}
7167
wenzelm
parents: 7141
diff changeset
   293
  axmdecl: name attributes? ':'
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   294
  ;
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   295
  thmdecl: thmbind ':'
7135
wenzelm
parents: 7134
diff changeset
   296
  ;
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   297
  thmdef: thmbind '='
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   298
  ;
7175
wenzelm
parents: 7167
diff changeset
   299
  thmref: nameref attributes?
wenzelm
parents: 7167
diff changeset
   300
  ;
wenzelm
parents: 7167
diff changeset
   301
  thmrefs: thmref +
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   302
  ;
7167
wenzelm
parents: 7141
diff changeset
   303
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   304
  thmbind: name attributes | name | attributes
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   305
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   306
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   307
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   308
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   309
\subsection{Proof methods}\label{sec:syn-meth}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   310
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   311
Proof methods are either basic ones, or expressions composed of methods via
7175
wenzelm
parents: 7167
diff changeset
   312
``\texttt{,}'' (sequential composition), ``\texttt{|}'' (alternative choices),
7981
wenzelm
parents: 7895
diff changeset
   313
``\texttt{?}'' (try), ``\texttt{+}'' (repeat at least once).  In practice,
wenzelm
parents: 7895
diff changeset
   314
proof methods are usually just a comma separated list of
wenzelm
parents: 7895
diff changeset
   315
\railqtoken{nameref}~\railnonterm{args} specifications.  Note that parentheses
wenzelm
parents: 7895
diff changeset
   316
may be dropped for single method specifications (with no arguments).
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   317
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   318
\indexouternonterm{method}
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   319
\begin{rail}
7430
6ea8cbf94118 removed "*" method combinator;
wenzelm
parents: 7335
diff changeset
   320
  method: (nameref | '(' methods ')') (() | '?' | '+')
7134
320b412e5800 more stuff;
wenzelm
parents: 7050
diff changeset
   321
  ;
7167
wenzelm
parents: 7141
diff changeset
   322
  methods: (nameref args | method) + (',' | '|')
7050
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   323
  ;
c70d3402fef5 checkpoint;
wenzelm
parents: 7046
diff changeset
   324
\end{rail}
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   325
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   326
Proper use of Isar proof methods does \emph{not} involve goal addressing.
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   327
Nevertheless, specifying goal ranges may occasionally come in handy in
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   328
emulating tactic scripts.  Note that $[n-]$ refers to all goals, starting from
8548
wenzelm
parents: 8532
diff changeset
   329
$n$.  All goals may be specified by $[!]$, which is the same as $[1-]$.
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   330
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   331
\indexouternonterm{goalspec}
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   332
\begin{rail}
8548
wenzelm
parents: 8532
diff changeset
   333
  goalspec: '[' (nat '-' nat | nat '-' | nat | '!' ) ']'
8532
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   334
  ;
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   335
\end{rail}
46bb6a4b3ac9 goalspec;
wenzelm
parents: 8378
diff changeset
   336
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   337
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   338
\subsection{Antiquotations}\label{sec:antiq}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   339
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   340
\begin{matharray}{rcl}
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   341
  thm & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   342
  prop & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   343
  term & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   344
  typ & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   345
  text & : & \isarantiq \\
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   346
  goals & : & \isarantiq \\
10351
770356c32ad9 added antiq. subgoals
nipkow
parents: 10336
diff changeset
   347
  subgoals & : & \isarantiq \\
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   348
\end{matharray}
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   349
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   350
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
   351
antiquotations of logical entities, such as theorems, terms and types, which
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   352
are to be presented in the final output produced by the Isabelle document
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   353
preparation system (see also \S\ref{sec:document-prep}).
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   354
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
   355
Thus embedding of
10160
wenzelm
parents: 10152
diff changeset
   356
\texttt{{\at}{\ttlbrace}term~[show_types]~"f(x)~=~a~+~x"{\ttrbrace}} within a
9601
69d2fb3dc4c6 updated command termination issue;
wenzelm
parents: 9234
diff changeset
   357
text block would cause
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   358
\isa{(f{\isasymColon}'a~{\isasymRightarrow}~'a)~(x{\isasymColon}'a)~=~(a{\isasymColon}'a)~+~x}
10160
wenzelm
parents: 10152
diff changeset
   359
to appear in the final {\LaTeX} document.  Also note that theorem
wenzelm
parents: 10152
diff changeset
   360
antiquotations may involve attributes as well.  For example,
wenzelm
parents: 10152
diff changeset
   361
\texttt{{\at}{\ttlbrace}thm~sym~[no_vars]{\ttrbrace}} would print the
wenzelm
parents: 10152
diff changeset
   362
statement where all schematic variables have been replaced by fixed ones,
wenzelm
parents: 10152
diff changeset
   363
which are better readable.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   364
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   365
\indexisarant{thm}\indexisarant{prop}\indexisarant{term}
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   366
\indexisarant{typ}\indexisarant{text}\indexisarant{goals}\indexisarant{subgoals}
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   367
\begin{rail}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   368
  atsign lbrace antiquotation rbrace
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   369
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   370
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   371
  antiquotation:
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   372
    'thm' options thmrefs |
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   373
    'prop' options prop |
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   374
    'term' options term |
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   375
    'typ' options type |
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   376
    'text' options name |
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   377
    'goals' options |
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   378
    'subgoals' options
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   379
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   380
  options: '[' (option * ',') ']'
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   381
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   382
  option: name | name '=' name
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   383
  ;
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   384
\end{rail}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   385
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   386
Note that the syntax of antiquotations may \emph{not} include source comments
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   387
\texttt{(*~\dots~*)} or verbatim text \verb|{*|~\dots~\verb|*}|.
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   388
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   389
\begin{descr}
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   390
\item [$\at\{thm~\vec a\}$] prints theorems $\vec a$. Note that attribute
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   391
  specifications may be included as well (see also \S\ref{sec:syn-att}); the
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   392
  $no_vars$ operation (see \S\ref{sec:misc-methods}) would be particularly
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   393
  useful to suppress printing of schematic variables.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   394
\item [$\at\{prop~\phi\}$] prints a well-typed proposition $\phi$.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   395
\item [$\at\{term~t\}$] prints a well-typed term $t$.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   396
\item [$\at\{typ~\tau\}$] prints a well-formed type $\tau$.
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   397
\item [$\at\{text~s\}$] prints uninterpreted source text $s$.  This is
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   398
  particularly useful to print portions of text according to the Isabelle
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   399
  {\LaTeX} output style, without demanding well-formedness (e.g.\ small pieces
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   400
  of terms that cannot be parsed or type-checked yet).
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   401
\item [$\at\{goals\}$] prints the current \emph{dynamic} goal state.  This is
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   402
  only for support of tactic-emulation scripts within Isar --- presentation of
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   403
  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
   404
  
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   405
  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
   406
  know what you are doing!
10355
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   407
\item [$\at\{subgoals\}$] behaves almost like $goals$, except that it does not
aef4f587a0e4 improved doc of "subgoals" antiquotation;
wenzelm
parents: 10351
diff changeset
   408
  print the main goal.
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   409
\end{descr}
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   410
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   411
\medskip
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   412
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   413
The following options are available to tune the output.  Note that most of
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   414
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
   415
\begin{descr}
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   416
\item[$show_types = bool$ and $show_sorts = bool$] control printing of
9234
0013b2aa98dd IGNORE last log message!
wenzelm
parents: 9233
diff changeset
   417
  explicit type and sort constraints.
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   418
\item[$long_names = bool$] forces names of types and constants etc.\ to be
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   419
  printed in their fully qualified internal form.
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   420
\item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   421
\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
   422
  ``display material'', rather than a small piece of text without line breaks
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   423
  (which is the default).
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   424
\item[$quotes = bool$] indicates if the output should be enclosed in double
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   425
  quotes.
9233
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   426
\item[$mode = name$] adds $name$ to the print mode to be used for presentation
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   427
  (see also \cite{isabelle-ref}).  Note that the standard setup for {\LaTeX}
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   428
  output is already present by default, including the modes ``$latex$'',
8c8399b9ecaa removed "help";
wenzelm
parents: 9200
diff changeset
   429
  ``$xsymbols$'', ``$symbols$''.
9728
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   430
\item[$margin = nat$ and $indent = nat$] change the margin or indentation for
1546ad1c7839 added antiquotation 'name' and option 'indent';
wenzelm
parents: 9617
diff changeset
   431
  pretty printing of display material.
9752
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   432
\item[$source = bool$] prints the source text of the antiquotation arguments,
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   433
  rather than the actual value.  Note that this does not affect
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   434
  well-formedness checks of $thm$, $term$, etc. (only the $text$ antiquotation
a09f4a7accea renamed antiquotation 'name' to 'text';
wenzelm
parents: 9728
diff changeset
   435
  admits arbitrary output).
10319
02463775cafb added antiquotation "goals" and option "goals_limit";
wenzelm
parents: 10160
diff changeset
   436
\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
   437
  printed.
9200
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   438
\end{descr}
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   439
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   440
For boolean flags, ``$name = true$'' may be abbreviated as ``$name$''.  All of
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   441
the above flags are disabled by default, unless changed from ML.
3a44c828be1d syntax: renamed 'thmname' to 'thmbind';
wenzelm
parents: 9051
diff changeset
   442
10336
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   443
\medskip Note that antiquotations do not only spare the author from tedious
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   444
typing, but also achieve some degree of consistency-checking of informal
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   445
explanations with formal developments, since well-formedness of terms and
209f502b55f7 improved antiquotations;
wenzelm
parents: 10319
diff changeset
   446
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
   447
7046
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   448
%%% Local Variables: 
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   449
%%% mode: latex
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   450
%%% TeX-master: "isar-ref"
9f755ff43cff skeleton only;
wenzelm
parents:
diff changeset
   451
%%% End: