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


5 

1142

6 
Tactics and lemmas for IFOLP (Intuitionistic FirstOrder Logic with Proofs)

0

7 
*)


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


9 

9263

10 
val prems= Goal


11 
"[ p:P&Q; !!x y.[ x:P; y:Q ] ==> f(x,y):R ] ==> ?a:R";


12 
by (REPEAT (resolve_tac prems 1


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


14 
qed "conjE";

0

15 

9263

16 
val prems= Goal


17 
"[ p:P>Q; q:P; !!x. x:Q ==> r(x):R ] ==> ?p:R";


18 
by (REPEAT (resolve_tac (prems@[mp]) 1)) ;


19 
qed "impE";

0

20 

9263

21 
val prems= Goal


22 
"[ p:ALL x. P(x); !!y. y:P(x) ==> q(y):R ] ==> ?p:R";


23 
by (REPEAT (resolve_tac (prems@[spec]) 1)) ;


24 
qed "allE";

0

25 


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

9263

27 
val prems= Goal

3836

28 
"[ p:ALL x. P(x); !!y z.[ y:P(x); z:ALL x. P(x) ] ==> q(y,z):R \

9263

29 
\ ] ==> ?p:R";


30 
by (REPEAT (resolve_tac (prems@[spec]) 1)) ;


31 
qed "all_dupE";

0

32 


33 


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


35 

3836

36 
val notI = prove_goalw IFOLP.thy [not_def] "(!!x. x:P ==> q(x):False) ==> ?p:~P"

0

37 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI]) 1)) ]);


38 


39 
val notE = prove_goalw IFOLP.thy [not_def] "[ p:~P; q:P ] ==> ?p:R"


40 
(fn prems=>


41 
[ (resolve_tac [mp RS FalseE] 1),


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


43 


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

9263

45 
val prems= Goal


46 
"[ p:~P; !!x. x:(P>False) ==> q(x):Q ] ==> ?p:Q";


47 
by (REPEAT (ares_tac (prems@[impI,notE]) 1)) ;


48 
qed "not_to_imp";

0

49 


50 


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


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


53 
To specify P use something like


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

9263

55 
Goal "[ p:P; q:P > Q ] ==> ?p:Q";


56 
by (REPEAT (ares_tac [mp] 1)) ;


57 
qed "rev_mp";

0

58 


59 


60 
(*Contrapositive of an inference rule*)

9263

61 
val [major,minor]= Goal "[ p:~Q; !!y. y:P==>q(y):Q ] ==> ?a:~P";


62 
by (rtac (major RS notE RS notI) 1);


63 
by (etac minor 1) ;


64 
qed "contrapos";

0

65 


66 
(** Unique assumption tactic.


67 
Ignores proof objects.


68 
Fails unless one assumption is equal and exactly one is unifiable


69 
**)


70 


71 
local


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


73 
in


74 
val uniq_assume_tac =


75 
SUBGOAL


76 
(fn (prem,i) =>


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


78 
and concl = discard_proof (Logic.strip_assums_concl prem)


79 
in

1459

80 
if exists (fn hyp => hyp aconv concl) hyps


81 
then case distinct (filter (fn hyp=> could_unify(hyp,concl)) hyps) of


82 
[_] => assume_tac i

0

83 
 _ => no_tac


84 
else no_tac


85 
end);


86 
end;


87 


88 


89 
(*** Modus Ponens Tactics ***)


90 


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


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


93 


94 
(*Like mp_tac but instantiates no variables*)

9263

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

0

96 


97 


98 
(*** Ifandonlyif ***)


99 


100 
val iffI = prove_goalw IFOLP.thy [iff_def]

3836

101 
"[ !!x. x:P ==> q(x):Q; !!x. x:Q ==> r(x):P ] ==> ?p:P<>Q"

0

102 
(fn prems=> [ (REPEAT (ares_tac (prems@[conjI, impI]) 1)) ]);


103 


104 


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


106 
val iffE = prove_goalw IFOLP.thy [iff_def]


107 
"[ p:P <> Q; !!x y.[ x:P>Q; y:Q>P ] ==> q(x,y):R ] ==> ?p:R"

1459

108 
(fn prems => [ (rtac conjE 1), (REPEAT (ares_tac prems 1)) ]);

0

109 


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


111 


112 
val iffD1 = prove_goalw IFOLP.thy [iff_def] "[ p:P <> Q; q:P ] ==> ?p:Q"


113 
(fn prems => [ (rtac (conjunct1 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);


114 


115 
val iffD2 = prove_goalw IFOLP.thy [iff_def] "[ p:P <> Q; q:Q ] ==> ?p:P"


116 
(fn prems => [ (rtac (conjunct2 RS mp) 1), (REPEAT (ares_tac prems 1)) ]);


117 

9263

118 
Goal "?p:P <> P";


119 
by (REPEAT (ares_tac [iffI] 1)) ;


120 
qed "iff_refl";

0

121 

9263

122 
Goal "p:Q <> P ==> ?p:P <> Q";


123 
by (etac iffE 1);


124 
by (rtac iffI 1);


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


126 
qed "iff_sym";

0

127 

9263

128 
Goal "[ p:P <> Q; q:Q<> R ] ==> ?p:P <> R";


129 
by (rtac iffI 1);


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


131 
qed "iff_trans";

0

132 


133 


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


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


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


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


138 
***)


139 

9263

140 
val prems = goalw IFOLP.thy [ex1_def]


141 
"[ p:P(a); !!x u. u:P(x) ==> f(u) : x=a ] ==> ?p:EX! x. P(x)";


142 
by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)) ;


143 
qed "ex1I";

0

144 

9263

145 
val prems = goalw IFOLP.thy [ex1_def]

3836

146 
"[ p:EX! x. P(x); \

0

147 
\ !!x u v. [ u:P(x); v:ALL y. P(y) > y=x ] ==> f(x,u,v):R ] ==>\

9263

148 
\ ?a : R";


149 
by (cut_facts_tac prems 1);


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


151 
qed "ex1E";

0

152 


153 


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


155 


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


157 
fun iff_tac prems i =


158 
resolve_tac (prems RL [iffE]) i THEN


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


160 


161 
val conj_cong = prove_goal IFOLP.thy

3836

162 
"[ p:P <> P'; !!x. x:P' ==> q(x):Q <> Q' ] ==> ?p:(P&Q) <> (P'&Q')"

0

163 
(fn prems =>


164 
[ (cut_facts_tac prems 1),


165 
(REPEAT (ares_tac [iffI,conjI] 1


166 
ORELSE eresolve_tac [iffE,conjE,mp] 1


167 
ORELSE iff_tac prems 1)) ]);


168 


169 
val disj_cong = prove_goal IFOLP.thy


170 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(PQ) <> (P'Q')"


171 
(fn prems =>


172 
[ (cut_facts_tac prems 1),


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


174 
ORELSE ares_tac [iffI] 1


175 
ORELSE mp_tac 1)) ]);


176 


177 
val imp_cong = prove_goal IFOLP.thy

3836

178 
"[ p:P <> P'; !!x. x:P' ==> q(x):Q <> Q' ] ==> ?p:(P>Q) <> (P'>Q')"

0

179 
(fn prems =>


180 
[ (cut_facts_tac prems 1),


181 
(REPEAT (ares_tac [iffI,impI] 1

1459

182 
ORELSE etac iffE 1

0

183 
ORELSE mp_tac 1 ORELSE iff_tac prems 1)) ]);


184 


185 
val iff_cong = prove_goal IFOLP.thy


186 
"[ p:P <> P'; q:Q <> Q' ] ==> ?p:(P<>Q) <> (P'<>Q')"


187 
(fn prems =>


188 
[ (cut_facts_tac prems 1),

1459

189 
(REPEAT (etac iffE 1

0

190 
ORELSE ares_tac [iffI] 1


191 
ORELSE mp_tac 1)) ]);


192 


193 
val not_cong = prove_goal IFOLP.thy


194 
"p:P <> P' ==> ?p:~P <> ~P'"


195 
(fn prems =>


196 
[ (cut_facts_tac prems 1),


197 
(REPEAT (ares_tac [iffI,notI] 1


198 
ORELSE mp_tac 1


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


200 


201 
val all_cong = prove_goal IFOLP.thy

3836

202 
"(!!x. f(x):P(x) <> Q(x)) ==> ?p:(ALL x. P(x)) <> (ALL x. Q(x))"

0

203 
(fn prems =>


204 
[ (REPEAT (ares_tac [iffI,allI] 1


205 
ORELSE mp_tac 1

1459

206 
ORELSE etac allE 1 ORELSE iff_tac prems 1)) ]);

0

207 


208 
val ex_cong = prove_goal IFOLP.thy

3836

209 
"(!!x. f(x):P(x) <> Q(x)) ==> ?p:(EX x. P(x)) <> (EX x. Q(x))"

0

210 
(fn prems =>

1459

211 
[ (REPEAT (etac exE 1 ORELSE ares_tac [iffI,exI] 1

0

212 
ORELSE mp_tac 1


213 
ORELSE iff_tac prems 1)) ]);


214 


215 
(*NOT PROVED


216 
val ex1_cong = prove_goal IFOLP.thy


217 
"(!!x.f(x):P(x) <> Q(x)) ==> ?p:(EX! x.P(x)) <> (EX! x.Q(x))"


218 
(fn prems =>


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


220 
ORELSE mp_tac 1


221 
ORELSE iff_tac prems 1)) ]);


222 
*)


223 


224 
(*** Equality rules ***)


225 


226 
val refl = ieqI;


227 


228 
val subst = prove_goal IFOLP.thy "[ p:a=b; q:P(a) ] ==> ?p : P(b)"


229 
(fn [prem1,prem2] => [ rtac (prem2 RS rev_mp) 1, (rtac (prem1 RS ieqE) 1),


230 
rtac impI 1, atac 1 ]);


231 

9263

232 
Goal "q:a=b ==> ?c:b=a";


233 
by (etac subst 1);


234 
by (rtac refl 1) ;


235 
qed "sym";

0

236 

9263

237 
Goal "[ p:a=b; q:b=c ] ==> ?d:a=c";


238 
by (etac subst 1 THEN assume_tac 1);


239 
qed "trans";

0

240 


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

9263

242 
Goal "p:~ b=a ==> ?q:~ a=b";


243 
by (etac contrapos 1);


244 
by (etac sym 1) ;


245 
qed "not_sym";

0

246 


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


248 
val ssubst = standard (sym RS subst);


249 


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

9263

251 
Goal "[ p:EX! x. P(x); q:P(a); r:P(b) ] ==> ?d:a=b";


252 
by (etac ex1E 1);


253 
by (rtac trans 1);


254 
by (rtac sym 2);


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


256 
qed "ex1_equalsE";

0

257 


258 
(** Polymorphic congruence rules **)


259 

9263

260 
Goal "[ p:a=b ] ==> ?d:t(a)=t(b)";


261 
by (etac ssubst 1);


262 
by (rtac refl 1) ;


263 
qed "subst_context";

0

264 

9263

265 
Goal "[ p:a=b; q:c=d ] ==> ?p:t(a,c)=t(b,d)";


266 
by (REPEAT (etac ssubst 1));


267 
by (rtac refl 1) ;


268 
qed "subst_context2";

0

269 

9263

270 
Goal "[ p:a=b; q:c=d; r:e=f ] ==> ?p:t(a,c,e)=t(b,d,f)";


271 
by (REPEAT (etac ssubst 1));


272 
by (rtac refl 1) ;


273 
qed "subst_context3";

0

274 


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

1459

276 
a = b


277 
 


278 
c = d *)

9263

279 
Goal "[ p:a=b; q:a=c; r:b=d ] ==> ?p:c=d";


280 
by (rtac trans 1);


281 
by (rtac trans 1);


282 
by (rtac sym 1);


283 
by (REPEAT (assume_tac 1)) ;


284 
qed "box_equals";

0

285 


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

9263

287 
Goal "[ p:a=c; q:b=d; r:c=d ] ==> ?p:a=b";


288 
by (rtac trans 1);


289 
by (rtac trans 1);


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


291 
qed "simp_equals";

0

292 


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


294 

9263

295 
Goal "p:a=a' ==> ?p:P(a) <> P(a')";


296 
by (rtac iffI 1);


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


298 
qed "pred1_cong";

0

299 

9263

300 
Goal "[ p:a=a'; q:b=b' ] ==> ?p:P(a,b) <> P(a',b')";


301 
by (rtac iffI 1);


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


303 
qed "pred2_cong";

0

304 

9263

305 
Goal "[ p:a=a'; q:b=b'; r:c=c' ] ==> ?p:P(a,b,c) <> P(a',b',c')";


306 
by (rtac iffI 1);


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


308 
qed "pred3_cong";

0

309 


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


311 


312 
val pred_congs =


313 
flat (map (fn c =>

1459

314 
map (fn th => read_instantiate [("P",c)] th)


315 
[pred1_cong,pred2_cong,pred3_cong])


316 
(explode"PQRS"));

0

317 


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


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


320 


321 


322 
(*** Simplifications of assumed implications.


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


324 
used with mp_tac (restricted to atomic formulae) is COMPLETE for


325 
intuitionistic propositional logic. See


326 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic


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


328 

9263

329 
val major::prems= Goal


330 
"[ p:(P&Q)>S; !!x. x:P>(Q>S) ==> q(x):R ] ==> ?p:R";


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


332 
qed "conj_impE";

0

333 

9263

334 
val major::prems= Goal


335 
"[ p:(PQ)>S; !!x y.[ x:P>S; y:Q>S ] ==> q(x,y):R ] ==> ?p:R";


336 
by (DEPTH_SOLVE (ares_tac ([disjI1, disjI2, impI, major RS mp]@prems) 1)) ;


337 
qed "disj_impE";

0

338 


339 
(*Simplifies the implication. Classical version is stronger.


340 
Still UNSAFE since Q must be provable  backtracking needed. *)

9263

341 
val major::prems= Goal

3836

342 
"[ p:(P>Q)>S; !!x y.[ x:P; y:Q>S ] ==> q(x,y):Q; !!x. x:S ==> r(x):R ] ==> \

9263

343 
\ ?p:R";


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


345 
qed "imp_impE";

0

346 


347 
(*Simplifies the implication. Classical version is stronger.


348 
Still UNSAFE since ~P must be provable  backtracking needed. *)

9263

349 
val major::prems= Goal


350 
"[ p:~P > S; !!y. y:P ==> q(y):False; !!y. y:S ==> r(y):R ] ==> ?p:R";


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


352 
qed "not_impE";

0

353 


354 
(*Simplifies the implication. UNSAFE. *)

9263

355 
val major::prems= Goal

0

356 
"[ p:(P<>Q)>S; !!x y.[ x:P; y:Q>S ] ==> q(x,y):Q; \

9263

357 
\ !!x y.[ x:Q; y:P>S ] ==> r(x,y):P; !!x. x:S ==> s(x):R ] ==> ?p:R";


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


359 
qed "iff_impE";

0

360 


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

9263

362 
val major::prems= Goal


363 
"[ p:(ALL x. P(x))>S; !!x. q:P(x); !!y. y:S ==> r(y):R ] ==> ?p:R";


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


365 
qed "all_impE";

0

366 


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

9263

368 
val major::prems= Goal


369 
"[ p:(EX x. P(x))>S; !!y. y:P(a)>S ==> q(y):R ] ==> ?p:R";


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


371 
qed "ex_impE";
