0
|
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 |
|