1 (* Title: FOLP/IFOLP.ML |
1 (* Title: FOLP/IFOLP.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
|
6 Tactics and lemmas for IFOLP (Intuitionistic First-Order Logic with Proofs) |
|
7 *) |
5 *) |
|
6 |
8 (*** Sequent-style elimination rules for & --> and ALL ***) |
7 (*** Sequent-style elimination rules for & --> and ALL ***) |
9 |
8 |
10 val prems= Goal |
9 val prems= Goal |
11 "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R"; |
10 "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R"; |
12 by (REPEAT (resolve_tac prems 1 |
11 by (REPEAT (resolve_tac prems 1 |
13 ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ; |
12 ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ; |
14 qed "conjE"; |
13 qed "conjE"; |
15 |
14 |
16 val prems= Goal |
15 val prems= Goal |
17 "[| p:P-->Q; q:P; !!x. x:Q ==> r(x):R |] ==> ?p:R"; |
16 "[| p:P-->Q; q:P; !!x. x:Q ==> r(x):R |] ==> ?p:R"; |
18 by (REPEAT (resolve_tac (prems@[mp]) 1)) ; |
17 by (REPEAT (resolve_tac (prems@[mp]) 1)) ; |
19 qed "impE"; |
18 qed "impE"; |
20 |
19 |
21 val prems= Goal |
20 val prems= Goal |
22 "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"; |
21 "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R"; |
23 by (REPEAT (resolve_tac (prems@[spec]) 1)) ; |
22 by (REPEAT (resolve_tac (prems@[spec]) 1)) ; |
24 qed "allE"; |
23 qed "allE"; |
25 |
24 |
26 (*Duplicates the quantifier; for use with eresolve_tac*) |
25 (*Duplicates the quantifier; for use with eresolve_tac*) |
27 val prems= Goal |
26 val prems= Goal |
28 "[| p:ALL x. P(x); !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \ |
27 "[| p:ALL x. P(x); !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \ |
29 \ |] ==> ?p:R"; |
28 \ |] ==> ?p:R"; |
30 by (REPEAT (resolve_tac (prems@[spec]) 1)) ; |
29 by (REPEAT (resolve_tac (prems@[spec]) 1)) ; |
31 qed "all_dupE"; |
30 qed "all_dupE"; |
32 |
31 |
33 |
32 |
34 (*** Negation rules, which translate between ~P and P-->False ***) |
33 (*** Negation rules, which translate between ~P and P-->False ***) |
35 |
34 |
36 val notI = prove_goalw IFOLP.thy [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P" |
35 val notI = prove_goalw (the_context ()) [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P" |
37 (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); |
36 (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); |
38 |
37 |
39 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P; q:P |] ==> ?p:R" |
38 val notE = prove_goalw (the_context ()) [not_def] "[| p:~P; q:P |] ==> ?p:R" |
40 (fn prems=> |
39 (fn prems=> |
41 [ (resolve_tac [mp RS FalseE] 1), |
40 [ (resolve_tac [mp RS FalseE] 1), |
42 (REPEAT (resolve_tac prems 1)) ]); |
41 (REPEAT (resolve_tac prems 1)) ]); |
43 |
42 |
44 (*This is useful with the special implication rules for each kind of P. *) |
43 (*This is useful with the special implication rules for each kind of P. *) |
45 val prems= Goal |
44 val prems= Goal |
46 "[| p:~P; !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"; |
45 "[| p:~P; !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q"; |
47 by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ; |
46 by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ; |
48 qed "not_to_imp"; |
47 qed "not_to_imp"; |
49 |
48 |
50 |
49 |
95 fun int_uniq_mp_tac i = eresolve_tac [notE,impE] i THEN uniq_assume_tac i; |
94 fun int_uniq_mp_tac i = eresolve_tac [notE,impE] i THEN uniq_assume_tac i; |
96 |
95 |
97 |
96 |
98 (*** If-and-only-if ***) |
97 (*** If-and-only-if ***) |
99 |
98 |
100 val iffI = prove_goalw IFOLP.thy [iff_def] |
99 val iffI = prove_goalw (the_context ()) [iff_def] |
101 "[| !!x. x:P ==> q(x):Q; !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q" |
100 "[| !!x. x:P ==> q(x):Q; !!x. x:Q ==> r(x):P |] ==> ?p:P<->Q" |
102 (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); |
101 (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); |
103 |
102 |
104 |
103 |
105 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
104 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
106 val iffE = prove_goalw IFOLP.thy [iff_def] |
105 val iffE = prove_goalw (the_context ()) [iff_def] |
107 "[| p:P <-> Q; !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R" |
106 "[| p:P <-> Q; !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R" |
108 (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); |
107 (fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); |
109 |
108 |
110 (* Destruct rules for <-> similar to Modus Ponens *) |
109 (* Destruct rules for <-> similar to Modus Ponens *) |
111 |
110 |
112 val iffD1 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; q:P |] ==> ?p:Q" |
111 val iffD1 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q; q:P |] ==> ?p:Q" |
113 (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
112 (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
114 |
113 |
115 val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; q:Q |] ==> ?p:P" |
114 val iffD2 = prove_goalw (the_context ()) [iff_def] "[| p:P <-> Q; q:Q |] ==> ?p:P" |
116 (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
115 (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
117 |
116 |
118 Goal "?p:P <-> P"; |
117 Goal "?p:P <-> P"; |
119 by (REPEAT (ares_tac [iffI] 1)) ; |
118 by (REPEAT (ares_tac [iffI] 1)) ; |
120 qed "iff_refl"; |
119 qed "iff_refl"; |
135 EX!x such that [EX!y such that P(x,y)] (sequential) |
134 EX!x such that [EX!y such that P(x,y)] (sequential) |
136 EX!x,y such that P(x,y) (simultaneous) |
135 EX!x,y such that P(x,y) (simultaneous) |
137 do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
136 do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
138 ***) |
137 ***) |
139 |
138 |
140 val prems = goalw IFOLP.thy [ex1_def] |
139 val prems = goalw (the_context ()) [ex1_def] |
141 "[| p:P(a); !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"; |
140 "[| p:P(a); !!x u. u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)"; |
142 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; |
141 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; |
143 qed "ex1I"; |
142 qed "ex1I"; |
144 |
143 |
145 val prems = goalw IFOLP.thy [ex1_def] |
144 val prems = goalw (the_context ()) [ex1_def] |
146 "[| p:EX! x. P(x); \ |
145 "[| p:EX! x. P(x); \ |
147 \ !!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\ |
146 \ !!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\ |
148 \ ?a : R"; |
147 \ ?a : R"; |
149 by (cut_facts_tac prems 1); |
148 by (cut_facts_tac prems 1); |
150 by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ; |
149 by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ; |
156 (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
155 (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
157 fun iff_tac prems i = |
156 fun iff_tac prems i = |
158 resolve_tac (prems RL [iffE]) i THEN |
157 resolve_tac (prems RL [iffE]) i THEN |
159 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
158 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
160 |
159 |
161 val conj_cong = prove_goal IFOLP.thy |
160 val conj_cong = prove_goal (the_context ()) |
162 "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')" |
161 "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')" |
163 (fn prems => |
162 (fn prems => |
164 [ (cut_facts_tac prems 1), |
163 [ (cut_facts_tac prems 1), |
165 (REPEAT (ares_tac [iffI,conjI] 1 |
164 (REPEAT (ares_tac [iffI,conjI] 1 |
166 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
165 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
167 ORELSE iff_tac prems 1)) ]); |
166 ORELSE iff_tac prems 1)) ]); |
168 |
167 |
169 val disj_cong = prove_goal IFOLP.thy |
168 val disj_cong = prove_goal (the_context ()) |
170 "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" |
169 "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" |
171 (fn prems => |
170 (fn prems => |
172 [ (cut_facts_tac prems 1), |
171 [ (cut_facts_tac prems 1), |
173 (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
172 (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
174 ORELSE ares_tac [iffI] 1 |
173 ORELSE ares_tac [iffI] 1 |
175 ORELSE mp_tac 1)) ]); |
174 ORELSE mp_tac 1)) ]); |
176 |
175 |
177 val imp_cong = prove_goal IFOLP.thy |
176 val imp_cong = prove_goal (the_context ()) |
178 "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')" |
177 "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')" |
179 (fn prems => |
178 (fn prems => |
180 [ (cut_facts_tac prems 1), |
179 [ (cut_facts_tac prems 1), |
181 (REPEAT (ares_tac [iffI,impI] 1 |
180 (REPEAT (ares_tac [iffI,impI] 1 |
182 ORELSE etac iffE 1 |
181 ORELSE etac iffE 1 |
183 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); |
182 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); |
184 |
183 |
185 val iff_cong = prove_goal IFOLP.thy |
184 val iff_cong = prove_goal (the_context ()) |
186 "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" |
185 "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" |
187 (fn prems => |
186 (fn prems => |
188 [ (cut_facts_tac prems 1), |
187 [ (cut_facts_tac prems 1), |
189 (REPEAT (etac iffE 1 |
188 (REPEAT (etac iffE 1 |
190 ORELSE ares_tac [iffI] 1 |
189 ORELSE ares_tac [iffI] 1 |
191 ORELSE mp_tac 1)) ]); |
190 ORELSE mp_tac 1)) ]); |
192 |
191 |
193 val not_cong = prove_goal IFOLP.thy |
192 val not_cong = prove_goal (the_context ()) |
194 "p:P <-> P' ==> ?p:~P <-> ~P'" |
193 "p:P <-> P' ==> ?p:~P <-> ~P'" |
195 (fn prems => |
194 (fn prems => |
196 [ (cut_facts_tac prems 1), |
195 [ (cut_facts_tac prems 1), |
197 (REPEAT (ares_tac [iffI,notI] 1 |
196 (REPEAT (ares_tac [iffI,notI] 1 |
198 ORELSE mp_tac 1 |
197 ORELSE mp_tac 1 |
199 ORELSE eresolve_tac [iffE,notE] 1)) ]); |
198 ORELSE eresolve_tac [iffE,notE] 1)) ]); |
200 |
199 |
201 val all_cong = prove_goal IFOLP.thy |
200 val all_cong = prove_goal (the_context ()) |
202 "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))" |
201 "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))" |
203 (fn prems => |
202 (fn prems => |
204 [ (REPEAT (ares_tac [iffI,allI] 1 |
203 [ (REPEAT (ares_tac [iffI,allI] 1 |
205 ORELSE mp_tac 1 |
204 ORELSE mp_tac 1 |
206 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); |
205 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); |
207 |
206 |
208 val ex_cong = prove_goal IFOLP.thy |
207 val ex_cong = prove_goal (the_context ()) |
209 "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))" |
208 "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))" |
210 (fn prems => |
209 (fn prems => |
211 [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 |
210 [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 |
212 ORELSE mp_tac 1 |
211 ORELSE mp_tac 1 |
213 ORELSE iff_tac prems 1)) ]); |
212 ORELSE iff_tac prems 1)) ]); |
214 |
213 |
215 (*NOT PROVED |
214 (*NOT PROVED |
216 val ex1_cong = prove_goal IFOLP.thy |
215 val ex1_cong = prove_goal (the_context ()) |
217 "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))" |
216 "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))" |
218 (fn prems => |
217 (fn prems => |
219 [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 |
218 [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 |
220 ORELSE mp_tac 1 |
219 ORELSE mp_tac 1 |
221 ORELSE iff_tac prems 1)) ]); |
220 ORELSE iff_tac prems 1)) ]); |
307 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; |
306 by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; |
308 qed "pred3_cong"; |
307 qed "pred3_cong"; |
309 |
308 |
310 (*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
309 (*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
311 |
310 |
312 val pred_congs = |
311 val pred_congs = |
313 List.concat (map (fn c => |
312 List.concat (map (fn c => |
314 map (fn th => read_instantiate [("P",c)] th) |
313 map (fn th => read_instantiate [("P",c)] th) |
315 [pred1_cong,pred2_cong,pred3_cong]) |
314 [pred1_cong,pred2_cong,pred3_cong]) |
316 (explode"PQRS")); |
315 (explode"PQRS")); |
317 |
316 |
318 (*special case for the equality predicate!*) |
317 (*special case for the equality predicate!*) |
319 val eq_cong = read_instantiate [("P","op =")] pred2_cong; |
318 val eq_cong = read_instantiate [("P","op =")] pred2_cong; |
320 |
319 |
321 |
320 |
322 (*** Simplifications of assumed implications. |
321 (*** Simplifications of assumed implications. |
323 Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE |
322 Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE |
324 used with mp_tac (restricted to atomic formulae) is COMPLETE for |
323 used with mp_tac (restricted to atomic formulae) is COMPLETE for |
325 intuitionistic propositional logic. See |
324 intuitionistic propositional logic. See |
326 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
325 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
327 (preprint, University of St Andrews, 1991) ***) |
326 (preprint, University of St Andrews, 1991) ***) |
328 |
327 |
329 val major::prems= Goal |
328 val major::prems= Goal |
330 "[| p:(P&Q)-->S; !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"; |
329 "[| p:(P&Q)-->S; !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R"; |
331 by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ; |
330 by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ; |
332 qed "conj_impE"; |
331 qed "conj_impE"; |
333 |
332 |
334 val major::prems= Goal |
333 val major::prems= Goal |
335 "[| p:(P|Q)-->S; !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R"; |
334 "[| p:(P|Q)-->S; !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R"; |
336 by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ; |
335 by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ; |
337 qed "disj_impE"; |
336 qed "disj_impE"; |
338 |
337 |
339 (*Simplifies the implication. Classical version is stronger. |
338 (*Simplifies the implication. Classical version is stronger. |
340 Still UNSAFE since Q must be provable -- backtracking needed. *) |
339 Still UNSAFE since Q must be provable -- backtracking needed. *) |
341 val major::prems= Goal |
340 val major::prems= Goal |
342 "[| p:(P-->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; !!x. x:S ==> r(x):R |] ==> \ |
341 "[| p:(P-->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; !!x. x:S ==> r(x):R |] ==> \ |
343 \ ?p:R"; |
342 \ ?p:R"; |
344 by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ; |
343 by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ; |
345 qed "imp_impE"; |
344 qed "imp_impE"; |
346 |
345 |
347 (*Simplifies the implication. Classical version is stronger. |
346 (*Simplifies the implication. Classical version is stronger. |
348 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
347 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
349 val major::prems= Goal |
348 val major::prems= Goal |
350 "[| p:~P --> S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R |] ==> ?p:R"; |
349 "[| p:~P --> S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R |] ==> ?p:R"; |
351 by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ; |
350 by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ; |
352 qed "not_impE"; |
351 qed "not_impE"; |
353 |
352 |
354 (*Simplifies the implication. UNSAFE. *) |
353 (*Simplifies the implication. UNSAFE. *) |
355 val major::prems= Goal |
354 val major::prems= Goal |
356 "[| p:(P<->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; \ |
355 "[| p:(P<->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; \ |
357 \ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x. x:S ==> s(x):R |] ==> ?p:R"; |
356 \ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x. x:S ==> s(x):R |] ==> ?p:R"; |
358 by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ; |
357 by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ; |
359 qed "iff_impE"; |
358 qed "iff_impE"; |
360 |
359 |
361 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
360 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
362 val major::prems= Goal |
361 val major::prems= Goal |
363 "[| p:(ALL x. P(x))-->S; !!x. q:P(x); !!y. y:S ==> r(y):R |] ==> ?p:R"; |
362 "[| p:(ALL x. P(x))-->S; !!x. q:P(x); !!y. y:S ==> r(y):R |] ==> ?p:R"; |
364 by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ; |
363 by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ; |
365 qed "all_impE"; |
364 qed "all_impE"; |
366 |
365 |
367 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
366 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
368 val major::prems= Goal |
367 val major::prems= Goal |
369 "[| p:(EX x. P(x))-->S; !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"; |
368 "[| p:(EX x. P(x))-->S; !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R"; |
370 by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ; |
369 by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ; |
371 qed "ex_impE"; |
370 qed "ex_impE"; |