author  haftmann 
Tue, 10 Jul 2007 17:30:50 +0200  
changeset 23709  fd31da8f752a 
parent 19046  bc5c6c9b114e 
child 25990  d98da4a40a79 
permissions  rwrr 
1459  1 
(* Title: FOLP/IFOLP.ML 
0  2 
ID: $Id$ 
1459  3 
Author: Martin D Coen, Cambridge University Computer Laboratory 
0  4 
Copyright 1992 University of Cambridge 
17480  5 
*) 
0  6 

7 
(*** Sequentstyle elimination rules for & > and ALL ***) 

8 

17480  9 
val prems= Goal 
9263  10 
"[ p:P&Q; !!x y.[ x:P; y:Q ] ==> f(x,y):R ] ==> ?a:R"; 
11 
by (REPEAT (resolve_tac prems 1 

12 
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN resolve_tac prems 1))) ; 

13 
qed "conjE"; 

0  14 

17480  15 
val prems= Goal 
9263  16 
"[ p:P>Q; q:P; !!x. x:Q ==> r(x):R ] ==> ?p:R"; 
17 
by (REPEAT (resolve_tac (prems@[mp]) 1)) ; 

18 
qed "impE"; 

0  19 

17480  20 
val prems= Goal 
9263  21 
"[ p:ALL x. P(x); !!y. y:P(x) ==> q(y):R ] ==> ?p:R"; 
22 
by (REPEAT (resolve_tac (prems@[spec]) 1)) ; 

23 
qed "allE"; 

0  24 

25 
(*Duplicates the quantifier; for use with eresolve_tac*) 

17480  26 
val prems= Goal 
3836  27 
"[ p:ALL x. P(x); !!y z.[ y:P(x); z:ALL x. P(x) ] ==> q(y,z):R \ 
9263  28 
\ ] ==> ?p:R"; 
29 
by (REPEAT (resolve_tac (prems@[spec]) 1)) ; 

30 
qed "all_dupE"; 

0  31 

32 

33 
(*** Negation rules, which translate between ~P and P>False ***) 

34 

17480  35 
val notI = prove_goalw (the_context ()) [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P" 
0  36 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]); 
37 

17480  38 
val notE = prove_goalw (the_context ()) [not_def] "[ p:~P; q:P ] ==> ?p:R" 
0  39 
(fn prems=> 
40 
[ (resolve_tac [mp RS FalseE] 1), 

41 
(REPEAT (resolve_tac prems 1)) ]); 

42 

43 
(*This is useful with the special implication rules for each kind of P. *) 

17480  44 
val prems= Goal 
9263  45 
"[ p:~P; !!x. x:(P>False) ==> q(x):Q ] ==> ?p:Q"; 
46 
by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ; 

47 
qed "not_to_imp"; 

0  48 

49 

50 
(* For substitution int an assumption P, reduce Q to P>Q, substitute into 

51 
this implication, then apply impI to move P back into the assumptions. 

52 
To specify P use something like 

53 
eres_inst_tac [ ("P","ALL y. ?S(x,y)") ] rev_mp 1 *) 

9263  54 
Goal "[ p:P; q:P > Q ] ==> ?p:Q"; 
55 
by (REPEAT (ares_tac [mp] 1)) ; 

56 
qed "rev_mp"; 

0  57 

58 

59 
(*Contrapositive of an inference rule*) 

9263  60 
val [major,minor]= Goal "[ p:~Q; !!y. y:P==>q(y):Q ] ==> ?a:~P"; 
61 
by (rtac (major RS notE RS notI) 1); 

62 
by (etac minor 1) ; 

63 
qed "contrapos"; 

0  64 

65 
(** Unique assumption tactic. 

66 
Ignores proof objects. 

17480  67 
Fails unless one assumption is equal and exactly one is unifiable 
0  68 
**) 
69 

70 
local 

71 
fun discard_proof (Const("Proof",_) $ P $ _) = P; 

72 
in 

73 
val uniq_assume_tac = 

74 
SUBGOAL 

75 
(fn (prem,i) => 

76 
let val hyps = map discard_proof (Logic.strip_assums_hyp prem) 

77 
and concl = discard_proof (Logic.strip_assums_concl prem) 

17480  78 
in 
1459  79 
if exists (fn hyp => hyp aconv concl) hyps 
19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18977
diff
changeset

80 
then case distinct (op =) (filter (fn hyp => could_unify (hyp, concl)) hyps) of 
1459  81 
[_] => assume_tac i 
0  82 
 _ => no_tac 
83 
else no_tac 

84 
end); 

85 
end; 

86 

87 

88 
(*** Modus Ponens Tactics ***) 

89 

90 
(*Finds P>Q and P in the assumptions, replaces implication by Q *) 

91 
fun mp_tac i = eresolve_tac [notE,make_elim mp] i THEN assume_tac i; 

92 

93 
(*Like mp_tac but instantiates no variables*) 

9263  94 
fun int_uniq_mp_tac i = eresolve_tac [notE,impE] i THEN uniq_assume_tac i; 
0  95 

96 

97 
(*** Ifandonlyif ***) 

98 

17480  99 
val iffI = prove_goalw (the_context ()) [iff_def] 
3836  100 
"[ !!x. x:P ==> q(x):Q; !!x. x:Q ==> r(x):P ] ==> ?p:P<>Q" 
0  101 
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]); 
102 

103 

104 
(*Observe use of rewrite_rule to unfold "<>" in metaassumptions (prems) *) 

17480  105 
val iffE = prove_goalw (the_context ()) [iff_def] 
0  106 
"[ p:P <> Q; !!x y.[ x:P>Q; y:Q>P ] ==> q(x,y):R ] ==> ?p:R" 
1459  107 
(fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]); 
0  108 

109 
(* Destruct rules for <> similar to Modus Ponens *) 

110 

17480  111 
val iffD1 = prove_goalw (the_context ()) [iff_def] "[ p:P <> Q; q:P ] ==> ?p:Q" 
0  112 
(fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 
113 

17480  114 
val iffD2 = prove_goalw (the_context ()) [iff_def] "[ p:P <> Q; q:Q ] ==> ?p:P" 
0  115 
(fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]); 
116 

9263  117 
Goal "?p:P <> P"; 
118 
by (REPEAT (ares_tac [iffI] 1)) ; 

119 
qed "iff_refl"; 

0  120 

9263  121 
Goal "p:Q <> P ==> ?p:P <> Q"; 
122 
by (etac iffE 1); 

123 
by (rtac iffI 1); 

124 
by (REPEAT (eresolve_tac [asm_rl,mp] 1)) ; 

125 
qed "iff_sym"; 

0  126 

9263  127 
Goal "[ p:P <> Q; q:Q<> R ] ==> ?p:P <> R"; 
128 
by (rtac iffI 1); 

129 
by (REPEAT (eresolve_tac [asm_rl,iffE] 1 ORELSE mp_tac 1)) ; 

130 
qed "iff_trans"; 

0  131 

132 

133 
(*** Unique existence. NOTE THAT the following 2 quantifications 

134 
EX!x such that [EX!y such that P(x,y)] (sequential) 

135 
EX!x,y such that P(x,y) (simultaneous) 

136 
do NOT mean the same thing. The parser treats EX!x y.P(x,y) as sequential. 

137 
***) 

138 

17480  139 
val prems = goalw (the_context ()) [ex1_def] 
9263  140 
"[ p:P(a); !!x u. u:P(x) ==> f(u) : x=a ] ==> ?p:EX! x. P(x)"; 
141 
by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ; 

142 
qed "ex1I"; 

0  143 

17480  144 
val prems = goalw (the_context ()) [ex1_def] 
3836  145 
"[ p:EX! x. P(x); \ 
0  146 
\ !!x u v. [ u:P(x); v:ALL y. P(y) > y=x ] ==> f(x,u,v):R ] ==>\ 
9263  147 
\ ?a : R"; 
148 
by (cut_facts_tac prems 1); 

149 
by (REPEAT (eresolve_tac [exE,conjE] 1 ORELSE ares_tac prems 1)) ; 

150 
qed "ex1E"; 

0  151 

152 

153 
(*** <> congruence rules for simplification ***) 

154 

155 
(*Use iffE on a premise. For conj_cong, imp_cong, all_cong, ex_cong*) 

156 
fun iff_tac prems i = 

157 
resolve_tac (prems RL [iffE]) i THEN 

158 
REPEAT1 (eresolve_tac [asm_rl,mp] i); 

159 

17480  160 
val conj_cong = prove_goal (the_context ()) 
3836  161 
"[ p:P <> P'; !!x. x:P' ==> q(x):Q <> Q' ] ==> ?p:(P&Q) <> (P'&Q')" 
0  162 
(fn prems => 
163 
[ (cut_facts_tac prems 1), 

164 
(REPEAT (ares_tac [iffI,conjI] 1 

165 
ORELSE eresolve_tac [iffE,conjE,mp] 1 

166 
ORELSE iff_tac prems 1)) ]); 

167 

17480  168 
val disj_cong = prove_goal (the_context ()) 
0  169 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(PQ) <> (P'Q')" 
170 
(fn prems => 

171 
[ (cut_facts_tac prems 1), 

172 
(REPEAT (eresolve_tac [iffE,disjE,disjI1,disjI2] 1 

173 
ORELSE ares_tac [iffI] 1 

174 
ORELSE mp_tac 1)) ]); 

175 

17480  176 
val imp_cong = prove_goal (the_context ()) 
3836  177 
"[ p:P <> P'; !!x. x:P' ==> q(x):Q <> Q' ] ==> ?p:(P>Q) <> (P'>Q')" 
0  178 
(fn prems => 
179 
[ (cut_facts_tac prems 1), 

180 
(REPEAT (ares_tac [iffI,impI] 1 

1459  181 
ORELSE etac iffE 1 
0  182 
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]); 
183 

17480  184 
val iff_cong = prove_goal (the_context ()) 
0  185 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(P<>Q) <> (P'<>Q')" 
186 
(fn prems => 

187 
[ (cut_facts_tac prems 1), 

1459  188 
(REPEAT (etac iffE 1 
0  189 
ORELSE ares_tac [iffI] 1 
190 
ORELSE mp_tac 1)) ]); 

191 

17480  192 
val not_cong = prove_goal (the_context ()) 
0  193 
"p:P <> P' ==> ?p:~P <> ~P'" 
194 
(fn prems => 

195 
[ (cut_facts_tac prems 1), 

196 
(REPEAT (ares_tac [iffI,notI] 1 

197 
ORELSE mp_tac 1 

198 
ORELSE eresolve_tac [iffE,notE] 1)) ]); 

199 

17480  200 
val all_cong = prove_goal (the_context ()) 
3836  201 
"(!!x. f(x):P(x) <> Q(x)) ==> ?p:(ALL x. P(x)) <> (ALL x. Q(x))" 
0  202 
(fn prems => 
203 
[ (REPEAT (ares_tac [iffI,allI] 1 

204 
ORELSE mp_tac 1 

1459  205 
ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]); 
0  206 

17480  207 
val ex_cong = prove_goal (the_context ()) 
3836  208 
"(!!x. f(x):P(x) <> Q(x)) ==> ?p:(EX x. P(x)) <> (EX x. Q(x))" 
0  209 
(fn prems => 
1459  210 
[ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1 
0  211 
ORELSE mp_tac 1 
212 
ORELSE iff_tac prems 1)) ]); 

213 

214 
(*NOT PROVED 

17480  215 
val ex1_cong = prove_goal (the_context ()) 
0  216 
"(!!x.f(x):P(x) <> Q(x)) ==> ?p:(EX! x.P(x)) <> (EX! x.Q(x))" 
217 
(fn prems => 

218 
[ (REPEAT (eresolve_tac [ex1E, spec RS mp] 1 ORELSE ares_tac [iffI,ex1I] 1 

219 
ORELSE mp_tac 1 

220 
ORELSE iff_tac prems 1)) ]); 

221 
*) 

222 

223 
(*** Equality rules ***) 

224 

225 
val refl = ieqI; 

226 

17480  227 
val subst = prove_goal (the_context ()) "[ p:a=b; q:P(a) ] ==> ?p : P(b)" 
228 
(fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1), 

0  229 
rtac impI 1, atac 1 ]); 
230 

9263  231 
Goal "q:a=b ==> ?c:b=a"; 
232 
by (etac subst 1); 

233 
by (rtac refl 1) ; 

234 
qed "sym"; 

0  235 

9263  236 
Goal "[ p:a=b; q:b=c ] ==> ?d:a=c"; 
17480  237 
by (etac subst 1 THEN assume_tac 1); 
9263  238 
qed "trans"; 
0  239 

240 
(** ~ b=a ==> ~ a=b **) 

9263  241 
Goal "p:~ b=a ==> ?q:~ a=b"; 
242 
by (etac contrapos 1); 

243 
by (etac sym 1) ; 

244 
qed "not_sym"; 

0  245 

246 
(*calling "standard" reduces maxidx to 0*) 

247 
val ssubst = standard (sym RS subst); 

248 

249 
(*A special case of ex1E that would otherwise need quantifier expansion*) 

9263  250 
Goal "[ p:EX! x. P(x); q:P(a); r:P(b) ] ==> ?d:a=b"; 
251 
by (etac ex1E 1); 

252 
by (rtac trans 1); 

253 
by (rtac sym 2); 

254 
by (REPEAT (eresolve_tac [asm_rl, spec RS mp] 1)) ; 

255 
qed "ex1_equalsE"; 

0  256 

257 
(** Polymorphic congruence rules **) 

258 

9263  259 
Goal "[ p:a=b ] ==> ?d:t(a)=t(b)"; 
260 
by (etac ssubst 1); 

261 
by (rtac refl 1) ; 

262 
qed "subst_context"; 

0  263 

9263  264 
Goal "[ p:a=b; q:c=d ] ==> ?p:t(a,c)=t(b,d)"; 
17480  265 
by (REPEAT (etac ssubst 1)); 
9263  266 
by (rtac refl 1) ; 
267 
qed "subst_context2"; 

0  268 

9263  269 
Goal "[ p:a=b; q:c=d; r:e=f ] ==> ?p:t(a,c,e)=t(b,d,f)"; 
17480  270 
by (REPEAT (etac ssubst 1)); 
9263  271 
by (rtac refl 1) ; 
272 
qed "subst_context3"; 

0  273 

274 
(*Useful with eresolve_tac for proving equalties from known equalities. 

1459  275 
a = b 
276 
  

277 
c = d *) 

9263  278 
Goal "[ p:a=b; q:a=c; r:b=d ] ==> ?p:c=d"; 
279 
by (rtac trans 1); 

280 
by (rtac trans 1); 

281 
by (rtac sym 1); 

282 
by (REPEAT (assume_tac 1)) ; 

283 
qed "box_equals"; 

0  284 

285 
(*Dual of box_equals: for proving equalities backwards*) 

9263  286 
Goal "[ p:a=c; q:b=d; r:c=d ] ==> ?p:a=b"; 
287 
by (rtac trans 1); 

288 
by (rtac trans 1); 

289 
by (REPEAT (eresolve_tac [asm_rl, sym] 1)) ; 

290 
qed "simp_equals"; 

0  291 

292 
(** Congruence rules for predicate letters **) 

293 

9263  294 
Goal "p:a=a' ==> ?p:P(a) <> P(a')"; 
295 
by (rtac iffI 1); 

296 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; 

297 
qed "pred1_cong"; 

0  298 

9263  299 
Goal "[ p:a=a'; q:b=b' ] ==> ?p:P(a,b) <> P(a',b')"; 
300 
by (rtac iffI 1); 

301 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; 

302 
qed "pred2_cong"; 

0  303 

9263  304 
Goal "[ p:a=a'; q:b=b'; r:c=c' ] ==> ?p:P(a,b,c) <> P(a',b',c')"; 
305 
by (rtac iffI 1); 

306 
by (DEPTH_SOLVE (eresolve_tac [asm_rl, subst, ssubst] 1)) ; 

307 
qed "pred3_cong"; 

0  308 

309 
(*special cases for free variables P, Q, R, S  up to 3 arguments*) 

310 

17480  311 
val pred_congs = 
312 
List.concat (map (fn c => 

1459  313 
map (fn th => read_instantiate [("P",c)] th) 
314 
[pred1_cong,pred2_cong,pred3_cong]) 

315 
(explode"PQRS")); 

0  316 

317 
(*special case for the equality predicate!*) 

318 
val eq_cong = read_instantiate [("P","op =")] pred2_cong; 

319 

320 

321 
(*** Simplifications of assumed implications. 

322 
Roy Dyckhoff has proved that conj_impE, disj_impE, and imp_impE 

17480  323 
used with mp_tac (restricted to atomic formulae) is COMPLETE for 
0  324 
intuitionistic propositional logic. See 
325 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic 

326 
(preprint, University of St Andrews, 1991) ***) 

327 

17480  328 
val major::prems= Goal 
9263  329 
"[ p:(P&Q)>S; !!x. x:P>(Q>S) ==> q(x):R ] ==> ?p:R"; 
330 
by (REPEAT (ares_tac ([conjI, impI, major RS mp]@prems) 1)) ; 

331 
qed "conj_impE"; 

0  332 

17480  333 
val major::prems= Goal 
9263  334 
"[ p:(PQ)>S; !!x y.[ x:P>S; y:Q>S ] ==> q(x,y):R ] ==> ?p:R"; 
335 
by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ; 

336 
qed "disj_impE"; 

0  337 

17480  338 
(*Simplifies the implication. Classical version is stronger. 
0  339 
Still UNSAFE since Q must be provable  backtracking needed. *) 
17480  340 
val major::prems= Goal 
3836  341 
"[ p:(P>Q)>S; !!x y.[ x:P; y:Q>S ] ==> q(x,y):Q; !!x. x:S ==> r(x):R ] ==> \ 
9263  342 
\ ?p:R"; 
343 
by (REPEAT (ares_tac ([impI, major RS mp]@prems) 1)) ; 

344 
qed "imp_impE"; 

0  345 

17480  346 
(*Simplifies the implication. Classical version is stronger. 
0  347 
Still UNSAFE since ~P must be provable  backtracking needed. *) 
9263  348 
val major::prems= Goal 
349 
"[ p:~P > S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R ] ==> ?p:R"; 

350 
by (REPEAT (ares_tac ([notI, impI, major RS mp]@prems) 1)) ; 

351 
qed "not_impE"; 

0  352 

353 
(*Simplifies the implication. UNSAFE. *) 

17480  354 
val major::prems= Goal 
0  355 
"[ p:(P<>Q)>S; !!x y.[ x:P; y:Q>S ] ==> q(x,y):Q; \ 
9263  356 
\ !!x y.[ x:Q; y:P>S ] ==> r(x,y):P; !!x. x:S ==> s(x):R ] ==> ?p:R"; 
357 
by (REPEAT (ares_tac ([iffI, impI, major RS mp]@prems) 1)) ; 

358 
qed "iff_impE"; 

0  359 

360 
(*What if (ALL x.~~P(x)) > ~~(ALL x.P(x)) is an assumption? UNSAFE*) 

17480  361 
val major::prems= Goal 
9263  362 
"[ p:(ALL x. P(x))>S; !!x. q:P(x); !!y. y:S ==> r(y):R ] ==> ?p:R"; 
363 
by (REPEAT (ares_tac ([allI, impI, major RS mp]@prems) 1)) ; 

364 
qed "all_impE"; 

0  365 

366 
(*Unsafe: (EX x.P(x))>S is equivalent to ALL x.P(x)>S. *) 

17480  367 
val major::prems= Goal 
9263  368 
"[ p:(EX x. P(x))>S; !!y. y:P(a)>S ==> q(y):R ] ==> ?p:R"; 
369 
by (REPEAT (ares_tac ([exI, impI, major RS mp]@prems) 1)) ; 

370 
qed "ex_impE"; 