wenzelm@17481
|
1 |
(* Title: Sequents/ILL.thy
|
paulson@2073
|
2 |
Author: Sara Kalvala and Valeria de Paiva
|
paulson@2073
|
3 |
Copyright 1995 University of Cambridge
|
paulson@2073
|
4 |
*)
|
paulson@2073
|
5 |
|
wenzelm@17481
|
6 |
theory ILL
|
wenzelm@17481
|
7 |
imports Sequents
|
wenzelm@17481
|
8 |
begin
|
paulson@2073
|
9 |
|
paulson@2073
|
10 |
consts
|
wenzelm@14765
|
11 |
Trueprop :: "two_seqi"
|
paulson@2073
|
12 |
|
wenzelm@22894
|
13 |
tens :: "[o, o] => o" (infixr "><" 35)
|
wenzelm@22894
|
14 |
limp :: "[o, o] => o" (infixr "-o" 45)
|
wenzelm@22894
|
15 |
liff :: "[o, o] => o" (infixr "o-o" 45)
|
wenzelm@22894
|
16 |
FShriek :: "o => o" ("! _" [100] 1000)
|
wenzelm@22894
|
17 |
lconj :: "[o, o] => o" (infixr "&&" 35)
|
wenzelm@22894
|
18 |
ldisj :: "[o, o] => o" (infixr "++" 35)
|
wenzelm@22894
|
19 |
zero :: "o" ("0")
|
wenzelm@22894
|
20 |
top :: "o" ("1")
|
wenzelm@22894
|
21 |
eye :: "o" ("I")
|
wenzelm@22894
|
22 |
aneg :: "o=>o" ("~_")
|
paulson@2073
|
23 |
|
paulson@2073
|
24 |
|
wenzelm@14765
|
25 |
(* context manipulation *)
|
paulson@2073
|
26 |
|
paulson@2073
|
27 |
Context :: "two_seqi"
|
paulson@2073
|
28 |
|
wenzelm@14765
|
29 |
(* promotion rule *)
|
paulson@2073
|
30 |
|
paulson@2073
|
31 |
PromAux :: "three_seqi"
|
wenzelm@14765
|
32 |
|
wenzelm@14765
|
33 |
syntax
|
wenzelm@35116
|
34 |
"_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
|
wenzelm@35116
|
35 |
"_Context" :: "two_seqe" ("((_)/ :=: (_))" [6,6] 5)
|
wenzelm@35116
|
36 |
"_PromAux" :: "three_seqe" ("promaux {_||_||_}")
|
paulson@2073
|
37 |
|
wenzelm@17481
|
38 |
parse_translation {*
|
wenzelm@35116
|
39 |
[(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
|
wenzelm@35116
|
40 |
(@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
|
wenzelm@35116
|
41 |
(@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
|
wenzelm@35116
|
42 |
*}
|
wenzelm@17481
|
43 |
|
wenzelm@17481
|
44 |
print_translation {*
|
wenzelm@35116
|
45 |
[(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
|
wenzelm@35116
|
46 |
(@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
|
wenzelm@35116
|
47 |
(@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
|
wenzelm@35116
|
48 |
*}
|
wenzelm@17481
|
49 |
|
paulson@2073
|
50 |
defs
|
paulson@2073
|
51 |
|
wenzelm@17481
|
52 |
liff_def: "P o-o Q == (P -o Q) >< (Q -o P)"
|
paulson@2073
|
53 |
|
wenzelm@17481
|
54 |
aneg_def: "~A == A -o 0"
|
paulson@2073
|
55 |
|
paulson@2073
|
56 |
|
wenzelm@17481
|
57 |
axioms
|
paulson@2073
|
58 |
|
wenzelm@17481
|
59 |
identity: "P |- P"
|
paulson@2073
|
60 |
|
wenzelm@17481
|
61 |
zerol: "$G, 0, $H |- A"
|
paulson@2073
|
62 |
|
paulson@2073
|
63 |
(* RULES THAT DO NOT DIVIDE CONTEXT *)
|
paulson@2073
|
64 |
|
wenzelm@17481
|
65 |
derelict: "$F, A, $G |- C ==> $F, !A, $G |- C"
|
paulson@2073
|
66 |
(* unfortunately, this one removes !A *)
|
paulson@2073
|
67 |
|
wenzelm@17481
|
68 |
contract: "$F, !A, !A, $G |- C ==> $F, !A, $G |- C"
|
wenzelm@14765
|
69 |
|
wenzelm@17481
|
70 |
weaken: "$F, $G |- C ==> $G, !A, $F |- C"
|
paulson@2073
|
71 |
(* weak form of weakening, in practice just to clean context *)
|
paulson@2073
|
72 |
(* weaken and contract not needed (CHECK) *)
|
paulson@2073
|
73 |
|
wenzelm@17481
|
74 |
promote2: "promaux{ || $H || B} ==> $H |- !B"
|
wenzelm@17481
|
75 |
promote1: "promaux{!A, $G || $H || B}
|
wenzelm@17481
|
76 |
==> promaux {$G || $H, !A || B}"
|
wenzelm@17481
|
77 |
promote0: "$G |- A ==> promaux {$G || || A}"
|
paulson@2073
|
78 |
|
paulson@2073
|
79 |
|
wenzelm@14765
|
80 |
|
wenzelm@17481
|
81 |
tensl: "$H, A, B, $G |- C ==> $H, A >< B, $G |- C"
|
paulson@2073
|
82 |
|
wenzelm@17481
|
83 |
impr: "A, $F |- B ==> $F |- A -o B"
|
paulson@2073
|
84 |
|
wenzelm@17481
|
85 |
conjr: "[| $F |- A ;
|
paulson@2073
|
86 |
$F |- B |]
|
paulson@2073
|
87 |
==> $F |- (A && B)"
|
paulson@2073
|
88 |
|
wenzelm@17481
|
89 |
conjll: "$G, A, $H |- C ==> $G, A && B, $H |- C"
|
paulson@2073
|
90 |
|
wenzelm@17481
|
91 |
conjlr: "$G, B, $H |- C ==> $G, A && B, $H |- C"
|
paulson@2073
|
92 |
|
wenzelm@17481
|
93 |
disjrl: "$G |- A ==> $G |- A ++ B"
|
wenzelm@17481
|
94 |
disjrr: "$G |- B ==> $G |- A ++ B"
|
wenzelm@17481
|
95 |
disjl: "[| $G, A, $H |- C ;
|
wenzelm@17481
|
96 |
$G, B, $H |- C |]
|
wenzelm@17481
|
97 |
==> $G, A ++ B, $H |- C"
|
paulson@2073
|
98 |
|
paulson@2073
|
99 |
|
paulson@2073
|
100 |
(* RULES THAT DIVIDE CONTEXT *)
|
paulson@2073
|
101 |
|
wenzelm@17481
|
102 |
tensr: "[| $F, $J :=: $G;
|
wenzelm@17481
|
103 |
$F |- A ;
|
wenzelm@17481
|
104 |
$J |- B |]
|
wenzelm@17481
|
105 |
==> $G |- A >< B"
|
paulson@2073
|
106 |
|
wenzelm@17481
|
107 |
impl: "[| $G, $F :=: $J, $H ;
|
wenzelm@17481
|
108 |
B, $F |- C ;
|
wenzelm@17481
|
109 |
$G |- A |]
|
wenzelm@17481
|
110 |
==> $J, A -o B, $H |- C"
|
paulson@2073
|
111 |
|
wenzelm@14765
|
112 |
|
wenzelm@17481
|
113 |
cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
|
wenzelm@17481
|
114 |
$H1, $H2, $H3, $H4 |- A ;
|
wenzelm@17481
|
115 |
$J1, $J2, A, $J3, $J4 |- B |] ==> $F |- B"
|
paulson@2073
|
116 |
|
paulson@2073
|
117 |
|
paulson@2073
|
118 |
(* CONTEXT RULES *)
|
paulson@2073
|
119 |
|
wenzelm@17481
|
120 |
context1: "$G :=: $G"
|
wenzelm@17481
|
121 |
context2: "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G"
|
wenzelm@17481
|
122 |
context3: "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J"
|
wenzelm@17481
|
123 |
context4a: "$F :=: $H, $G ==> $F :=: $H, !A, $G"
|
wenzelm@17481
|
124 |
context4b: "$F, $H :=: $G ==> $F, !A, $H :=: $G"
|
wenzelm@17481
|
125 |
context5: "$F, $G :=: $H ==> $G, $F :=: $H"
|
paulson@2073
|
126 |
|
wenzelm@21427
|
127 |
|
wenzelm@21427
|
128 |
ML {*
|
wenzelm@39406
|
129 |
val lazy_cs = empty_pack
|
wenzelm@39406
|
130 |
add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},
|
wenzelm@39406
|
131 |
@{thm context2}, @{thm context3}]
|
wenzelm@39406
|
132 |
add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},
|
wenzelm@39406
|
133 |
@{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},
|
wenzelm@39406
|
134 |
@{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},
|
wenzelm@39406
|
135 |
@{thm context1}, @{thm context4a}, @{thm context4b}];
|
wenzelm@21427
|
136 |
|
wenzelm@39406
|
137 |
fun prom_tac n =
|
wenzelm@39406
|
138 |
REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)
|
wenzelm@21427
|
139 |
*}
|
wenzelm@21427
|
140 |
|
wenzelm@21427
|
141 |
method_setup best_lazy =
|
wenzelm@30549
|
142 |
{* Scan.succeed (K (SIMPLE_METHOD' (best_tac lazy_cs))) *}
|
wenzelm@21588
|
143 |
"lazy classical reasoning"
|
wenzelm@21427
|
144 |
|
wenzelm@21427
|
145 |
lemma aux_impl: "$F, $G |- A ==> $F, !(A -o B), $G |- B"
|
wenzelm@21427
|
146 |
apply (rule derelict)
|
wenzelm@21427
|
147 |
apply (rule impl)
|
wenzelm@21427
|
148 |
apply (rule_tac [2] identity)
|
wenzelm@21427
|
149 |
apply (rule context1)
|
wenzelm@21427
|
150 |
apply assumption
|
wenzelm@21427
|
151 |
done
|
wenzelm@21427
|
152 |
|
wenzelm@21427
|
153 |
lemma conj_lemma: " $F, !A, !B, $G |- C ==> $F, !(A && B), $G |- C"
|
wenzelm@21427
|
154 |
apply (rule contract)
|
wenzelm@21427
|
155 |
apply (rule_tac A = " (!A) >< (!B) " in cut)
|
wenzelm@21427
|
156 |
apply (rule_tac [2] tensr)
|
wenzelm@21427
|
157 |
prefer 3
|
wenzelm@21427
|
158 |
apply (subgoal_tac "! (A && B) |- !A")
|
wenzelm@21427
|
159 |
apply assumption
|
wenzelm@21427
|
160 |
apply best_lazy
|
wenzelm@21427
|
161 |
prefer 3
|
wenzelm@21427
|
162 |
apply (subgoal_tac "! (A && B) |- !B")
|
wenzelm@21427
|
163 |
apply assumption
|
wenzelm@21427
|
164 |
apply best_lazy
|
wenzelm@21427
|
165 |
apply (rule_tac [2] context1)
|
wenzelm@21427
|
166 |
apply (rule_tac [2] tensl)
|
wenzelm@21427
|
167 |
prefer 2 apply (assumption)
|
wenzelm@21427
|
168 |
apply (rule context3)
|
wenzelm@21427
|
169 |
apply (rule context3)
|
wenzelm@21427
|
170 |
apply (rule context1)
|
wenzelm@21427
|
171 |
done
|
wenzelm@21427
|
172 |
|
wenzelm@21427
|
173 |
lemma impr_contract: "!A, !A, $G |- B ==> $G |- (!A) -o B"
|
wenzelm@21427
|
174 |
apply (rule impr)
|
wenzelm@21427
|
175 |
apply (rule contract)
|
wenzelm@21427
|
176 |
apply assumption
|
wenzelm@21427
|
177 |
done
|
wenzelm@21427
|
178 |
|
wenzelm@21427
|
179 |
lemma impr_contr_der: "A, !A, $G |- B ==> $G |- (!A) -o B"
|
wenzelm@21427
|
180 |
apply (rule impr)
|
wenzelm@21427
|
181 |
apply (rule contract)
|
wenzelm@21427
|
182 |
apply (rule derelict)
|
wenzelm@21427
|
183 |
apply assumption
|
wenzelm@21427
|
184 |
done
|
wenzelm@21427
|
185 |
|
wenzelm@21427
|
186 |
lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
|
wenzelm@21427
|
187 |
apply (rule impl)
|
wenzelm@21427
|
188 |
apply (rule_tac [3] identity)
|
wenzelm@21427
|
189 |
apply (rule context3)
|
wenzelm@21427
|
190 |
apply (rule context1)
|
wenzelm@21427
|
191 |
apply (rule zerol)
|
wenzelm@21427
|
192 |
done
|
wenzelm@21427
|
193 |
|
wenzelm@21427
|
194 |
|
wenzelm@21427
|
195 |
lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
|
wenzelm@21427
|
196 |
apply (rule impl)
|
wenzelm@21427
|
197 |
apply (rule_tac [3] identity)
|
wenzelm@21427
|
198 |
apply (rule context3)
|
wenzelm@21427
|
199 |
apply (rule context1)
|
wenzelm@21427
|
200 |
apply (rule zerol)
|
wenzelm@21427
|
201 |
done
|
wenzelm@21427
|
202 |
|
wenzelm@21427
|
203 |
lemma ll_mp: "A -o B, A |- B"
|
wenzelm@21427
|
204 |
apply (rule impl)
|
wenzelm@21427
|
205 |
apply (rule_tac [2] identity)
|
wenzelm@21427
|
206 |
apply (rule_tac [2] identity)
|
wenzelm@21427
|
207 |
apply (rule context1)
|
wenzelm@21427
|
208 |
done
|
wenzelm@21427
|
209 |
|
wenzelm@21427
|
210 |
lemma mp_rule1: "$F, B, $G, $H |- C ==> $F, A, $G, A -o B, $H |- C"
|
wenzelm@21427
|
211 |
apply (rule_tac A = "B" in cut)
|
wenzelm@21427
|
212 |
apply (rule_tac [2] ll_mp)
|
wenzelm@21427
|
213 |
prefer 2 apply (assumption)
|
wenzelm@21427
|
214 |
apply (rule context3)
|
wenzelm@21427
|
215 |
apply (rule context3)
|
wenzelm@21427
|
216 |
apply (rule context1)
|
wenzelm@21427
|
217 |
done
|
wenzelm@21427
|
218 |
|
wenzelm@21427
|
219 |
lemma mp_rule2: "$F, B, $G, $H |- C ==> $F, A -o B, $G, A, $H |- C"
|
wenzelm@21427
|
220 |
apply (rule_tac A = "B" in cut)
|
wenzelm@21427
|
221 |
apply (rule_tac [2] ll_mp)
|
wenzelm@21427
|
222 |
prefer 2 apply (assumption)
|
wenzelm@21427
|
223 |
apply (rule context3)
|
wenzelm@21427
|
224 |
apply (rule context3)
|
wenzelm@21427
|
225 |
apply (rule context1)
|
wenzelm@21427
|
226 |
done
|
wenzelm@21427
|
227 |
|
wenzelm@21427
|
228 |
lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
|
wenzelm@21427
|
229 |
by best_lazy
|
wenzelm@21427
|
230 |
|
wenzelm@21427
|
231 |
lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C ==>
|
wenzelm@21427
|
232 |
$F, !((!(A ++ B)) -o 0), $G |- C"
|
wenzelm@21427
|
233 |
apply (rule cut)
|
wenzelm@21427
|
234 |
apply (rule_tac [2] or_to_and)
|
wenzelm@21427
|
235 |
prefer 2 apply (assumption)
|
wenzelm@21427
|
236 |
apply (rule context3)
|
wenzelm@21427
|
237 |
apply (rule context1)
|
wenzelm@21427
|
238 |
done
|
wenzelm@21427
|
239 |
|
wenzelm@21427
|
240 |
lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
|
wenzelm@21427
|
241 |
apply (rule impr)
|
wenzelm@21427
|
242 |
apply (rule conj_lemma)
|
wenzelm@21427
|
243 |
apply (rule disjl)
|
wenzelm@21427
|
244 |
apply (rule mp_rule1, best_lazy)+
|
wenzelm@21427
|
245 |
done
|
wenzelm@21427
|
246 |
|
wenzelm@21427
|
247 |
lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
|
wenzelm@21427
|
248 |
by best_lazy
|
wenzelm@21427
|
249 |
|
wenzelm@21427
|
250 |
lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
|
wenzelm@21427
|
251 |
apply (rule impr)
|
wenzelm@21427
|
252 |
apply (rule contract)
|
wenzelm@21427
|
253 |
apply (rule impl)
|
wenzelm@21427
|
254 |
apply (rule_tac [3] identity)
|
wenzelm@21427
|
255 |
apply (rule context1)
|
wenzelm@21427
|
256 |
apply best_lazy
|
wenzelm@21427
|
257 |
done
|
wenzelm@21427
|
258 |
|
wenzelm@21427
|
259 |
lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B ==> $J1, !A -o (!A -o 0), $J2 |- B"
|
wenzelm@21427
|
260 |
apply (rule_tac A = "!A -o 0" in cut)
|
wenzelm@21427
|
261 |
apply (rule_tac [2] a_not_a)
|
wenzelm@21427
|
262 |
prefer 2 apply (assumption)
|
wenzelm@21427
|
263 |
apply best_lazy
|
wenzelm@21427
|
264 |
done
|
wenzelm@21427
|
265 |
|
wenzelm@21427
|
266 |
ML {*
|
wenzelm@39406
|
267 |
val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},
|
wenzelm@39406
|
268 |
@{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},
|
wenzelm@39406
|
269 |
@{thm a_not_a_rule}]
|
wenzelm@39406
|
270 |
add_unsafes [@{thm aux_impl}];
|
wenzelm@21427
|
271 |
|
wenzelm@39406
|
272 |
val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];
|
wenzelm@21427
|
273 |
*}
|
wenzelm@21427
|
274 |
|
wenzelm@21427
|
275 |
|
wenzelm@21427
|
276 |
method_setup best_safe =
|
wenzelm@43685
|
277 |
{* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *}
|
wenzelm@21427
|
278 |
|
wenzelm@21427
|
279 |
method_setup best_power =
|
wenzelm@43685
|
280 |
{* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *}
|
wenzelm@21427
|
281 |
|
wenzelm@21427
|
282 |
|
wenzelm@21427
|
283 |
(* Some examples from Troelstra and van Dalen *)
|
wenzelm@21427
|
284 |
|
wenzelm@21427
|
285 |
lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
|
wenzelm@21427
|
286 |
by best_safe
|
wenzelm@21427
|
287 |
|
wenzelm@21427
|
288 |
lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
|
wenzelm@21427
|
289 |
by best_safe
|
wenzelm@21427
|
290 |
|
wenzelm@21427
|
291 |
lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
|
wenzelm@21427
|
292 |
(!A) -o ( (! ((!B) -o 0)) -o 0)"
|
wenzelm@21427
|
293 |
by best_safe
|
wenzelm@21427
|
294 |
|
wenzelm@21427
|
295 |
lemma "!( (!A) -o ( (! ((!B) -o 0)) -o 0) ) |-
|
wenzelm@21427
|
296 |
(!((! ((!A) -o B) ) -o 0)) -o 0"
|
wenzelm@21427
|
297 |
by best_power
|
wenzelm@21427
|
298 |
|
wenzelm@21427
|
299 |
end
|