author  haftmann 
Thu, 23 Nov 2017 17:03:27 +0000  
changeset 67087  733017b19de9 
parent 62144  bdab93ccfaf8 
child 69593  3dda49e08b9d 
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 

61385  13 
tens :: "[o, o] \<Rightarrow> o" (infixr "><" 35) 
14 
limp :: "[o, o] \<Rightarrow> o" (infixr "o" 45) 

15 
FShriek :: "o \<Rightarrow> o" ("! _" [100] 1000) 

16 
lconj :: "[o, o] \<Rightarrow> o" (infixr "&&" 35) 

17 
ldisj :: "[o, o] \<Rightarrow> o" (infixr "++" 35) 

22894  18 
zero :: "o" ("0") 
19 
top :: "o" ("1") 

20 
eye :: "o" ("I") 

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

21 

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

22 

14765  23 
(* context manipulation *) 
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 
Context :: "two_seqi" 
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

26 

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

28 

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

29 
PromAux :: "three_seqi" 
14765  30 

31 
syntax 

61386  32 
"_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5) 
35113  33 
"_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5) 
34 
"_PromAux" :: "three_seqe" ("promaux {___}") 

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

35 

60770  36 
parse_translation \<open> 
52143  37 
[(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})), 
38 
(@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})), 

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

60770  40 
\<close> 
17481  41 

60770  42 
print_translation \<open> 
52143  43 
[(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})), 
44 
(@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})), 

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

60770  46 
\<close> 
17481  47 

62144  48 
definition liff :: "[o, o] \<Rightarrow> o" (infixr "oo" 45) 
49 
where "P oo Q == (P o Q) >< (Q o P)" 

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

50 

62144  51 
definition aneg :: "o\<Rightarrow>o" ("~_") 
52 
where "~A == A o 0" 

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

53 

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

54 

51309  55 
axiomatization where 
14765  56 

61386  57 
identity: "P \<turnstile> P" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

58 

61386  59 
zerol: "$G, 0, $H \<turnstile> A" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

60 

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

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

62 

61386  63 
derelict: "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

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

65 

61386  66 
contract: "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and 
14765  67 

61386  68 
weaken: "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> C" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

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

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

71 

61386  72 
promote2: "promaux{  $H  B} \<Longrightarrow> $H \<turnstile> !B" and 
17481  73 
promote1: "promaux{!A, $G  $H  B} 
61385  74 
\<Longrightarrow> promaux {$G  $H, !A  B}" and 
61386  75 
promote0: "$G \<turnstile> A \<Longrightarrow> promaux {$G   A}" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

76 

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

77 

14765  78 

61386  79 
tensl: "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

80 

61386  81 
impr: "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A o B" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

82 

61386  83 
conjr: "\<lbrakk>$F \<turnstile> A ; 
84 
$F \<turnstile> B\<rbrakk> 

85 
\<Longrightarrow> $F \<turnstile> (A && B)" and 

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

86 

61386  87 
conjll: "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

88 

61386  89 
conjlr: "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and 
2073
fb0655539d05
New unified treatment of sequent calculi by Sara Kalvala
paulson
parents:
diff
changeset

90 

61386  91 
disjrl: "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and 
92 
disjrr: "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and 

93 
disjl: "\<lbrakk>$G, A, $H \<turnstile> C ; 

94 
$G, B, $H \<turnstile> C\<rbrakk> 

95 
\<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and 

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

96 

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

99 

61385  100 
tensr: "\<lbrakk>$F, $J :=: $G; 
61386  101 
$F \<turnstile> A ; 
102 
$J \<turnstile> B\<rbrakk> 

103 
\<Longrightarrow> $G \<turnstile> A >< B" and 

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

104 

61385  105 
impl: "\<lbrakk>$G, $F :=: $J, $H ; 
61386  106 
B, $F \<turnstile> C ; 
107 
$G \<turnstile> A\<rbrakk> 

108 
\<Longrightarrow> $J, A o B, $H \<turnstile> C" and 

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

109 

14765  110 

61385  111 
cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ; 
61386  112 
$H1, $H2, $H3, $H4 \<turnstile> A ; 
113 
$J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and 

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

114 

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

117 

51309  118 
context1: "$G :=: $G" and 
61385  119 
context2: "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and 
120 
context3: "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and 

121 
context4a: "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and 

122 
context4b: "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and 

123 
context5: "$F, $G :=: $H \<Longrightarrow> $G, $F :=: $H" 

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

124 

55232  125 
text "declarations for lazy classical reasoning:" 
126 
lemmas [safe] = 

127 
context3 

128 
context2 

129 
promote0 

130 
disjl 

131 
conjr 

132 
tensl 

133 
lemmas [unsafe] = 

134 
context4b 

135 
context4a 

136 
context1 

137 
promote2 

138 
promote1 

139 
weaken 

140 
derelict 

141 
impl 

142 
tensr 

143 
impr 

144 
disjrr 

145 
disjrl 

146 
conjlr 

147 
conjll 

148 
zerol 

149 
identity 

21427  150 

61386  151 
lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A o B), $G \<turnstile> B" 
21427  152 
apply (rule derelict) 
153 
apply (rule impl) 

154 
apply (rule_tac [2] identity) 

155 
apply (rule context1) 

156 
apply assumption 

157 
done 

158 

61386  159 
lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> C" 
21427  160 
apply (rule contract) 
161 
apply (rule_tac A = " (!A) >< (!B) " in cut) 

162 
apply (rule_tac [2] tensr) 

163 
prefer 3 

61386  164 
apply (subgoal_tac "! (A && B) \<turnstile> !A") 
21427  165 
apply assumption 
55232  166 
apply best 
21427  167 
prefer 3 
61386  168 
apply (subgoal_tac "! (A && B) \<turnstile> !B") 
21427  169 
apply assumption 
55232  170 
apply best 
21427  171 
apply (rule_tac [2] context1) 
172 
apply (rule_tac [2] tensl) 

55232  173 
prefer 2 apply assumption 
21427  174 
apply (rule context3) 
175 
apply (rule context3) 

176 
apply (rule context1) 

177 
done 

178 

61386  179 
lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) o B" 
21427  180 
apply (rule impr) 
181 
apply (rule contract) 

182 
apply assumption 

183 
done 

184 

61386  185 
lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) o B" 
21427  186 
apply (rule impr) 
187 
apply (rule contract) 

188 
apply (rule derelict) 

189 
apply assumption 

190 
done 

191 

61386  192 
lemma contrad1: "$F, (!B) o 0, $G, !B, $H \<turnstile> A" 
21427  193 
apply (rule impl) 
194 
apply (rule_tac [3] identity) 

195 
apply (rule context3) 

196 
apply (rule context1) 

197 
apply (rule zerol) 

198 
done 

199 

200 

61386  201 
lemma contrad2: "$F, !B, $G, (!B) o 0, $H \<turnstile> A" 
21427  202 
apply (rule impl) 
203 
apply (rule_tac [3] identity) 

204 
apply (rule context3) 

205 
apply (rule context1) 

206 
apply (rule zerol) 

207 
done 

208 

61386  209 
lemma ll_mp: "A o B, A \<turnstile> B" 
21427  210 
apply (rule impl) 
211 
apply (rule_tac [2] identity) 

212 
apply (rule_tac [2] identity) 

213 
apply (rule context1) 

214 
done 

215 

61386  216 
lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A o B, $H \<turnstile> C" 
21427  217 
apply (rule_tac A = "B" in cut) 
218 
apply (rule_tac [2] ll_mp) 

219 
prefer 2 apply (assumption) 

220 
apply (rule context3) 

221 
apply (rule context3) 

222 
apply (rule context1) 

223 
done 

224 

61386  225 
lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A o B, $G, A, $H \<turnstile> C" 
21427  226 
apply (rule_tac A = "B" in cut) 
227 
apply (rule_tac [2] ll_mp) 

228 
prefer 2 apply (assumption) 

229 
apply (rule context3) 

230 
apply (rule context3) 

231 
apply (rule context1) 

232 
done 

233 

61386  234 
lemma or_to_and: "!((!(A ++ B)) o 0) \<turnstile> !( ((!A) o 0) && ((!B) o 0))" 
55232  235 
by best 
21427  236 

61386  237 
lemma o_a_rule: "$F, !( ((!A) o 0) && ((!B) o 0)), $G \<turnstile> C \<Longrightarrow> 
238 
$F, !((!(A ++ B)) o 0), $G \<turnstile> C" 

21427  239 
apply (rule cut) 
240 
apply (rule_tac [2] or_to_and) 

241 
prefer 2 apply (assumption) 

242 
apply (rule context3) 

243 
apply (rule context1) 

244 
done 

245 

61386  246 
lemma conj_imp: "((!A) o C) ++ ((!B) o C) \<turnstile> (!(A && B)) o C" 
21427  247 
apply (rule impr) 
248 
apply (rule conj_lemma) 

249 
apply (rule disjl) 

55232  250 
apply (rule mp_rule1, best)+ 
21427  251 
done 
252 

61386  253 
lemma not_imp: "!A, !((!B) o 0) \<turnstile> (!((!A) o B)) o 0" 
55232  254 
by best 
21427  255 

61386  256 
lemma a_not_a: "!A o (!A o 0) \<turnstile> !A o 0" 
21427  257 
apply (rule impr) 
258 
apply (rule contract) 

259 
apply (rule impl) 

260 
apply (rule_tac [3] identity) 

261 
apply (rule context1) 

55232  262 
apply best 
21427  263 
done 
264 

61386  265 
lemma a_not_a_rule: "$J1, !A o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A o (!A o 0), $J2 \<turnstile> B" 
21427  266 
apply (rule_tac A = "!A o 0" in cut) 
267 
apply (rule_tac [2] a_not_a) 

55232  268 
prefer 2 apply assumption 
269 
apply best 

21427  270 
done 
271 

60770  272 
ML \<open> 
55228  273 
val safe_pack = 
55232  274 
@{context} 
55228  275 
> fold_rev Cla.add_safe @{thms conj_lemma ll_mp contrad1 
276 
contrad2 mp_rule1 mp_rule2 o_a_rule a_not_a_rule} 

277 
> Cla.add_unsafe @{thm aux_impl} 

278 
> Cla.get_pack; 

21427  279 

55228  280 
val power_pack = 
281 
Cla.put_pack safe_pack @{context} 

282 
> Cla.add_unsafe @{thm impr_contr_der} 

283 
> Cla.get_pack; 

60770  284 
\<close> 
21427  285 

286 
method_setup best_safe = 

60770  287 
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack safe_pack ctxt)))\<close> 
21427  288 

289 
method_setup best_power = 

60770  290 
\<open>Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack power_pack ctxt)))\<close> 
21427  291 

292 

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

294 

61386  295 
lemma "!((!A) o ((!B) o 0)) \<turnstile> (!(A && B)) o 0" 
21427  296 
by best_safe 
297 

61386  298 
lemma "!((!(A && B)) o 0) \<turnstile> !((!A) o ((!B) o 0))" 
21427  299 
by best_safe 
300 

61386  301 
lemma "!( (!((! ((!A) o B) ) o 0)) o 0) \<turnstile> 
21427  302 
(!A) o ( (! ((!B) o 0)) o 0)" 
303 
by best_safe 

304 

61386  305 
lemma "!( (!A) o ( (! ((!B) o 0)) o 0) ) \<turnstile> 
21427  306 
(!((! ((!A) o B) ) o 0)) o 0" 
307 
by best_power 

308 

309 
end 