doc-src/Ref/defining.tex
author wenzelm
Mon, 05 May 2008 15:23:59 +0200
changeset 26783 1651ff6a34b5
parent 20093 164a42b7385f
child 30184 37969710e61f
permissions -rw-r--r--
added isasymIN/STRUCTURE;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     1
%% $Id$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     2
\chapter{Defining Logics} \label{Defining-Logics}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     3
This chapter explains how to define new formal systems --- in particular,
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     4
their concrete syntax.  While Isabelle can be regarded as a theorem prover
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     5
for set theory, higher-order logic or the sequent calculus, its
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     6
distinguishing feature is support for the definition of new logics.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     7
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
     8
Isabelle logics are hierarchies of theories, which are described and
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
     9
illustrated in
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    10
\iflabelundefined{sec:defining-theories}{{\em Introduction to Isabelle}}%
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    11
{\S\ref{sec:defining-theories}}.  That material, together with the theory
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    12
files provided in the examples directories, should suffice for all simple
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    13
applications.  The easiest way to define a new theory is by modifying a
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    14
copy of an existing theory.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    15
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    16
This chapter documents the meta-logic syntax, mixfix declarations and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    17
pretty printing.  The extended examples in \S\ref{sec:min_logics}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    18
demonstrate the logical aspects of the definition of theories.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    19
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    20
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    21
\section{Priority grammars} \label{sec:priority_grammars}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    22
\index{priority grammars|(}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    23
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    24
A context-free grammar contains a set of {\bf nonterminal symbols}, a set of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    25
{\bf terminal symbols} and a set of {\bf productions}\index{productions}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    26
Productions have the form ${A=\gamma}$, where $A$ is a nonterminal and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    27
$\gamma$ is a string of terminals and nonterminals.  One designated
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    28
nonterminal is called the {\bf start symbol}.  The language defined by the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    29
grammar consists of all strings of terminals that can be derived from the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    30
start symbol by applying productions as rewrite rules.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    31
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    32
The syntax of an Isabelle logic is specified by a {\bf priority
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    33
  grammar}.\index{priorities} Each nonterminal is decorated by an integer
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    34
priority, as in~$A^{(p)}$.  A nonterminal $A^{(p)}$ in a derivation may be
14231
6d8b6eb8623b Fixed spelling error.
skalberg
parents: 12465
diff changeset
    35
rewritten using a production $A^{(q)} = \gamma$ only if~$p \leq q$.  Any
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    36
priority grammar can be translated into a normal context free grammar by
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    37
introducing new nonterminals and productions.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    38
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    39
Formally, a set of context free productions $G$ induces a derivation
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    40
relation $\longrightarrow@G$.  Let $\alpha$ and $\beta$ denote strings of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    41
terminal or nonterminal symbols.  Then
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    42
\[ \alpha\, A^{(p)}\, \beta ~\longrightarrow@G~ \alpha\,\gamma\,\beta \]
14231
6d8b6eb8623b Fixed spelling error.
skalberg
parents: 12465
diff changeset
    43
if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \leq q$.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    44
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    45
The following simple grammar for arithmetic expressions demonstrates how
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    46
binding power and associativity of operators can be enforced by priorities.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    47
\begin{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    48
\begin{tabular}{rclr}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    49
  $A^{(9)}$ & = & {\tt0} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    50
  $A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    51
  $A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    52
  $A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    53
  $A^{(3)}$ & = & {\tt-} $A^{(3)}$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    54
\end{tabular}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    55
\end{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    56
The choice of priorities determines that {\tt -} binds tighter than {\tt *},
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    57
which binds tighter than {\tt +}.  Furthermore {\tt +} associates to the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    58
left and {\tt *} to the right.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    59
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    60
For clarity, grammars obey these conventions:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    61
\begin{itemize}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    62
\item All priorities must lie between~0 and \ttindex{max_pri}, which is a
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    63
  some fixed integer.  Sometimes {\tt max_pri} is written as $\infty$.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    64
\item Priority 0 on the right-hand side and priority \ttindex{max_pri} on
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    65
  the left-hand side may be omitted.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    66
\item The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$; the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    67
  priority of the left-hand side actually appears in a column on the far
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    68
  right.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    69
\item Alternatives are separated by~$|$.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    70
\item Repetition is indicated by dots~(\dots) in an informal but obvious
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    71
  way.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    72
\end{itemize}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    73
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    74
Using these conventions and assuming $\infty=9$, the grammar
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    75
takes the form
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    76
\begin{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    77
\begin{tabular}{rclc}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    78
$A$ & = & {\tt0} & \hspace*{4em} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    79
 & $|$ & {\tt(} $A$ {\tt)} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    80
 & $|$ & $A$ {\tt+} $A^{(1)}$ & (0) \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    81
 & $|$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    82
 & $|$ & {\tt-} $A^{(3)}$ & (3)
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    83
\end{tabular}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    84
\end{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    85
\index{priority grammars|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    86
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    87
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4543
diff changeset
    88
\begin{figure}\small
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    89
\begin{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    90
\begin{tabular}{rclc}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
    91
$any$ &=& $prop$ ~~$|$~~ $logic$ \\\\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    92
$prop$ &=& {\tt(} $prop$ {\tt)} \\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    93
     &$|$& $prop^{(4)}$ {\tt::} $type$ & (3) \\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    94
     &$|$& {\tt PROP} $aprop$ \\
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
    95
     &$|$& $any^{(3)}$ {\tt ==} $any^{(2)}$ & (2) \\
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
    96
     &$|$& $any^{(3)}$ {\tt =?=} $any^{(2)}$ & (2) \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    97
     &$|$& $prop^{(2)}$ {\tt ==>} $prop^{(1)}$ & (1) \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    98
     &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop^{(1)}$ & (1) \\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
    99
     &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   100
     &$|$& {\tt OFCLASS} {\tt(} $type$ {\tt,} $logic$ {\tt)} \\\\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   101
$aprop$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   102
    ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\\\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   103
$logic$ &=& {\tt(} $logic$ {\tt)} \\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   104
      &$|$& $logic^{(4)}$ {\tt::} $type$ & (3) \\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   105
      &$|$& $id$ ~~$|$~~ $longid$ ~~$|$~~ $var$
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   106
    ~~$|$~~ $logic^{(\infty)}$ {\tt(} $any$ {\tt,} \dots {\tt,} $any$ {\tt)} \\
11621
a19bc891e4bf Added TYPE to Pure grammar.
berghofe
parents: 8136
diff changeset
   107
      &$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\
a19bc891e4bf Added TYPE to Pure grammar.
berghofe
parents: 8136
diff changeset
   108
      &$|$& {\tt TYPE} {\tt(} $type$ {\tt)} \\\\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   109
$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   110
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   111
    &$|$& $id$ {\tt ::} $type$ & (0) \\\\
3694
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   112
$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   113
$pttrn$ &=& $idt$ \\\\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   114
$type$ &=& {\tt(} $type$ {\tt)} \\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   115
     &$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   116
       ~~$|$~~ $tvar$ {\tt::} $sort$ \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   117
     &$|$& $id$ ~~$|$~~ $type^{(\infty)}$ $id$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   118
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   119
     &$|$& $longid$ ~~$|$~~ $type^{(\infty)}$ $longid$
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   120
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $longid$ \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   121
     &$|$& $type^{(1)}$ {\tt =>} $type$ & (0) \\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   122
     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0) \\\\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   123
$sort$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ {\tt\ttlbrace\ttrbrace} ~~$|$~~
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 6592
diff changeset
   124
  {\tt\ttlbrace} $id$ ~$|$~ $longid${\tt,}\dots{\tt,} $id$ ~$|$~$longid$ {\tt\ttrbrace}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   125
\end{tabular}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   126
\index{*PROP symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   127
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   128
\index{*:: symbol}\index{*=> symbol}
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   129
\index{sort constraints}
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   130
%the index command: a percent is permitted, but braces must match!
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   131
\index{%@{\tt\%} symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   132
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   133
\index{*[ symbol}\index{*] symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   134
\index{*"!"! symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   135
\index{*"["| symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   136
\index{*"|"] symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   137
\end{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   138
\caption{Meta-logic syntax}\label{fig:pure_gram}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   139
\end{figure}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   140
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   141
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   142
\section{The Pure syntax} \label{sec:basic_syntax}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   143
\index{syntax!Pure|(}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   144
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   145
At the root of all object-logics lies the theory \thydx{Pure}.  It
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   146
contains, among many other things, the Pure syntax.  An informal account of
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   147
this basic syntax (types, terms and formulae) appears in
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   148
\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}%
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   149
{\S\ref{sec:forward}}.  A more precise description using a priority grammar
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   150
appears in Fig.\ts\ref{fig:pure_gram}.  It defines the following
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   151
nonterminals:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   152
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   153
  \item[\ndxbold{any}] denotes any term.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   154
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   155
  \item[\ndxbold{prop}] denotes terms of type {\tt prop}.  These are formulae
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   156
    of the meta-logic.  Note that user constants of result type {\tt prop}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   157
    (i.e.\ $c :: \ldots \To prop$) should always provide concrete syntax.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   158
    Otherwise atomic propositions with head $c$ may be printed incorrectly.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   159
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   160
  \item[\ndxbold{aprop}] denotes atomic propositions.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   161
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   162
%% FIXME huh!?
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   163
%  These typically
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   164
%  include the judgement forms of the object-logic; its definition
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   165
%  introduces a meta-level predicate for each judgement form.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   166
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   167
  \item[\ndxbold{logic}] denotes terms whose type belongs to class
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   168
    \cldx{logic}, excluding type \tydx{prop}.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   169
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   170
  \item[\ndxbold{idts}] denotes a list of identifiers, possibly constrained
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   171
    by types.
3694
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   172
    
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   173
  \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   174
    abstraction, cases etc.  Initially the same as $idt$ and $idts$,
14231
6d8b6eb8623b Fixed spelling error.
skalberg
parents: 12465
diff changeset
   175
    these are intended to be augmented by user extensions.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   176
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   177
  \item[\ndxbold{type}] denotes types of the meta-logic.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   178
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   179
  \item[\ndxbold{sort}] denotes meta-level sorts.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   180
\end{ttdescription}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   181
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   182
\begin{warn}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   183
  In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|,
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   184
  treating {\tt y} like a type constructor applied to {\tt nat}.  The
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   185
  likely result is an error message.  To avoid this interpretation, use
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   186
  parentheses and write \verb|(x::nat) y|.
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   187
  \index{type constraints}\index{*:: symbol}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   188
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   189
  Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   190
  yields an error.  The correct form is \verb|(x::nat) (y::nat)|.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   191
\end{warn}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   192
452
395bbf6e55f9 changed priority of ::
nipkow
parents: 332
diff changeset
   193
\begin{warn}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   194
  Type constraints bind very weakly.  For example, \verb!x<y::nat! is normally
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   195
  parsed as \verb!(x<y)::nat!, unless \verb$<$ has priority of 3 or less, in
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   196
  which case the string is likely to be ambiguous.  The correct form is
452
395bbf6e55f9 changed priority of ::
nipkow
parents: 332
diff changeset
   197
  \verb!x<(y::nat)!.
395bbf6e55f9 changed priority of ::
nipkow
parents: 332
diff changeset
   198
\end{warn}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   199
867
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   200
\subsection{Logical types and default syntax}\label{logical-types}
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   201
\index{lambda calc@$\lambda$-calculus}
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   202
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   203
Isabelle's representation of mathematical languages is based on the
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   204
simply typed $\lambda$-calculus.  All logical types, namely those of
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   205
class \cldx{logic}, are automatically equipped with a basic syntax of
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   206
types, identifiers, variables, parentheses, $\lambda$-abstraction and
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   207
application.
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   208
\begin{warn}
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   209
  Isabelle combines the syntaxes for all types of class \cldx{logic} by
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   210
  mapping all those types to the single nonterminal $logic$.  Thus all
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   211
  productions of $logic$, in particular $id$, $var$ etc, become available.
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   212
\end{warn}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   213
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   214
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   215
\subsection{Lexical matters}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   216
The parser does not process input strings directly.  It operates on token
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   217
lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   218
tokens: \bfindex{delimiters} and \bfindex{name tokens}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   219
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   220
\index{reserved words}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   221
Delimiters can be regarded as reserved words of the syntax.  You can
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   222
add new ones when extending theories.  In Fig.\ts\ref{fig:pure_gram} they
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   223
appear in typewriter font, for example {\tt ==}, {\tt =?=} and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   224
{\tt PROP}\@.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   225
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   226
Name tokens have a predefined syntax.  The lexer distinguishes six disjoint
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   227
classes of names: \rmindex{identifiers}, \rmindex{unknowns}, type
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   228
identifiers\index{type identifiers}, type unknowns\index{type unknowns},
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   229
\rmindex{numerals}, \rmindex{strings}.  They are denoted by \ndxbold{id},
14948
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   230
\ndxbold{var}, \ndxbold{tid}, \ndxbold{tvar}, \ndxbold{num}, \ndxbold{xnum},
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   231
\ndxbold{xstr}, respectively.  Typical examples are {\tt x}, {\tt ?x7}, {\tt
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   232
  'a}, {\tt ?'a3}, {\tt \#42}, {\tt ''foo bar''}.  Here is the precise syntax:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   233
\begin{eqnarray*}
14955
wenzelm
parents: 14948
diff changeset
   234
id        & =   & letter\,quasiletter^* \\
wenzelm
parents: 14948
diff changeset
   235
longid    & =   & id (\mbox{\tt .}id)^+ \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   236
var       & =   & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   237
tid       & =   & \mbox{\tt '}id \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   238
tvar      & =   & \mbox{\tt ?}tid ~~|~~
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   239
                  \mbox{\tt ?}tid\mbox{\tt .}nat \\
20093
164a42b7385f num/xnum: bin or hex;
wenzelm
parents: 14960
diff changeset
   240
num       & =   & nat ~~|~~ \mbox{\tt-}nat ~~|~~ \verb,0x,\,hex^+ ~~|~~ \verb,0b,\,bin^+ \\
164a42b7385f num/xnum: bin or hex;
wenzelm
parents: 14960
diff changeset
   241
xnum      & =   & \mbox{\tt \#}num \\
14955
wenzelm
parents: 14948
diff changeset
   242
xstr      & =   & \mbox{\tt ''~\dots~\tt ''} \\[1ex]
14960
wenzelm
parents: 14955
diff changeset
   243
letter & = & latin ~|~ \verb,\<,latin\verb,>, ~|~ \verb,\<,latin\,latin\verb,>, ~|~ greek ~| \\
wenzelm
parents: 14955
diff changeset
   244
      &   & \verb,\<^isub>, ~|~ \verb,\<^isup>, \\
wenzelm
parents: 14955
diff changeset
   245
quasiletter & = & letter ~|~ digit ~|~ \verb,_, ~|~ \verb,', \\
14948
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   246
latin & = & \verb,a, ~|~ \dots ~|~ \verb,z, ~|~ \verb,A, ~|~ \dots ~|~ \verb,Z, \\
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   247
digit & = & \verb,0, ~|~ \dots ~|~ \verb,9, \\
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   248
nat & = & digit^+ \\
20093
164a42b7385f num/xnum: bin or hex;
wenzelm
parents: 14960
diff changeset
   249
bin & = & \verb,0, ~|~ \verb,1, \\
164a42b7385f num/xnum: bin or hex;
wenzelm
parents: 14960
diff changeset
   250
hex & = & digit  ~|~  \verb,a, ~|~ \dots ~|~ \verb,f, ~|~ \verb,A, ~|~ \dots ~|~ \verb,F, \\
14955
wenzelm
parents: 14948
diff changeset
   251
greek & = & \verb,\<alpha>, ~|~ \verb,\<beta>, ~|~ \verb,\<gamma>, ~|~ \verb,\<delta>, ~| \\
wenzelm
parents: 14948
diff changeset
   252
      &   & \verb,\<epsilon>, ~|~ \verb,\<zeta>, ~|~ \verb,\<eta>, ~|~ \verb,\<theta>, ~| \\
wenzelm
parents: 14948
diff changeset
   253
      &   & \verb,\<iota>, ~|~ \verb,\<kappa>, ~|~ \verb,\<mu>, ~|~ \verb,\<nu>, ~| \\
wenzelm
parents: 14948
diff changeset
   254
      &   & \verb,\<xi>, ~|~ \verb,\<pi>, ~|~ \verb,\<rho>, ~|~ \verb,\<sigma>, ~| \\
wenzelm
parents: 14948
diff changeset
   255
      &   & \verb,\<tau>, ~|~ \verb,\<upsilon>, ~|~ \verb,\<phi>, ~|~ \verb,\<psi>, ~| \\
wenzelm
parents: 14948
diff changeset
   256
      &   & \verb,\<omega>, ~|~ \verb,\<Gamma>, ~|~ \verb,\<Delta>, ~|~ \verb,\<Theta>, ~| \\
wenzelm
parents: 14948
diff changeset
   257
      &   & \verb,\<Lambda>, ~|~ \verb,\<Xi>, ~|~ \verb,\<Pi>, ~|~ \verb,\<Sigma>, ~| \\
wenzelm
parents: 14948
diff changeset
   258
      &   & \verb,\<Upsilon>, ~|~ \verb,\<Phi>, ~|~ \verb,\<Psi>, ~|~ \verb,\<Omega>, \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   259
\end{eqnarray*}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   260
The lexer repeatedly takes the longest prefix of the input string that
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   261
forms a valid token.  A maximal prefix that is both a delimiter and a
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   262
name is treated as a delimiter.  Spaces, tabs, newlines and formfeeds
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   263
are separators; they never occur within tokens, except those of class
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   264
$xstr$.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   265
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   266
\medskip
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   267
Delimiters need not be separated by white space.  For example, if {\tt -}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   268
is a delimiter but {\tt --} is not, then the string {\tt --} is treated as
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   269
two consecutive occurrences of the token~{\tt -}.  In contrast, \ML\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   270
treats {\tt --} as a single symbolic name.  The consequence of Isabelle's
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   271
more liberal scheme is that the same string may be parsed in different ways
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   272
after extending the syntax: after adding {\tt --} as a delimiter, the input
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   273
{\tt --} is treated as a single token.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   274
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   275
A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   276
a pair of base name and index (\ML\ type \mltydx{indexname}).  These
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   277
components are either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   278
run together as in {\tt ?x1}.  The latter form is possible if the base name
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   279
does not end with digits.  If the index is 0, it may be dropped altogether:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   280
{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   281
14948
aa6d54648b32 tuned lexical syntax;
wenzelm
parents: 14893
diff changeset
   282
Tokens of class $num$, $xnum$ or $xstr$ are not used by the meta-logic.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   283
Object-logics may provide numerals and string constants by adding appropriate
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   284
productions and translation functions.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   285
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   286
\medskip
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   287
Although name tokens are returned from the lexer rather than the parser, it
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   288
is more logical to regard them as nonterminals.  Delimiters, however, are
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   289
terminals; they are just syntactic sugar and contribute nothing to the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   290
abstract syntax tree.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   291
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   292
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   293
\subsection{*Inspecting the syntax} \label{pg:print_syn}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   294
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   295
syn_of              : theory -> Syntax.syntax
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   296
print_syntax        : theory -> unit
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   297
Syntax.print_syntax : Syntax.syntax -> unit
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   298
Syntax.print_gram   : Syntax.syntax -> unit
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   299
Syntax.print_trans  : Syntax.syntax -> unit
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   300
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   301
The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   302
in \ML.  You can display values of this type by calling the following
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   303
functions:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   304
\begin{ttdescription}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   305
\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   306
  theory~{\it thy} as an \ML\ value.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   307
8136
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 6592
diff changeset
   308
\item[\ttindexbold{print_syntax} $thy$] uses {\tt Syntax.print_syntax}
8c65f3ca13f2 fixed many bad line & page breaks
paulson
parents: 6592
diff changeset
   309
 to display the syntax part of theory $thy$.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   310
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   311
\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   312
  information contained in the syntax {\it syn}.  The displayed output can
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   313
  be large.  The following two functions are more selective.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   314
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   315
\item[\ttindexbold{Syntax.print_gram} {\it syn}] shows the grammar part
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   316
  of~{\it syn}, namely the lexicon, logical types and productions.  These are
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   317
  discussed below.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   318
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   319
\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   320
  part of~{\it syn}, namely the constants, parse/print macros and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   321
  parse/print translations.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   322
\end{ttdescription}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   323
12465
wenzelm
parents: 11621
diff changeset
   324
The output of the above print functions is divided into labelled sections.
wenzelm
parents: 11621
diff changeset
   325
The grammar is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}.
wenzelm
parents: 11621
diff changeset
   326
The rest refers to syntactic translations and macro expansion.  Here is an
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   327
explanation of the various sections.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   328
\begin{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   329
  \item[{\tt lexicon}] lists the delimiters used for lexical
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   330
    analysis.\index{delimiters}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   331
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   332
  \item[{\tt logtypes}] lists the types that are regarded the same as {\tt
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   333
    logic} syntactically.  Thus types of object-logics (e.g.\ {\tt nat}, say)
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   334
    will be automatically equipped with the standard syntax of
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   335
    $\lambda$-calculus.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   336
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   337
  \item[{\tt prods}] lists the \rmindex{productions} of the priority grammar.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   338
    The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   339
    Each delimiter is quoted.  Some productions are shown with {\tt =>} and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   340
    an attached string.  These strings later become the heads of parse
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   341
    trees; they also play a vital role when terms are printed (see
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   342
    \S\ref{sec:asts}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   343
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   344
    Productions with no strings attached are called {\bf copy
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   345
      productions}\indexbold{productions!copy}.  Their right-hand side must
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   346
    have exactly one nonterminal symbol (or name token).  The parser does
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   347
    not create a new parse tree node for copy productions, but simply
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   348
    returns the parse tree of the right-hand symbol.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   349
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   350
    If the right-hand side consists of a single nonterminal with no
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   351
    delimiters, then the copy production is called a {\bf chain
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   352
      production}.  Chain productions act as abbreviations:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   353
    conceptually, they are removed from the grammar by adding new
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   354
    productions.  Priority information attached to chain productions is
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   355
    ignored; only the dummy value $-1$ is displayed.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   356
    
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   357
  \item[\ttindex{print_modes}] lists the alternative print modes
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   358
    provided by this syntax (see \S\ref{sec:prmodes}).
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   359
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   360
  \item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}]
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   361
    relate to macros (see \S\ref{sec:macros}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   362
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   363
  \item[{\tt parse_ast_translation}, {\tt print_ast_translation}]
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   364
    list sets of constants that invoke translation functions for abstract
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   365
    syntax trees.  Section \S\ref{sec:asts} below discusses this obscure
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   366
    matter.\index{constants!for translations}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   367
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4543
diff changeset
   368
  \item[{\tt parse_translation}, {\tt print_translation}] list the sets
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   369
    of constants that invoke translation functions for terms (see
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   370
    \S\ref{sec:tr_funs}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   371
\end{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   372
\index{syntax!Pure|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   373
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   374
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   375
\section{Mixfix declarations} \label{sec:mixfix}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   376
\index{mixfix declarations|(}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   377
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   378
When defining a theory, you declare new constants by giving their names,
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   379
their type, and an optional {\bf mixfix annotation}.  Mixfix annotations
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   380
allow you to extend Isabelle's basic $\lambda$-calculus syntax with
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   381
readable notation.  They can express any context-free priority grammar.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   382
Isabelle syntax definitions are inspired by \OBJ~\cite{OBJ}; they are more
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   383
general than the priority declarations of \ML\ and Prolog.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   384
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   385
A mixfix annotation defines a production of the priority grammar.  It
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   386
describes the concrete syntax, the translation to abstract syntax, and the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   387
pretty printing.  Special case annotations provide a simple means of
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   388
specifying infix operators and binders.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   389
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   390
\subsection{The general mixfix form}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   391
Here is a detailed account of mixfix declarations.  Suppose the following
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   392
line occurs within a {\tt consts} or {\tt syntax} section of a {\tt .thy}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   393
file:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   394
\begin{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   395
  {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   396
\end{center}
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   397
This constant declaration and mixfix annotation are interpreted as follows:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   398
\begin{itemize}\index{productions}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   399
\item The string {\tt $c$} is the name of the constant associated with the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   400
  production; unless it is a valid identifier, it must be enclosed in
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   401
  quotes.  If $c$ is empty (given as~{\tt ""}) then this is a copy
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   402
  production.\index{productions!copy} Otherwise, parsing an instance of the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   403
  phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   404
    $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   405
  argument.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   406
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   407
  \item The constant $c$, if non-empty, is declared to have type $\sigma$
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   408
    ({\tt consts} section only).
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   409
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   410
  \item The string $template$ specifies the right-hand side of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   411
    the production.  It has the form
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   412
    \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \]
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   413
    where each occurrence of {\tt_} denotes an argument position and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   414
    the~$w@i$ do not contain~{\tt _}.  (If you want a literal~{\tt _} in
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   415
    the concrete syntax, you must escape it as described below.)  The $w@i$
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   416
    may consist of \rmindex{delimiters}, spaces or
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   417
    \rmindex{pretty printing} annotations (see below).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   418
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   419
  \item The type $\sigma$ specifies the production's nonterminal symbols
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   420
    (or name tokens).  If $template$ is of the form above then $\sigma$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   421
    must be a function type with at least~$n$ argument positions, say
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   422
    $\sigma = [\tau@1, \dots, \tau@n] \To \tau$.  Nonterminal symbols are
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   423
    derived from the types $\tau@1$, \ldots,~$\tau@n$, $\tau$ as described
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   424
    below.  Any of these may be function types.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   425
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   426
  \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   427
      [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   428
    priority\indexbold{priorities} required of any phrase that may appear
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   429
    as the $i$-th argument.  Missing priorities default to~0.
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   430
    
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   431
  \item The integer $p$ is the priority of this production.  If
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   432
    omitted, it defaults to the maximal priority.  Priorities range
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   433
    between 0 and \ttindexbold{max_pri} (= 1000).
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   434
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   435
\end{itemize}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   436
%
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   437
The resulting production is \[ A^{(p)}= w@0\, A@1^{(p@1)}\, w@1\,
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   438
A@2^{(p@2)}\, \dots\, A@n^{(p@n)}\, w@n \] where $A$ and the $A@i$ are the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   439
nonterminals corresponding to the types $\tau$ and $\tau@i$ respectively.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   440
The nonterminal symbol associated with a type $(\ldots)ty$ is {\tt logic}, if
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   441
this is a logical type (namely one of class {\tt logic} excluding {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   442
prop}).  Otherwise it is $ty$ (note that only the outermost type constructor
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   443
is taken into account).  Finally, the nonterminal of a type variable is {\tt
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   444
any}.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   445
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   446
\begin{warn}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   447
  Theories must sometimes declare types for purely syntactic purposes ---
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   448
  merely playing the role of nonterminals.  One example is \tydx{type}, the
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   449
  built-in type of types.  This is a `type of all types' in the syntactic
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   450
  sense only.  Do not declare such types under {\tt arities} as belonging to
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   451
  class {\tt logic}\index{*logic class}, for that would make them useless as
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   452
  separate nonterminal symbols.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   453
\end{warn}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   454
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   455
Associating nonterminals with types allows a constant's type to specify
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   456
syntax as well.  We can declare the function~$f$ to have type $[\tau@1,
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   457
\ldots, \tau@n]\To \tau$ and, through a mixfix annotation, specify the layout
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   458
of the function's $n$ arguments.  The constant's name, in this case~$f$, will
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   459
also serve as the label in the abstract syntax tree.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   460
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   461
You may also declare mixfix syntax without adding constants to the theory's
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   462
signature, by using a {\tt syntax} section instead of {\tt consts}.  Thus a
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   463
production need not map directly to a logical function (this typically
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   464
requires additional syntactic translations, see also
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   465
Chapter~\ref{chap:syntax}).
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   466
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   467
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   468
\medskip
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   469
As a special case of the general mixfix declaration, the form
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   470
\begin{center}
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   471
  {\tt $c$ ::\ "$\sigma$" ("$template$")}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   472
\end{center}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   473
specifies no priorities.  The resulting production puts no priority
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   474
constraints on any of its arguments and has maximal priority itself.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   475
Omitting priorities in this manner is prone to syntactic ambiguities unless
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   476
the production's right-hand side is fully bracketed, as in
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   477
\verb|"if _ then _ else _ fi"|.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   478
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   479
Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   480
is sensible only if~$c$ is an identifier.  Otherwise you will be unable to
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   481
write terms involving~$c$.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   482
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   483
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   484
\subsection{Example: arithmetic expressions}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   485
\index{examples!of mixfix declarations}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   486
This theory specification contains a {\tt syntax} section with mixfix
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   487
declarations encoding the priority grammar from
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   488
\S\ref{sec:priority_grammars}:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   489
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   490
ExpSyntax = Pure +
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   491
types
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   492
  exp
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   493
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   494
  "0" :: exp                 ("0"      9)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   495
  "+" :: [exp, exp] => exp   ("_ + _"  [0, 1] 0)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   496
  "*" :: [exp, exp] => exp   ("_ * _"  [3, 2] 2)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   497
  "-" :: exp => exp          ("- _"    [3] 3)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   498
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   499
\end{ttbox}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   500
Executing {\tt Syntax.print_gram} reveals the productions derived from the
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   501
above mixfix declarations (lots of additional information deleted):
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   502
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   503
Syntax.print_gram (syn_of ExpSyntax.thy);
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   504
{\out exp = "0"  => "0" (9)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   505
{\out exp = exp[0] "+" exp[1]  => "+" (0)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   506
{\out exp = exp[3] "*" exp[2]  => "*" (2)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   507
{\out exp = "-" exp[3]  => "-" (3)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   508
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   509
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   510
Note that because {\tt exp} is not of class {\tt logic}, it has been
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   511
retained as a separate nonterminal.  This also entails that the syntax
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   512
does not provide for identifiers or paranthesized expressions.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   513
Normally you would also want to add the declaration {\tt arities
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   514
  exp::logic} after {\tt types} and use {\tt consts} instead of {\tt
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   515
  syntax}.  Try this as an exercise and study the changes in the
867
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   516
grammar.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   517
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   518
\subsection{The mixfix template}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   519
Let us now take a closer look at the string $template$ appearing in mixfix
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   520
annotations.  This string specifies a list of parsing and printing
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   521
directives: delimiters\index{delimiters}, arguments, spaces, blocks of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   522
indentation and line breaks.  These are encoded by the following character
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   523
sequences:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   524
\index{pretty printing|(}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   525
\begin{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   526
\item[~$d$~] is a delimiter, namely a non-empty sequence of characters
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   527
  other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   528
  Even these characters may appear if escaped; this means preceding it with
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   529
  a~{\tt '} (single quote).  Thus you have to write {\tt ''} if you really
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   530
  want a single quote.  Furthermore, a~{\tt '} followed by a space separates
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   531
  delimiters without extra white space being added for printing.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   532
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   533
\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   534
  or name token.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   535
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   536
\item[~$s$~] is a non-empty sequence of spaces for printing.  This and the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   537
  following specifications do not affect parsing at all.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   538
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   539
\item[~{\tt(}$n$~] opens a pretty printing block.  The optional number $n$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   540
  specifies how much indentation to add when a line break occurs within the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   541
  block.  If {\tt(} is not followed by digits, the indentation defaults
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   542
  to~0.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   543
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   544
\item[~{\tt)}~] closes a pretty printing block.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   545
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   546
\item[~{\tt//}~] forces a line break.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   547
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   548
\item[~{\tt/}$s$~] allows a line break.  Here $s$ stands for the string of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   549
  spaces (zero or more) right after the {\tt /} character.  These spaces
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   550
  are printed if the break is not taken.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   551
\end{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   552
For example, the template {\tt"(_ +/ _)"} specifies an infix operator.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   553
There are two argument positions; the delimiter~{\tt+} is preceded by a
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   554
space and followed by a space or line break; the entire phrase is a pretty
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   555
printing block.  Other examples appear in Fig.\ts\ref{fig:set_trans} below.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   556
Isabelle's pretty printer resembles the one described in
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 5542
diff changeset
   557
Paulson~\cite{paulson-ml2}.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   558
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   559
\index{pretty printing|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   560
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   561
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   562
\subsection{Infixes}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   563
\indexbold{infixes}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   564
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   565
Infix operators associating to the left or right can be declared using
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   566
{\tt infixl} or {\tt infixr}.  Basically, the form {\tt $c$ ::\ 
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   567
  $\sigma$ (infixl $p$)} abbreviates the mixfix declarations
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   568
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   569
"op \(c\)" :: \(\sigma\)   ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   570
"op \(c\)" :: \(\sigma\)   ("op \(c\)")
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   571
\end{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   572
and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   573
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   574
"op \(c\)" :: \(\sigma\)   ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   575
"op \(c\)" :: \(\sigma\)   ("op \(c\)")
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   576
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   577
The infix operator is declared as a constant with the prefix {\tt op}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   578
Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   579
function symbols, as in \ML.  Special characters occurring in~$c$ must be
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   580
escaped, as in delimiters, using a single quote.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   581
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   582
A slightly more general form of infix declarations allows constant
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   583
names to be independent from their concrete syntax, namely \texttt{$c$
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   584
  ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}.  As
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   585
an example consider:
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   586
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   587
and :: [bool, bool] => bool  (infixr "&" 35)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   588
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   589
The internal constant name will then be just \texttt{and}, without any
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   590
\texttt{op} prefixed.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   591
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   592
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   593
\subsection{Binders}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   594
\indexbold{binders}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   595
\begingroup
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   596
\def\Q{{\cal Q}}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   597
A {\bf binder} is a variable-binding construct such as a quantifier.  The
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   598
constant declaration
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   599
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   600
\(c\) :: \(\sigma\)   (binder "\(\Q\)" [\(pb\)] \(p\))
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   601
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   602
introduces a constant~$c$ of type~$\sigma$, which must have the form
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   603
$(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   604
$x$ is a bound variable of type~$\tau@1$, the body~$P$ has type $\tau@2$
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   605
and the whole term has type~$\tau@3$.  The optional integer $pb$
1060
a122584b5cc5 In binders, the default body priority is now p instead of 0.
lcp
parents: 911
diff changeset
   606
specifies the body's priority, by default~$p$.  Special characters
877
e528724951b0 added optional body priority to binder declaration
clasohm
parents: 867
diff changeset
   607
in $\Q$ must be escaped using a single quote.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   608
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   609
The declaration is expanded internally to something like
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   610
\begin{ttbox}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   611
\(c\)\hskip3pt    :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   612
"\(\Q\)"  :: [idts, \(\tau@2\)] => \(\tau@3\)   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   613
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   614
Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   615
\index{type constraints}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   616
optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   617
declaration also installs a parse translation\index{translations!parse}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   618
for~$\Q$ and a print translation\index{translations!print} for~$c$ to
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   619
translate between the internal and external forms.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   620
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   621
A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   622
list of variables.  The external form $\Q~x@1~x@2 \ldots x@n. P$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   623
corresponds to the internal form
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   624
\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \]
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   625
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   626
\medskip
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   627
For example, let us declare the quantifier~$\forall$:\index{quantifiers}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   628
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   629
All :: ('a => o) => o   (binder "ALL " 10)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   630
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   631
This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   632
  $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   633
back on ${\tt All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   634
  $x$.$P$} have type~$o$, the type of formulae, while the bound variable
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   635
can be polymorphic.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   636
\endgroup
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   637
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   638
\index{mixfix declarations|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   639
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   640
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   641
\section{*Alternative print modes} \label{sec:prmodes}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   642
\index{print modes|(}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   643
%
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   644
Isabelle's pretty printer supports alternative output syntaxes.  These
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   645
may be used independently or in cooperation.  The currently active
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   646
print modes (with precedence from left to right) are determined by a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   647
reference variable.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   648
\begin{ttbox}\index{*print_mode}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   649
print_mode: string list ref
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   650
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   651
Initially this may already contain some print mode identifiers,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   652
depending on how Isabelle has been invoked (e.g.\ by some user
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   653
interface).  So changes should be incremental --- adding or deleting
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   654
modes relative to the current value.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   655
12465
wenzelm
parents: 11621
diff changeset
   656
Any \ML{} string is a legal print mode identifier, without any predeclaration
wenzelm
parents: 11621
diff changeset
   657
required.  The following names should be considered reserved, though:
wenzelm
parents: 11621
diff changeset
   658
\texttt{""} (the empty string), \texttt{symbols}, \texttt{xsymbols}, and
wenzelm
parents: 11621
diff changeset
   659
\texttt{latex}.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   660
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   661
There is a separate table of mixfix productions for pretty printing
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   662
associated with each print mode.  The currently active ones are
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   663
conceptually just concatenated from left to right, with the standard
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   664
syntax output table always coming last as default.  Thus mixfix
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   665
productions of preceding modes in the list may override those of later
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   666
ones.  Also note that token translations are always relative to some
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   667
print mode (see \S\ref{sec:tok_tr}).
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   668
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   669
\medskip The canonical application of print modes is optional printing
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   670
of mathematical symbols from a special screen font instead of {\sc
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   671
  ascii}.  Another example is to re-use Isabelle's advanced
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   672
$\lambda$-term printing mechanisms to generate completely different
3228
41ad2d5077be index: model checkers;
wenzelm
parents: 3214
diff changeset
   673
output, say for interfacing external tools like \rmindex{model
41ad2d5077be index: model checkers;
wenzelm
parents: 3214
diff changeset
   674
  checkers} (see also \texttt{HOL/Modelcheck}).
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   675
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   676
\index{print modes|)}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   677
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   678
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   679
\section{Ambiguity of parsed expressions} \label{sec:ambiguity}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   680
\index{ambiguity!of parsed expressions}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   681
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   682
To keep the grammar small and allow common productions to be shared
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   683
all logical types (except {\tt prop}) are internally represented
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   684
by one nonterminal, namely {\tt logic}.  This and omitted or too freely
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   685
chosen priorities may lead to ways of parsing an expression that were
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   686
not intended by the theory's maker.  In most cases Isabelle is able to
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   687
select one of multiple parse trees that an expression has lead
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   688
to by checking which of them can be typed correctly.  But this may not
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   689
work in every case and always slows down parsing.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   690
The warning and error messages that can be produced during this process are
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   691
as follows:
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   692
880
667dc43e3b98 added documentation of Sign.ambiguity_level
clasohm
parents: 877
diff changeset
   693
If an ambiguity can be resolved by type inference the following
667dc43e3b98 added documentation of Sign.ambiguity_level
clasohm
parents: 877
diff changeset
   694
warning is shown to remind the user that parsing is (unnecessarily)
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   695
slowed down.  In cases where it's not easily possible to eliminate the
880
667dc43e3b98 added documentation of Sign.ambiguity_level
clasohm
parents: 877
diff changeset
   696
ambiguity the frequency of the warning can be controlled by changing
883
92abd2ad9d08 renamed Sign.ambiguity_level to Syntax.ambiguity_level
clasohm
parents: 880
diff changeset
   697
the value of {\tt Syntax.ambiguity_level} which has type {\tt int
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   698
ref}.  Its default value is 1 and by increasing it one can control how
883
92abd2ad9d08 renamed Sign.ambiguity_level to Syntax.ambiguity_level
clasohm
parents: 880
diff changeset
   699
many parse trees are necessary to generate the warning.
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   700
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   701
\begin{ttbox}
3801
5ba459e15dd7 tuned warning msg;
wenzelm
parents: 3694
diff changeset
   702
{\out Ambiguous input "\dots"}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   703
{\out produces the following parse trees:}
3801
5ba459e15dd7 tuned warning msg;
wenzelm
parents: 3694
diff changeset
   704
{\out \dots}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   705
{\out Fortunately, only one parse tree is type correct.}
3801
5ba459e15dd7 tuned warning msg;
wenzelm
parents: 3694
diff changeset
   706
{\out You may still want to disambiguate your grammar or your input.}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   707
\end{ttbox}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   708
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   709
The following message is normally caused by using the same
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   710
syntax in two different productions:
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   712
\begin{ttbox}
3802
wenzelm
parents: 3801
diff changeset
   713
{\out Ambiguous input "..."}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   714
{\out produces the following parse trees:}
3802
wenzelm
parents: 3801
diff changeset
   715
{\out \dots}
wenzelm
parents: 3801
diff changeset
   716
{\out More than one term is type correct:}
wenzelm
parents: 3801
diff changeset
   717
{\out \dots}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   718
\end{ttbox}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   719
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   720
Ambiguities occuring in syntax translation rules cannot be resolved by
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   721
type inference because it is not necessary for these rules to be type
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   722
correct.  Therefore Isabelle always generates an error message and the
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   723
ambiguity should be eliminated by changing the grammar or the rule.
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   724
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   725
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   726
\section{Example: some minimal logics} \label{sec:min_logics}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   727
\index{examples!of logic definitions}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   728
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   729
This section presents some examples that have a simple syntax.  They
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   730
demonstrate how to define new object-logics from scratch.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   731
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   732
First we must define how an object-logic syntax is embedded into the
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   733
meta-logic.  Since all theorems must conform to the syntax for~\ndx{prop}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   734
(see Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   735
object-level syntax.  Assume that the syntax of your object-logic defines a
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   736
meta-type~\tydx{o} of formulae which refers to the nonterminal {\tt logic}.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   737
These formulae can now appear in axioms and theorems wherever \ndx{prop} does
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   738
if you add the production
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   739
\[ prop ~=~ logic. \]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   740
This is not supposed to be a copy production but an implicit coercion from
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   741
formulae to propositions:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   742
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   743
Base = Pure +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   744
types
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   745
  o
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   746
arities
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   747
  o :: logic
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   748
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   749
  Trueprop :: o => prop   ("_" 5)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   750
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   751
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   752
The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   753
coercion function.  Assuming this definition resides in a file {\tt Base.thy},
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   754
you have to load it with the command {\tt use_thy "Base"}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   755
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   756
One of the simplest nontrivial logics is {\bf minimal logic} of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   757
implication.  Its definition in Isabelle needs no advanced features but
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   758
illustrates the overall mechanism nicely:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   759
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   760
Hilbert = Base +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   761
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   762
  "-->" :: [o, o] => o   (infixr 10)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   763
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   764
  K     "P --> Q --> P"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   765
  S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   766
  MP    "[| P --> Q; P |] ==> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   767
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   768
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   769
After loading this definition from the file {\tt Hilbert.thy}, you can
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   770
start to prove theorems in the logic:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   771
\begin{ttbox}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4597
diff changeset
   772
Goal "P --> P";
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   773
{\out Level 0}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   774
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   775
{\out  1.  P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   776
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   777
by (resolve_tac [Hilbert.MP] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   778
{\out Level 1}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   779
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   780
{\out  1.  ?P --> P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   781
{\out  2.  ?P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   782
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   783
by (resolve_tac [Hilbert.MP] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   784
{\out Level 2}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   785
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   786
{\out  1.  ?P1 --> ?P --> P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   787
{\out  2.  ?P1}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   788
{\out  3.  ?P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   789
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   790
by (resolve_tac [Hilbert.S] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   791
{\out Level 3}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   792
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   793
{\out  1.  P --> ?Q2 --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   794
{\out  2.  P --> ?Q2}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   795
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   796
by (resolve_tac [Hilbert.K] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   797
{\out Level 4}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   798
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   799
{\out  1.  P --> ?Q2}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   800
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   801
by (resolve_tac [Hilbert.K] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   802
{\out Level 5}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   803
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   804
{\out No subgoals!}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   805
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   806
As we can see, this Hilbert-style formulation of minimal logic is easy to
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   807
define but difficult to use.  The following natural deduction formulation is
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   808
better:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   809
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   810
MinI = Base +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   811
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   812
  "-->" :: [o, o] => o   (infixr 10)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   813
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   814
  impI  "(P ==> Q) ==> P --> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   815
  impE  "[| P --> Q; P |] ==> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   816
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   817
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   818
Note, however, that although the two systems are equivalent, this fact
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   819
cannot be proved within Isabelle.  Axioms {\tt S} and {\tt K} can be
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   820
derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   821
  Hilbert}.  The reason is that {\tt impI} is only an {\bf admissible} rule
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   822
in {\tt Hilbert}, something that can only be shown by induction over all
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   823
possible proofs in {\tt Hilbert}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   824
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   825
We may easily extend minimal logic with falsity:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   826
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   827
MinIF = MinI +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   828
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   829
  False :: o
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   830
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   831
  FalseE "False ==> P"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   832
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   833
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   834
On the other hand, we may wish to introduce conjunction only:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   835
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   836
MinC = Base +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   837
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   838
  "&" :: [o, o] => o   (infixr 30)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   839
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   840
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   841
  conjI  "[| P; Q |] ==> P & Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   842
  conjE1 "P & Q ==> P"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   843
  conjE2 "P & Q ==> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   844
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   845
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   846
And if we want to have all three connectives together, we create and load a
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   847
theory file consisting of a single line:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   848
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   849
MinIFC = MinIF + MinC
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   850
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   851
Now we can prove mixed theorems like
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   852
\begin{ttbox}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4597
diff changeset
   853
Goal "P & False --> Q";
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   854
by (resolve_tac [MinI.impI] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   855
by (dresolve_tac [MinC.conjE2] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   856
by (eresolve_tac [MinIF.FalseE] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   857
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   858
Try this as an exercise!
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   859
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   860
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   861
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   862
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   863
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   864
%%% End: