author | wenzelm |
Tue, 31 Mar 2015 20:18:10 +0200 | |
changeset 59884 | bbf49d7dfd6f |
parent 59780 | 23b67731f4f0 |
child 60754 | 02924903a6fd |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: Sequents/LK0.thy |
7093 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1993 University of Cambridge |
|
4 |
||
5 |
There may be printing problems if a seqent is in expanded normal form |
|
35113 | 6 |
(eta-expanded, beta-contracted). |
7093 | 7 |
*) |
8 |
||
58889 | 9 |
section {* Classical First-Order Sequent Calculus *} |
17481 | 10 |
|
11 |
theory LK0 |
|
12 |
imports Sequents |
|
13 |
begin |
|
7093 | 14 |
|
55380
4de48353034e
prefer vacuous definitional type classes over axiomatic ones;
wenzelm
parents:
55233
diff
changeset
|
15 |
class "term" |
36452 | 16 |
default_sort "term" |
7093 | 17 |
|
18 |
consts |
|
19 |
||
21524 | 20 |
Trueprop :: "two_seqi" |
7093 | 21 |
|
17481 | 22 |
True :: o |
23 |
False :: o |
|
22894 | 24 |
equal :: "['a,'a] => o" (infixl "=" 50) |
17481 | 25 |
Not :: "o => o" ("~ _" [40] 40) |
22894 | 26 |
conj :: "[o,o] => o" (infixr "&" 35) |
27 |
disj :: "[o,o] => o" (infixr "|" 30) |
|
28 |
imp :: "[o,o] => o" (infixr "-->" 25) |
|
29 |
iff :: "[o,o] => o" (infixr "<->" 25) |
|
17481 | 30 |
The :: "('a => o) => 'a" (binder "THE " 10) |
31 |
All :: "('a => o) => o" (binder "ALL " 10) |
|
32 |
Ex :: "('a => o) => o" (binder "EX " 10) |
|
7093 | 33 |
|
34 |
syntax |
|
35113 | 35 |
"_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5) |
17481 | 36 |
|
52143 | 37 |
parse_translation {* [(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))] *} |
38 |
print_translation {* [(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))] *} |
|
7093 | 39 |
|
22894 | 40 |
abbreviation |
41 |
not_equal (infixl "~=" 50) where |
|
42 |
"x ~= y == ~ (x = y)" |
|
7093 | 43 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
44 |
notation (xsymbols) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
45 |
Not ("\<not> _" [40] 40) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
46 |
conj (infixr "\<and>" 35) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
47 |
disj (infixr "\<or>" 30) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
48 |
imp (infixr "\<longrightarrow>" 25) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
49 |
iff (infixr "\<longleftrightarrow>" 25) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
50 |
All (binder "\<forall>" 10) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
51 |
Ex (binder "\<exists>" 10) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
52 |
not_equal (infixl "\<noteq>" 50) |
7093 | 53 |
|
35355
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
54 |
notation (HTML output) |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
55 |
Not ("\<not> _" [40] 40) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
56 |
conj (infixr "\<and>" 35) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
57 |
disj (infixr "\<or>" 30) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
58 |
All (binder "\<forall>" 10) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
59 |
Ex (binder "\<exists>" 10) and |
613e133966ea
modernized syntax declarations, and make them actually work with authentic syntax;
wenzelm
parents:
35113
diff
changeset
|
60 |
not_equal (infixl "\<noteq>" 50) |
7093 | 61 |
|
51309 | 62 |
axiomatization where |
7093 | 63 |
|
64 |
(*Structural rules: contraction, thinning, exchange [Soren Heilmann] *) |
|
65 |
||
51309 | 66 |
contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and |
67 |
contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and |
|
7093 | 68 |
|
51309 | 69 |
thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and |
70 |
thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and |
|
7093 | 71 |
|
51309 | 72 |
exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" and |
73 |
exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" and |
|
7093 | 74 |
|
51309 | 75 |
cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" and |
7093 | 76 |
|
77 |
(*Propositional rules*) |
|
78 |
||
51309 | 79 |
basic: "$H, P, $G |- $E, P, $F" and |
7093 | 80 |
|
51309 | 81 |
conjR: "[| $H|- $E, P, $F; $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" and |
82 |
conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" and |
|
7093 | 83 |
|
51309 | 84 |
disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" and |
85 |
disjL: "[| $H, P, $G |- $E; $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" and |
|
7093 | 86 |
|
51309 | 87 |
impR: "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" and |
88 |
impL: "[| $H,$G |- $E,P; $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" and |
|
7093 | 89 |
|
51309 | 90 |
notR: "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and |
91 |
notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and |
|
7093 | 92 |
|
51309 | 93 |
FalseL: "$H, False, $G |- $E" and |
7093 | 94 |
|
51309 | 95 |
True_def: "True == False-->False" and |
17481 | 96 |
iff_def: "P<->Q == (P-->Q) & (Q-->P)" |
7093 | 97 |
|
51309 | 98 |
axiomatization where |
7093 | 99 |
(*Quantifiers*) |
100 |
||
51309 | 101 |
allR: "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" and |
102 |
allL: "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" and |
|
7093 | 103 |
|
51309 | 104 |
exR: "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" and |
105 |
exL: "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" and |
|
7093 | 106 |
|
107 |
(*Equality*) |
|
51309 | 108 |
refl: "$H |- $E, a=a, $F" and |
109 |
subst: "\<And>G H E. $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)" |
|
7093 | 110 |
|
111 |
(* Reflection *) |
|
112 |
||
51309 | 113 |
axiomatization where |
114 |
eq_reflection: "|- x=y ==> (x==y)" and |
|
17481 | 115 |
iff_reflection: "|- P<->Q ==> (P==Q)" |
7093 | 116 |
|
117 |
(*Descriptions*) |
|
118 |
||
51309 | 119 |
axiomatization where |
17481 | 120 |
The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==> |
7093 | 121 |
$H |- $E, P(THE x. P(x)), $F" |
122 |
||
51309 | 123 |
definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10) |
124 |
where "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)" |
|
7093 | 125 |
|
21426 | 126 |
|
127 |
(** Structural Rules on formulas **) |
|
128 |
||
129 |
(*contraction*) |
|
130 |
||
131 |
lemma contR: "$H |- $E, P, P, $F ==> $H |- $E, P, $F" |
|
132 |
by (rule contRS) |
|
133 |
||
134 |
lemma contL: "$H, P, P, $G |- $E ==> $H, P, $G |- $E" |
|
135 |
by (rule contLS) |
|
136 |
||
137 |
(*thinning*) |
|
138 |
||
139 |
lemma thinR: "$H |- $E, $F ==> $H |- $E, P, $F" |
|
140 |
by (rule thinRS) |
|
141 |
||
142 |
lemma thinL: "$H, $G |- $E ==> $H, P, $G |- $E" |
|
143 |
by (rule thinLS) |
|
144 |
||
145 |
(*exchange*) |
|
146 |
||
147 |
lemma exchR: "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F" |
|
148 |
by (rule exchRS) |
|
149 |
||
150 |
lemma exchL: "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E" |
|
151 |
by (rule exchLS) |
|
152 |
||
153 |
ML {* |
|
154 |
(*Cut and thin, replacing the right-side formula*) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset
|
155 |
fun cutR_tac ctxt s i = |
59780 | 156 |
Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN |
59763 | 157 |
rtac @{thm thinR} i |
21426 | 158 |
|
159 |
(*Cut and thin, replacing the left-side formula*) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
27146
diff
changeset
|
160 |
fun cutL_tac ctxt s i = |
59780 | 161 |
Rule_Insts.res_inst_tac ctxt [((("P", 0), Position.none), s)] [] @{thm cut} i THEN |
59763 | 162 |
rtac @{thm thinL} (i + 1) |
21426 | 163 |
*} |
164 |
||
165 |
||
166 |
(** If-and-only-if rules **) |
|
55228 | 167 |
lemma iffR: |
21426 | 168 |
"[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F" |
169 |
apply (unfold iff_def) |
|
170 |
apply (assumption | rule conjR impR)+ |
|
171 |
done |
|
172 |
||
55228 | 173 |
lemma iffL: |
21426 | 174 |
"[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E" |
175 |
apply (unfold iff_def) |
|
176 |
apply (assumption | rule conjL impL basic)+ |
|
177 |
done |
|
178 |
||
179 |
lemma iff_refl: "$H |- $E, (P <-> P), $F" |
|
180 |
apply (rule iffR basic)+ |
|
181 |
done |
|
182 |
||
183 |
lemma TrueR: "$H |- $E, True, $F" |
|
184 |
apply (unfold True_def) |
|
185 |
apply (rule impR) |
|
186 |
apply (rule basic) |
|
187 |
done |
|
188 |
||
189 |
(*Descriptions*) |
|
190 |
lemma the_equality: |
|
191 |
assumes p1: "$H |- $E, P(a), $F" |
|
192 |
and p2: "!!x. $H, P(x) |- $E, x=a, $F" |
|
193 |
shows "$H |- $E, (THE x. P(x)) = a, $F" |
|
194 |
apply (rule cut) |
|
195 |
apply (rule_tac [2] p2) |
|
196 |
apply (rule The, rule thinR, rule exchRS, rule p1) |
|
197 |
apply (rule thinR, rule exchRS, rule p2) |
|
198 |
done |
|
199 |
||
200 |
||
201 |
(** Weakened quantifier rules. Incomplete, they let the search terminate.**) |
|
202 |
||
203 |
lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E" |
|
204 |
apply (rule allL) |
|
205 |
apply (erule thinL) |
|
206 |
done |
|
207 |
||
208 |
lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F" |
|
209 |
apply (rule exR) |
|
210 |
apply (erule thinR) |
|
211 |
done |
|
212 |
||
213 |
(*The rules of LK*) |
|
214 |
||
55228 | 215 |
lemmas [safe] = |
216 |
iffR iffL |
|
217 |
notR notL |
|
218 |
impR impL |
|
219 |
disjR disjL |
|
220 |
conjR conjL |
|
221 |
FalseL TrueR |
|
222 |
refl basic |
|
223 |
ML {* val prop_pack = Cla.get_pack @{context} *} |
|
224 |
||
225 |
lemmas [safe] = exL allR |
|
226 |
lemmas [unsafe] = the_equality exR_thin allL_thin |
|
227 |
ML {* val LK_pack = Cla.get_pack @{context} *} |
|
21426 | 228 |
|
55228 | 229 |
ML {* |
230 |
val LK_dup_pack = |
|
231 |
Cla.put_pack prop_pack @{context} |
|
232 |
|> fold_rev Cla.add_safe @{thms allR exL} |
|
233 |
|> fold_rev Cla.add_unsafe @{thms allL exR the_equality} |
|
234 |
|> Cla.get_pack; |
|
235 |
*} |
|
21426 | 236 |
|
55228 | 237 |
method_setup fast_prop = |
238 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack prop_pack ctxt))) *} |
|
21426 | 239 |
|
55228 | 240 |
method_setup fast_dup = |
241 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.fast_tac (Cla.put_pack LK_dup_pack ctxt))) *} |
|
242 |
||
243 |
method_setup best_dup = |
|
244 |
{* Scan.succeed (fn ctxt => SIMPLE_METHOD' (Cla.best_tac (Cla.put_pack LK_dup_pack ctxt))) *} |
|
7093 | 245 |
|
55233 | 246 |
method_setup lem = {* |
247 |
Attrib.thm >> (fn th => fn _ => |
|
248 |
SIMPLE_METHOD' (fn i => |
|
249 |
rtac (@{thm thinR} RS @{thm cut}) i THEN |
|
250 |
REPEAT (rtac @{thm thinL} i) THEN |
|
251 |
rtac th i)) |
|
252 |
*} |
|
253 |
||
7118
ee384c7b7416
adding missing declarations for the <<...>> notation
paulson
parents:
7093
diff
changeset
|
254 |
|
21426 | 255 |
lemma mp_R: |
256 |
assumes major: "$H |- $E, $F, P --> Q" |
|
257 |
and minor: "$H |- $E, $F, P" |
|
258 |
shows "$H |- $E, Q, $F" |
|
259 |
apply (rule thinRS [THEN cut], rule major) |
|
55228 | 260 |
apply step |
21426 | 261 |
apply (rule thinR, rule minor) |
262 |
done |
|
263 |
||
264 |
lemma mp_L: |
|
265 |
assumes major: "$H, $G |- $E, P --> Q" |
|
266 |
and minor: "$H, $G, Q |- $E" |
|
267 |
shows "$H, P, $G |- $E" |
|
268 |
apply (rule thinL [THEN cut], rule major) |
|
55228 | 269 |
apply step |
21426 | 270 |
apply (rule thinL, rule minor) |
271 |
done |
|
272 |
||
273 |
||
274 |
(** Two rules to generate left- and right- rules from implications **) |
|
275 |
||
276 |
lemma R_of_imp: |
|
277 |
assumes major: "|- P --> Q" |
|
278 |
and minor: "$H |- $E, $F, P" |
|
279 |
shows "$H |- $E, Q, $F" |
|
280 |
apply (rule mp_R) |
|
281 |
apply (rule_tac [2] minor) |
|
282 |
apply (rule thinRS, rule major [THEN thinLS]) |
|
283 |
done |
|
284 |
||
285 |
lemma L_of_imp: |
|
286 |
assumes major: "|- P --> Q" |
|
287 |
and minor: "$H, $G, Q |- $E" |
|
288 |
shows "$H, P, $G |- $E" |
|
289 |
apply (rule mp_L) |
|
290 |
apply (rule_tac [2] minor) |
|
291 |
apply (rule thinRS, rule major [THEN thinLS]) |
|
292 |
done |
|
293 |
||
294 |
(*Can be used to create implications in a subgoal*) |
|
295 |
lemma backwards_impR: |
|
296 |
assumes prem: "$H, $G |- $E, $F, P --> Q" |
|
297 |
shows "$H, P, $G |- $E, Q, $F" |
|
298 |
apply (rule mp_L) |
|
299 |
apply (rule_tac [2] basic) |
|
300 |
apply (rule thinR, rule prem) |
|
301 |
done |
|
302 |
||
303 |
lemma conjunct1: "|-P&Q ==> |-P" |
|
304 |
apply (erule thinR [THEN cut]) |
|
305 |
apply fast |
|
306 |
done |
|
307 |
||
308 |
lemma conjunct2: "|-P&Q ==> |-Q" |
|
309 |
apply (erule thinR [THEN cut]) |
|
310 |
apply fast |
|
311 |
done |
|
312 |
||
313 |
lemma spec: "|- (ALL x. P(x)) ==> |- P(x)" |
|
314 |
apply (erule thinR [THEN cut]) |
|
315 |
apply fast |
|
316 |
done |
|
317 |
||
318 |
||
319 |
(** Equality **) |
|
320 |
||
321 |
lemma sym: "|- a=b --> b=a" |
|
55228 | 322 |
by (safe add!: subst) |
21426 | 323 |
|
324 |
lemma trans: "|- a=b --> b=c --> a=c" |
|
55228 | 325 |
by (safe add!: subst) |
21426 | 326 |
|
327 |
(* Symmetry of equality in hypotheses *) |
|
45602 | 328 |
lemmas symL = sym [THEN L_of_imp] |
21426 | 329 |
|
330 |
(* Symmetry of equality in hypotheses *) |
|
45602 | 331 |
lemmas symR = sym [THEN R_of_imp] |
21426 | 332 |
|
333 |
lemma transR: "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F" |
|
334 |
by (rule trans [THEN R_of_imp, THEN mp_R]) |
|
335 |
||
336 |
(* Two theorms for rewriting only one instance of a definition: |
|
337 |
the first for definitions of formulae and the second for terms *) |
|
338 |
||
339 |
lemma def_imp_iff: "(A == B) ==> |- A <-> B" |
|
340 |
apply unfold |
|
341 |
apply (rule iff_refl) |
|
342 |
done |
|
343 |
||
344 |
lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B" |
|
345 |
apply unfold |
|
346 |
apply (rule refl) |
|
347 |
done |
|
348 |
||
349 |
||
350 |
(** if-then-else rules **) |
|
351 |
||
352 |
lemma if_True: "|- (if True then x else y) = x" |
|
353 |
unfolding If_def by fast |
|
354 |
||
355 |
lemma if_False: "|- (if False then x else y) = y" |
|
356 |
unfolding If_def by fast |
|
357 |
||
358 |
lemma if_P: "|- P ==> |- (if P then x else y) = x" |
|
359 |
apply (unfold If_def) |
|
360 |
apply (erule thinR [THEN cut]) |
|
361 |
apply fast |
|
362 |
done |
|
363 |
||
58860 | 364 |
lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y" |
21426 | 365 |
apply (unfold If_def) |
366 |
apply (erule thinR [THEN cut]) |
|
367 |
apply fast |
|
368 |
done |
|
369 |
||
370 |
end |