paulson@7160

1 
%% $Id$

paulson@7160

2 
\chapter{Defining A SequentBased Logic}

paulson@7160

3 
\label{chap:sequents}

paulson@7160

4 

paulson@7160

5 
\underscoreon %this file contains the @ character

paulson@7160

6 

paulson@7160

7 
The Isabelle theory \texttt{Sequents.thy} provides facilities for using

paulson@7160

8 
sequent notation in users' object logics. This theory allows users to

paulson@7160

9 
easily interface the surface syntax of sequences with an underlying

paulson@7160

10 
representation suitable for higherorder unification.

paulson@7160

11 

paulson@7160

12 
\section{Concrete syntax of sequences}

paulson@7160

13 

paulson@7160

14 
Mathematicians and logicians have used sequences in an informal way

paulson@7160

15 
much before proof systems such as Isabelle were created. It seems

paulson@7160

16 
sensible to allow people using Isabelle to express sequents and

paulson@7160

17 
perform proofs in this same informal way, and without requiring the

paulson@7160

18 
theory developer to spend a lot of time in \ML{} programming.

paulson@7160

19 

paulson@7160

20 
By using {\tt Sequents.thy}

paulson@7160

21 
appropriately, a logic developer can allow users to refer to sequences

paulson@7160

22 
in several ways:

paulson@7160

23 
%

paulson@7160

24 
\begin{itemize}

paulson@7160

25 
\item A sequence variable is any alphanumeric string with the first

paulson@7160

26 
character being a \verb%$% sign.

paulson@7160

27 
So, consider the sequent \verb%$A  B%, where \verb%$A%

paulson@7160

28 
is intended to match a sequence of zero or more items.

paulson@7160

29 

paulson@7160

30 
\item A sequence with unspecified subsequences and unspecified or

paulson@7160

31 
individual items is written as a commaseparated list of regular

paulson@7160

32 
variables (representing items), particular items, and

paulson@7160

33 
sequence variables, as in

paulson@7160

34 
\begin{ttbox}

paulson@7160

35 
$A, B, C, $D(x)  E

paulson@7160

36 
\end{ttbox}

paulson@7160

37 
Here both \verb%$A% and \verb%$D(x)%

paulson@7160

38 
are allowed to match any subsequences of items on either side of the

paulson@7160

39 
two items that match $B$ and $C$. Moreover, the sequence matching

paulson@7160

40 
\verb%$D(x)% may contain occurrences of~$x$.

paulson@7160

41 

paulson@7160

42 
\item An empty sequence can be represented by a blank space, as in

paulson@7160

43 
\verb?  true?.

paulson@7160

44 
\end{itemize}

paulson@7160

45 

paulson@7160

46 
These syntactic constructs need to be assimilated into the object

paulson@7160

47 
theory being developed. The type that we use for these visible objects

paulson@7160

48 
is given the name {\tt seq}.

paulson@7160

49 
A {\tt seq} is created either by the empty space, a {\tt seqobj} or a

paulson@7160

50 
{\tt seqobj} followed by a {\tt seq}, with a comma between them. A

paulson@7160

51 
{\tt seqobj} is either an item or a variable representing a

paulson@7160

52 
sequence. Thus, a theory designer can specify a function that takes

paulson@7160

53 
two sequences and returns a metalevel proposition by giving it the

paulson@7160

54 
Isabelle type \verb[seq, seq] => prop.

paulson@7160

55 

paulson@7160

56 
This is all part of the concrete syntax, but one may wish to

paulson@7160

57 
exploit Isabelle's higherorder abstract syntax by actually having a

paulson@7160

58 
different, more powerful {\em internal} syntax.

paulson@7160

59 

paulson@7160

60 

paulson@7160

61 

paulson@7160

62 
\section{ Basis}

paulson@7160

63 

paulson@7160

64 
One could opt to represent sequences as firstorder objects (such as

paulson@7160

65 
simple lists), but this would not allow us to use many facilities

paulson@7160

66 
Isabelle provides for matching. By using a slightly more complex

paulson@7160

67 
representation, users of the logic can reap many benefits in

paulson@7160

68 
facilities for proofs and ease of reading logical terms.

paulson@7160

69 

paulson@7160

70 
A sequence can be represented as a function  a constructor for

paulson@7160

71 
further sequences  by defining a binary {\em abstract} function

paulson@7160

72 
\verbSeq0' with type \verb[o,seq']=>seq', and translating a

paulson@7160

73 
sequence such as \verbA, B, C into

paulson@7160

74 
\begin{ttbox}

paulson@7160

75 
\%s. Seq0'(A, SeqO'(B, SeqO'(C, s)))

paulson@7160

76 
\end{ttbox}

paulson@7160

77 
This sequence can therefore be seen as a constructor

paulson@7160

78 
for further sequences. The constructor \verbSeq0' is never given a

paulson@7160

79 
value, and therefore it is not possible to evaluate this expression

paulson@7160

80 
into a basic value.

paulson@7160

81 

paulson@7160

82 
Furthermore, if we want to represent the sequence \verbA, $B, C,

paulson@7160

83 
we note that \verb$B already represents a sequence, so we can use

paulson@7160

84 
\verbB itself to refer to the function, and therefore the sequence

paulson@7160

85 
can be mapped to the internal form:

paulson@7160

86 
\verb%s. SeqO'(A, B(SeqO'(C, s))).

paulson@7160

87 

paulson@7160

88 
So, while we wish to continue with the standard, wellliked {\em

paulson@7160

89 
external} representation of sequences, we can represent them {\em

paulson@7160

90 
internally} as functions of type \verbseq'=>seq'.

paulson@7160

91 

paulson@7160

92 

paulson@7160

93 
\section{Object logics}

paulson@7160

94 

paulson@7160

95 
Recall that object logics are defined by mapping elements of

paulson@7160

96 
particular types to the Isabelle type \verbprop, usually with a

paulson@7160

97 
function called {\tt Trueprop}. So, an object

paulson@7160

98 
logic proposition {\tt P} is matched to the Isabelle proposition

paulson@7160

99 
{\tt Trueprop(P)}\@. The name of the function is often hidden, so the

paulson@7160

100 
user just sees {\tt P}\@. Isabelle is eager to make types match, so it

paulson@7160

101 
inserts {\tt Trueprop} automatically when an object of type {\tt prop}

paulson@7160

102 
is expected. This mechanism can be observed in most of the object

paulson@7160

103 
logics which are direct descendants of {\tt Pure}.

paulson@7160

104 

paulson@7160

105 
In order to provide the desired syntactic facilities for sequent

paulson@7160

106 
calculi, rather than use just one function that maps objectlevel

paulson@7160

107 
propositions to metalevel propositions, we use two functions, and

paulson@7160

108 
separate internal from the external representation.

paulson@7160

109 

paulson@7160

110 
These functions need to be given a type that is appropriate for the particular

paulson@7160

111 
form of sequents required: single or multiple conclusions. So

paulson@7160

112 
multipleconclusion sequents (used in the LK logic) can be

paulson@7160

113 
specified by the following two definitions, which are lifted from the inbuilt

paulson@7160

114 
{\tt Sequents/LK.thy}:

paulson@7160

115 
\begin{ttbox}

paulson@7160

116 
Trueprop :: two_seqi

paulson@7160

117 
"@Trueprop" :: two_seqe ("((_)/  (_))" [6,6] 5)

paulson@7160

118 
\end{ttbox}

paulson@7160

119 
%

paulson@7160

120 
where the types used are defined in {\tt Sequents.thy} as

paulson@7160

121 
abbreviations:

paulson@7160

122 
\begin{ttbox}

paulson@7160

123 
two_seqi = [seq'=>seq', seq'=>seq'] => prop

paulson@7160

124 
two_seqe = [seq, seq] => prop

paulson@7160

125 
\end{ttbox}

paulson@7160

126 

paulson@7160

127 
The next step is to actually create links into the lowlevel parsing

paulson@7160

128 
and prettyprinting mechanisms, which map external and internal

paulson@7160

129 
representations. These functions go below the user level and capture

paulson@7160

130 
the underlying structure of Isabelle terms in \ML{}\@. Fortunately the

paulson@7160

131 
theory developer need not delve in this level; {\tt Sequents.thy}

paulson@7160

132 
provides the necessary facilities. All the theory developer needs to

paulson@7160

133 
add in the \ML{} section is a specification of the two translation

paulson@7160

134 
functions:

paulson@7160

135 
\begin{ttbox}

paulson@7160

136 
ML

paulson@7160

137 
val parse_translation = [("@Trueprop",Sequents.two_seq_tr "Trueprop")];

paulson@7160

138 
val print_translation = [("Trueprop",Sequents.two_seq_tr' "@Trueprop")];

paulson@7160

139 
\end{ttbox}

paulson@7160

140 

paulson@7160

141 
In summary: in the logic theory being developed, the developer needs

paulson@7160

142 
to specify the types for the internal and external representation of

paulson@7160

143 
the sequences, and use the appropriate parsing and prettyprinting

paulson@7160

144 
functions.

paulson@7160

145 

paulson@7160

146 
\section{What's in \texttt{Sequents.thy}}

paulson@7160

147 

paulson@7160

148 
Theory \texttt{Sequents.thy} makes many declarations that you need to know

paulson@7160

149 
about:

paulson@7160

150 
\begin{enumerate}

paulson@7160

151 
\item The Isabelle types given below, which can be used for the

paulson@7160

152 
constants that map objectlevel sequents and metalevel propositions:

paulson@7160

153 
%

paulson@7160

154 
\begin{ttbox}

paulson@7160

155 
single_seqe = [seq,seqobj] => prop

paulson@7160

156 
single_seqi = [seq'=>seq',seq'=>seq'] => prop

paulson@7160

157 
two_seqi = [seq'=>seq', seq'=>seq'] => prop

paulson@7160

158 
two_seqe = [seq, seq] => prop

paulson@7160

159 
three_seqi = [seq'=>seq', seq'=>seq', seq'=>seq'] => prop

paulson@7160

160 
three_seqe = [seq, seq, seq] => prop

paulson@7160

161 
four_seqi = [seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop

paulson@7160

162 
four_seqe = [seq, seq, seq, seq] => prop

paulson@7160

163 
\end{ttbox}

paulson@7160

164 

paulson@7160

165 
The \verbsingle_ and \verbtwo_ sets of mappings for internal and

paulson@7160

166 
external representations are the ones used for, say single and

paulson@7160

167 
multiple conclusion sequents. The other functions are provided to

paulson@7160

168 
allow rules that manipulate more than two functions, as can be seen in

paulson@7160

169 
the inbuilt object logics.

paulson@7160

170 

paulson@7160

171 
\item An auxiliary syntactic constant has been

paulson@7160

172 
defined that directly maps a sequence to its internal representation:

paulson@7160

173 
\begin{ttbox}

paulson@7160

174 
"@Side" :: seq=>(seq'=>seq') ("<<(_)>>")

paulson@7160

175 
\end{ttbox}

paulson@7160

176 
Whenever a sequence (such as \verb<< A, $B, $C>>) is entered using this

paulson@7160

177 
syntax, it is translated into the appropriate internal representation. This

paulson@7160

178 
form can be used only where a sequence is expected.

paulson@7160

179 

paulson@7160

180 
\item The \ML{} functions \texttt{single\_tr}, \texttt{two\_seq\_tr},

paulson@7160

181 
\texttt{three\_seq\_tr}, \texttt{four\_seq\_tr} for parsing, that is, the

paulson@7160

182 
translation from external to internal form. Analogously there are

paulson@7160

183 
\texttt{single\_tr'}, \texttt{two\_seq\_tr'}, \texttt{three\_seq\_tr'},

paulson@7160

184 
\texttt{four\_seq\_tr'} for prettyprinting, that is, the translation from

paulson@7160

185 
internal to external form. These functions can be used in the \ML{} section

paulson@7160

186 
of a theory file to specify the translations to be used. As an example of

paulson@7160

187 
use, note that in {\tt LK.thy} we declare two identifiers:

paulson@7160

188 
\begin{ttbox}

paulson@7160

189 
val parse_translation =

paulson@7160

190 
[("@Trueprop",Sequents.two_seq_tr "Trueprop")];

paulson@7160

191 
val print_translation =

paulson@7160

192 
[("Trueprop",Sequents.two_seq_tr' "@Trueprop")];

paulson@7160

193 
\end{ttbox}

paulson@7160

194 
The given parse translation will be applied whenever a \verb@Trueprop

paulson@7160

195 
constant is found, translating using \verbtwo_seq_tr and inserting the

paulson@7160

196 
constant \verbTrueprop. The prettyprinting translation is applied

paulson@7160

197 
analogously; a term that contains \verbTrueprop is printed as a

paulson@7160

198 
\verb@Trueprop.

paulson@7160

199 
\end{enumerate}

paulson@7160

200 

paulson@7160

201 
