author  wenzelm 
Tue, 07 Oct 1997 17:06:05 +0200  
changeset 3801  5ba459e15dd7 
parent 3694  fe7b812837ad 
child 3802  f13d5b840858 
permissions  rwrr 
320  1 
%% $Id$ 
2 
\chapter{Defining Logics} \label{DefiningLogics} 

3 
This chapter explains how to define new formal systems  in particular, 

4 
their concrete syntax. While Isabelle can be regarded as a theorem prover 

5 
for set theory, higherorder logic or the sequent calculus, its 

6 
distinguishing feature is support for the definition of new logics. 

7 

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  10 
\iflabelundefined{sec:definingtheories}{{\em Introduction to Isabelle}}% 
11 
{\S\ref{sec:definingtheories}}. That material, together with the theory 

12 
files provided in the examples directories, should suffice for all simple 

13 
applications. The easiest way to define a new theory is by modifying a 

14 
copy of an existing theory. 

15 

16 
This chapter documents the metalogic syntax, mixfix declarations and 

17 
pretty printing. The extended examples in \S\ref{sec:min_logics} 

18 
demonstrate the logical aspects of the definition of theories. 

19 

20 

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  23 

24 
A contextfree grammar contains a set of {\bf nonterminal symbols}, a set of 

25 
{\bf terminal symbols} and a set of {\bf productions}\index{productions}. 

26 
Productions have the form ${A=\gamma}$, where $A$ is a nonterminal and 

27 
$\gamma$ is a string of terminals and nonterminals. One designated 

28 
nonterminal is called the {\bf start symbol}. The language defined by the 

29 
grammar consists of all strings of terminals that can be derived from the 

30 
start symbol by applying productions as rewrite rules. 

31 

32 
The syntax of an Isabelle logic is specified by a {\bf priority 

33 
grammar}.\index{priorities} Each nonterminal is decorated by an integer 

34 
priority, as in~$A^{(p)}$. A nonterminal $A^{(p)}$ in a derivation may be 

35 
rewritten using a production $A^{(q)} = \gamma$ only if~$p \le q$. Any 

36 
priority grammar can be translated into a normal context free grammar by 

37 
introducing new nonterminals and productions. 

38 

39 
Formally, a set of context free productions $G$ induces a derivation 

40 
relation $\longrightarrow@G$. Let $\alpha$ and $\beta$ denote strings of 

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  43 
if and only if $G$ contains some production $A^{(q)}=\gamma$ for~$p \le q$. 
44 

45 
The following simple grammar for arithmetic expressions demonstrates how 

46 
binding power and associativity of operators can be enforced by priorities. 

47 
\begin{center} 

48 
\begin{tabular}{rclr} 

49 
$A^{(9)}$ & = & {\tt0} \\ 

50 
$A^{(9)}$ & = & {\tt(} $A^{(0)}$ {\tt)} \\ 

51 
$A^{(0)}$ & = & $A^{(0)}$ {\tt+} $A^{(1)}$ \\ 

52 
$A^{(2)}$ & = & $A^{(3)}$ {\tt*} $A^{(2)}$ \\ 

53 
$A^{(3)}$ & = & {\tt} $A^{(3)}$ 

54 
\end{tabular} 

55 
\end{center} 

56 
The choice of priorities determines that {\tt } binds tighter than {\tt *}, 

57 
which binds tighter than {\tt +}. Furthermore {\tt +} associates to the 

58 
left and {\tt *} to the right. 

59 

60 
For clarity, grammars obey these conventions: 

61 
\begin{itemize} 

62 
\item All priorities must lie between~0 and \ttindex{max_pri}, which is a 

63 
some fixed integer. Sometimes {\tt max_pri} is written as $\infty$. 

64 
\item Priority 0 on the righthand side and priority \ttindex{max_pri} on 

65 
the lefthand side may be omitted. 

66 
\item The production $A^{(p)} = \alpha$ is written as $A = \alpha~(p)$; the 

67 
priority of the lefthand 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  70 
\item Repetition is indicated by dots~(\dots) in an informal but obvious 
71 
way. 

72 
\end{itemize} 

73 

74 
Using these conventions and assuming $\infty=9$, the grammar 

75 
takes the form 

76 
\begin{center} 

77 
\begin{tabular}{rclc} 

78 
$A$ & = & {\tt0} & \hspace*{4em} \\ 

79 
& $$ & {\tt(} $A$ {\tt)} \\ 

80 
& $$ & $A$ {\tt+} $A^{(1)}$ & (0) \\ 

81 
& $$ & $A^{(3)}$ {\tt*} $A^{(2)}$ & (2) \\ 

82 
& $$ & {\tt} $A^{(3)}$ & (3) 

83 
\end{tabular} 

84 
\end{center} 

85 
\index{priority grammars)} 

86 

87 

88 
\begin{figure} 

89 
\begin{center} 

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  97 
&$$& $prop^{(2)}$ {\tt ==>} $prop^{(1)}$ & (1) \\ 
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  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  107 
&$$& {\tt \%} $pttrns$ {\tt.} $any^{(3)}$ & (3) \\\\ 
320  108 
$idts$ &=& $idt$ ~~$$~~ $idt^{(1)}$ $idts$ \\\\ 
109 
$idt$ &=& $id$ ~~$$~~ {\tt(} $idt$ {\tt)} \\ 

110 
&$$& $id$ {\tt ::} $type$ & (0) \\\\ 

3694  111 
$pttrns$ &=& $pttrn$ ~~$$~~ $pttrn^{(1)}$ $pttrns$ \\\\ 
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  116 
&$$& $id$ ~~$$~~ $type^{(\infty)}$ $id$ 
117 
~~$$~~ {\tt(} $type$ {\tt,} \dots {\tt,} $type$ {\tt)} $id$ \\ 

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  120 
$sort$ &=& $id$ ~~$$~~ {\tt\ttlbrace\ttrbrace} 
121 
~~$$~~ {\tt\ttlbrace} $id$ {\tt,} \dots {\tt,} $id$ {\tt\ttrbrace} 

122 
\end{tabular} 

123 
\index{*PROP symbol} 

124 
\index{*== symbol}\index{*=?= symbol}\index{*==> symbol} 

125 
\index{*:: symbol}\index{*=> symbol} 

332  126 
\index{sort constraints} 
127 
%the index command: a percent is permitted, but braces must match! 

320  128 
\index{%@{\tt\%} symbol} 
129 
\index{{}@{\tt\ttlbrace} symbol}\index{{}@{\tt\ttrbrace} symbol} 

130 
\index{*[ symbol}\index{*] symbol} 

131 
\index{*"!"! symbol} 

132 
\index{*"[" symbol} 

133 
\index{*""] symbol} 

134 
\end{center} 

135 
\caption{Metalogic syntax}\label{fig:pure_gram} 

136 
\end{figure} 

137 

138 

139 
\section{The Pure syntax} \label{sec:basic_syntax} 

140 
\index{syntax!Pure(} 

141 

142 
At the root of all objectlogics lies the theory \thydx{Pure}. It 

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  145 
\iflabelundefined{sec:forward}{{\em Introduction to Isabelle}}% 
146 
{\S\ref{sec:forward}}. A more precise description using a priority grammar 

147 
appears in Fig.\ts\ref{fig:pure_gram}. It defines the following 

148 
nonterminals: 

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 metalogic. 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  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 objectlogic; its definition 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset

162 
% introduces a metalevel predicate for each judgement form. 
320  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  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  169 

170 
\item[\ndxbold{pttrn}, \ndxbold{pttrns}] denote patterns for 

171 
abstraction, cases etc. Initially the same as $idt$ and $idts$, 

172 
these are indetended to be augmented by user extensions. 

320  173 

174 
\item[\ndxbold{type}] denotes types of the metalogic. 

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 metalevel sorts. 
320  177 
\end{ttdescription} 
178 

179 
\begin{warn} 

180 
In {\tt idts}, note that \verbx::nat y is parsed as \verbx::(nat y), 

181 
treating {\tt y} like a type constructor applied to {\tt nat}. The 

182 
likely result is an error message. To avoid this interpretation, use 

183 
parentheses and write \verb(x::nat) y. 

332  184 
\index{type constraints}\index{*:: symbol} 
320  185 

186 
Similarly, \verbx::nat y::nat is parsed as \verbx::(nat y::nat) and 

187 
yields an error. The correct form is \verb(x::nat) (y::nat). 

188 
\end{warn} 

189 

452  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  194 
\verb!x<(y::nat)!. 
195 
\end{warn} 

320  196 

867  197 
\subsection{Logical types and default syntax}\label{logicaltypes} 
198 
\index{lambda calc@$\lambda$calculus} 

199 

200 
Isabelle's representation of mathematical languages is based on the 

201 
simply typed $\lambda$calculus. All logical types, namely those of 

202 
class \cldx{logic}, are automatically equipped with a basic syntax of 

203 
types, identifiers, variables, parentheses, $\lambda$abstraction and 

204 
application. 

205 
\begin{warn} 

206 
Isabelle combines the syntaxes for all types of class \cldx{logic} by 

207 
mapping all those types to the single nonterminal $logic$. Thus all 

208 
productions of $logic$, in particular $id$, $var$ etc, become available. 

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  212 
\subsection{Lexical matters} 
213 
The parser does not process input strings directly. It operates on token 

214 
lists provided by Isabelle's \bfindex{lexer}. There are two kinds of 

215 
tokens: \bfindex{delimiters} and \bfindex{name tokens}. 

216 

217 
\index{reserved words} 

218 
Delimiters can be regarded as reserved words of the syntax. You can 

219 
add new ones when extending theories. In Fig.\ts\ref{fig:pure_gram} they 

220 
appear in typewriter font, for example {\tt ==}, {\tt =?=} and 

221 
{\tt PROP}\@. 

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  230 
\begin{eqnarray*} 
231 
id & = & letter~quasiletter^* \\ 

232 
var & = & \mbox{\tt ?}id ~~~~ \mbox{\tt ?}id\mbox{\tt .}nat \\ 

233 
tid & = & \mbox{\tt '}id \\ 

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  238 
letter & = & \mbox{one of {\tt a}\dots {\tt z} {\tt A}\dots {\tt Z}} \\ 
239 
digit & = & \mbox{one of {\tt 0}\dots {\tt 9}} \\ 

240 
quasiletter & = & letter ~~~~ digit ~~~~ \mbox{\tt _} ~~~~ \mbox{\tt '} \\ 

241 
nat & = & digit^+ 

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  257 
A \ndxbold{var} or \ndxbold{tvar} describes an unknown, which is internally 
258 
a pair of base name and index (\ML\ type \mltydx{indexname}). These 

259 
components are either separated by a dot as in {\tt ?x.1} or {\tt ?x7.3} or 

260 
run together as in {\tt ?x1}. The latter form is possible if the base name 

261 
does not end with digits. If the index is 0, it may be dropped altogether: 

262 
{\tt ?x} abbreviates both {\tt ?x0} and {\tt ?x.0}. 

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 metalogic. 
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset

265 
Objectlogics 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  267 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset

268 
\medskip 
320  269 
Although name tokens are returned from the lexer rather than the parser, it 
270 
is more logical to regard them as nonterminals. Delimiters, however, are 

271 
terminals; they are just syntactic sugar and contribute nothing to the 

272 
abstract syntax tree. 

273 

274 

3108  275 
\subsection{*Inspecting the syntax} \label{pg:print_syn} 
320  276 
\begin{ttbox} 
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  279 
Syntax.print_syntax : Syntax.syntax > unit 
280 
Syntax.print_gram : Syntax.syntax > unit 

281 
Syntax.print_trans : Syntax.syntax > unit 

282 
\end{ttbox} 

283 
The abstract type \mltydx{Syntax.syntax} allows manipulation of syntaxes 

284 
in \ML. You can display values of this type by calling the following 

285 
functions: 

286 
\begin{ttdescription} 

287 
\item[\ttindexbold{syn_of} {\it thy}] returns the syntax of the Isabelle 

288 
theory~{\it thy} as an \ML\ value. 

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  293 
\item[\ttindexbold{Syntax.print_syntax} {\it syn}] shows virtually all 
294 
information contained in the syntax {\it syn}. The displayed output can 

295 
be large. The following two functions are more selective. 

296 

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  299 
discussed below. 
300 

301 
\item[\ttindexbold{Syntax.print_trans} {\it syn}] shows the translation 

302 
part of~{\it syn}, namely the constants, parse/print macros and 

303 
parse/print translations. 

304 
\end{ttdescription} 

305 

306 
Let us demonstrate these functions by inspecting Pure's syntax. Even that 

307 
is too verbose to display in full. 

308 
\begin{ttbox}\index{*Pure theory} 

309 
Syntax.print_syntax (syn_of Pure.thy); 

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  312 
{\out prods:} 
313 
{\out type = tid (1000)} 

314 
{\out type = tvar (1000)} 

315 
{\out type = id (1000)} 

316 
{\out type = tid "::" sort[0] => "_ofsort" (1000)} 

317 
{\out type = tvar "::" sort[0] => "_ofsort" (1000)} 

318 
{\out \vdots} 

319 
\ttbreak 

3108  320 
{\out print modes: "symbols" "xterm"} 
320  321 
{\out consts: "_K" "_appl" "_aprop" "_args" "_asms" "_bigimpl" \dots} 
322 
{\out parse_ast_translation: "_appl" "_bigimpl" "_bracket"} 

323 
{\out "_idtyp" "_lambda" "_tapp" "_tappl"} 

324 
{\out parse_rules:} 

325 
{\out parse_translation: "!!" "_K" "_abs" "_aprop"} 

326 
{\out print_translation: "all"} 

327 
{\out print_rules:} 

328 
{\out print_ast_translation: "==>" "_abs" "_idts" "fun"} 

329 
\end{ttbox} 

330 

332  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  333 
refers to syntactic translations and macro expansion. Here is an 
334 
explanation of the various sections. 

335 
\begin{description} 

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  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 objectlogics (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  343 

344 
\item[{\tt prods}] lists the \rmindex{productions} of the priority grammar. 

345 
The nonterminal $A^{(n)}$ is rendered in {\sc ascii} as {\tt $A$[$n$]}. 

346 
Each delimiter is quoted. Some productions are shown with {\tt =>} and 

347 
an attached string. These strings later become the heads of parse 

348 
trees; they also play a vital role when terms are printed (see 

349 
\S\ref{sec:asts}). 

350 

351 
Productions with no strings attached are called {\bf copy 

352 
productions}\indexbold{productions!copy}. Their righthand side must 

353 
have exactly one nonterminal symbol (or name token). The parser does 

354 
not create a new parse tree node for copy productions, but simply 

355 
returns the parse tree of the righthand symbol. 

356 

357 
If the righthand side consists of a single nonterminal with no 

358 
delimiters, then the copy production is called a {\bf chain 

359 
production}. Chain productions act as abbreviations: 

360 
conceptually, they are removed from the grammar by adding new 

361 
productions. Priority information attached to chain productions is 

362 
ignored; only the dummy value $1$ is displayed. 

3108  363 

364 
\item[\ttindex{print_modes}] lists the alternative print modes 

365 
provided by this syntax (see \S\ref{sec:prmodes}). 

320  366 

367 
\item[{\tt consts}, {\tt parse_rules}, {\tt print_rules}] 

368 
relate to macros (see \S\ref{sec:macros}). 

369 

370 
\item[{\tt parse_ast_translation}, {\tt print_ast_translation}] 

371 
list sets of constants that invoke translation functions for abstract 

372 
syntax trees. Section \S\ref{sec:asts} below discusses this obscure 

373 
matter.\index{constants!for translations} 

374 

375 
\item[{\tt parse_translation}, {\tt print_translation}] list sets 

376 
of constants that invoke translation functions for terms (see 

377 
\S\ref{sec:tr_funs}). 

378 
\end{description} 

379 
\index{syntax!Pure)} 

380 

381 

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  384 

385 
When defining a theory, you declare new constants by giving their names, 

386 
their type, and an optional {\bf mixfix annotation}. Mixfix annotations 

387 
allow you to extend Isabelle's basic $\lambda$calculus syntax with 

388 
readable notation. They can express any contextfree priority grammar. 

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  391 

392 
A mixfix annotation defines a production of the priority grammar. It 

393 
describes the concrete syntax, the translation to abstract syntax, and the 

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  396 

397 
\subsection{The general mixfix form} 

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  401 
\begin{center} 
402 
{\tt $c$ ::\ "$\sigma$" ("$template$" $ps$ $p$)} 

403 
\end{center} 

332  404 
This constant declaration and mixfix annotation are interpreted as follows: 
320  405 
\begin{itemize}\index{productions} 
406 
\item The string {\tt $c$} is the name of the constant associated with the 

407 
production; unless it is a valid identifier, it must be enclosed in 

408 
quotes. If $c$ is empty (given as~{\tt ""}) then this is a copy 

409 
production.\index{productions!copy} Otherwise, parsing an instance of the 

410 
phrase $template$ generates the \AST{} {\tt ("$c$" $a@1$ $\ldots$ 

411 
$a@n$)}, where $a@i$ is the \AST{} generated by parsing the $i$th 

412 
argument. 

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 nonempty, 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  416 

417 
\item The string $template$ specifies the righthand side of 

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  420 
where each occurrence of {\tt_} denotes an argument position and 
421 
the~$w@i$ do not contain~{\tt _}. (If you want a literal~{\tt _} in 

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  424 
\rmindex{pretty printing} annotations (see below). 
425 

426 
\item The type $\sigma$ specifies the production's nonterminal symbols 

427 
(or name tokens). If $template$ is of the form above then $\sigma$ 

428 
must be a function type with at least~$n$ argument positions, say 

429 
$\sigma = [\tau@1, \dots, \tau@n] \To \tau$. Nonterminal symbols are 

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  432 

433 
\item The optional list~$ps$ may contain at most $n$ integers, say {\tt 

434 
[$p@1$, $\ldots$, $p@m$]}, where $p@i$ is the minimal 

435 
priority\indexbold{priorities} required of any phrase that may appear 

436 
as the $i$th argument. Missing priorities default to~0. 

437 

438 
\item The integer $p$ is the priority of this production. If omitted, it 

439 
defaults to the maximal priority. 

440 
Priorities range between 0 and \ttindexbold{max_pri} (= 1000). 

441 
\end{itemize} 

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 
builtin 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  482 
the production's righthand side is fully bracketed, as in 
483 
\verb"if _ then _ else _ fi". 

320  484 

485 
Omitting the mixfix annotation completely, as in {\tt $c$ ::\ "$\sigma$"}, 

486 
is sensible only if~$c$ is an identifier. Otherwise you will be unable to 

487 
write terms involving~$c$. 

488 

489 

490 
\subsection{Example: arithmetic expressions} 

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  493 
declarations encoding the priority grammar from 
494 
\S\ref{sec:priority_grammars}: 

495 
\begin{ttbox} 

3108  496 
ExpSyntax = Pure + 
320  497 
types 
498 
exp 

864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset

499 
syntax 
1387  500 
"0" :: exp ("0" 9) 
501 
"+" :: [exp, exp] => exp ("_ + _" [0, 1] 0) 

502 
"*" :: [exp, exp] => exp ("_ * _" [3, 2] 2) 

503 
"" :: exp => exp (" _" [3] 3) 

320  504 
end 
505 
\end{ttbox} 

3108  506 
If you put this into a file {\tt ExpSyntax.thy} and load it via {\tt 
507 
use_thy"ExpSyntax"}, you can run some tests: 

320  508 
\begin{ttbox} 
3108  509 
val read_exp = Syntax.test_read (syn_of ExpSyntax.thy) "exp"; 
320  510 
{\out val it = fn : string > unit} 
511 
read_exp "0 * 0 * 0 * 0 + 0 + 0 + 0"; 

512 
{\out tokens: "0" "*" "0" "*" "0" "*" "0" "+" "0" "+" "0" "+" "0"} 

513 
{\out raw: ("+" ("+" ("+" ("*" "0" ("*" "0" ("*" "0" "0"))) "0") "0") "0")} 

514 
{\out \vdots} 

515 
read_exp "0 +  0 + 0"; 

516 
{\out tokens: "0" "+" "" "0" "+" "0"} 

517 
{\out raw: ("+" ("+" "0" ("" "0")) "0")} 

518 
{\out \vdots} 

519 
\end{ttbox} 

520 
The output of \ttindex{Syntax.test_read} includes the token list ({\tt 

521 
tokens}) and the raw \AST{} directly derived from the parse tree, 

522 
ignoring parse \AST{} translations. The rest is tracing information 

523 
provided by the macro expander (see \S\ref{sec:macros}). 

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  527 
\begin{ttbox} 
3108  528 
Syntax.print_gram (syn_of ExpSyntax.thy); 
320  529 
{\out exp = "0" => "0" (9)} 
530 
{\out exp = exp[0] "+" exp[1] => "+" (0)} 

531 
{\out exp = exp[3] "*" exp[2] => "*" (2)} 

532 
{\out exp = "" exp[3] => "" (3)} 

533 
\end{ttbox} 

534 

3108  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  537 
does not provide for identifiers or paranthesized expressions. 
538 
Normally you would also want to add the declaration {\tt arities 

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  541 
grammar. 
320  542 

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  545 
annotations. This string specifies a list of parsing and printing 
546 
directives: delimiters\index{delimiters}, arguments, spaces, blocks of 

547 
indentation and line breaks. These are encoded by the following character 

548 
sequences: 

549 
\index{pretty printing(} 

550 
\begin{description} 

551 
\item[~$d$~] is a delimiter, namely a nonempty sequence of characters 

552 
other than the special characters {\tt _}, {\tt(}, {\tt)} and~{\tt/}. 

553 
Even these characters may appear if escaped; this means preceding it with 

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  557 

558 
\item[~{\tt_}~] is an argument position, which stands for a nonterminal symbol 

559 
or name token. 

560 

561 
\item[~$s$~] is a nonempty sequence of spaces for printing. This and the 

562 
following specifications do not affect parsing at all. 

563 

564 
\item[~{\tt(}$n$~] opens a pretty printing block. The optional number $n$ 

565 
specifies how much indentation to add when a line break occurs within the 

566 
block. If {\tt(} is not followed by digits, the indentation defaults 

567 
to~0. 

568 

569 
\item[~{\tt)}~] closes a pretty printing block. 

570 

571 
\item[~{\tt//}~] forces a line break. 

572 

573 
\item[~{\tt/}$s$~] allows a line break. Here $s$ stands for the string of 

574 
spaces (zero or more) right after the {\tt /} character. These spaces 

575 
are printed if the break is not taken. 

576 
\end{description} 

577 
For example, the template {\tt"(_ +/ _)"} specifies an infix operator. 

578 
There are two argument positions; the delimiter~{\tt+} is preceded by a 

579 
space and followed by a space or line break; the entire phrase is a pretty 

580 
printing block. Other examples appear in Fig.\ts\ref{fig:set_trans} below. 

581 
Isabelle's pretty printer resembles the one described in 

582 
Paulson~\cite{paulson91}. 

583 

584 
\index{pretty printing)} 

585 

586 

587 
\subsection{Infixes} 

588 
\indexbold{infixes} 

589 

3108  590 
Infix operators associating to the left or right can be declared using 
591 
{\tt infixl} or {\tt infixr}. Basically, the form {\tt $c$ ::\ 

592 
$\sigma$ (infixl $p$)} abbreviates the mixfix declarations 

320  593 
\begin{ttbox} 
1387  594 
"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p\), \(p+1\)] \(p\)) 
595 
"op \(c\)" :: \(\sigma\) ("op \(c\)") 

320  596 
\end{ttbox} 
1387  597 
and {\tt $c$ ::\ $\sigma$ (infixr $p$)} abbreviates the mixfix declarations 
320  598 
\begin{ttbox} 
1387  599 
"op \(c\)" :: \(\sigma\) ("(_ \(c\)/ _)" [\(p+1\), \(p\)] \(p\)) 
600 
"op \(c\)" :: \(\sigma\) ("op \(c\)") 

320  601 
\end{ttbox} 
602 
The infix operator is declared as a constant with the prefix {\tt op}. 

603 
Thus, prefixing infixes with \sdx{op} makes them behave like ordinary 

604 
function symbols, as in \ML. Special characters occurring in~$c$ must be 

605 
escaped, as in delimiters, using a single quote. 

606 

3108  607 
A slightly more general form of infix declarations allows constant 
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  610 
an example consider: 
611 
\begin{ttbox} 

612 
and :: [bool, bool] => bool (infixr "&" 35) 

613 
\end{ttbox} 

614 
The internal constant name will then be just \texttt{and}, without any 

615 
\texttt{op} prefixed. 

616 

320  617 

618 
\subsection{Binders} 

619 
\indexbold{binders} 

620 
\begingroup 

621 
\def\Q{{\cal Q}} 

622 
A {\bf binder} is a variablebinding construct such as a quantifier. The 

623 
constant declaration 

624 
\begin{ttbox} 

1387  625 
\(c\) :: \(\sigma\) (binder "\(\Q\)" [\(pb\)] \(p\)) 
320  626 
\end{ttbox} 
627 
introduces a constant~$c$ of type~$\sigma$, which must have the form 

628 
$(\tau@1 \To \tau@2) \To \tau@3$. Its concrete syntax is $\Q~x.P$, where 

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  632 
in $\Q$ must be escaped using a single quote. 
320  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  635 
\begin{ttbox} 
3098  636 
\(c\)\hskip3pt :: (\(\tau@1\) => \(\tau@2\)) => \(\tau@3\) 
637 
"\(\Q\)" :: [idts, \(\tau@2\)] => \(\tau@3\) ("(3\(\Q\)_./ _)" [0, \(pb\)] \(p\)) 

320  638 
\end{ttbox} 
639 
Here \ndx{idts} is the nonterminal symbol for a list of identifiers with 

332  640 
\index{type constraints} 
320  641 
optional type constraints (see Fig.\ts\ref{fig:pure_gram}). The 
642 
declaration also installs a parse translation\index{translations!parse} 

643 
for~$\Q$ and a print translation\index{translations!print} for~$c$ to 

644 
translate between the internal and external forms. 

645 

646 
A binder of type $(\sigma \To \tau) \To \tau$ can be nested by giving a 

647 
list of variables. The external form $\Q~x@1~x@2 \ldots x@n. P$ 

648 
corresponds to the internal form 

649 
\[ c(\lambda x@1. c(\lambda x@2. \ldots c(\lambda x@n. P) \ldots)). \] 

650 

651 
\medskip 

652 
For example, let us declare the quantifier~$\forall$:\index{quantifiers} 

653 
\begin{ttbox} 

1387  654 
All :: ('a => o) => o (binder "ALL " 10) 
320  655 
\end{ttbox} 
656 
This lets us write $\forall x.P$ as either {\tt All(\%$x$.$P$)} or {\tt ALL 

657 
$x$.$P$}. When printing, Isabelle prefers the latter form, but must fall 

658 
back on ${\tt All}(P)$ if $P$ is not an abstraction. Both $P$ and {\tt ALL 

659 
$x$.$P$} have type~$o$, the type of formulae, while the bound variable 

660 
can be polymorphic. 

661 
\endgroup 

662 

663 
\index{mixfix declarations)} 

664 

3108  665 

666 
\section{*Alternative print modes} \label{sec:prmodes} 

667 
\index{print modes(} 

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  671 
print modes (with precedence from left to right) are determined by a 
672 
reference variable. 

673 
\begin{ttbox}\index{*print_mode} 

674 
print_mode: string list ref 

675 
\end{ttbox} 

676 
Initially this may already contain some print mode identifiers, 

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  679 
modes relative to the current value. 
680 

681 
Any \ML{} string is a legal print mode identifier, without any 

682 
predeclaration required. The following names should be considered 

683 
reserved, though: \texttt{""} (yes, the empty string), 

684 
\texttt{symbols}, \texttt{latex}, \texttt{xterm}. 

685 

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  688 
conceptually just concatenated from left to right, with the standard 
689 
syntax output table always coming last as default. Thus mixfix 

690 
productions of preceding modes in the list may override those of later 

691 
ones. Also note that token translations are always relative to some 

692 
print mode (see \S\ref{sec:tok_tr}). 

693 

694 
\medskip The canonical application of print modes is optional printing 

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 reuse Isabelle's advanced 
3108  697 
$\lambda$term printing mechanisms to generate completely different 
3228  698 
output, say for interfacing external tools like \rmindex{model 
699 
checkers} (see also \texttt{HOL/Modelcheck}). 

3108  700 

701 
\index{print modes)} 

702 

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  718 
If an ambiguity can be resolved by type inference the following 
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  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  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  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  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} 
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset

738 
{\out Warning: Ambiguous input "..."} 
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset

739 
{\out produces the following parse trees:} 
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset

740 
{\out ...} 
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset

741 
{\out Error: More than one term is type correct:} 
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset

742 
{\out ...} 
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  750 

751 
\section{Example: some minimal logics} \label{sec:min_logics} 

752 
\index{examples!of logic definitions} 

753 

754 
This section presents some examples that have a simple syntax. They 

755 
demonstrate how to define new objectlogics from scratch. 

756 

711
bb868a30e66f
updated remarks about grammar; added section about ambiguities
clasohm
parents:
452
diff
changeset

757 
First we must define how an objectlogic 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 
metalogic. 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  760 
objectlevel syntax. Assume that the syntax of your objectlogic defines a 
864
d63b111b917a
quite a lot of minor and major revisions (inspecting theories, read_axm,
wenzelm
parents:
711
diff
changeset

761 
metatype~\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  767 
\begin{ttbox} 
768 
Base = Pure + 

769 
types 

770 
o 

771 
arities 

772 
o :: logic 

773 
consts 

1387  774 
Trueprop :: o => prop ("_" 5) 
320  775 
end 
776 
\end{ttbox} 

777 
The constant \cdx{Trueprop} (the name is arbitrary) acts as an invisible 

332  778 
coercion function. Assuming this definition resides in a file {\tt Base.thy}, 
320  779 
you have to load it with the command {\tt use_thy "Base"}. 
780 

781 
One of the simplest nontrivial logics is {\bf minimal logic} of 

782 
implication. Its definition in Isabelle needs no advanced features but 

783 
illustrates the overall mechanism nicely: 

784 
\begin{ttbox} 

785 
Hilbert = Base + 

786 
consts 

1387  787 
">" :: [o, o] => o (infixr 10) 
320  788 
rules 
789 
K "P > Q > P" 

790 
S "(P > Q > R) > (P > Q) > P > R" 

791 
MP "[ P > Q; P ] ==> Q" 

792 
end 

793 
\end{ttbox} 

332  794 
After loading this definition from the file {\tt Hilbert.thy}, you can 
320  795 
start to prove theorems in the logic: 
796 
\begin{ttbox} 

797 
goal Hilbert.thy "P > P"; 

798 
{\out Level 0} 

799 
{\out P > P} 

800 
{\out 1. P > P} 

801 
\ttbreak 

802 
by (resolve_tac [Hilbert.MP] 1); 

803 
{\out Level 1} 

804 
{\out P > P} 

805 
{\out 1. ?P > P > P} 

806 
{\out 2. ?P} 

807 
\ttbreak 

808 
by (resolve_tac [Hilbert.MP] 1); 

809 
{\out Level 2} 

810 
{\out P > P} 

811 
{\out 1. ?P1 > ?P > P > P} 

812 
{\out 2. ?P1} 

813 
{\out 3. ?P} 

814 
\ttbreak 

815 
by (resolve_tac [Hilbert.S] 1); 

816 
{\out Level 3} 

817 
{\out P > P} 

818 
{\out 1. P > ?Q2 > P} 

819 
{\out 2. P > ?Q2} 

820 
\ttbreak 

821 
by (resolve_tac [Hilbert.K] 1); 

822 
{\out Level 4} 

823 
{\out P > P} 

824 
{\out 1. P > ?Q2} 

825 
\ttbreak 

826 
by (resolve_tac [Hilbert.K] 1); 

827 
{\out Level 5} 

828 
{\out P > P} 

829 
{\out No subgoals!} 

830 
\end{ttbox} 

831 
As we can see, this Hilbertstyle formulation of minimal logic is easy to 

832 
define but difficult to use. The following natural deduction formulation is 

833 
better: 

834 
\begin{ttbox} 

835 
MinI = Base + 

836 
consts 

1387  837 
">" :: [o, o] => o (infixr 10) 
320  838 
rules 
839 
impI "(P ==> Q) ==> P > Q" 

840 
impE "[ P > Q; P ] ==> Q" 

841 
end 

842 
\end{ttbox} 

843 
Note, however, that although the two systems are equivalent, this fact 

844 
cannot be proved within Isabelle. Axioms {\tt S} and {\tt K} can be 

845 
derived in {\tt MinI} (exercise!), but {\tt impI} cannot be derived in {\tt 

846 
Hilbert}. The reason is that {\tt impI} is only an {\bf admissible} rule 

847 
in {\tt Hilbert}, something that can only be shown by induction over all 

848 
possible proofs in {\tt Hilbert}. 

849 

850 
We may easily extend minimal logic with falsity: 

851 
\begin{ttbox} 

852 
MinIF = MinI + 

853 
consts 

1387  854 
False :: o 
320  855 
rules 
856 
FalseE "False ==> P" 

857 
end 

858 
\end{ttbox} 

859 
On the other hand, we may wish to introduce conjunction only: 

860 
\begin{ttbox} 

861 
MinC = Base + 

862 
consts 

1387  863 
"&" :: [o, o] => o (infixr 30) 
320  864 
\ttbreak 
865 
rules 

866 
conjI "[ P; Q ] ==> P & Q" 

867 
conjE1 "P & Q ==> P" 

868 
conjE2 "P & Q ==> Q" 

869 
end 

870 
\end{ttbox} 

871 
And if we want to have all three connectives together, we create and load a 

3108  872 
theory file consisting of a single line: 
320  873 
\begin{ttbox} 
874 
MinIFC = MinIF + MinC 

875 
\end{ttbox} 

876 
Now we can prove mixed theorems like 

877 
\begin{ttbox} 

878 
goal MinIFC.thy "P & False > Q"; 

879 
by (resolve_tac [MinI.impI] 1); 

880 
by (dresolve_tac [MinC.conjE2] 1); 

881 
by (eresolve_tac [MinIF.FalseE] 1); 

882 
\end{ttbox} 

883 
Try this as an exercise! 