1 (* Title: Sequents/LK0.thy
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3 Copyright 1993 University of Cambridge
5 There may be printing problems if a seqent is in expanded normal form
6 (eta-expanded, beta-contracted).
9 header {* Classical First-Order Sequent Calculus *}
20 Trueprop :: "two_seqi"
24 equal :: "['a,'a] => o" (infixl "=" 50)
25 Not :: "o => o" ("~ _" [40] 40)
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)
30 The :: "('a => o) => 'a" (binder "THE " 10)
31 All :: "('a => o) => o" (binder "ALL " 10)
32 Ex :: "('a => o) => o" (binder "EX " 10)
35 "_Trueprop" :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
37 parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
38 print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
41 not_equal (infixl "~=" 50) where
45 Not ("\<not> _" [40] 40) and
46 conj (infixr "\<and>" 35) and
47 disj (infixr "\<or>" 30) and
48 imp (infixr "\<longrightarrow>" 25) and
49 iff (infixr "\<longleftrightarrow>" 25) and
50 All (binder "\<forall>" 10) and
51 Ex (binder "\<exists>" 10) and
52 not_equal (infixl "\<noteq>" 50)
54 notation (HTML output)
55 Not ("\<not> _" [40] 40) and
56 conj (infixr "\<and>" 35) and
57 disj (infixr "\<or>" 30) and
58 All (binder "\<forall>" 10) and
59 Ex (binder "\<exists>" 10) and
60 not_equal (infixl "\<noteq>" 50)
64 (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
66 contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and
67 contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and
69 thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and
70 thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and
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
75 cut: "[| $H |- $E, P; $H, P |- $E |] ==> $H |- $E" and
77 (*Propositional rules*)
79 basic: "$H, P, $G |- $E, P, $F" and
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
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
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
90 notR: "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and
91 notL: "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and
93 FalseL: "$H, False, $G |- $E" and
95 True_def: "True == False-->False" and
96 iff_def: "P<->Q == (P-->Q) & (Q-->P)"
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
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
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)"
114 eq_reflection: "|- x=y ==> (x==y)" and
115 iff_reflection: "|- P<->Q ==> (P==Q)"
120 The: "[| $H |- $E, P(a), $F; !!x.$H, P(x) |- $E, x=a, $F |] ==>
121 $H |- $E, P(THE x. P(x)), $F"
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)"
127 (** Structural Rules on formulas **)
131 lemma contR: "$H |- $E, P, P, $F ==> $H |- $E, P, $F"
134 lemma contL: "$H, P, P, $G |- $E ==> $H, P, $G |- $E"
139 lemma thinR: "$H |- $E, $F ==> $H |- $E, P, $F"
142 lemma thinL: "$H, $G |- $E ==> $H, P, $G |- $E"
147 lemma exchR: "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F"
150 lemma exchL: "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E"
154 (*Cut and thin, replacing the right-side formula*)
155 fun cutR_tac ctxt s i =
156 res_inst_tac ctxt [(("P", 0), s) ] @{thm cut} i THEN rtac @{thm thinR} i
158 (*Cut and thin, replacing the left-side formula*)
159 fun cutL_tac ctxt s i =
160 res_inst_tac ctxt [(("P", 0), s)] @{thm cut} i THEN rtac @{thm thinL} (i+1)
164 (** If-and-only-if rules **)
166 "[| $H,P |- $E,Q,$F; $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
167 apply (unfold iff_def)
168 apply (assumption | rule conjR impR)+
172 "[| $H,$G |- $E,P,Q; $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
173 apply (unfold iff_def)
174 apply (assumption | rule conjL impL basic)+
177 lemma iff_refl: "$H |- $E, (P <-> P), $F"
178 apply (rule iffR basic)+
181 lemma TrueR: "$H |- $E, True, $F"
182 apply (unfold True_def)
189 assumes p1: "$H |- $E, P(a), $F"
190 and p2: "!!x. $H, P(x) |- $E, x=a, $F"
191 shows "$H |- $E, (THE x. P(x)) = a, $F"
193 apply (rule_tac [2] p2)
194 apply (rule The, rule thinR, rule exchRS, rule p1)
195 apply (rule thinR, rule exchRS, rule p2)
199 (** Weakened quantifier rules. Incomplete, they let the search terminate.**)
201 lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
206 lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
214 val prop_pack = empty_pack add_safes
215 [@{thm basic}, @{thm refl}, @{thm TrueR}, @{thm FalseL},
216 @{thm conjL}, @{thm conjR}, @{thm disjL}, @{thm disjR}, @{thm impL}, @{thm impR},
217 @{thm notL}, @{thm notR}, @{thm iffL}, @{thm iffR}];
219 val LK_pack = prop_pack add_safes [@{thm allR}, @{thm exL}]
220 add_unsafes [@{thm allL_thin}, @{thm exR_thin}, @{thm the_equality}];
222 val LK_dup_pack = prop_pack add_safes [@{thm allR}, @{thm exL}]
223 add_unsafes [@{thm allL}, @{thm exR}, @{thm the_equality}];
227 rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i;
230 method_setup fast_prop = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
231 method_setup fast = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
232 method_setup fast_dup = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
233 method_setup best = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
234 method_setup best_dup = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
238 assumes major: "$H |- $E, $F, P --> Q"
239 and minor: "$H |- $E, $F, P"
240 shows "$H |- $E, Q, $F"
241 apply (rule thinRS [THEN cut], rule major)
242 apply (tactic "step_tac LK_pack 1")
243 apply (rule thinR, rule minor)
247 assumes major: "$H, $G |- $E, P --> Q"
248 and minor: "$H, $G, Q |- $E"
249 shows "$H, P, $G |- $E"
250 apply (rule thinL [THEN cut], rule major)
251 apply (tactic "step_tac LK_pack 1")
252 apply (rule thinL, rule minor)
256 (** Two rules to generate left- and right- rules from implications **)
259 assumes major: "|- P --> Q"
260 and minor: "$H |- $E, $F, P"
261 shows "$H |- $E, Q, $F"
263 apply (rule_tac [2] minor)
264 apply (rule thinRS, rule major [THEN thinLS])
268 assumes major: "|- P --> Q"
269 and minor: "$H, $G, Q |- $E"
270 shows "$H, P, $G |- $E"
272 apply (rule_tac [2] minor)
273 apply (rule thinRS, rule major [THEN thinLS])
276 (*Can be used to create implications in a subgoal*)
277 lemma backwards_impR:
278 assumes prem: "$H, $G |- $E, $F, P --> Q"
279 shows "$H, P, $G |- $E, Q, $F"
281 apply (rule_tac [2] basic)
282 apply (rule thinR, rule prem)
285 lemma conjunct1: "|-P&Q ==> |-P"
286 apply (erule thinR [THEN cut])
290 lemma conjunct2: "|-P&Q ==> |-Q"
291 apply (erule thinR [THEN cut])
295 lemma spec: "|- (ALL x. P(x)) ==> |- P(x)"
296 apply (erule thinR [THEN cut])
303 lemma sym: "|- a=b --> b=a"
304 by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
306 lemma trans: "|- a=b --> b=c --> a=c"
307 by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
309 (* Symmetry of equality in hypotheses *)
310 lemmas symL = sym [THEN L_of_imp]
312 (* Symmetry of equality in hypotheses *)
313 lemmas symR = sym [THEN R_of_imp]
315 lemma transR: "[| $H|- $E, $F, a=b; $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
316 by (rule trans [THEN R_of_imp, THEN mp_R])
318 (* Two theorms for rewriting only one instance of a definition:
319 the first for definitions of formulae and the second for terms *)
321 lemma def_imp_iff: "(A == B) ==> |- A <-> B"
323 apply (rule iff_refl)
326 lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B"
332 (** if-then-else rules **)
334 lemma if_True: "|- (if True then x else y) = x"
335 unfolding If_def by fast
337 lemma if_False: "|- (if False then x else y) = y"
338 unfolding If_def by fast
340 lemma if_P: "|- P ==> |- (if P then x else y) = x"
341 apply (unfold If_def)
342 apply (erule thinR [THEN cut])
346 lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y";
347 apply (unfold If_def)
348 apply (erule thinR [THEN cut])