80 [ (REPEAT (resolve_tac prems 1 |
80 [ (REPEAT (resolve_tac prems 1 |
81 ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN |
81 ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN |
82 resolve_tac prems 1))) ]); |
82 resolve_tac prems 1))) ]); |
83 |
83 |
84 val impE = prove_goal IFOLP.thy |
84 val impE = prove_goal IFOLP.thy |
85 "[| p:P-->Q; q:P; !!x.x:Q ==> r(x):R |] ==> ?p:R" |
85 "[| p:P-->Q; q:P; !!x. x:Q ==> r(x):R |] ==> ?p:R" |
86 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
86 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
87 |
87 |
88 val allE = prove_goal IFOLP.thy |
88 val allE = prove_goal IFOLP.thy |
89 "[| p:ALL x.P(x); !!y.y:P(x) ==> q(y):R |] ==> ?p:R" |
89 "[| p:ALL x. P(x); !!y. y:P(x) ==> q(y):R |] ==> ?p:R" |
90 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
90 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
91 |
91 |
92 (*Duplicates the quantifier; for use with eresolve_tac*) |
92 (*Duplicates the quantifier; for use with eresolve_tac*) |
93 val all_dupE = prove_goal IFOLP.thy |
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 \ |
94 "[| p:ALL x. P(x); !!y z.[| y:P(x); z:ALL x. P(x) |] ==> q(y,z):R \ |
95 \ |] ==> ?p:R" |
95 \ |] ==> ?p:R" |
96 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
96 (fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]); |
97 |
97 |
98 |
98 |
99 (*** Negation rules, which translate between ~P and P-->False ***) |
99 (*** Negation rules, which translate between ~P and P-->False ***) |
100 |
100 |
101 val notI = prove_goalw IFOLP.thy [not_def] "(!!x.x:P ==> q(x):False) ==> ?p:~P" |
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)) ]); |
102 (fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); |
103 |
103 |
104 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P; q:P |] ==> ?p:R" |
104 val notE = prove_goalw IFOLP.thy [not_def] "[| p:~P; q:P |] ==> ?p:R" |
105 (fn prems=> |
105 (fn prems=> |
106 [ (resolve_tac [mp RS FalseE] 1), |
106 [ (resolve_tac [mp RS FalseE] 1), |
107 (REPEAT (resolve_tac prems 1)) ]); |
107 (REPEAT (resolve_tac prems 1)) ]); |
108 |
108 |
109 (*This is useful with the special implication rules for each kind of P. *) |
109 (*This is useful with the special implication rules for each kind of P. *) |
110 val not_to_imp = prove_goal IFOLP.thy |
110 val not_to_imp = prove_goal IFOLP.thy |
111 "[| p:~P; !!x.x:(P-->False) ==> q(x):Q |] ==> ?p:Q" |
111 "[| p:~P; !!x. x:(P-->False) ==> q(x):Q |] ==> ?p:Q" |
112 (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); |
112 (fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]); |
113 |
113 |
114 |
114 |
115 (* For substitution int an assumption P, reduce Q to P-->Q, substitute into |
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. |
116 this implication, then apply impI to move P back into the assumptions. |
119 val rev_mp = prove_goal IFOLP.thy "[| p:P; q:P --> Q |] ==> ?p:Q" |
119 val rev_mp = prove_goal IFOLP.thy "[| p:P; q:P --> Q |] ==> ?p:Q" |
120 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
120 (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]); |
121 |
121 |
122 |
122 |
123 (*Contrapositive of an inference rule*) |
123 (*Contrapositive of an inference rule*) |
124 val contrapos = prove_goal IFOLP.thy "[| p:~Q; !!y.y:P==>q(y):Q |] ==> ?a:~P" |
124 val contrapos = prove_goal IFOLP.thy "[| p:~Q; !!y. y:P==>q(y):Q |] ==> ?a:~P" |
125 (fn [major,minor]=> |
125 (fn [major,minor]=> |
126 [ (rtac (major RS notE RS notI) 1), |
126 [ (rtac (major RS notE RS notI) 1), |
127 (etac minor 1) ]); |
127 (etac minor 1) ]); |
128 |
128 |
129 (** Unique assumption tactic. |
129 (** Unique assumption tactic. |
159 |
159 |
160 |
160 |
161 (*** If-and-only-if ***) |
161 (*** If-and-only-if ***) |
162 |
162 |
163 val iffI = prove_goalw IFOLP.thy [iff_def] |
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" |
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)) ]); |
165 (fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); |
166 |
166 |
167 |
167 |
168 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
168 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
169 val iffE = prove_goalw IFOLP.thy [iff_def] |
169 val iffE = prove_goalw IFOLP.thy [iff_def] |
199 EX!x,y such that P(x,y) (simultaneous) |
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. |
200 do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. |
201 ***) |
201 ***) |
202 |
202 |
203 val ex1I = prove_goalw IFOLP.thy [ex1_def] |
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)" |
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)) ]); |
205 (fn prems => [ (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ]); |
206 |
206 |
207 val ex1E = prove_goalw IFOLP.thy [ex1_def] |
207 val ex1E = prove_goalw IFOLP.thy [ex1_def] |
208 "[| p:EX! x.P(x); \ |
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 |] ==>\ |
209 \ !!x u v. [| u:P(x); v:ALL y. P(y) --> y=x |] ==> f(x,u,v):R |] ==>\ |
210 \ ?a : R" |
210 \ ?a : R" |
211 (fn prems => |
211 (fn prems => |
212 [ (cut_facts_tac prems 1), |
212 [ (cut_facts_tac prems 1), |
213 (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); |
213 (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ]); |
219 fun iff_tac prems i = |
219 fun iff_tac prems i = |
220 resolve_tac (prems RL [iffE]) i THEN |
220 resolve_tac (prems RL [iffE]) i THEN |
221 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
221 REPEAT1 (eresolve_tac [asm_rl,mp] i); |
222 |
222 |
223 val conj_cong = prove_goal IFOLP.thy |
223 val conj_cong = prove_goal IFOLP.thy |
224 "[| p:P <-> P'; !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')" |
224 "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P&Q) <-> (P'&Q')" |
225 (fn prems => |
225 (fn prems => |
226 [ (cut_facts_tac prems 1), |
226 [ (cut_facts_tac prems 1), |
227 (REPEAT (ares_tac [iffI,conjI] 1 |
227 (REPEAT (ares_tac [iffI,conjI] 1 |
228 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
228 ORELSE eresolve_tac [iffE,conjE,mp] 1 |
229 ORELSE iff_tac prems 1)) ]); |
229 ORELSE iff_tac prems 1)) ]); |
235 (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
235 (REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 |
236 ORELSE ares_tac [iffI] 1 |
236 ORELSE ares_tac [iffI] 1 |
237 ORELSE mp_tac 1)) ]); |
237 ORELSE mp_tac 1)) ]); |
238 |
238 |
239 val imp_cong = prove_goal IFOLP.thy |
239 val imp_cong = prove_goal IFOLP.thy |
240 "[| p:P <-> P'; !!x.x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')" |
240 "[| p:P <-> P'; !!x. x:P' ==> q(x):Q <-> Q' |] ==> ?p:(P-->Q) <-> (P'-->Q')" |
241 (fn prems => |
241 (fn prems => |
242 [ (cut_facts_tac prems 1), |
242 [ (cut_facts_tac prems 1), |
243 (REPEAT (ares_tac [iffI,impI] 1 |
243 (REPEAT (ares_tac [iffI,impI] 1 |
244 ORELSE etac iffE 1 |
244 ORELSE etac iffE 1 |
245 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); |
245 ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); |
259 (REPEAT (ares_tac [iffI,notI] 1 |
259 (REPEAT (ares_tac [iffI,notI] 1 |
260 ORELSE mp_tac 1 |
260 ORELSE mp_tac 1 |
261 ORELSE eresolve_tac [iffE,notE] 1)) ]); |
261 ORELSE eresolve_tac [iffE,notE] 1)) ]); |
262 |
262 |
263 val all_cong = prove_goal IFOLP.thy |
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))" |
264 "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(ALL x. P(x)) <-> (ALL x. Q(x))" |
265 (fn prems => |
265 (fn prems => |
266 [ (REPEAT (ares_tac [iffI,allI] 1 |
266 [ (REPEAT (ares_tac [iffI,allI] 1 |
267 ORELSE mp_tac 1 |
267 ORELSE mp_tac 1 |
268 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); |
268 ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); |
269 |
269 |
270 val ex_cong = prove_goal IFOLP.thy |
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))" |
271 "(!!x. f(x):P(x) <-> Q(x)) ==> ?p:(EX x. P(x)) <-> (EX x. Q(x))" |
272 (fn prems => |
272 (fn prems => |
273 [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 |
273 [ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 |
274 ORELSE mp_tac 1 |
274 ORELSE mp_tac 1 |
275 ORELSE iff_tac prems 1)) ]); |
275 ORELSE iff_tac prems 1)) ]); |
276 |
276 |
393 intuitionistic propositional logic. See |
393 intuitionistic propositional logic. See |
394 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
394 R. Dyckhoff, Contraction-free sequent calculi for intuitionistic logic |
395 (preprint, University of St Andrews, 1991) ***) |
395 (preprint, University of St Andrews, 1991) ***) |
396 |
396 |
397 val conj_impE = prove_goal IFOLP.thy |
397 val conj_impE = prove_goal IFOLP.thy |
398 "[| p:(P&Q)-->S; !!x.x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R" |
398 "[| p:(P&Q)-->S; !!x. x:P-->(Q-->S) ==> q(x):R |] ==> ?p:R" |
399 (fn major::prems=> |
399 (fn major::prems=> |
400 [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); |
400 [ (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ]); |
401 |
401 |
402 val disj_impE = prove_goal IFOLP.thy |
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" |
403 "[| p:(P|Q)-->S; !!x y.[| x:P-->S; y:Q-->S |] ==> q(x,y):R |] ==> ?p:R" |
405 [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); |
405 [ (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ]); |
406 |
406 |
407 (*Simplifies the implication. Classical version is stronger. |
407 (*Simplifies the implication. Classical version is stronger. |
408 Still UNSAFE since Q must be provable -- backtracking needed. *) |
408 Still UNSAFE since Q must be provable -- backtracking needed. *) |
409 val imp_impE = prove_goal IFOLP.thy |
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 |] ==> \ |
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" |
411 \ ?p:R" |
412 (fn major::prems=> |
412 (fn major::prems=> |
413 [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); |
413 [ (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ]); |
414 |
414 |
415 (*Simplifies the implication. Classical version is stronger. |
415 (*Simplifies the implication. Classical version is stronger. |
416 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
416 Still UNSAFE since ~P must be provable -- backtracking needed. *) |
417 val not_impE = prove_goal IFOLP.thy |
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" |
418 "[| p:~P --> S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R |] ==> ?p:R" |
419 (fn major::prems=> |
419 (fn major::prems=> |
420 [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); |
420 [ (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ]); |
421 |
421 |
422 (*Simplifies the implication. UNSAFE. *) |
422 (*Simplifies the implication. UNSAFE. *) |
423 val iff_impE = prove_goal IFOLP.thy |
423 val iff_impE = prove_goal IFOLP.thy |
424 "[| p:(P<->Q)-->S; !!x y.[| x:P; y:Q-->S |] ==> q(x,y):Q; \ |
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" |
425 \ !!x y.[| x:Q; y:P-->S |] ==> r(x,y):P; !!x. x:S ==> s(x):R |] ==> ?p:R" |
426 (fn major::prems=> |
426 (fn major::prems=> |
427 [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); |
427 [ (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ]); |
428 |
428 |
429 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
429 (*What if (ALL x.~~P(x)) --> ~~(ALL x.P(x)) is an assumption? UNSAFE*) |
430 val all_impE = prove_goal IFOLP.thy |
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" |
431 "[| p:(ALL x. P(x))-->S; !!x. q:P(x); !!y. y:S ==> r(y):R |] ==> ?p:R" |
432 (fn major::prems=> |
432 (fn major::prems=> |
433 [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); |
433 [ (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ]); |
434 |
434 |
435 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
435 (*Unsafe: (EX x.P(x))-->S is equivalent to ALL x.P(x)-->S. *) |
436 val ex_impE = prove_goal IFOLP.thy |
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" |
437 "[| p:(EX x. P(x))-->S; !!y. y:P(a)-->S ==> q(y):R |] ==> ?p:R" |
438 (fn major::prems=> |
438 (fn major::prems=> |
439 [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); |
439 [ (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ]); |
440 |
440 |
441 end; |
441 end; |
442 |
442 |