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

18977

80 
then case gen_distinct (op =) (List.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";
