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 firstorder 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 
(*** Sequentstyle 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 
(*** Ifandonlyif ***)


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 metaassumptions (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:(PQ) <> (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, Contractionfree 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:(PQ)>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 
