author  wenzelm 
Sat, 01 Feb 2014 18:07:10 +0100  
changeset 55231  264d34c19bf2 
parent 55228  901a6696cdd8 
child 55232  7a46672934a3 
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 {* 
52143  39 
[(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})), 
40 
(@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})), 

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

35113  42 
*} 
17481  43 

44 
print_translation {* 

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

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

35113  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 

51309  57 
axiomatization where 
14765  58 

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

60 

51309  61 
zerol: "$G, 0, $H  A" and 
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 

51309  65 
derelict: "$F, A, $G  C ==> $F, !A, $G  C" and 
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 

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

51309  70 
weaken: "$F, $G  C ==> $G, !A, $F  C" and 
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 

51309  74 
promote2: "promaux{  $H  B} ==> $H  !B" and 
17481  75 
promote1: "promaux{!A, $G  $H  B} 
51309  76 
==> promaux {$G  $H, !A  B}" and 
77 
promote0: "$G  A ==> promaux {$G   A}" and 

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 

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

82 

51309  83 
impr: "A, $F  B ==> $F  A o B" and 
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 ] 
51309  87 
==> $F  (A && B)" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

88 

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

90 

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

92 

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

17481  95 
disjl: "[ $G, A, $H  C ; 
96 
$G, B, $H  C ] 

51309  97 
==> $G, A ++ B, $H  C" and 
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 ] 

51309  105 
==> $G  A >< B" and 
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 ] 

51309  110 
==> $J, A o B, $H  C" and 
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 ; 

51309  115 
$J1, $J2, A, $J3, $J4  B ] ==> $F  B" and 
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 

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

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

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

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

17481  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 {* 

55228  129 
val lazy_pack = 
130 
Cla.put_pack Cla.empty_pack @{context} 

131 
> fold_rev Cla.add_safe @{thms tensl conjr disjl promote0 context2 context3} 

132 
> fold_rev Cla.add_unsafe @{thms 

133 
identity zerol conjll conjlr 

134 
disjrl disjrr impr tensr impl 

135 
derelict weaken promote1 promote2 

136 
context1 context4a context4b} 

137 
> Cla.get_pack; 

21427  138 
*} 
139 

55228  140 
method_setup best_lazy = {* 
141 
Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack lazy_pack ctxt))) 

142 
*} "lazy classical reasoning" 

21427  143 

55228  144 
lemma aux_impl: "$F, $G  A \<Longrightarrow> $F, !(A o B), $G  B" 
21427  145 
apply (rule derelict) 
146 
apply (rule impl) 

147 
apply (rule_tac [2] identity) 

148 
apply (rule context1) 

149 
apply assumption 

150 
done 

151 

55228  152 
lemma conj_lemma: " $F, !A, !B, $G  C \<Longrightarrow> $F, !(A && B), $G  C" 
21427  153 
apply (rule contract) 
154 
apply (rule_tac A = " (!A) >< (!B) " in cut) 

155 
apply (rule_tac [2] tensr) 

156 
prefer 3 

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

158 
apply assumption 

159 
apply best_lazy 

160 
prefer 3 

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

162 
apply assumption 

163 
apply best_lazy 

164 
apply (rule_tac [2] context1) 

165 
apply (rule_tac [2] tensl) 

166 
prefer 2 apply (assumption) 

167 
apply (rule context3) 

168 
apply (rule context3) 

169 
apply (rule context1) 

170 
done 

171 

55228  172 
lemma impr_contract: "!A, !A, $G  B \<Longrightarrow> $G  (!A) o B" 
21427  173 
apply (rule impr) 
174 
apply (rule contract) 

175 
apply assumption 

176 
done 

177 

55228  178 
lemma impr_contr_der: "A, !A, $G  B \<Longrightarrow> $G  (!A) o B" 
21427  179 
apply (rule impr) 
180 
apply (rule contract) 

181 
apply (rule derelict) 

182 
apply assumption 

183 
done 

184 

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

186 
apply (rule impl) 

187 
apply (rule_tac [3] identity) 

188 
apply (rule context3) 

189 
apply (rule context1) 

190 
apply (rule zerol) 

191 
done 

192 

193 

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

195 
apply (rule impl) 

196 
apply (rule_tac [3] identity) 

197 
apply (rule context3) 

198 
apply (rule context1) 

199 
apply (rule zerol) 

200 
done 

201 

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

203 
apply (rule impl) 

204 
apply (rule_tac [2] identity) 

205 
apply (rule_tac [2] identity) 

206 
apply (rule context1) 

207 
done 

208 

55228  209 
lemma mp_rule1: "$F, B, $G, $H  C \<Longrightarrow> $F, A, $G, A o B, $H  C" 
21427  210 
apply (rule_tac A = "B" in cut) 
211 
apply (rule_tac [2] ll_mp) 

212 
prefer 2 apply (assumption) 

213 
apply (rule context3) 

214 
apply (rule context3) 

215 
apply (rule context1) 

216 
done 

217 

55228  218 
lemma mp_rule2: "$F, B, $G, $H  C \<Longrightarrow> $F, A o B, $G, A, $H  C" 
21427  219 
apply (rule_tac A = "B" in cut) 
220 
apply (rule_tac [2] ll_mp) 

221 
prefer 2 apply (assumption) 

222 
apply (rule context3) 

223 
apply (rule context3) 

224 
apply (rule context1) 

225 
done 

226 

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

228 
by best_lazy 

229 

55228  230 
lemma o_a_rule: "$F, !( ((!A) o 0) && ((!B) o 0)), $G  C \<Longrightarrow> 
21427  231 
$F, !((!(A ++ B)) o 0), $G  C" 
232 
apply (rule cut) 

233 
apply (rule_tac [2] or_to_and) 

234 
prefer 2 apply (assumption) 

235 
apply (rule context3) 

236 
apply (rule context1) 

237 
done 

238 

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

240 
apply (rule impr) 

241 
apply (rule conj_lemma) 

242 
apply (rule disjl) 

243 
apply (rule mp_rule1, best_lazy)+ 

244 
done 

245 

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

247 
by best_lazy 

248 

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

250 
apply (rule impr) 

251 
apply (rule contract) 

252 
apply (rule impl) 

253 
apply (rule_tac [3] identity) 

254 
apply (rule context1) 

255 
apply best_lazy 

256 
done 

257 

55228  258 
lemma a_not_a_rule: "$J1, !A o 0, $J2  B \<Longrightarrow> $J1, !A o (!A o 0), $J2  B" 
21427  259 
apply (rule_tac A = "!A o 0" in cut) 
260 
apply (rule_tac [2] a_not_a) 

261 
prefer 2 apply (assumption) 

262 
apply best_lazy 

263 
done 

264 

265 
ML {* 

55228  266 
val safe_pack = 
267 
Cla.put_pack lazy_pack @{context} 

268 
> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1 

269 
contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule} 

270 
> Cla.add_unsafe @{thm aux_impl} 

271 
> Cla.get_pack; 

21427  272 

55228  273 
val power_pack = 
274 
Cla.put_pack safe_pack @{context} 

275 
> Cla.add_unsafe @{thm impr_contr_der} 

276 
> Cla.get_pack; 

21427  277 
*} 
278 

279 

280 
method_setup best_safe = 

55228  281 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt))) *} 
21427  282 

283 
method_setup best_power = 

55228  284 
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt))) *} 
21427  285 

286 

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

288 

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

290 
by best_safe 

291 

292 
lemma "!((!(A && B)) o 0)  !((!A) o ((!B) 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_safe 

298 

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

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

301 
by best_power 

302 

303 
end 