|
1 (* Title: FOLP/ifol.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 Tactics and lemmas for ifol.thy (intuitionistic first-order logic) |
|
7 *) |
|
8 |
|
9 open IFOLP; |
|
10 |
|
11 signature IFOLP_LEMMAS = |
|
12 sig |
|
13 val allE: thm |
|
14 val all_cong: thm |
|
15 val all_dupE: thm |
|
16 val all_impE: thm |
|
17 val box_equals: thm |
|
18 val conjE: thm |
|
19 val conj_cong: thm |
|
20 val conj_impE: thm |
|
21 val contrapos: thm |
|
22 val disj_cong: thm |
|
23 val disj_impE: thm |
|
24 val eq_cong: thm |
|
25 val ex1I: thm |
|
26 val ex1E: thm |
|
27 val ex1_equalsE: thm |
|
28 (* val ex1_cong: thm****) |
|
29 val ex_cong: thm |
|
30 val ex_impE: thm |
|
31 val iffD1: thm |
|
32 val iffD2: thm |
|
33 val iffE: thm |
|
34 val iffI: thm |
|
35 val iff_cong: thm |
|
36 val iff_impE: thm |
|
37 val iff_refl: thm |
|
38 val iff_sym: thm |
|
39 val iff_trans: thm |
|
40 val impE: thm |
|
41 val imp_cong: thm |
|
42 val imp_impE: thm |
|
43 val mp_tac: int -> tactic |
|
44 val notE: thm |
|
45 val notI: thm |
|
46 val not_cong: thm |
|
47 val not_impE: thm |
|
48 val not_sym: thm |
|
49 val not_to_imp: thm |
|
50 val pred1_cong: thm |
|
51 val pred2_cong: thm |
|
52 val pred3_cong: thm |
|
53 val pred_congs: thm list |
|
54 val refl: thm |
|
55 val rev_mp: thm |
|
56 val simp_equals: thm |
|
57 val subst: thm |
|
58 val ssubst: thm |
|
59 val subst_context: thm |
|
60 val subst_context2: thm |
|
61 val subst_context3: thm |
|
62 val sym: thm |
|
63 val trans: thm |
|
64 val TrueI: thm |
|
65 val uniq_assume_tac: int -> tactic |
|
66 val uniq_mp_tac: int -> tactic |
|
67 end; |
|
68 |
|
69 |
|
70 structure IFOLP_Lemmas : IFOLP_LEMMAS = |
|
71 struct |
|
72 |
|
73 val TrueI = TrueI; |
|
74 |
|
75 (*** Sequent-style elimination rules for & --> and ALL ***) |
|
76 |
|
77 val conjE = prove_goal IFOLP.thy |
|
78 "[| p:P&Q; !!x y.[| x:P; y:Q |] ==> f(x,y):R |] ==> ?a:R" |
|
79 (fn prems=> |
|
80 [ (REPEAT (resolve_tac prems 1 |
|
81 ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN |
|
82 resolve_tac prems 1))) ]); |
|
83 |
|
84 val impE = prove_goal IFOLP.thy |
|
85 "[| p:P-->Q; q:P; !!x.x:Q ==> r(x):R |] ==> ?p:R" |
|
86 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
|
87 |
|
88 val allE = prove_goal IFOLP.thy |
|
89 "[| p:ALL x.P(x); !!y.y:P(x) ==> q(y):R |] ==> ?p:R" |
|
90 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
|
91 |
|
92 (*Duplicates the quantifier; for use with eresolve_tac*) |
|
93 val all_dupE = prove_goal IFOLP.thy |
|
94 "[| p:ALL x.P(x); !!y z.[| y:P(x); z:ALL x.P(x) |] ==> q(y,z):R \ |
|
95 \ |] ==> ?p:R" |
|
96 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
|
97 |
|
98 |
|
99 (*** Negation rules, which translate between ~P and P-->False ***) |
|
100 |
|
101 val notI = prove_goalw IFOLP.thy [not_def] "(!!x.x:P ==> q(x):False) ==> ?p:~P" |
|
102 (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); |
|
103 |
|
104 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P; q:P |] ==> ?p:R" |
|
105 (fn prems=> |
|
106 [ (resolve_tac [mp RS FalseE] 1), |
|
107 (REPEAT (resolve_tac prems 1)) ]); |
|
108 |
|
109 (*This is useful with the special implication rules for each kind of P. *) |
|
110 val not_to_imp = prove_goal IFOLP.thy |
|
111 "[| p:~P; !!x.x:(P-->False) ==> q(x):Q |] ==> ?p:Q" |
|
112 (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); |
|
113 |
|
114 |
|
115 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into |
|
116 this implication, then apply impI to move P back into the assumptions. |
|
117 To specify P use something like |
|
118 eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) |
|
119 val rev_mp = prove_goal IFOLP.thy "[| p:P; q:P --> Q |] ==> ?p:Q" |
|
120 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
|
121 |
|
122 |
|
123 (*Contrapositive of an inference rule*) |
|
124 val contrapos = prove_goal IFOLP.thy "[| p:~Q; !!y.y:P==>q(y):Q |] ==> ?a:~P" |
|
125 (fn [major,minor]=> |
|
126 [ (rtac (major RS notE RS notI) 1), |
|
127 (etac minor 1) ]); |
|
128 |
|
129 (** Unique assumption tactic. |
|
130 Ignores proof objects. |
|
131 Fails unless one assumption is equal and exactly one is unifiable |
|
132 **) |
|
133 |
|
134 local |
|
135 fun discard_proof (Const("Proof",_) $ P $ _) = P; |
|
136 in |
|
137 val uniq_assume_tac = |
|
138 SUBGOAL |
|
139 (fn (prem,i) => |
|
140 let val hyps = map discard_proof (Logic.strip_assums_hyp prem) |
|
141 and concl = discard_proof (Logic.strip_assums_concl prem) |
|
142 in |
|
143 if exists (fn hyp => hyp aconv concl) hyps |
|
144 then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of |
|
145 [_] => assume_tac i |
|
146 | _ => no_tac |
|
147 else no_tac |
|
148 end); |
|
149 end; |
|
150 |
|
151 |
|
152 (*** Modus Ponens Tactics ***) |
|
153 |
|
154 (*Finds P-->Q and P in the assumptions, replaces implication by Q *) |
|
155 fun mp_tac i = eresolve_tac [notE,make_elim mp] i THEN assume_tac i; |
|
156 |
|
157 (*Like mp_tac but instantiates no variables*) |
|
158 fun uniq_mp_tac i = eresolve_tac [notE,impE] i THEN uniq_assume_tac i; |
|
159 |
|
160 |
|
161 (*** If-and-only-if ***) |
|
162 |
|
163 val iffI = prove_goalw IFOLP.thy [iff_def] |
|
164 "[| !!x.x:P ==> q(x):Q; !!x.x:Q ==> r(x):P |] ==> ?p:P<->Q" |
|
165 (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); |
|
166 |
|
167 |
|
168 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
|
169 val iffE = prove_goalw IFOLP.thy [iff_def] |
|
170 "[| p:P <-> Q; !!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R |] ==> ?p:R" |
|
171 (fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]); |
|
172 |
|
173 (* Destruct rules for <-> similar to Modus Ponens *) |
|
174 |
|
175 val iffD1 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; q:P |] ==> ?p:Q" |
|
176 (fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
|
177 |
|
178 val iffD2 = prove_goalw IFOLP.thy [iff_def] "[| p:P <-> Q; q:Q |] ==> ?p:P" |
|
179 (fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); |
|
180 |
|
181 val iff_refl = prove_goal IFOLP.thy "?p:P <-> P" |
|
182 (fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]); |
|
183 |
|
184 val iff_sym = prove_goal IFOLP.thy "p:Q <-> P ==> ?p:P <-> Q" |
|
185 (fn [major] => |
|
186 [ (rtac (major RS iffE) 1), |
|
187 (rtac iffI 1), |
|
188 (REPEAT (eresolve_tac [asm_rl,mp] 1)) ]); |
|
189 |
|
190 val iff_trans = prove_goal IFOLP.thy "[| p:P <-> Q; q:Q<-> R |] ==> ?p:P <-> R" |
|
191 (fn prems => |
|
192 [ (cut_facts_tac prems 1), |
|
193 (rtac iffI 1), |
|
194 (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ]); |
|
195 |
|
196 |
|
197 (*** Unique existence. NOTE THAT the following 2 quantifications |
|
198 EX!x such that [EX!y such that P(x,y)] (sequential) |
|
199 EX!x,y such that P(x,y) (simultaneous) |
|
200 do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
|
201 ***) |
|
202 |
|
203 val ex1I = prove_goalw IFOLP.thy [ex1_def] |
|
204 "[| p:P(a); !!x u.u:P(x) ==> f(u) : x=a |] ==> ?p:EX! x. P(x)" |
|
205 (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); |
|
206 |
|
207 val ex1E = prove_goalw IFOLP.thy [ex1_def] |
|
208 "[| p:EX! x.P(x); \ |
|
209 \ !!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\ |
|
210 \ ?a : R" |
|
211 (fn prems => |
|
212 [ (cut_facts_tac prems 1), |
|
213 (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); |
|
214 |
|
215 |
|
216 (*** <-> congruence rules for simplification ***) |
|
217 |
|
218 (*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) |
|
219 fun iff_tac prems i = |
|
220 resolve_tac (prems RL [iffE]) i THEN |
|
221 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
|
222 |
|
223 val conj_cong = prove_goal IFOLP.thy |
|
224 "[| p:P <-> P'; !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')" |
|
225 (fn prems => |
|
226 [ (cut_facts_tac prems 1), |
|
227 (REPEAT (ares_tac [iffI,conjI] 1 |
|
228 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
|
229 ORELSE iff_tac prems 1)) ]); |
|
230 |
|
231 val disj_cong = prove_goal IFOLP.thy |
|
232 "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P|Q) <-> (P'|Q')" |
|
233 (fn prems => |
|
234 [ (cut_facts_tac prems 1), |
|
235 (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
|
236 ORELSE ares_tac [iffI] 1 |
|
237 ORELSE mp_tac 1)) ]); |
|
238 |
|
239 val imp_cong = prove_goal IFOLP.thy |
|
240 "[| p:P <-> P'; !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')" |
|
241 (fn prems => |
|
242 [ (cut_facts_tac prems 1), |
|
243 (REPEAT (ares_tac [iffI,impI] 1 |
|
244 ORELSE eresolve_tac [iffE] 1 |
|
245 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); |
|
246 |
|
247 val iff_cong = prove_goal IFOLP.thy |
|
248 "[| p:P <-> P'; q:Q <-> Q' |] ==> ?p:(P<->Q) <-> (P'<->Q')" |
|
249 (fn prems => |
|
250 [ (cut_facts_tac prems 1), |
|
251 (REPEAT (eresolve_tac [iffE] 1 |
|
252 ORELSE ares_tac [iffI] 1 |
|
253 ORELSE mp_tac 1)) ]); |
|
254 |
|
255 val not_cong = prove_goal IFOLP.thy |
|
256 "p:P <-> P' ==> ?p:~P <-> ~P'" |
|
257 (fn prems => |
|
258 [ (cut_facts_tac prems 1), |
|
259 (REPEAT (ares_tac [iffI,notI] 1 |
|
260 ORELSE mp_tac 1 |
|
261 ORELSE eresolve_tac [iffE,notE] 1)) ]); |
|
262 |
|
263 val all_cong = prove_goal IFOLP.thy |
|
264 "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(ALL x.P(x)) <-> (ALL x.Q(x))" |
|
265 (fn prems => |
|
266 [ (REPEAT (ares_tac [iffI,allI] 1 |
|
267 ORELSE mp_tac 1 |
|
268 ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]); |
|
269 |
|
270 val ex_cong = prove_goal IFOLP.thy |
|
271 "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX x.P(x)) <-> (EX x.Q(x))" |
|
272 (fn prems => |
|
273 [ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1 |
|
274 ORELSE mp_tac 1 |
|
275 ORELSE iff_tac prems 1)) ]); |
|
276 |
|
277 (*NOT PROVED |
|
278 val ex1_cong = prove_goal IFOLP.thy |
|
279 "(!!x.f(x):P(x) <-> Q(x)) ==> ?p:(EX! x.P(x)) <-> (EX! x.Q(x))" |
|
280 (fn prems => |
|
281 [ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 |
|
282 ORELSE mp_tac 1 |
|
283 ORELSE iff_tac prems 1)) ]); |
|
284 *) |
|
285 |
|
286 (*** Equality rules ***) |
|
287 |
|
288 val refl = ieqI; |
|
289 |
|
290 val subst = prove_goal IFOLP.thy "[| p:a=b; q:P(a) |] ==> ?p : P(b)" |
|
291 (fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1), |
|
292 rtac impI 1, atac 1 ]); |
|
293 |
|
294 val sym = prove_goal IFOLP.thy "q:a=b ==> ?c:b=a" |
|
295 (fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]); |
|
296 |
|
297 val trans = prove_goal IFOLP.thy "[| p:a=b; q:b=c |] ==> ?d:a=c" |
|
298 (fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]); |
|
299 |
|
300 (** ~ b=a ==> ~ a=b **) |
|
301 val not_sym = prove_goal IFOLP.thy "p:~ b=a ==> ?q:~ a=b" |
|
302 (fn [prem] => [ (rtac (prem RS contrapos) 1), (etac sym 1) ]); |
|
303 |
|
304 (*calling "standard" reduces maxidx to 0*) |
|
305 val ssubst = standard (sym RS subst); |
|
306 |
|
307 (*A special case of ex1E that would otherwise need quantifier expansion*) |
|
308 val ex1_equalsE = prove_goal IFOLP.thy |
|
309 "[| p:EX! x.P(x); q:P(a); r:P(b) |] ==> ?d:a=b" |
|
310 (fn prems => |
|
311 [ (cut_facts_tac prems 1), |
|
312 (etac ex1E 1), |
|
313 (rtac trans 1), |
|
314 (rtac sym 2), |
|
315 (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ]); |
|
316 |
|
317 (** Polymorphic congruence rules **) |
|
318 |
|
319 val subst_context = prove_goal IFOLP.thy |
|
320 "[| p:a=b |] ==> ?d:t(a)=t(b)" |
|
321 (fn prems=> |
|
322 [ (resolve_tac (prems RL [ssubst]) 1), |
|
323 (resolve_tac [refl] 1) ]); |
|
324 |
|
325 val subst_context2 = prove_goal IFOLP.thy |
|
326 "[| p:a=b; q:c=d |] ==> ?p:t(a,c)=t(b,d)" |
|
327 (fn prems=> |
|
328 [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); |
|
329 |
|
330 val subst_context3 = prove_goal IFOLP.thy |
|
331 "[| p:a=b; q:c=d; r:e=f |] ==> ?p:t(a,c,e)=t(b,d,f)" |
|
332 (fn prems=> |
|
333 [ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]); |
|
334 |
|
335 (*Useful with eresolve_tac for proving equalties from known equalities. |
|
336 a = b |
|
337 | | |
|
338 c = d *) |
|
339 val box_equals = prove_goal IFOLP.thy |
|
340 "[| p:a=b; q:a=c; r:b=d |] ==> ?p:c=d" |
|
341 (fn prems=> |
|
342 [ (resolve_tac [trans] 1), |
|
343 (resolve_tac [trans] 1), |
|
344 (resolve_tac [sym] 1), |
|
345 (REPEAT (resolve_tac prems 1)) ]); |
|
346 |
|
347 (*Dual of box_equals: for proving equalities backwards*) |
|
348 val simp_equals = prove_goal IFOLP.thy |
|
349 "[| p:a=c; q:b=d; r:c=d |] ==> ?p:a=b" |
|
350 (fn prems=> |
|
351 [ (resolve_tac [trans] 1), |
|
352 (resolve_tac [trans] 1), |
|
353 (REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]); |
|
354 |
|
355 (** Congruence rules for predicate letters **) |
|
356 |
|
357 val pred1_cong = prove_goal IFOLP.thy |
|
358 "p:a=a' ==> ?p:P(a) <-> P(a')" |
|
359 (fn prems => |
|
360 [ (cut_facts_tac prems 1), |
|
361 (rtac iffI 1), |
|
362 (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); |
|
363 |
|
364 val pred2_cong = prove_goal IFOLP.thy |
|
365 "[| p:a=a'; q:b=b' |] ==> ?p:P(a,b) <-> P(a',b')" |
|
366 (fn prems => |
|
367 [ (cut_facts_tac prems 1), |
|
368 (rtac iffI 1), |
|
369 (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); |
|
370 |
|
371 val pred3_cong = prove_goal IFOLP.thy |
|
372 "[| p:a=a'; q:b=b'; r:c=c' |] ==> ?p:P(a,b,c) <-> P(a',b',c')" |
|
373 (fn prems => |
|
374 [ (cut_facts_tac prems 1), |
|
375 (rtac iffI 1), |
|
376 (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ]); |
|
377 |
|
378 (*special cases for free variables P, Q, R, S -- up to 3 arguments*) |
|
379 |
|
380 val pred_congs = |
|
381 flat (map (fn c => |
|
382 map (fn th => read_instantiate [("P",c)] th) |
|
383 [pred1_cong,pred2_cong,pred3_cong]) |
|
384 (explode"PQRS")); |
|
385 |
|
386 (*special case for the equality predicate!*) |
|
387 val eq_cong = read_instantiate [("P","op =")] pred2_cong; |
|
388 |
|
389 |
|
390 (*** Simplifications of assumed implications. |
|
391 Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE |
|
392 used with mp_tac (restricted to atomic formulae) is COMPLETE for |
|
393 intuitionistic propositional logic. See |
|
394 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
|
395 (preprint, University of St Andrews, 1991) ***) |
|
396 |
|
397 val conj_impE = prove_goal IFOLP.thy |
|
398 "[| p:(P&Q)-->S; !!x.x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R" |
|
399 (fn major::prems=> |
|
400 [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); |
|
401 |
|
402 val disj_impE = prove_goal IFOLP.thy |
|
403 "[| p:(P|Q)-->S; !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R" |
|
404 (fn major::prems=> |
|
405 [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); |
|
406 |
|
407 (*Simplifies the implication. Classical version is stronger. |
|
408 Still UNSAFE since Q must be provable -- backtracking needed. *) |
|
409 val imp_impE = prove_goal IFOLP.thy |
|
410 "[| p:(P-->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; !!x.x:S ==> r(x):R |] ==> \ |
|
411 \ ?p:R" |
|
412 (fn major::prems=> |
|
413 [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); |
|
414 |
|
415 (*Simplifies the implication. Classical version is stronger. |
|
416 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
|
417 val not_impE = prove_goal IFOLP.thy |
|
418 "[| p:~P --> S; !!y.y:P ==> q(y):False; !!y.y:S ==> r(y):R |] ==> ?p:R" |
|
419 (fn major::prems=> |
|
420 [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); |
|
421 |
|
422 (*Simplifies the implication. UNSAFE. *) |
|
423 val iff_impE = prove_goal IFOLP.thy |
|
424 "[| p:(P<->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; \ |
|
425 \ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x.x:S ==> s(x):R |] ==> ?p:R" |
|
426 (fn major::prems=> |
|
427 [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); |
|
428 |
|
429 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
|
430 val all_impE = prove_goal IFOLP.thy |
|
431 "[| p:(ALL x.P(x))-->S; !!x.q:P(x); !!y.y:S ==> r(y):R |] ==> ?p:R" |
|
432 (fn major::prems=> |
|
433 [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); |
|
434 |
|
435 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
|
436 val ex_impE = prove_goal IFOLP.thy |
|
437 "[| p:(EX x.P(x))-->S; !!y.y:P(a)-->S ==> q(y):R |] ==> ?p:R" |
|
438 (fn major::prems=> |
|
439 [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); |
|
440 |
|
441 end; |
|
442 |
|
443 open IFOLP_Lemmas; |
|
444 |