author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 22894  619b270607ac 
child 30510  4120fc59dd85 
permissions  rwrr 
17481  1 
(* Title: Sequents/ILL.thy 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

2 
ID: $Id$ 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

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

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

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

6 

17481  7 
theory ILL 
8 
imports Sequents 

9 
begin 

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

10 

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

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

13 

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

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

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

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

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

20 
zero :: "o" ("0") 

21 
top :: "o" ("1") 

22 
eye :: "o" ("I") 

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

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

24 

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

25 

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

27 

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

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

29 

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

31 

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

32 
PromAux :: "three_seqi" 
14765  33 

34 
syntax 

35 
"@Trueprop" :: "single_seqe" ("((_)/  (_))" [6,6] 5) 

36 
"@Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) 

37 
"@PromAux" :: "three_seqe" ("promaux {___}") 

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

38 

17481  39 
parse_translation {* 
40 
[("@Trueprop", single_tr "Trueprop"), 

41 
("@Context", two_seq_tr "Context"), 

42 
("@PromAux", three_seq_tr "PromAux")] *} 

43 

44 
print_translation {* 

45 
[("Trueprop", single_tr' "@Trueprop"), 

46 
("Context", two_seq_tr'"@Context"), 

47 
("PromAux", three_seq_tr'"@PromAux")] *} 

48 

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

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

50 

17481  51 
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

52 

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

54 

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

55 

17481  56 
axioms 
14765  57 

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

59 

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

61 

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

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

63 

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

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

66 

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

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

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

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

72 

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

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

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

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

77 

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

78 

14765  79 

17481  80 
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

81 

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

83 

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

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

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

87 

17481  88 
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

89 

17481  90 
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

91 

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

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

95 
$G, B, $H  C ] 

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

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

97 

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 
(* RULES THAT DIVIDE CONTEXT *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

100 

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

103 
$J  B ] 

104 
==> $G  A >< B" 

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

105 

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

108 
$G  A ] 

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

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

110 

14765  111 

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

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

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

115 

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 
(* CONTEXT RULES *) 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

118 

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

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

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

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

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

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

125 

21427  126 

127 
ML {* 

128 

129 
val lazy_cs = empty_pack 

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"]; 

136 

137 
local 

138 
val promote0 = thm "promote0" 

139 
val promote1 = thm "promote1" 

140 
val promote2 = thm "promote2" 

141 
in 

142 

143 
fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n) 

14765  144 

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

145 
end 
21427  146 
*} 
147 

148 
method_setup best_lazy = 

21588  149 
{* Method.no_args (Method.SIMPLE_METHOD' (best_tac lazy_cs)) *} 
150 
"lazy classical reasoning" 

21427  151 

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

153 
apply (rule derelict) 

154 
apply (rule impl) 

155 
apply (rule_tac [2] identity) 

156 
apply (rule context1) 

157 
apply assumption 

158 
done 

159 

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

161 
apply (rule contract) 

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

163 
apply (rule_tac [2] tensr) 

164 
prefer 3 

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

166 
apply assumption 

167 
apply best_lazy 

168 
prefer 3 

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

170 
apply assumption 

171 
apply best_lazy 

172 
apply (rule_tac [2] context1) 

173 
apply (rule_tac [2] tensl) 

174 
prefer 2 apply (assumption) 

175 
apply (rule context3) 

176 
apply (rule context3) 

177 
apply (rule context1) 

178 
done 

179 

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

181 
apply (rule impr) 

182 
apply (rule contract) 

183 
apply assumption 

184 
done 

185 

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

187 
apply (rule impr) 

188 
apply (rule contract) 

189 
apply (rule derelict) 

190 
apply assumption 

191 
done 

192 

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

194 
apply (rule impl) 

195 
apply (rule_tac [3] identity) 

196 
apply (rule context3) 

197 
apply (rule context1) 

198 
apply (rule zerol) 

199 
done 

200 

201 

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

203 
apply (rule impl) 

204 
apply (rule_tac [3] identity) 

205 
apply (rule context3) 

206 
apply (rule context1) 

207 
apply (rule zerol) 

208 
done 

209 

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

211 
apply (rule impl) 

212 
apply (rule_tac [2] identity) 

213 
apply (rule_tac [2] identity) 

214 
apply (rule context1) 

215 
done 

216 

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

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

219 
apply (rule_tac [2] ll_mp) 

220 
prefer 2 apply (assumption) 

221 
apply (rule context3) 

222 
apply (rule context3) 

223 
apply (rule context1) 

224 
done 

225 

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

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

228 
apply (rule_tac [2] ll_mp) 

229 
prefer 2 apply (assumption) 

230 
apply (rule context3) 

231 
apply (rule context3) 

232 
apply (rule context1) 

233 
done 

234 

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

236 
by best_lazy 

237 

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

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

240 
apply (rule cut) 

241 
apply (rule_tac [2] or_to_and) 

242 
prefer 2 apply (assumption) 

243 
apply (rule context3) 

244 
apply (rule context1) 

245 
done 

246 

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

248 
apply (rule impr) 

249 
apply (rule conj_lemma) 

250 
apply (rule disjl) 

251 
apply (rule mp_rule1, best_lazy)+ 

252 
done 

253 

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

255 
by best_lazy 

256 

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

258 
apply (rule impr) 

259 
apply (rule contract) 

260 
apply (rule impl) 

261 
apply (rule_tac [3] identity) 

262 
apply (rule context1) 

263 
apply best_lazy 

264 
done 

265 

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

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

268 
apply (rule_tac [2] a_not_a) 

269 
prefer 2 apply (assumption) 

270 
apply best_lazy 

271 
done 

272 

273 
ML {* 

274 

275 
val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1", 

276 
thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule", 

277 
thm "a_not_a_rule"] 

278 
add_unsafes [thm "aux_impl"]; 

279 

280 
val power_cs = safe_cs add_unsafes [thm "impr_contr_der"]; 

281 
*} 

282 

283 

284 
method_setup best_safe = 

21588  285 
{* Method.no_args (Method.SIMPLE_METHOD' (best_tac safe_cs)) *} "" 
21427  286 

287 
method_setup best_power = 

21588  288 
{* Method.no_args (Method.SIMPLE_METHOD' (best_tac power_cs)) *} "" 
21427  289 

290 

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

292 

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

294 
by best_safe 

295 

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

297 
by best_safe 

298 

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

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

301 
by best_safe 

302 

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

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

305 
by best_power 

306 

307 
end 