author  wenzelm 
Wed, 03 Nov 2010 21:53:56 +0100  
changeset 40335  3e4bb6e7c3ca 
parent 39159  0dec18004e75 
child 42814  5af15f1e2ef6 
permissions  rwrr 
17481  1 
(* Title: Sequents/ILL.thy 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

2 
Author: Sara Kalvala and Valeria de Paiva 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

3 
Copyright 1995 University of Cambridge 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

4 
*) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

5 

17481  6 
theory ILL 
7 
imports Sequents 

8 
begin 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

9 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

10 
consts 
14765  11 
Trueprop :: "two_seqi" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

12 

22894  13 
tens :: "[o, o] => o" (infixr "><" 35) 
14 
limp :: "[o, o] => o" (infixr "o" 45) 

15 
liff :: "[o, o] => o" (infixr "oo" 45) 

16 
FShriek :: "o => o" ("! _" [100] 1000) 

17 
lconj :: "[o, o] => o" (infixr "&&" 35) 

18 
ldisj :: "[o, o] => o" (infixr "++" 35) 

19 
zero :: "o" ("0") 

20 
top :: "o" ("1") 

21 
eye :: "o" ("I") 

22 
aneg :: "o=>o" ("~_") 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

23 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

24 

14765  25 
(* context manipulation *) 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

26 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

27 
Context :: "two_seqi" 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

28 

14765  29 
(* promotion rule *) 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

30 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

31 
PromAux :: "three_seqi" 
14765  32 

33 
syntax 

35113  34 
"_Trueprop" :: "single_seqe" ("((_)/  (_))" [6,6] 5) 
35 
"_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) 

36 
"_PromAux" :: "three_seqe" ("promaux {___}") 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

37 

17481  38 
parse_translation {* 
35113  39 
[(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}), 
40 
(@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}), 

41 
(@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})] 

42 
*} 

17481  43 

44 
print_translation {* 

35113  45 
[(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}), 
46 
(@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}), 

47 
(@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})] 

48 
*} 

17481  49 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

50 
defs 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

51 

17481  52 
liff_def: "P oo Q == (P o Q) >< (Q o P)" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

53 

17481  54 
aneg_def: "~A == A o 0" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

55 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

56 

17481  57 
axioms 
14765  58 

17481  59 
identity: "P  P" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

60 

17481  61 
zerol: "$G, 0, $H  A" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

62 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

63 
(* RULES THAT DO NOT DIVIDE CONTEXT *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

64 

17481  65 
derelict: "$F, A, $G  C ==> $F, !A, $G  C" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

66 
(* unfortunately, this one removes !A *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

67 

17481  68 
contract: "$F, !A, !A, $G  C ==> $F, !A, $G  C" 
14765  69 

17481  70 
weaken: "$F, $G  C ==> $G, !A, $F  C" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

71 
(* weak form of weakening, in practice just to clean context *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

72 
(* weaken and contract not needed (CHECK) *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

73 

17481  74 
promote2: "promaux{  $H  B} ==> $H  !B" 
75 
promote1: "promaux{!A, $G  $H  B} 

76 
==> promaux {$G  $H, !A  B}" 

77 
promote0: "$G  A ==> promaux {$G   A}" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

78 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

79 

14765  80 

17481  81 
tensl: "$H, A, B, $G  C ==> $H, A >< B, $G  C" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

82 

17481  83 
impr: "A, $F  B ==> $F  A o B" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

84 

17481  85 
conjr: "[ $F  A ; 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

86 
$F  B ] 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

87 
==> $F  (A && B)" 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

88 

17481  89 
conjll: "$G, A, $H  C ==> $G, A && B, $H  C" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

90 

17481  91 
conjlr: "$G, B, $H  C ==> $G, A && B, $H  C" 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

92 

17481  93 
disjrl: "$G  A ==> $G  A ++ B" 
94 
disjrr: "$G  B ==> $G  A ++ B" 

95 
disjl: "[ $G, A, $H  C ; 

96 
$G, B, $H  C ] 

97 
==> $G, A ++ B, $H  C" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

98 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

99 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

100 
(* RULES THAT DIVIDE CONTEXT *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

101 

17481  102 
tensr: "[ $F, $J :=: $G; 
103 
$F  A ; 

104 
$J  B ] 

105 
==> $G  A >< B" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

106 

17481  107 
impl: "[ $G, $F :=: $J, $H ; 
108 
B, $F  C ; 

109 
$G  A ] 

110 
==> $J, A o B, $H  C" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

111 

14765  112 

17481  113 
cut: " [ $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; 
114 
$H1, $H2, $H3, $H4  A ; 

115 
$J1, $J2, A, $J3, $J4  B ] ==> $F  B" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

116 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

117 

fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

118 
(* CONTEXT RULES *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

119 

17481  120 
context1: "$G :=: $G" 
121 
context2: "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" 

122 
context3: "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" 

123 
context4a: "$F :=: $H, $G ==> $F :=: $H, !A, $G" 

124 
context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G" 

125 
context5: "$F, $G :=: $H ==> $G, $F :=: $H" 

2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

126 

21427  127 

128 
ML {* 

129 
val lazy_cs = empty_pack 

39159  130 
add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0}, 
131 
@{thm context2}, @{thm context3}] 

132 
add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr}, 

133 
@{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl}, 

134 
@{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2}, 

135 
@{thm context1}, @{thm context4a}, @{thm context4b}]; 

21427  136 

39159  137 
fun prom_tac n = 
138 
REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n) 

21427  139 
*} 
140 

141 
method_setup best_lazy = 

30549  142 
{* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *} 
21588  143 
"lazy classical reasoning" 
21427  144 

145 
lemma aux_impl: "$F, $G  A ==> $F, !(A o B), $G  B" 

146 
apply (rule derelict) 

147 
apply (rule impl) 

148 
apply (rule_tac [2] identity) 

149 
apply (rule context1) 

150 
apply assumption 

151 
done 

152 

153 
lemma conj_lemma: " $F, !A, !B, $G  C ==> $F, !(A && B), $G  C" 

154 
apply (rule contract) 

155 
apply (rule_tac A = " (!A) >< (!B) " in cut) 

156 
apply (rule_tac [2] tensr) 

157 
prefer 3 

158 
apply (subgoal_tac "! (A && B)  !A") 

159 
apply assumption 

160 
apply best_lazy 

161 
prefer 3 

162 
apply (subgoal_tac "! (A && B)  !B") 

163 
apply assumption 

164 
apply best_lazy 

165 
apply (rule_tac [2] context1) 

166 
apply (rule_tac [2] tensl) 

167 
prefer 2 apply (assumption) 

168 
apply (rule context3) 

169 
apply (rule context3) 

170 
apply (rule context1) 

171 
done 

172 

173 
lemma impr_contract: "!A, !A, $G  B ==> $G  (!A) o B" 

174 
apply (rule impr) 

175 
apply (rule contract) 

176 
apply assumption 

177 
done 

178 

179 
lemma impr_contr_der: "A, !A, $G  B ==> $G  (!A) o B" 

180 
apply (rule impr) 

181 
apply (rule contract) 

182 
apply (rule derelict) 

183 
apply assumption 

184 
done 

185 

186 
lemma contrad1: "$F, (!B) o 0, $G, !B, $H  A" 

187 
apply (rule impl) 

188 
apply (rule_tac [3] identity) 

189 
apply (rule context3) 

190 
apply (rule context1) 

191 
apply (rule zerol) 

192 
done 

193 

194 

195 
lemma contrad2: "$F, !B, $G, (!B) o 0, $H  A" 

196 
apply (rule impl) 

197 
apply (rule_tac [3] identity) 

198 
apply (rule context3) 

199 
apply (rule context1) 

200 
apply (rule zerol) 

201 
done 

202 

203 
lemma ll_mp: "A o B, A  B" 

204 
apply (rule impl) 

205 
apply (rule_tac [2] identity) 

206 
apply (rule_tac [2] identity) 

207 
apply (rule context1) 

208 
done 

209 

210 
lemma mp_rule1: "$F, B, $G, $H  C ==> $F, A, $G, A o B, $H  C" 

211 
apply (rule_tac A = "B" in cut) 

212 
apply (rule_tac [2] ll_mp) 

213 
prefer 2 apply (assumption) 

214 
apply (rule context3) 

215 
apply (rule context3) 

216 
apply (rule context1) 

217 
done 

218 

219 
lemma mp_rule2: "$F, B, $G, $H  C ==> $F, A o B, $G, A, $H  C" 

220 
apply (rule_tac A = "B" in cut) 

221 
apply (rule_tac [2] ll_mp) 

222 
prefer 2 apply (assumption) 

223 
apply (rule context3) 

224 
apply (rule context3) 

225 
apply (rule context1) 

226 
done 

227 

228 
lemma or_to_and: "!((!(A ++ B)) o 0)  !( ((!A) o 0) && ((!B) o 0))" 

229 
by best_lazy 

230 

231 
lemma o_a_rule: "$F, !( ((!A) o 0) && ((!B) o 0)), $G  C ==> 

232 
$F, !((!(A ++ B)) o 0), $G  C" 

233 
apply (rule cut) 

234 
apply (rule_tac [2] or_to_and) 

235 
prefer 2 apply (assumption) 

236 
apply (rule context3) 

237 
apply (rule context1) 

238 
done 

239 

240 
lemma conj_imp: "((!A) o C) ++ ((!B) o C)  (!(A && B)) o C" 

241 
apply (rule impr) 

242 
apply (rule conj_lemma) 

243 
apply (rule disjl) 

244 
apply (rule mp_rule1, best_lazy)+ 

245 
done 

246 

247 
lemma not_imp: "!A, !((!B) o 0)  (!((!A) o B)) o 0" 

248 
by best_lazy 

249 

250 
lemma a_not_a: "!A o (!A o 0)  !A o 0" 

251 
apply (rule impr) 

252 
apply (rule contract) 

253 
apply (rule impl) 

254 
apply (rule_tac [3] identity) 

255 
apply (rule context1) 

256 
apply best_lazy 

257 
done 

258 

259 
lemma a_not_a_rule: "$J1, !A o 0, $J2  B ==> $J1, !A o (!A o 0), $J2  B" 

260 
apply (rule_tac A = "!A o 0" in cut) 

261 
apply (rule_tac [2] a_not_a) 

262 
prefer 2 apply (assumption) 

263 
apply best_lazy 

264 
done 

265 

266 
ML {* 

39159  267 
val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1}, 
268 
@{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule}, 

269 
@{thm a_not_a_rule}] 

270 
add_unsafes [@{thm aux_impl}]; 

21427  271 

39159  272 
val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}]; 
21427  273 
*} 
274 

275 

276 
method_setup best_safe = 

30549  277 
{* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} "" 
21427  278 

279 
method_setup best_power = 

30549  280 
{* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} "" 
21427  281 

282 

283 
(* Some examples from Troelstra and van Dalen *) 

284 

285 
lemma "!((!A) o ((!B) o 0))  (!(A && B)) o 0" 

286 
by best_safe 

287 

288 
lemma "!((!(A && B)) o 0)  !((!A) o ((!B) o 0))" 

289 
by best_safe 

290 

291 
lemma "!( (!((! ((!A) o B) ) o 0)) o 0)  

292 
(!A) o ( (! ((!B) o 0)) o 0)" 

293 
by best_safe 

294 

295 
lemma "!( (!A) o ( (! ((!B) o 0)) o 0) )  

296 
(!((! ((!A) o B) ) o 0)) o 0" 

297 
by best_power 

298 

299 
end 