doc-src/Logics/old.defining.tex
author clasohm
Thu, 29 Jun 1995 12:28:27 +0200
changeset 1163 c080ff36d24e
parent 104 d8205bb279a7
permissions -rw-r--r--
changed 'chol' labels to 'hol'; added a few parentheses
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
\chapter{Defining Logics} \label{Defining-Logics}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
This chapter is intended for Isabelle experts.  It explains how to define new
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
logical systems, Isabelle's {\it raison d'\^etre}.  Isabelle logics are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
hierarchies of theories.  A number of simple examples are contained in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
introductory manual; the full syntax of theory definitions is shown in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
{\em Reference Manual}.  The purpose of this chapter is to explain the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
remaining subtleties, especially some context conditions on the class
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
structure and the definition of new mixfix syntax.  A full understanding of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
the material requires knowledge of the internal representation of terms (data
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
type {\tt term}) as detailed in the {\em Reference Manual}.  Sections marked
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
with a * can be skipped on first reading.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
\section{Classes and Types *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
\index{*arities!context conditions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
Type declarations are subject to the following two well-formedness
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
conditions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
\item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
  with $\vec{r} \neq \vec{s}$.  For example
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
types ty 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
arities ty :: (\{logic\}) logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
        ty :: (\{\})logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
leads to an error message and fails.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
  (s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
  for $i=1,\dots,n$.  The relationship $\preceq$, defined as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
expresses that the set of types represented by $s'$ is a subset of the set of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
types represented by $s$.  For example
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
classes term < logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
types ty 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
arities ty :: (\{logic\})logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
        ty :: (\{\})term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
leads to an error message and fails.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
These conditions guarantee principal types~\cite{nipkow-prehofer}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
\section{Precedence Grammars}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\label{PrecedenceGrammars}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
\index{precedence grammar|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
The precise syntax of a logic is best defined by a context-free grammar.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
These grammars obey the following conventions: identifiers denote
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
nonterminals, {\tt typewriter} fount denotes terminals, repetition is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
indicated by \dots, and alternatives are separated by $|$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
In order to simplify the description of mathematical languages, we introduce
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
an extended format which permits {\bf precedences}\index{precedence}.  This
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
scheme generalizes precedence declarations in \ML\ and {\sc prolog}.  In this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
extended grammar format, nonterminals are decorated by integers, their
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
precedence.  In the sequel, precedences are shown as subscripts.  A nonterminal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
$A@p$ on the right-hand side of a production may only be replaced using a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
production $A@q = \gamma$ where $p \le q$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
Formally, a set of context free productions $G$ induces a derivation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
relation $\rew@G$ on strings as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
\[ \alpha A@p \beta ~\rew@G~ \alpha\gamma\beta ~~~iff~~~
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
   \exists q \ge p.~(A@q=\gamma) \in G
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
Any extended grammar of this kind can be translated into a normal context
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
free grammar.  However, this translation may require the introduction of a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
large number of new nonterminals and productions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
\begin{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
\label{PrecedenceEx}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
The following simple grammar for arithmetic expressions demonstrates how
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
binding power and associativity of operators can be enforced by precedences.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
\begin{tabular}{rclr}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
$A@9$ & = & {\tt0} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
$A@9$ & = & {\tt(} $A@0$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
$A@0$ & = & $A@0$ {\tt+} $A@1$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
$A@2$ & = & $A@3$ {\tt*} $A@2$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
$A@3$ & = & {\tt-} $A@3$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
The choice of precedences determines that \verb$-$ binds tighter than
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
\verb$*$ which binds tighter than \verb$+$, and that \verb$+$ and \verb$*$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
associate to the left and right, respectively.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
To minimize the number of subscripts, we adopt the following conventions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
\item all precedences $p$ must be in the range $0 \leq p \leq max_pri$ for
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
  some fixed $max_pri$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
\item precedence $0$ on the right-hand side and precedence $max_pri$ on the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
  left-hand side may be omitted.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
In addition, we write the production $A@p = \alpha$ as $A = \alpha~(p)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
Using these conventions and assuming $max_pri=9$, the grammar in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
Example~\ref{PrecedenceEx} becomes
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
$A$ & = & {\tt0} & \hspace*{4em} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
 & $|$ & {\tt(} $A$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
 & $|$ & $A$ {\tt+} $A@1$ & (0) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
 & $|$ & $A@3$ {\tt*} $A@2$ & (2) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
 & $|$ & {\tt-} $A@3$ & (3)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\index{precedence grammar|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
\section{Basic syntax *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
An informal account of most of Isabelle's syntax (meta-logic, types etc) is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
contained in {\em Introduction to Isabelle}.  A precise description using a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
precedence grammar is shown in Figure~\ref{MetaLogicSyntax}.  This description
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
is the basis of all extensions by object-logics.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
\begin{figure}[htb]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
$prop$ &=& \ttindex{PROP} $aprop$ ~~$|$~~ {\tt(} $prop$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
     &$|$& $logic@3$ \ttindex{==} $logic@2$ & (2) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
     &$|$& $prop@2$ \ttindex{==>} $prop@1$ & (1) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
     &$|$& {\tt[|} $prop$ {\tt;} \dots {\tt;} $prop$ {\tt|]} {\tt==>} $prop@1$ & (1) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
     &$|$& {\tt!!} $idts$ {\tt.} $prop$ & (0) \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
$logic$ &=& $prop$ ~~$|$~~ $fun$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
$aprop$ &=& $id$ ~~$|$~~ $var$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
    ~~$|$~~ $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)} \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
$fun$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $fun$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
    &$|$& \ttindex{\%} $idts$ {\tt.} $logic$ & (0) \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
$idts$ &=& $idt$ ~~$|$~~ $idt@1$ $idts$ \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
$idt$ &=& $id$ ~~$|$~~ {\tt(} $idt$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
    &$|$& $id$ \ttindex{::} $type$ & (0) \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
$type$ &=& $tfree$ ~~$|$~~ $tvar$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
     &$|$& $tfree$ {\tt::} $sort$ ~~$|$~~ $tvar$ {\tt::} $sort$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
     &$|$& $id$ ~~$|$~~ $type@{max_pri}$ $id$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
                ~~$|$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
     &$|$& $type@1$ \ttindex{=>} $type$ & (0) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
     &$|$& {\tt[}  $type$ {\tt,} \dots {\tt,} $type$ {\tt]} {\tt=>} $type$&(0)\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
     &$|$& {\tt(} $type$ {\tt)} \\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
$sort$ &=& $id$ ~~$|$~~ {\tt\{\}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
                ~~$|$~~ {\tt\{} $id$ {\tt,} \dots {\tt,} $id$ {\tt\}} 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
\end{tabular}\index{*"!"!}\index{*"["|}\index{*"|"]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
\indexbold{type@$type$}\indexbold{sort@$sort$}\indexbold{idts@$idts$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\indexbold{logic@$logic$}\indexbold{prop@$prop$}\indexbold{fun@$fun$}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
\caption{Meta-Logic Syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\label{MetaLogicSyntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
\end{figure}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
The following main categories are defined:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
\item[$prop$] Terms of type $prop$, i.e.\ formulae of the meta-logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
\item[$aprop$] Atomic propositions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
\item[$logic$] Terms of types in class $logic$.  Initially, $logic$ contains
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
  merely $prop$.  As the syntax is extended by new object-logics, more
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
  productions for $logic$ are added (see below).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
\item[$fun$] Terms potentially of function type.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\item[$type$] Types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\item[$idts$] a list of identifiers, possibly constrained by types.  Note
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
  that $x::nat~y$ is parsed as $x::(nat~y)$, i.e.\ $y$ is treated like a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
  type constructor applied to $nat$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
The predefined types $id$, $var$, $tfree$ and $tvar$ represent identifiers
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   164
({\tt f}), unknowns ({\tt ?f}), type variables ({\tt 'a}), and type unknowns
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   165
({\tt ?'a}) respectively.  If we think of them as nonterminals with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
predefined syntax, we may assume that all their productions have precedence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
$max_pri$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
\subsection{Logical types and default syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
Isabelle is concerned with mathematical languages which have a certain
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
minimal vocabulary: identifiers, variables, parentheses, and the lambda
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
calculus.  Logical types, i.e.\ those of class $logic$, are automatically
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
equipped with this basic syntax.  More precisely, for any type constructor
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
$ty$ with arity $(\dots)c$, where $c$ is a subclass of $logic$, the following
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
productions are added:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
\begin{tabular}{rclc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
$ty$ &=& $id$ ~~$|$~~ $var$ ~~$|$~~ {\tt(} $ty$ {\tt)} \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
  &$|$& $fun@{max_pri}$ {\tt(} $logic$ {\tt,} \dots {\tt,} $logic$ {\tt)}\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
  &$|$& $ty@{max_pri}$ {\tt::} $type$\\\\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
$logic$ &=& $ty$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
\section{Mixfix syntax}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
\index{mixfix|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
We distinguish between abstract and concrete syntax.  The {\em abstract}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
syntax is given by the typed constants of a theory.  Abstract syntax trees are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
well-typed terms, i.e.\ values of \ML\ type {\tt term}.  If none of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
constants are introduced with mixfix annotations, there is no concrete syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
to speak of: terms can only be abstractions or applications of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
$f(t@1,\dots,t@n)$, where $f$ is a constant or variable.  Since this notation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
quickly becomes unreadable, Isabelle supports syntax definitions in the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
of unrestricted context-free grammars using mixfix annotations.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
Mixfix annotations describe the {\em concrete} syntax, its translation into
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
the abstract syntax, and a pretty-printing scheme, all in one.  Isabelle
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
syntax definitions are inspired by \OBJ's~\cite{OBJ} {\em mixfix\/} syntax.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
Each mixfix annotation defines a precedence grammar production and associates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
an Isabelle constant with it.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
A {\em mixfix declaration} {\tt consts $c$ ::\ $\tau$ ($sy$ $ps$ $p$)} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
interpreted as a grammar pro\-duction as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
\item $sy$ is the right-hand side of this production, specified as a {\em
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
    mixfix annotation}.  In general, $sy$ is of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
  $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$, where each occurrence of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
  ``\ttindex{_}'' denotes an argument/nonterminal and the strings
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
  $\alpha@i$ do not contain ``{\tt_}''.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
\item $\tau$ specifies the types of the nonterminals on the left and right
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
  hand side. If $sy$ is of the form above, $\tau$ must be of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
  $[\tau@1,\dots,\tau@n] \To \tau'$.  Then argument $i$ is of type $\tau@i$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
  and the result, i.e.\ the left-hand side of the production, is of type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
  $\tau'$.  Both the $\tau@i$ and $\tau'$ may be function types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
\item $c$ is the name of the Isabelle constant associated with this production.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
  Parsing an instance of the phrase $sy$ generates the {\tt term} {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
    Const($c$,dummyT\footnote{Proper types are inserted later on.  See
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
      \S\ref{Typing}})\$$a@1$\$$\dots$\$$a@n$}\index{*dummyT}, where $a@i$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
  the term generated by parsing the $i^{th}$ argument.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
\item $ps$ must be of the form $[p@1,\dots,p@n]$, where $p@i$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
  minimal precedence\index{precedence} required of any phrase that may appear
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
  as the $i^{th}$ argument.  The null list is interpreted as a list of 0's of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
  the appropriate length.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
\item $p$ is the precedence of this production.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
Notice that there is a close connection between abstract and concrete syntax:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
each production has an associated constant, and types act as {\bf syntactic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   231
  categories} in the concrete syntax.  To emphasize this connection, we
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
sometimes refer to the nonterminals on the right-hand side of a production as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
its arguments and to the nonterminal on the left-hand side as its result.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
The maximal legal precedence is called \ttindexbold{max_pri}, which is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
currently 1000.  If you want to ignore precedences, the safest way to do so is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
to use the annotation {\tt($sy$)}: this production puts no precedence
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
constraints on any of its arguments and has maximal precedence itself, i.e.\ 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
it is always applicable and does not exclude any productions of its
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   240
arguments.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   242
\begin{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   243
In mixfix notation the grammar in Example~\ref{PrecedenceEx} can be written
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   244
as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
types exp 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
consts "0"  ::              "exp"  ("0" 9)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
       "+"  :: "[exp,exp] => exp"  ("_ + _" [0,1] 0)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
       "*"  :: "[exp,exp] => exp"  ("_ * _" [3,2] 2)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
       "-"  ::       "exp => exp"  ("- _"   [3]   3)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
Parsing the string \verb!"0 + - 0 + 0"! produces the term {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
  $p$\$($p$\$($m$\$$z$)\$$z$)\$$z$} where {\tt$p =$ Const("+",dummyT)},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
{\tt$m =$ Const("-",dummyT)}, and {\tt$z =$ Const("0",dummyT)}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
The interpretation of \ttindex{_} in a mixfix annotation is always as a {\bf
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
  meta-character}\index{meta-character} which does not represent itself but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
an argument position.  The following characters are also meta-characters:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
'   (   )   /
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
Preceding any character with a quote (\verb$'$) turns it into an ordinary
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
character.  Thus you can write \verb!''! if you really want a single quote.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
The purpose of the other meta-characters is explained in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
\S\ref{PrettyPrinting}.  Remember that in \ML\ strings \verb$\$ is already a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
(different kind of) meta-character.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   269
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   270
\subsection{Types and syntactic categories *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   271
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   272
The precise mapping from types to syntactic categories is defined by the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   273
following function:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   274
\begin{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   275
N(\tau@1\To\tau@2) &=& fun \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   276
N((\tau@1,\dots,\tau@n)ty) &=& ty \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   277
N(\alpha) &=& logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   278
\end{eqnarray*}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   279
Only the outermost type constructor is taken into account and type variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   280
can range over all logical types.  This catches some ill-typed terms (like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   281
$Cons(x,0)$, where $Cons :: [\alpha,\alpha list] \To \alpha list$ and $0 ::
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   282
nat$) but leaves the real work to the type checker.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   283
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   284
In terms of the precedence grammar format introduced in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   285
\S\ref{PrecedenceGrammars}, the declaration
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   286
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   287
consts \(c\) :: "[\(\tau@1\),\dots,\(\tau@n\)]\(\To\tau\)" ("\(\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n\)") [\(p@1\),\dots,\(p@n\)] \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   288
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   289
defines the production
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   290
\[ N(\tau)@p ~~=~~ \alpha@0 ~N(\tau@1)@{p@1}~ \alpha@1~ \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   291
                  ~\alpha@{n-1} ~N(\tau@n)@{p@n}~ \alpha@n
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   292
\]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   293
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   294
\subsection{Copy productions *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   295
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   296
Productions which do not create a new node in the abstract syntax tree are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   297
called {\bf copy productions}.  They must have exactly one nonterminal on
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   298
the right hand side.  The term generated when parsing that nonterminal is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   299
simply passed up as the result of parsing the whole copy production.  In
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   300
Isabelle a copy production is indicated by an empty constant name, i.e.\ by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   301
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   302
consts "" :: \(\tau\)  (\(sy\) \(ps\) \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   303
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   304
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   305
A special kind of copy production is one where, modulo white space, $sy$ is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   306
{\tt"_"}.  It is called a {\bf chain production}.  Chain productions should be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   307
seen as an abbreviation mechanism.  Conceptually, they are removed from the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   308
grammar by adding appropriate new rules.  Precedence information attached to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   309
chain productions is ignored.  The following example demonstrates the effect:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   310
the grammar defined by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   311
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   312
types A,B,C 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   313
consts AB :: "B => A"  ("A _" [10] 517)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   314
       "" :: "C => B"  ("_"   [0]  100)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   315
       x  :: "C"       ("x"          5)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   316
       y  :: "C"       ("y"         15)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   317
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   318
admits {\tt"A y"} but not {\tt"A x"}.  Had the constant in the second
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   319
production been some non-empty string, both {\tt"A y"} and {\tt"A x"} would
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   320
be legal.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   321
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   322
\index{mixfix|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   323
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   324
\section{Lexical conventions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   325
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   326
The lexical analyzer distinguishes the following kinds of tokens: delimiters,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   327
identifiers, unknowns, type variables and type unknowns.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   328
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   329
Delimiters are user-defined, i.e.\ they are extracted from the syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   330
definition.  If $\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$ is a mixfix
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   331
annotation, each $\alpha@i$ is decomposed into substrings
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   332
$\beta@1~\dots~\beta@k$ which are separated by and do not contain
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   333
\bfindex{white space} ( = blanks, tabs, newlines).  Each $\beta@j$ becomes a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   334
delimiter.  Thus a delimiter can be an arbitrary string not containing white
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   335
space.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   336
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   337
The lexical syntax of identifiers and variables ( = unknowns) is defined in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   338
the introductory manual.  Parsing an identifier $f$ generates {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   339
  Free($f$,dummyT)}\index{*dummyT}.  Parsing a variable {\tt?}$v$ generates
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   340
{\tt Var(($u$,$i$),dummyT)} where $i$ is the integer value of the longest
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   341
numeric suffix of $v$ (possibly $0$), and $u$ is the remaining prefix.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   342
Parsing a variable {\tt?}$v{.}i$ generates {\tt Var(($v$,$i$),dummyT)}.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   343
following table covers the four different cases that can arise:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   344
\begin{center}\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   345
\begin{tabular}{cccc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   346
"?v" & "?v.7" & "?v5" & "?v7.5" \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   347
Var(("v",0),$d$) & Var(("v",7),$d$) & Var(("v",5),$d$) & Var(("v7",5),$d$)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   348
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   349
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   350
where $d = {\tt dummyT}$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   351
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   352
In mixfix annotations, \ttindexbold{id}, \ttindexbold{var},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   353
\ttindexbold{tfree} and \ttindexbold{tvar} are the predefined categories of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   354
identifiers, unknowns, type variables and type unknowns, respectively.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   355
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   356
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   357
The lexical analyzer translates input strings to token lists by repeatedly
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   358
taking the maximal prefix of the input string that forms a valid token.  A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   359
maximal prefix that is both a delimiter and an identifier or variable (like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   360
{\tt ALL}) is treated as a delimiter.  White spaces are separators.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   361
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   362
An important consequence of this translation scheme is that delimiters need
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   363
not be separated by white space to be recognized as separate.  If \verb$"-"$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   364
is a delimiter but \verb$"--"$ is not, the string \verb$"--"$ is treated as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   365
two consecutive occurrences of \verb$"-"$.  This is in contrast to \ML\ which
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   366
would treat \verb$"--"$ as a single (undeclared) identifier.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   367
consequence of Isabelle's more liberal scheme is that the same string may be
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   368
parsed in a different way after extending the syntax: after adding
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   369
\verb$"--"$ as a delimiter, the input \verb$"--"$ is treated as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   370
a single occurrence of \verb$"--"$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   371
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   372
\section{Infix operators}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   373
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   374
{\tt Infixl} and {\tt infixr} declare infix operators which associate to the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   375
left and right respectively.  As in \ML, prefixing infix operators with
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   376
\ttindexbold{op} turns them into curried functions.  Infix declarations can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   377
be reduced to mixfix ones as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   378
\begin{center}\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   379
\begin{tabular}{l@{~~$\Longrightarrow$~~}l}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   380
"$c$" ::~$\tau$ (\ttindexbold{infixl} $p$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   381
"op $c$" ::~$\tau$ ("_ $c$ _" [$p$,$p+1$] $p$) \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   382
"$c$" ::~$\tau$ (\ttindexbold{infixr} $p$) &
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   383
"op $c$" ::~$\tau$ ("_ $c$ _" [$p+1$,$p$] $p$)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   384
\end{tabular}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   385
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   386
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   387
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   388
\section{Binders}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   389
A {\bf binder} is a variable-binding constant, such as a quantifier.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   390
The declaration
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   391
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   392
consts \(c\) :: \(\tau\)  (binder \(Q\) \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   393
\end{ttbox}\indexbold{*binder}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   394
introduces a binder $c$ of type $\tau$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   395
which must have the form $(\tau@1\To\tau@2)\To\tau@3$.  Its concrete syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   396
is $Q~x.t$.  A binder is like a generalized quantifier where $\tau@1$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   397
type of the bound variable $x$, $\tau@2$ the type of the body $t$, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   398
$\tau@3$ the type of the whole term.  For example $\forall$ can be declared
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   399
like this:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   400
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   401
consts All :: "('a => o) => o"  (binder "ALL " 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   402
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   403
This allows us to write $\forall x.P$ either as {\tt ALL $x$.$P$} or {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   404
  All(\%$x$.$P$)}; the latter form is for purists only.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   405
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   406
In case $\tau@2 = \tau@3$, nested quantifications can be written as $Q~x@1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   407
\dots x@n.t$.  From a syntactic point of view,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   408
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   409
consts \(c\) :: "\((\tau@1\To\tau@2)\To\tau@3\)"  (binder "\(Q\)" \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   410
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   411
is equivalent to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   412
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   413
consts \(c\)   :: "\((\tau@1\To\tau@2)\To\tau@3\)"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   414
       "\(Q\)" :: "[idts,\(\tau@2\)] => \(\tau@3\)"  ("\(Q\)_.  _" \(p\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   415
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   416
where {\tt idts} is the syntactic category $idts$ defined in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   417
Figure~\ref{MetaLogicSyntax}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   418
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   419
However, there is more to binders than concrete syntax: behind the scenes the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   420
body of the quantified expression has to be converted into a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   421
$\lambda$-abstraction (when parsing) and back again (when printing).  This
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   422
is performed by the translation mechanism, which is discussed below.  For
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   423
binders, the definition of the required translation functions has been
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   424
automated.  Many other syntactic forms, such as set comprehension, require
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   425
special treatment.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   426
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   427
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   428
\section{Parse translations *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   429
\label{Parse-translations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   430
\index{parse translation|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   431
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   432
So far we have pretended that there is a close enough relationship between
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   433
concrete and abstract syntax to allow an automatic translation from one to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   434
the other using the constant name supplied with each production.  In many
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   435
cases this scheme is not powerful enough, especially for constructs involving
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   436
variable bindings.  Therefore the $ML$-section of a theory definition can
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   437
associate constant names with user-defined translation functions by including
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   438
a line
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   439
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   440
val parse_translation = \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   441
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   442
where the right-hand side of this binding must be an \ML-expression of type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   443
\verb$(string * (term list -> term))list$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   444
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   445
After the input string has been translated into a term according to the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   446
syntax definition, there is a second phase in which the term is translated
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   447
using the user-supplied functions in a bottom-up manner.  Given a list $tab$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   448
of the above type, a term $t$ is translated as follows.  If $t$ is not of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   449
form {\tt Const($c$,$\tau$)\$$t@1$\$\dots\$$t@n$}, then $t$ is returned
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   450
unchanged.  Otherwise all $t@i$ are translated into $t@i'$.  Let {\tt $t' =$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   451
  Const($c$,$\tau$)\$$t@1'$\$\dots\$$t@n'$}.  If there is no pair $(c,f)$ in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   452
$tab$, return $t'$.  Otherwise apply $f$ to $[t@1',\dots,t@n']$.  If that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   453
raises an exception, return $t'$, otherwise return the result.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   454
\begin{example}\label{list-enum}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   455
\ML-lists are constructed by {\tt[]} and {\tt::}.  For readability the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   456
list \hbox{\tt$x$::$y$::$z$::[]} can be written \hbox{\tt[$x$,$y$,$z$]}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   457
In Isabelle the two forms of lists are declared as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   458
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   459
types list 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   460
      enum 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   461
arities list :: (term)term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   462
consts "[]" :: "'a list"                   ("[]")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   463
       ":"  :: "['a, 'a list] => 'a list"  (infixr 50)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   464
       enum :: "enum => 'a list"           ("[_]")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   465
       sing :: "'a => enum"                ("_")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   466
       cons :: "['a,enum] => enum"         ("_, _")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   467
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   468
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   469
Because \verb$::$ is already used for type constraints, it is replaced by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   470
\verb$:$ as the infix list constructor.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   471
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   472
In order to allow list enumeration, the new type {\tt enum} is introduced.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   473
Its only purpose is syntactic and hence it does not need an arity, in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   474
contrast to the logical type {\tt list}.  Although \hbox{\tt[$x$,$y$,$z$]} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   475
syntactically legal, it needs to be translated into a term built up from
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   476
\verb$[]$ and \verb$:$.  This is what \verb$make_list$ accomplishes:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   477
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   478
val cons = Const("op :", dummyT);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   479
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   480
fun make_list (Const("sing",_)$e) = cons $ e $ Const("[]", dummyT)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   481
  | make_list (Const("cons",_)$e$es) = cons $ e $ make_list es;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   482
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   483
To hook this translation up to Isabelle's parser, the theory definition needs
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   484
to contain the following $ML$-section:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   485
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   486
ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   487
fun enum_tr[enum] = make_list enum;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   488
val parse_translation = [("enum",enum_tr)]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   489
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   490
This causes \verb!Const("enum",_)$!$t$ to be replaced by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   491
\verb$enum_tr[$$t$\verb$]$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   492
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   493
Of course the definition of \verb$make_list$ should be included in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   494
$ML$-section.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   495
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   496
\begin{example}\label{SET}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   497
  Isabelle represents the set $\{ x \mid P(x) \}$ internally by $Set(\lambda
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   498
  x.P(x))$.  The internal and external forms need separate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   499
constants:\footnote{In practice, the external form typically has a name
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   500
beginning with an {\at} sign, such as {\tt {\at}SET}.  This emphasizes that
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   501
the constant should be used only for parsing/printing.}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   502
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   503
types set 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   504
arities set :: (term)term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   505
consts Set :: "('a => o) => 'a set"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   506
       SET :: "[id,o] => 'a set"  ("\{_ | _\}")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   507
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   508
Parsing {\tt"\{$x$ | $P$\}"} according to this syntax yields the term {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   509
  Const("SET",dummyT) \$ Free("\(x\)",dummyT) \$ \(p\)}, where $p$ is the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   510
result of parsing $P$.  What we need is the term {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   511
  Const("Set",dummyT)\$Abs("$x$",dummyT,$p'$)}, where $p'$ is some
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   512
``abstracted'' version of $p$.  Therefore we define a function
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   513
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   514
fun set_tr[Free(s,T), p] = Const("Set", dummyT) $
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   515
                           Abs(s, T, abstract_over(Free(s,T), p));
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   516
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   517
where \verb$abstract_over: term*term -> term$ is a predefined function such
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   518
that {\tt abstract_over($u$,$t$)} replaces every occurrence of $u$ in $t$ by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   519
a {\tt Bound} variable of the correct index (i.e.\ 0 at top level).  Remember
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   520
that {\tt dummyT} is replaced by the correct types at a later stage (see
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   521
\S\ref{Typing}).  Function {\tt set_tr} is associated with {\tt SET} by
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   522
including the \ML-text
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   523
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   524
val parse_translation = [("SET", set_tr)];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   525
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   526
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   527
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   528
If you want to run the above examples in Isabelle, you should note that an
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   529
$ML$-section needs to contain not just a definition of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   530
\verb$parse_translation$ but also of a variable \verb$print_translation$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   531
purpose of the latter is to reverse the effect of the former during printing;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   532
details are found in \S\ref{Print-translations}.  Hence you need to include
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   533
the line
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   534
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   535
val print_translation = [];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   536
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   537
This is instructive because the terms are then printed out in their internal
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   538
form.  For example the input \hbox{\tt[$x$,$y$,$z$]} is echoed as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   539
\hbox{\tt$x$:$y$:$z$:[]}.  This helps to check that your parse translation is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   540
working correctly.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   541
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   542
%\begin{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   543
%Explicit type constraints disappear with type checking but are still
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   544
%visible to the parse translation functions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   545
%\end{warn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   546
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   547
\index{parse translation|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   548
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   549
\section{Printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   550
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   551
Syntax definitions provide printing information in three distinct ways:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   552
through
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   553
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   554
\item the syntax of the language (as used for parsing),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   555
\item pretty printing information, and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   556
\item print translation functions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   557
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   558
The bare mixfix declarations enable Isabelle to print terms, but the result
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   559
will not necessarily be pretty and may look different from what you expected.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   560
To produce a pleasing layout, you need to read the following sections.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   561
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   562
\subsection{Printing with mixfix declarations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   563
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   564
Let {\tt$t =$ Const($c$,_)\$$t@1$\$\dots\$$t@n$} be a term and let
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   565
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   566
consts \(c\) :: \(\tau\) (\(sy\))
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   567
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   568
be a mixfix declaration where $sy$ is of the form
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   569
$\alpha@0\_\alpha@1\dots\alpha@{n-1}\_\alpha@n$.  Printing $t$ according to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   570
$sy$ means printing the string
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   571
$\alpha@0\beta@1\alpha@1\ldots\alpha@{n-1}\beta@n\alpha@n$, where $\beta@i$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   572
is the result of printing $t@i$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   573
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   574
Note that the system does {\em not\/} insert blanks.  They should be part of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   575
the mixfix syntax if they are required to separate tokens or achieve a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   576
certain layout.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   577
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   578
\subsection{Pretty printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   579
\label{PrettyPrinting}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   580
\index{pretty printing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   581
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   582
In order to format the output, it is possible to embed pretty printing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   583
directives in mixfix annotations.  These directives are ignored during parsing
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   584
and affect only printing.  The characters {\tt(}, {\tt)} and {\tt/} are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   585
interpreted as meta-characters\index{meta-character} when found in a mixfix
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   586
annotation.  Their meaning is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   587
\begin{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   588
\item[~{\tt(}~] Open a block.  A sequence of digits following it is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   589
  interpreted as the \bfindex{indentation} of this block.  It causes the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   590
  output to be indented by $n$ positions if a line break occurs within the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   591
  block.  If {\tt(} is not followed by a digit, the indentation defaults to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   592
  $0$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   593
\item[~{\tt)}~] Close a block.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   594
\item[~\ttindex{/}~] Allow a \bfindex{line break}.  White space immediately
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   595
  following {\tt/} is not printed if the line is broken at this point.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   596
\end{description}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   597
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   598
\subsection{Print translations *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   599
\label{Print-translations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   600
\index{print translation|(}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   601
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   602
Since terms are translated after parsing (see \S\ref{Parse-translations}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   603
there is a similar mechanism to translate them back before printing.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   604
Therefore the $ML$-section of a theory definition can associate constant
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   605
names with user-defined translation functions by including a line
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   606
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   607
val print_translation = \dots
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   608
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   609
where the right-hand side of this binding is again an \ML-expression of type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   610
\verb$(string * (term list -> term))list$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   611
Including a pair $(c,f)$ in this list causes the printer to print
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   612
$f[t@1,\dots,t@n]$ whenever it finds {\tt Const($c$,_)\$$t@1$\$\dots\$$t@n$}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   613
\begin{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   614
Reversing the effect of the parse translation in Example~\ref{list-enum} is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   615
accomplished by the following function:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   616
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   617
fun make_enum (Const("op :",_) $ e $ es) = case es of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   618
        Const("[]",_)  =>  Const("sing",dummyT) $ e
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   619
      | _  =>  Const("enum",dummyT) $ e $ make_enum es;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   620
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   621
It translates \hbox{\tt$x$:$y$:$z$:[]} to \hbox{\tt[$x$,$y$,$z$]}.  However,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   622
if the input does not terminate with an empty list, e.g.\ \hbox{\tt$x$:$xs$},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   623
\verb$make_enum$ raises exception {\tt Match}.  This signals that the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   624
attempted translation has failed and the term should be printed as is.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   625
The connection with Isabelle's pretty printer is established as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   626
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   627
fun enum_tr'[x,xs] = Const("enum",dummyT) $
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   628
                     make_enum(Const("op :",dummyT)$x$xs);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   629
val print_translation = [("op :", enum_tr')];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   630
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   631
This declaration causes the printer to print \hbox{\tt enum_tr'[$x$,$y$]}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   632
whenever it finds \verb!Const("op :",_)$!$x$\verb!$!$y$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   633
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   634
\begin{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   635
  In Example~\ref{SET} we showed how to translate the concrete syntax for set
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   636
  comprehension into the proper internal form.  The string {\tt"\{$x$ |
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   637
    $P$\}"} now becomes {\tt Const("Set",_)\$Abs("$x$",_,$p$)}.  If, however,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   638
  the latter term were printed without translating it back, it would result
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   639
  in {\tt"Set(\%$x$.$P$)"}.  Therefore the abstraction has to be turned back
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   640
  into a term that matches the concrete mixfix syntax:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   641
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   642
fun set_tr'[Abs(x,T,P)] =
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   643
      let val (x',P') = variant_abs(x,T,P)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   644
      in Const("SET",dummyT) $ Free(x',T) $ P' end;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   645
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   646
The function \verb$variant_abs$, a basic term manipulation function, replaces
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   647
the bound variable $x$ by a {\tt Free} variable $x'$ having a unique name.  A
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   648
term produced by {\tt set_tr'} can now be printed according to the concrete
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   649
syntax defined in Example~\ref{SET} above.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   650
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   651
Notice that the application of {\tt set_tr'} fails if the second component of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   652
the argument is not an abstraction, but for example just a {\tt Free}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   653
variable.  This is intentional because it signals to the caller that the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   654
translation is inapplicable.  As a result {\tt Const("Set",_)\$Free("P",_)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   655
prints as {\tt"Set(P)"}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   656
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   657
The full theory extension, including concrete syntax and both translation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   658
functions, has the following form:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   659
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   660
types set 1
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   661
arities set :: (term)term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   662
consts Set :: "('a => o) => 'a set"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   663
       SET :: "[id,o] => 'a set"  ("\{_ | _\}")
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   664
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   665
ML
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   666
fun set_tr[Free(s,T), p] = \dots;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   667
val parse_translation = [("SET", set_tr)];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   668
fun set_tr'[Abs(x,T,P)] = \dots;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   669
val print_translation = [("Set", set_tr')];
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   670
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   671
\end{example}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   672
As during the parse translation process, the types attached to constants
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   673
during print translation are ignored.  Thus {\tt Const("SET",dummyT)} in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   674
{\tt set_tr'} above is acceptable.  The types of {\tt Free}s and {\tt Var}s
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   675
however must be preserved because they may get printed (see {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   676
show_types}).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   677
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   678
\index{print translation|)}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   679
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   680
\subsection{Printing a term}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   681
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   682
Let $tab$ be the set of all string-function pairs of print translations in the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   683
current syntax.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   684
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   685
Terms are printed recursively; print translations are applied top down:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   686
\begin{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   687
\item {\tt Free($x$,_)} is printed as $x$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   688
\item {\tt Var(($x$,$i$),_)} is printed as $x$, if $i = 0$ and $x$ does not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   689
  end with a digit, as $x$ followed by $i$, if $i \neq 0$ and $x$ does not
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   690
  end with a digit, and as {\tt $x$.$i$}, if $x$ ends with a digit.  Thus the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   691
  following cases can arise:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   692
\begin{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   693
{\tt\begin{tabular}{cccc}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   694
\verb$Var(("v",0),_)$ & \verb$Var(("v",7),_)$ & \verb$Var(("v5",0),_)$ \\
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   695
"?v" & "?v7" & "?v5.0"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   696
\end{tabular}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   697
\end{center}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   698
\item {\tt Abs($x@1$,_,Abs($x@2$,_,\dots Abs($x@n$,_,$p$)\dots))}, where $p$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   699
  is not an abstraction, is printed as {\tt \%$y@1\dots y@n$.$P$}, where $P$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   700
  is the result of printing $p$, and the $x@i$ are replaced by $y@i$.  The
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   701
  latter are (possibly new) unique names.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   702
\item {\tt Bound($i$)} is printed as {\tt B.$i$} \footnote{The occurrence of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   703
    such ``loose'' bound variables indicates that either you are trying to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   704
    print a subterm of an abstraction, or there is something wrong with your
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   705
    print translations.}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   706
\item The application {\tt$t =$ Const($c$,_)\$$t@1$\$\dots\$$t@n$} (where
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   707
  $n$ may be $0$!) is printed as follows:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   708
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   709
  If there is a pair $(c,f)$ in $tab$, print $f[t@1,\dots,t@n]$.  If this
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   710
  application raises exception {\tt Match} or there is no pair $(c,f)$ in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   711
  $tab$, let $sy$ be the mixfix annotation associated with $c$.  If there is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   712
  no such $sy$, or if $sy$ does not have exactly $n$ argument positions, $t$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   713
  is printed as an application; otherwise $t$ is printed according to $sy$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   714
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   715
  All other applications are printed as applications.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   716
\end{itemize}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   717
Printing a term {\tt $c$\$$t@1$\$\dots\$$t@n$} as an application means
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   718
printing it as {\tt $s$($s@1$,\dots,$s@n$)}, where $s@i$ is the result of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   719
printing $t@i$.  If $c$ is a {\tt Const}, $s$ is its first argument;
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   720
otherwise $s$ is the result of printing $c$ as described above.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   721
\medskip
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   722
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   723
The printer also inserts parentheses where they are necessary for reasons
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   724
of precedence.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   725
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   726
\section{Identifiers, constants, and type inference *}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   727
\label{Typing}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   728
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   729
There is one final step in the translation from strings to terms that we have
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   730
not covered yet.  It explains how constants are distinguished from {\tt Free}s
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   731
and how {\tt Free}s and {\tt Var}s are typed.  Both issues arise because {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   732
  Free}s and {\tt Var}s are not declared.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   733
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   734
An identifier $f$ that does not appear as a delimiter in the concrete syntax
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   735
can be either a free variable or a constant.  Since the parser knows only
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   736
about those constants which appear in mixfix annotations, it parses $f$ as
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   737
{\tt Free("$f$",dummyT)}, where \ttindex{dummyT} is the predefined dummy {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   738
  typ}.  Although the parser produces these very raw terms, most user
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   739
interface level functions like {\tt goal} type terms according to the given
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   740
theory, say $T$.  In a first step, every occurrence of {\tt Free($f$,_)} or
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   741
{\tt Const($f$,_)} is replaced by {\tt Const($f$,$\tau$)}, provided there is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   742
a constant $f$ of {\tt typ} $\tau$ in $T$.  This means that identifiers are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   743
treated as {\tt Free}s iff they are not declared in the theory.  The types of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   744
the remaining {\tt Free}s (and {\tt Var}s) are inferred as in \ML.  Type
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   745
constraints can be used to remove ambiguities.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   746
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   747
One peculiarity of the current type inference algorithm is that variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   748
with the same name must have the same type, irrespective of whether they are
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   749
schematic, free or bound.  For example, take the first-order formula $f(x) = x
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   750
\land (\forall f.~ f=f)$ where ${=} :: [\alpha{::}term,\alpha]\To o$ and
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   751
$\forall :: (\alpha{::}term\To o)\To o$.  The first conjunct forces
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   752
$x::\alpha{::}term$ and $f::\alpha\To\alpha$, the second one
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   753
$f::\beta{::}term$.  Although the two $f$'s are distinct, they are required to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   754
have the same type.  Unifying $\alpha\To\alpha$ and $\beta{::}term$ fails
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   755
because, in first-order logic, function types are not in class $term$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   756
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   757
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   758
\section{Putting it all together}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   759
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   760
Having discussed the individual building blocks of a logic definition, it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   761
remains to be shown how they fit together.  In particular we need to say how
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   762
an object-logic syntax is hooked up to the meta-logic.  Since all theorems
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   763
must conform to the syntax for $prop$ (see Figure~\ref{MetaLogicSyntax}),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   764
that syntax has to be extended with the object-level syntax.  Assume that the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   765
syntax of your object-logic defines a category $o$ of formulae.  These
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   766
formulae can now appear in axioms and theorems wherever $prop$ does if you
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   767
add the production
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   768
\[ prop ~=~ form.  \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   769
More precisely, you need a coercion from formulae to propositions:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   770
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   771
Base = Pure +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   772
types o 0
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   773
arities o :: logic
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   774
consts Trueprop :: "o => prop"  ("_"  5)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   775
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   776
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   777
The constant {\tt Trueprop} (the name is arbitrary) acts as an invisible
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   778
coercion function.  Assuming this definition resides in a file {\tt base.thy},
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   779
you have to load it with the command {\tt use_thy"base"}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   780
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   781
One of the simplest nontrivial logics is {\em minimal logic} of
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   782
implication.  Its definition in Isabelle needs no advanced features but
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   783
illustrates the overall mechanism quite nicely:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   784
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   785
Hilbert = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   786
consts "-->" :: "[o,o] => o"  (infixr 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   787
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   788
K   "P --> Q --> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   789
S   "(P --> Q --> R) --> (P --> Q) --> P --> R"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   790
MP  "[| P --> Q; P |] ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   791
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   792
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   793
After loading this definition you can start to prove theorems in this logic:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   794
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   795
goal Hilbert.thy "P --> P";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   796
{\out Level 0}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   797
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   798
{\out  1.  P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   799
by (resolve_tac [Hilbert.MP] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   800
{\out Level 1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   801
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   802
{\out  1.  ?P --> P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   803
{\out  2.  ?P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   804
by (resolve_tac [Hilbert.MP] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   805
{\out Level 2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   806
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   807
{\out  1.  ?P1 --> ?P --> P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   808
{\out  2.  ?P1}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   809
{\out  3.  ?P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   810
by (resolve_tac [Hilbert.S] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   811
{\out Level 3}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   812
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   813
{\out  1.  P --> ?Q2 --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   814
{\out  2.  P --> ?Q2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   815
by (resolve_tac [Hilbert.K] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   816
{\out Level 4}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   817
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   818
{\out  1.  P --> ?Q2}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   819
by (resolve_tac [Hilbert.K] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   820
{\out Level 5}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   821
{\out P --> P}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   822
{\out No subgoals!}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   823
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   824
As you can see, this Hilbert-style formulation of minimal logic is easy to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   825
define but difficult to use.  The following natural deduction formulation is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   826
far preferable:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   827
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   828
MinI = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   829
consts "-->" :: "[o,o] => o"  (infixr 10)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   830
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   831
impI  "(P ==> Q) ==> P --> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   832
impE  "[| P --> Q; P |] ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   833
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   834
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   835
Note, however, that although the two systems are equivalent, this fact cannot
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   836
be proved within Isabelle: {\tt S} and {\tt K} can be derived in \verb$MinI$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   837
(exercise!), but {\tt impI} cannot be derived in \verb!Hilbert!.  The reason
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   838
is that {\tt impI} is only an {\em admissible} rule in \verb!Hilbert!,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   839
something that can only be shown by induction over all possible proofs in
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   840
\verb!Hilbert!.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   841
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   842
It is a very simple matter to extend minimal logic with falsity:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   843
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   844
MinIF = MinI +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   845
consts False :: "o"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   846
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   847
FalseE  "False ==> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   848
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   849
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   850
On the other hand, we may wish to introduce conjunction only:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   851
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   852
MinC = Base +
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   853
consts "&" :: "[o,o] => o"  (infixr 30)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   854
rules
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   855
conjI  "[| P; Q |] ==> P & Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   856
conjE1 "P & Q ==> P"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   857
conjE2 "P & Q ==> Q"
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   858
end
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   859
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   860
And if we want to have all three connectives together, we define:
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   861
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   862
MinIFC = MinIF + MinC
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   863
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   864
Now we can prove mixed theorems like
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   865
\begin{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   866
goal MinIFC.thy "P & False --> Q";
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   867
by (resolve_tac [MinI.impI] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   868
by (dresolve_tac [MinC.conjE2] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   869
by (eresolve_tac [MinIF.FalseE] 1);
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   870
\end{ttbox}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   871
Try this as an exercise!