doc-src/Ref/defining.tex
author wenzelm
Fri, 16 Jul 1999 22:24:42 +0200
changeset 7024 44bd3c094fd6
parent 6592 c120262044b6
child 8136 8c65f3ca13f2
permissions -rw-r--r--
tuned;
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
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    35
rewritten using a production $A^{(q)} = \gamma$ only if~$p \le q$.  Any
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 \]
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
    43
if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \le q$.
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)} \\
3694
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   107
      &$|$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\\\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   108
$idts$ &=& $idt$ ~~$|$~~ $idt^{(1)}$ $idts$ \\\\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   109
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   110
    &$|$& $id$ {\tt ::} $type$ & (0) \\\\
3694
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   111
$pttrns$ &=& $pttrn$ ~~$|$~~ $pttrn^{(1)}$ $pttrns$ \\\\
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   112
$pttrn$ &=& $idt$ \\\\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   113
$type$ &=& {\tt(} $type$ {\tt)} \\
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   114
     &$|$& $tid$ ~~$|$~~ $tvar$ ~~$|$~~ $tid$ {\tt::} $sort$
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   115
       ~~$|$~~ $tvar$ {\tt::} $sort$ \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   116
     &$|$& $id$ ~~$|$~~ $type^{(\infty)}$ $id$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   117
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   118
     &$|$& $longid$ ~~$|$~~ $type^{(\infty)}$ $longid$
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   119
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $longid$ \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   120
     &$|$& $type^{(1)}$ {\tt =>} $type$ & (0) \\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   121
     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0) \\\\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   122
$sort$ &=& $id$ ~~$|$~~ $longid$ ~~$|$~~ {\tt\ttlbrace\ttrbrace} ~~$|$~~
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   123
  {\tt\ttlbrace} $id$ ~$|$~ $longid$ {\tt,} \dots {\tt,} $id$ ~$|$~ $longid$ {\tt\ttrbrace}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   124
\end{tabular}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   125
\index{*PROP symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   126
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   127
\index{*:: symbol}\index{*=> symbol}
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   128
\index{sort constraints}
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   129
%the index command: a percent is permitted, but braces must match!
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   130
\index{%@{\tt\%} symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   131
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   132
\index{*[ symbol}\index{*] symbol}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   133
\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
\end{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   137
\caption{Meta-logic syntax}\label{fig:pure_gram}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   138
\end{figure}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   139
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   140
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   141
\section{The Pure syntax} \label{sec:basic_syntax}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   142
\index{syntax!Pure|(}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   143
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   144
At the root of all object-logics lies the theory \thydx{Pure}.  It
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   145
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
   146
this basic syntax (types, terms and formulae) appears in
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   147
\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}%
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   148
{\S\ref{sec:forward}}.  A more precise description using a priority grammar
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   149
appears in Fig.\ts\ref{fig:pure_gram}.  It defines the following
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   150
nonterminals:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   151
\begin{ttdescription}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   152
  \item[\ndxbold{any}] denotes any term.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   153
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   154
  \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
   155
    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
   156
    (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
   157
    Otherwise atomic propositions with head $c$ may be printed incorrectly.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   158
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   159
  \item[\ndxbold{aprop}] denotes atomic propositions.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   160
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   161
%% FIXME huh!?
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   162
%  These typically
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   163
%  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
   164
%  introduces a meta-level predicate for each judgement form.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   165
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   166
  \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
   167
    \cldx{logic}, excluding type \tydx{prop}.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   168
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   169
  \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
   170
    by types.
3694
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   171
    
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   172
  \item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   173
    abstraction, cases etc.  Initially the same as $idt$ and $idts$,
fe7b812837ad fixed pttrn syntax;
wenzelm
parents: 3485
diff changeset
   174
    these are indetended to be augmented by user extensions.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   175
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   176
  \item[\ndxbold{type}] denotes types of the meta-logic.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   177
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   178
  \item[\ndxbold{sort}] denotes meta-level sorts.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   179
\end{ttdescription}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   180
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   181
\begin{warn}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   182
  In {\tt idts}, note that \verb|x::nat y| is parsed as \verb|x::(nat y)|,
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   183
  treating {\tt y} like a type constructor applied to {\tt nat}.  The
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   184
  likely result is an error message.  To avoid this interpretation, use
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   185
  parentheses and write \verb|(x::nat) y|.
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   186
  \index{type constraints}\index{*:: symbol}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   187
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   188
  Similarly, \verb|x::nat y::nat| is parsed as \verb|x::(nat y::nat)| and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   189
  yields an error.  The correct form is \verb|(x::nat) (y::nat)|.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   190
\end{warn}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   191
452
395bbf6e55f9 changed priority of ::
nipkow
parents: 332
diff changeset
   192
\begin{warn}
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   193
  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
   194
  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
   195
  which case the string is likely to be ambiguous.  The correct form is
452
395bbf6e55f9 changed priority of ::
nipkow
parents: 332
diff changeset
   196
  \verb!x<(y::nat)!.
395bbf6e55f9 changed priority of ::
nipkow
parents: 332
diff changeset
   197
\end{warn}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   198
867
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   199
\subsection{Logical types and default syntax}\label{logical-types}
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   200
\index{lambda calc@$\lambda$-calculus}
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   201
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   202
Isabelle's representation of mathematical languages is based on the
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   203
simply typed $\lambda$-calculus.  All logical types, namely those of
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   204
class \cldx{logic}, are automatically equipped with a basic syntax of
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   205
types, identifiers, variables, parentheses, $\lambda$-abstraction and
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   206
application.
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   207
\begin{warn}
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   208
  Isabelle combines the syntaxes for all types of class \cldx{logic} by
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   209
  mapping all those types to the single nonterminal $logic$.  Thus all
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   210
  productions of $logic$, in particular $id$, $var$ etc, become available.
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   211
\end{warn}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   212
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   213
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   214
\subsection{Lexical matters}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   215
The parser does not process input strings directly.  It operates on token
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   216
lists provided by Isabelle's \bfindex{lexer}.  There are two kinds of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   217
tokens: \bfindex{delimiters} and \bfindex{name tokens}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   218
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   219
\index{reserved words}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   220
Delimiters can be regarded as reserved words of the syntax.  You can
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   221
add new ones when extending theories.  In Fig.\ts\ref{fig:pure_gram} they
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   222
appear in typewriter font, for example {\tt ==}, {\tt =?=} and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   223
{\tt PROP}\@.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   224
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   225
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
   226
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
   227
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
   228
\rmindex{numerals}, \rmindex{strings}.  They are denoted by \ndxbold{id},
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   229
\ndxbold{var}, \ndxbold{tid}, \ndxbold{tvar}, \ndxbold{xnum}, \ndxbold{xstr},
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   230
respectively.  Typical examples are {\tt x}, {\tt ?x7}, {\tt 'a}, {\tt ?'a3},
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   231
{\tt \#42}, {\tt ''foo bar''}.  Here is the precise syntax:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   232
\begin{eqnarray*}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   233
id        & =   & letter~quasiletter^* \\
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   234
longid    & =   & id\mbox{\tt .}id~\dots~id \\
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   235
var       & =   & \mbox{\tt ?}id ~~|~~ \mbox{\tt ?}id\mbox{\tt .}nat \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   236
tid       & =   & \mbox{\tt '}id \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   237
tvar      & =   & \mbox{\tt ?}tid ~~|~~
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   238
                  \mbox{\tt ?}tid\mbox{\tt .}nat \\
5542
f0c303f53730 changed xnum token syntax;
wenzelm
parents: 5371
diff changeset
   239
xnum      & =   & \mbox{\tt \#}nat ~~|~~ \mbox{\tt \#-}nat \\
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   240
xstr      & =   & \mbox{\tt ''\rm text\tt ''} \\[1ex]
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   241
letter    & =   & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   242
digit     & =   & \mbox{one of {\tt 0}\dots {\tt 9}} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   243
quasiletter & =  & letter ~~|~~ digit ~~|~~ \mbox{\tt _} ~~|~~ \mbox{\tt '} \\
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   244
nat       & =   & digit^+
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   245
\end{eqnarray*}
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   246
The lexer repeatedly takes the longest prefix of the input string that
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   247
forms a valid token.  A maximal prefix that is both a delimiter and a
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   248
name is treated as a delimiter.  Spaces, tabs, newlines and formfeeds
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   249
are separators; they never occur within tokens, except those of class
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   250
$xstr$.
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   251
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   252
\medskip
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   253
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
   254
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
   255
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
   256
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
   257
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
   258
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
   259
{\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
   260
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   261
A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   262
a pair of base name and index (\ML\ type \mltydx{indexname}).  These
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   263
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
   264
run together as in {\tt ?x1}.  The latter form is possible if the base name
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   265
does not end with digits.  If the index is 0, it may be dropped altogether:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   266
{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   267
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   268
Tokens of class $xnum$ or $xstr$ are not used by the meta-logic.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   269
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
   270
productions and translation functions.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   271
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   272
\medskip
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   273
Although name tokens are returned from the lexer rather than the parser, it
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   274
is more logical to regard them as nonterminals.  Delimiters, however, are
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   275
terminals; they are just syntactic sugar and contribute nothing to the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   276
abstract syntax tree.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   277
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   278
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   279
\subsection{*Inspecting the syntax} \label{pg:print_syn}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   280
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   281
syn_of              : theory -> Syntax.syntax
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   282
print_syntax        : theory -> unit
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   283
Syntax.print_syntax : Syntax.syntax -> unit
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   284
Syntax.print_gram   : Syntax.syntax -> unit
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   285
Syntax.print_trans  : Syntax.syntax -> unit
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   286
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   287
The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   288
in \ML.  You can display values of this type by calling the following
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   289
functions:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   290
\begin{ttdescription}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   291
\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   292
  theory~{\it thy} as an \ML\ value.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   293
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   294
\item[\ttindexbold{print_syntax} $thy$] displays the syntax part of $thy$
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   295
  using {\tt Syntax.print_syntax}.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   296
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   297
\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   298
  information contained in the syntax {\it syn}.  The displayed output can
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   299
  be large.  The following two functions are more selective.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   300
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   301
\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
   302
  of~{\it syn}, namely the lexicon, logical types and productions.  These are
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   303
  discussed below.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   304
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   305
\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   306
  part of~{\it syn}, namely the constants, parse/print macros and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   307
  parse/print translations.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   308
\end{ttdescription}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   309
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   310
Let us demonstrate these functions by inspecting Pure's syntax.  Even that
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   311
is too verbose to display in full.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   312
\begin{ttbox}\index{*Pure theory}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   313
Syntax.print_syntax (syn_of Pure.thy);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   314
{\out lexicon: "!!" "\%" "(" ")" "," "." "::" ";" "==" "==>" \dots}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   315
{\out logtypes: fun itself}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   316
{\out prods:}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   317
{\out   type = tid  (1000)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   318
{\out   type = tvar  (1000)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   319
{\out   type = id  (1000)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   320
{\out   type = tid "::" sort[0]  => "_ofsort" (1000)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   321
{\out   type = tvar "::" sort[0]  => "_ofsort" (1000)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   322
{\out   \vdots}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   323
\ttbreak
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   324
{\out print modes: "symbols" "xterm"}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   325
{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   326
{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   327
{\out   "_idtyp" "_lambda" "_tapp" "_tappl"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   328
{\out parse_rules:}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   329
{\out parse_translation: "!!" "_K" "_abs" "_aprop"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   330
{\out print_translation: "all"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   331
{\out print_rules:}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   332
{\out print_ast_translation: "==>" "_abs" "_idts" "fun"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   333
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   334
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   335
As you can see, the output is divided into labelled sections.  The grammar
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   336
is represented by {\tt lexicon}, {\tt logtypes} and {\tt prods}.  The rest
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   337
refers to syntactic translations and macro expansion.  Here is an
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   338
explanation of the various sections.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   339
\begin{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   340
  \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
   341
    analysis.\index{delimiters}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   342
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   343
  \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
   344
    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
   345
    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
   346
    $\lambda$-calculus.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   347
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   348
  \item[{\tt prods}] lists the \rmindex{productions} of the priority grammar.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   349
    The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   350
    Each delimiter is quoted.  Some productions are shown with {\tt =>} and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   351
    an attached string.  These strings later become the heads of parse
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   352
    trees; they also play a vital role when terms are printed (see
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   353
    \S\ref{sec:asts}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   354
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   355
    Productions with no strings attached are called {\bf copy
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   356
      productions}\indexbold{productions!copy}.  Their right-hand side must
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   357
    have exactly one nonterminal symbol (or name token).  The parser does
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   358
    not create a new parse tree node for copy productions, but simply
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   359
    returns the parse tree of the right-hand symbol.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   360
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   361
    If the right-hand side consists of a single nonterminal with no
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   362
    delimiters, then the copy production is called a {\bf chain
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   363
      production}.  Chain productions act as abbreviations:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   364
    conceptually, they are removed from the grammar by adding new
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   365
    productions.  Priority information attached to chain productions is
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   366
    ignored; only the dummy value $-1$ is displayed.
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   367
    
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   368
  \item[\ttindex{print_modes}] lists the alternative print modes
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   369
    provided by this syntax (see \S\ref{sec:prmodes}).
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   370
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   371
  \item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}]
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   372
    relate to macros (see \S\ref{sec:macros}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   373
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   374
  \item[{\tt parse_ast_translation}, {\tt print_ast_translation}]
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   375
    list sets of constants that invoke translation functions for abstract
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   376
    syntax trees.  Section \S\ref{sec:asts} below discusses this obscure
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   377
    matter.\index{constants!for translations}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   378
4597
a0bdee64194c Fixed a lot of overfull and underfull lines (hboxes)
paulson
parents: 4543
diff changeset
   379
  \item[{\tt parse_translation}, {\tt print_translation}] list the sets
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   380
    of constants that invoke translation functions for terms (see
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   381
    \S\ref{sec:tr_funs}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   382
\end{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   383
\index{syntax!Pure|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   384
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   385
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   386
\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
   387
\index{mixfix declarations|(}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   388
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   389
When defining a theory, you declare new constants by giving their names,
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   390
their type, and an optional {\bf mixfix annotation}.  Mixfix annotations
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   391
allow you to extend Isabelle's basic $\lambda$-calculus syntax with
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   392
readable notation.  They can express any context-free priority grammar.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   393
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
   394
general than the priority declarations of \ML\ and Prolog.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   395
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   396
A mixfix annotation defines a production of the priority grammar.  It
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   397
describes the concrete syntax, the translation to abstract syntax, and the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   398
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
   399
specifying infix operators and binders.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   400
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   401
\subsection{The general mixfix form}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   402
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
   403
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
   404
file:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   405
\begin{center}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   406
  {\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   407
\end{center}
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   408
This constant declaration and mixfix annotation are interpreted as follows:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   409
\begin{itemize}\index{productions}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   410
\item The string {\tt $c$} is the name of the constant associated with the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   411
  production; unless it is a valid identifier, it must be enclosed in
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   412
  quotes.  If $c$ is empty (given as~{\tt ""}) then this is a copy
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   413
  production.\index{productions!copy} Otherwise, parsing an instance of the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   414
  phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   415
    $a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$-th
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   416
  argument.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   417
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   418
  \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
   419
    ({\tt consts} section only).
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   420
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   421
  \item The string $template$ specifies the right-hand side of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   422
    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
   423
    \[ w@0 \;_\; w@1 \;_\; \ldots \;_\; w@n, \]
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   424
    where each occurrence of {\tt_} denotes an argument position and
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   425
    the~$w@i$ do not contain~{\tt _}.  (If you want a literal~{\tt _} in
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   426
    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
   427
    may consist of \rmindex{delimiters}, spaces or
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   428
    \rmindex{pretty printing} annotations (see below).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   429
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   430
  \item The type $\sigma$ specifies the production's nonterminal symbols
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   431
    (or name tokens).  If $template$ is of the form above then $\sigma$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   432
    must be a function type with at least~$n$ argument positions, say
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   433
    $\sigma = [\tau@1, \dots, \tau@n] \To \tau$.  Nonterminal symbols are
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   434
    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
   435
    below.  Any of these may be function types.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   436
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   437
  \item The optional list~$ps$ may contain at most $n$ integers, say {\tt
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   438
      [$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   439
    priority\indexbold{priorities} required of any phrase that may appear
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   440
    as the $i$-th argument.  Missing priorities default to~0.
4543
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   441
    
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   442
  \item The integer $p$ is the priority of this production.  If
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   443
    omitted, it defaults to the maximal priority.  Priorities range
82a45bdd0e80 several minor updates;
wenzelm
parents: 3802
diff changeset
   444
    between 0 and \ttindexbold{max_pri} (= 1000).
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   445
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   446
\end{itemize}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   447
%
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   448
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
   449
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
   450
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
   451
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
   452
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
   453
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
   454
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
   455
any}.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   456
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   457
\begin{warn}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   458
  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
   459
  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
   460
  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
   461
  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
   462
  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
   463
  separate nonterminal symbols.
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   464
\end{warn}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   465
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   466
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
   467
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
   468
\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
   469
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
   470
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
   471
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   472
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
   473
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
   474
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
   475
requires additional syntactic translations, see also
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   476
Chapter~\ref{chap:syntax}).
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   477
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   478
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   479
\medskip
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   480
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
   481
\begin{center}
911
55754d6d399c new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm
parents: 885
diff changeset
   482
  {\tt $c$ ::\ "$\sigma$" ("$template$")}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   483
\end{center}
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   484
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
   485
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
   486
Omitting priorities in this manner is prone to syntactic ambiguities unless
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   487
the production's right-hand side is fully bracketed, as in
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   488
\verb|"if _ then _ else _ fi"|.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   489
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   490
Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"},
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   491
is sensible only if~$c$ is an identifier.  Otherwise you will be unable to
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   492
write terms involving~$c$.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   493
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   494
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   495
\subsection{Example: arithmetic expressions}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   496
\index{examples!of mixfix declarations}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   497
This theory specification contains a {\tt syntax} section with mixfix
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   498
declarations encoding the priority grammar from
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   499
\S\ref{sec:priority_grammars}:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   500
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   501
ExpSyntax = Pure +
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   502
types
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   503
  exp
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   504
syntax
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   505
  "0" :: exp                 ("0"      9)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   506
  "+" :: [exp, exp] => exp   ("_ + _"  [0, 1] 0)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   507
  "*" :: [exp, exp] => exp   ("_ * _"  [3, 2] 2)
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   508
  "-" :: exp => exp          ("- _"    [3] 3)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   509
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   510
\end{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   511
If you put this into a file {\tt ExpSyntax.thy} and load it via {\tt
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   512
  use_thy"ExpSyntax"}, you can run some tests:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   513
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   514
val read_exp = Syntax.test_read (syn_of ExpSyntax.thy) "exp";
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   515
{\out val it = fn : string -> unit}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   516
read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0";
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   517
{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   518
{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   519
{\out \vdots}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   520
read_exp "0 + - 0 + 0";
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   521
{\out tokens: "0" "+" "-" "0" "+" "0"}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   522
{\out raw: ("+" ("+" "0" ("-" "0")) "0")}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   523
{\out \vdots}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   524
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   525
The output of \ttindex{Syntax.test_read} includes the token list ({\tt
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   526
  tokens}) and the raw \AST{} directly derived from the parse tree,
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   527
ignoring parse \AST{} translations.  The rest is tracing information
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   528
provided by the macro expander (see \S\ref{sec:macros}).
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   529
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   530
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
   531
above mixfix declarations (lots of additional information deleted):
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   532
\begin{ttbox}
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   533
Syntax.print_gram (syn_of ExpSyntax.thy);
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   534
{\out exp = "0"  => "0" (9)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   535
{\out exp = exp[0] "+" exp[1]  => "+" (0)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   536
{\out exp = exp[3] "*" exp[2]  => "*" (2)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   537
{\out exp = "-" exp[3]  => "-" (3)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   538
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   539
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   540
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
   541
retained as a separate nonterminal.  This also entails that the syntax
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   542
does not provide for identifiers or paranthesized expressions.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   543
Normally you would also want to add the declaration {\tt arities
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   544
  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
   545
  syntax}.  Try this as an exercise and study the changes in the
867
e1a654c29b05 some cosmetic changes
nipkow
parents: 866
diff changeset
   546
grammar.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   547
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   548
\subsection{The mixfix template}
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   549
Let us now take a closer look at the string $template$ appearing in mixfix
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   550
annotations.  This string specifies a list of parsing and printing
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   551
directives: delimiters\index{delimiters}, arguments, spaces, blocks of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   552
indentation and line breaks.  These are encoded by the following character
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   553
sequences:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   554
\index{pretty printing|(}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   555
\begin{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   556
\item[~$d$~] is a delimiter, namely a non-empty sequence of characters
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   557
  other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   558
  Even these characters may appear if escaped; this means preceding it with
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   559
  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
   560
  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
   561
  delimiters without extra white space being added for printing.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   562
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   563
\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   564
  or name token.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   565
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   566
\item[~$s$~] is a non-empty sequence of spaces for printing.  This and the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   567
  following specifications do not affect parsing at all.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   568
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   569
\item[~{\tt(}$n$~] opens a pretty printing block.  The optional number $n$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   570
  specifies how much indentation to add when a line break occurs within the
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   571
  block.  If {\tt(} is not followed by digits, the indentation defaults
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   572
  to~0.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   573
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   574
\item[~{\tt)}~] closes a pretty printing block.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   575
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   576
\item[~{\tt//}~] forces a line break.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   577
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   578
\item[~{\tt/}$s$~] allows a line break.  Here $s$ stands for the string of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   579
  spaces (zero or more) right after the {\tt /} character.  These spaces
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   580
  are printed if the break is not taken.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   581
\end{description}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   582
For example, the template {\tt"(_ +/ _)"} specifies an infix operator.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   583
There are two argument positions; the delimiter~{\tt+} is preceded by a
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   584
space and followed by a space or line break; the entire phrase is a pretty
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   585
printing block.  Other examples appear in Fig.\ts\ref{fig:set_trans} below.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   586
Isabelle's pretty printer resembles the one described in
6592
c120262044b6 Now uses manual.bib; some references updated
paulson
parents: 5542
diff changeset
   587
Paulson~\cite{paulson-ml2}.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   588
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   589
\index{pretty printing|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   590
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   591
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   592
\subsection{Infixes}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   593
\indexbold{infixes}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   594
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   595
Infix operators associating to the left or right can be declared using
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   596
{\tt infixl} or {\tt infixr}.  Basically, the form {\tt $c$ ::\ 
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   597
  $\sigma$ (infixl $p$)} abbreviates the mixfix declarations
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   598
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   599
"op \(c\)" :: \(\sigma\)   ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\))
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   600
"op \(c\)" :: \(\sigma\)   ("op \(c\)")
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   601
\end{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   602
and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   603
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   604
"op \(c\)" :: \(\sigma\)   ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\))
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   605
"op \(c\)" :: \(\sigma\)   ("op \(c\)")
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   606
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   607
The infix operator is declared as a constant with the prefix {\tt op}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   608
Thus, prefixing infixes with \sdx{op} makes them behave like ordinary
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   609
function symbols, as in \ML.  Special characters occurring in~$c$ must be
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   610
escaped, as in delimiters, using a single quote.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   611
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   612
A slightly more general form of infix declarations allows constant
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   613
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
   614
  ::\ $\sigma$\ (infixl "$sy$" $p$)}, the same for \texttt{infixr}.  As
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   615
an example consider:
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   616
\begin{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   617
and :: [bool, bool] => bool  (infixr "&" 35)
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   618
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   619
The internal constant name will then be just \texttt{and}, without any
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   620
\texttt{op} prefixed.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   621
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   622
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   623
\subsection{Binders}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   624
\indexbold{binders}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   625
\begingroup
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   626
\def\Q{{\cal Q}}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   627
A {\bf binder} is a variable-binding construct such as a quantifier.  The
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   628
constant declaration
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   629
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   630
\(c\) :: \(\sigma\)   (binder "\(\Q\)" [\(pb\)] \(p\))
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   631
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   632
introduces a constant~$c$ of type~$\sigma$, which must have the form
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   633
$(\tau@1 \To \tau@2) \To \tau@3$.  Its concrete syntax is $\Q~x.P$, where
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   634
$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
   635
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
   636
specifies the body's priority, by default~$p$.  Special characters
877
e528724951b0 added optional body priority to binder declaration
clasohm
parents: 867
diff changeset
   637
in $\Q$ must be escaped using a single quote.
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   638
864
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   639
The declaration is expanded internally to something like
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   640
\begin{ttbox}
3098
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   641
\(c\)\hskip3pt    :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\)
a31170b67367 Updated to LaTeX 2e
berghofe
parents: 1387
diff changeset
   642
"\(\Q\)"  :: [idts, \(\tau@2\)] => \(\tau@3\)   ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\))
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   643
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   644
Here \ndx{idts} is the nonterminal symbol for a list of identifiers with
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   645
\index{type constraints}
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   646
optional type constraints (see Fig.\ts\ref{fig:pure_gram}).  The
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   647
declaration also installs a parse translation\index{translations!parse}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   648
for~$\Q$ and a print translation\index{translations!print} for~$c$ to
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   649
translate between the internal and external forms.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   650
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   651
A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   652
list of variables.  The external form $\Q~x@1~x@2 \ldots x@n. P$
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   653
corresponds to the internal form
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   654
\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \]
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   655
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   656
\medskip
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   657
For example, let us declare the quantifier~$\forall$:\index{quantifiers}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   658
\begin{ttbox}
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   659
All :: ('a => o) => o   (binder "ALL " 10)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   660
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   661
This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   662
  $x$.$P$}.  When printing, Isabelle prefers the latter form, but must fall
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   663
back on ${\tt All}(P)$ if $P$ is not an abstraction.  Both $P$ and {\tt ALL
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   664
  $x$.$P$} have type~$o$, the type of formulae, while the bound variable
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   665
can be polymorphic.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   666
\endgroup
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   667
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   668
\index{mixfix declarations|)}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   669
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   670
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   671
\section{*Alternative print modes} \label{sec:prmodes}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   672
\index{print modes|(}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   673
%
3485
f27a30a18a17 Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents: 3318
diff changeset
   674
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
   675
may be used independently or in cooperation.  The currently active
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   676
print modes (with precedence from left to right) are determined by a
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   677
reference variable.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   678
\begin{ttbox}\index{*print_mode}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   679
print_mode: string list ref
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   680
\end{ttbox}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   681
Initially this may already contain some print mode identifiers,
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   682
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
   683
interface).  So changes should be incremental --- adding or deleting
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   684
modes relative to the current value.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   685
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   686
Any \ML{} string is a legal print mode identifier, without any
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   687
predeclaration required.  The following names should be considered
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   688
reserved, though: \texttt{""} (yes, the empty string),
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   689
\texttt{symbols}, \texttt{latex}, \texttt{xterm}.
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   690
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   691
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
   692
associated with each print mode.  The currently active ones are
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   693
conceptually just concatenated from left to right, with the standard
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   694
syntax output table always coming last as default.  Thus mixfix
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   695
productions of preceding modes in the list may override those of later
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   696
ones.  Also note that token translations are always relative to some
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   697
print mode (see \S\ref{sec:tok_tr}).
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   698
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   699
\medskip The canonical application of print modes is optional printing
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   700
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
   701
  ascii}.  Another example is to re-use Isabelle's advanced
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   702
$\lambda$-term printing mechanisms to generate completely different
3228
41ad2d5077be index: model checkers;
wenzelm
parents: 3214
diff changeset
   703
output, say for interfacing external tools like \rmindex{model
41ad2d5077be index: model checkers;
wenzelm
parents: 3214
diff changeset
   704
  checkers} (see also \texttt{HOL/Modelcheck}).
3108
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   705
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   706
\index{print modes|)}
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   707
335efc3f5632 misc updates, tuning, cleanup;
wenzelm
parents: 3098
diff changeset
   708
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   709
\section{Ambiguity of parsed expressions} \label{sec:ambiguity}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   710
\index{ambiguity!of parsed expressions}
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
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
   713
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
   714
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
   715
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
   716
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
   717
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
   718
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
   719
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
   720
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
   721
as follows:
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   722
880
667dc43e3b98 added documentation of Sign.ambiguity_level
clasohm
parents: 877
diff changeset
   723
If an ambiguity can be resolved by type inference the following
667dc43e3b98 added documentation of Sign.ambiguity_level
clasohm
parents: 877
diff changeset
   724
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
   725
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
   726
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
   727
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
   728
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
   729
many parse trees are necessary to generate the warning.
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   730
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   731
\begin{ttbox}
3801
5ba459e15dd7 tuned warning msg;
wenzelm
parents: 3694
diff changeset
   732
{\out Ambiguous input "\dots"}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   733
{\out produces the following parse trees:}
3801
5ba459e15dd7 tuned warning msg;
wenzelm
parents: 3694
diff changeset
   734
{\out \dots}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   735
{\out Fortunately, only one parse tree is type correct.}
3801
5ba459e15dd7 tuned warning msg;
wenzelm
parents: 3694
diff changeset
   736
{\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
   737
\end{ttbox}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   738
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   739
The following message is normally caused by using the same
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   740
syntax in two different productions:
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   741
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   742
\begin{ttbox}
3802
wenzelm
parents: 3801
diff changeset
   743
{\out Ambiguous input "..."}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   744
{\out produces the following parse trees:}
3802
wenzelm
parents: 3801
diff changeset
   745
{\out \dots}
wenzelm
parents: 3801
diff changeset
   746
{\out More than one term is type correct:}
wenzelm
parents: 3801
diff changeset
   747
{\out \dots}
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   748
\end{ttbox}
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   749
866
2d3d020eef11 added documentation of bind_thm, qed, qed_goal, get_thm, thms_of
clasohm
parents: 864
diff changeset
   750
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
   751
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
   752
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
   753
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
   754
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   755
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   756
\section{Example: some minimal logics} \label{sec:min_logics}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   757
\index{examples!of logic definitions}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   758
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   759
This section presents some examples that have a simple syntax.  They
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   760
demonstrate how to define new object-logics from scratch.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   761
711
bb868a30e66f updated remarks about grammar; added section about ambiguities
clasohm
parents: 452
diff changeset
   762
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
   763
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
   764
(see Fig.\ts\ref{fig:pure_gram}), that syntax has to be extended with the
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   765
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
   766
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
   767
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
   768
if you add the production
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   769
\[ prop ~=~ logic. \]
d63b111b917a quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents: 711
diff changeset
   770
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
   771
formulae to propositions:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   772
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   773
Base = Pure +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   774
types
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   775
  o
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   776
arities
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   777
  o :: logic
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   778
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   779
  Trueprop :: o => prop   ("_" 5)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   780
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   781
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   782
The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   783
coercion function.  Assuming this definition resides in a file {\tt Base.thy},
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   784
you have to load it with the command {\tt use_thy "Base"}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   785
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   786
One of the simplest nontrivial logics is {\bf minimal logic} of
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   787
implication.  Its definition in Isabelle needs no advanced features but
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   788
illustrates the overall mechanism nicely:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   789
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   790
Hilbert = Base +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   791
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   792
  "-->" :: [o, o] => o   (infixr 10)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   793
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   794
  K     "P --> Q --> P"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   795
  S     "(P --> Q --> R) --> (P --> Q) --> P --> R"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   796
  MP    "[| P --> Q; P |] ==> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   797
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   798
\end{ttbox}
332
01b87a921967 final Springer copy
lcp
parents: 320
diff changeset
   799
After loading this definition from the file {\tt Hilbert.thy}, you can
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   800
start to prove theorems in the logic:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   801
\begin{ttbox}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4597
diff changeset
   802
Goal "P --> P";
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   803
{\out Level 0}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   804
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   805
{\out  1.  P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   806
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   807
by (resolve_tac [Hilbert.MP] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   808
{\out Level 1}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   809
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   810
{\out  1.  ?P --> P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   811
{\out  2.  ?P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   812
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   813
by (resolve_tac [Hilbert.MP] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   814
{\out Level 2}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   815
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   816
{\out  1.  ?P1 --> ?P --> P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   817
{\out  2.  ?P1}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   818
{\out  3.  ?P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   819
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   820
by (resolve_tac [Hilbert.S] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   821
{\out Level 3}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   822
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   823
{\out  1.  P --> ?Q2 --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   824
{\out  2.  P --> ?Q2}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   825
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   826
by (resolve_tac [Hilbert.K] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   827
{\out Level 4}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   828
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   829
{\out  1.  P --> ?Q2}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   830
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   831
by (resolve_tac [Hilbert.K] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   832
{\out Level 5}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   833
{\out P --> P}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   834
{\out No subgoals!}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   835
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   836
As we can see, this Hilbert-style formulation of minimal logic is easy to
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   837
define but difficult to use.  The following natural deduction formulation is
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   838
better:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   839
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   840
MinI = Base +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   841
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   842
  "-->" :: [o, o] => o   (infixr 10)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   843
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   844
  impI  "(P ==> Q) ==> P --> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   845
  impE  "[| P --> Q; P |] ==> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   846
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   847
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   848
Note, however, that although the two systems are equivalent, this fact
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   849
cannot be proved within Isabelle.  Axioms {\tt S} and {\tt K} can be
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   850
derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   851
  Hilbert}.  The reason is that {\tt impI} is only an {\bf admissible} rule
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   852
in {\tt Hilbert}, something that can only be shown by induction over all
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   853
possible proofs in {\tt Hilbert}.
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   854
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   855
We may easily extend minimal logic with falsity:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   856
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   857
MinIF = MinI +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   858
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   859
  False :: o
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   860
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   861
  FalseE "False ==> P"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   862
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   863
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   864
On the other hand, we may wish to introduce conjunction only:
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   865
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   866
MinC = Base +
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   867
consts
1387
9bcad9c22fd4 removed quotes from syntax and consts sections
clasohm
parents: 1060
diff changeset
   868
  "&" :: [o, o] => o   (infixr 30)
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   869
\ttbreak
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   870
rules
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   871
  conjI  "[| P; Q |] ==> P & Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   872
  conjE1 "P & Q ==> P"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   873
  conjE2 "P & Q ==> Q"
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   874
end
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   875
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   876
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
   877
theory file consisting of a single line:
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   878
\begin{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   879
MinIFC = MinIF + MinC
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   880
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   881
Now we can prove mixed theorems like
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   882
\begin{ttbox}
5205
602354039306 Changed "goal" to "Goal"
paulson
parents: 4597
diff changeset
   883
Goal "P & False --> Q";
320
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   884
by (resolve_tac [MinI.impI] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   885
by (dresolve_tac [MinC.conjE2] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   886
by (eresolve_tac [MinIF.FalseE] 1);
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   887
\end{ttbox}
76ae17549558 penultimate Springer draft
lcp
parents:
diff changeset
   888
Try this as an exercise!
5371
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   889
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   890
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   891
%%% Local Variables: 
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   892
%%% mode: latex
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   893
%%% TeX-master: "ref"
e27558a68b8d emacs local vars;
wenzelm
parents: 5205
diff changeset
   894
%%% End: