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