
1 %% $Id$ 

2 \chapter{Defining A SequentBased Logic} 

3 \label{chap:sequents} 

4 

5 \underscoreon %this file contains the @ character 

6 

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

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

9 easily interface the surface syntax of sequences with an underlying 

10 representation suitable for higherorder unification. 

11 

12 \section{Concrete syntax of sequences} 

13 

14 Mathematicians and logicians have used sequences in an informal way 

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

16 sensible to allow people using Isabelle to express sequents and 

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

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

19 

20 By using {\tt Sequents.thy} 

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

22 in several ways: 

23 % 

24 \begin{itemize} 

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

26 character being a \verb%$% sign. 

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

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

29 

30 \item A sequence with unspecified subsequences and unspecified or 

31 individual items is written as a commaseparated list of regular 

32 variables (representing items), particular items, and 

33 sequence variables, as in 

34 \begin{ttbox} 

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

36 \end{ttbox} 

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

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

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

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

41 

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

43 \verb?  true?. 

44 \end{itemize} 

45 

46 These syntactic constructs need to be assimilated into the object 

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

48 is given the name {\tt seq}. 

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

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

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

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

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

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

55 

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

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

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

59 

60 

61 

62 \section{ Basis} 

63 

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

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

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

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

68 facilities for proofs and ease of reading logical terms. 

69 

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

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

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

73 sequence such as \verbA, B, C into 

74 \begin{ttbox} 

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

76 \end{ttbox} 

77 This sequence can therefore be seen as a constructor 

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

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

80 into a basic value. 

81 

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

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

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

85 can be mapped to the internal form: 

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

87 

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

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

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

91 

92 

93 \section{Object logics} 

94 

95 Recall that object logics are defined by mapping elements of 

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

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

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

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

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

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

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

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

104 

105 In order to provide the desired syntactic facilities for sequent 

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

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

108 separate internal from the external representation. 

109 

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

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

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

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

114 {\tt Sequents/LK.thy}: 

115 \begin{ttbox} 

116 Trueprop :: two_seqi 

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

118 \end{ttbox} 

119 % 

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

121 abbreviations: 

122 \begin{ttbox} 

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

124 two_seqe = [seq, seq] => prop 

125 \end{ttbox} 

126 

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

128 and prettyprinting mechanisms, which map external and internal 

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

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

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

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

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

134 functions: 

135 \begin{ttbox} 

136 ML 

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

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

139 \end{ttbox} 

140 

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

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

143 the sequences, and use the appropriate parsing and prettyprinting 

144 functions. 

145 

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

147 

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

149 about: 

150 \begin{enumerate} 

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

152 constants that map objectlevel sequents and metalevel propositions: 

153 % 

154 \begin{ttbox} 

155 single_seqe = [seq,seqobj] => prop 

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

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

158 two_seqe = [seq, seq] => prop 

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

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

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

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

163 \end{ttbox} 

164 

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

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

167 multiple conclusion sequents. The other functions are provided to 

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

169 the inbuilt object logics. 

170 

171 \item An auxiliary syntactic constant has been 

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

173 \begin{ttbox} 

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

175 \end{ttbox} 

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

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

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

179 

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

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

182 translation from external to internal form. Analogously there are 

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

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

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

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

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

188 \begin{ttbox} 

189 val parse_translation = 

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

191 val print_translation = 

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

193 \end{ttbox} 

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

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

196 constant \verbTrueprop. The prettyprinting translation is applied 

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

198 \verb@Trueprop. 

199 \end{enumerate} 

200 

201 