0

1 
(* Title: FOL/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 IFOL;


10 


11 
signature IFOL_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 eq_mp_tac: int > tactic


26 
val ex1I: thm


27 
val ex1E: thm


28 
val ex1_equalsE: thm


29 
val ex1_cong: thm


30 
val ex_cong: thm


31 
val ex_impE: thm


32 
val iffD1: thm


33 
val iffD2: thm


34 
val iffE: thm


35 
val iffI: thm


36 
val iff_cong: thm


37 
val iff_impE: thm


38 
val iff_refl: thm


39 
val iff_sym: thm


40 
val iff_trans: thm


41 
val impE: thm


42 
val imp_cong: thm


43 
val imp_impE: thm


44 
val mp_tac: int > tactic


45 
val notE: thm


46 
val notI: thm


47 
val not_cong: thm


48 
val not_impE: thm


49 
val not_sym: thm


50 
val not_to_imp: thm


51 
val pred1_cong: thm


52 
val pred2_cong: thm


53 
val pred3_cong: thm


54 
val pred_congs: thm list


55 
val rev_mp: thm


56 
val simp_equals: thm


57 
val ssubst: thm


58 
val subst_context: thm


59 
val subst_context2: thm


60 
val subst_context3: thm


61 
val sym: thm


62 
val trans: thm


63 
val TrueI: thm


64 
end;


65 


66 


67 
structure IFOL_Lemmas : IFOL_LEMMAS =


68 
struct


69 


70 
val TrueI = prove_goalw IFOL.thy [True_def] "True"


71 
(fn _ => [ (REPEAT (ares_tac [impI] 1)) ]);


72 


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


74 


75 
val conjE = prove_goal IFOL.thy


76 
"[ P&Q; [ P; Q ] ==> R ] ==> R"


77 
(fn prems=>


78 
[ (REPEAT (resolve_tac prems 1


79 
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN


80 
resolve_tac prems 1))) ]);


81 


82 
val impE = prove_goal IFOL.thy


83 
"[ P>Q; P; Q ==> R ] ==> R"


84 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);


85 


86 
val allE = prove_goal IFOL.thy


87 
"[ ALL x.P(x); P(x) ==> R ] ==> R"


88 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);


89 


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


91 
val all_dupE = prove_goal IFOL.thy


92 
"[ ALL x.P(x); [ P(x); ALL x.P(x) ] ==> R \


93 
\ ] ==> R"


94 
(fn prems=> [ (REPEAT (resolve_tac (prems@[spec]) 1)) ]);


95 


96 


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


98 


99 
val notI = prove_goalw IFOL.thy [not_def] "(P ==> False) ==> ~P"


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


101 


102 
val notE = prove_goalw IFOL.thy [not_def] "[ ~P; P ] ==> R"


103 
(fn prems=>


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


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


106 


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


108 
val not_to_imp = prove_goal IFOL.thy


109 
"[ ~P; (P>False) ==> Q ] ==> Q"


110 
(fn prems=> [ (REPEAT (ares_tac (prems@[impI,notE]) 1)) ]);


111 


112 


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


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


115 
To specify P use something like


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


117 
val rev_mp = prove_goal IFOL.thy "[ P; P > Q ] ==> Q"


118 
(fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);


119 


120 


121 
(*Contrapositive of an inference rule*)


122 
val contrapos = prove_goal IFOL.thy "[ ~Q; P==>Q ] ==> ~P"


123 
(fn [major,minor]=>


124 
[ (rtac (major RS notE RS notI) 1),


125 
(etac minor 1) ]);


126 


127 


128 
(*** Modus Ponens Tactics ***)


129 


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


131 
fun mp_tac i = eresolve_tac [notE,impE] i THEN assume_tac i;


132 


133 
(*Like mp_tac but instantiates no variables*)


134 
fun eq_mp_tac i = eresolve_tac [notE,impE] i THEN eq_assume_tac i;


135 


136 


137 
(*** Ifandonlyif ***)


138 


139 
val iffI = prove_goalw IFOL.thy [iff_def]


140 
"[ P ==> Q; Q ==> P ] ==> P<>Q"


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


142 


143 


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


145 
val iffE = prove_goalw IFOL.thy [iff_def]


146 
"[ P <> Q; [ P>Q; Q>P ] ==> R ] ==> R"


147 
(fn prems => [ (resolve_tac [conjE] 1), (REPEAT (ares_tac prems 1)) ]);


148 


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


150 


151 
val iffD1 = prove_goalw IFOL.thy [iff_def] "[ P <> Q; P ] ==> Q"


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


153 


154 
val iffD2 = prove_goalw IFOL.thy [iff_def] "[ P <> Q; Q ] ==> P"


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


156 


157 
val iff_refl = prove_goal IFOL.thy "P <> P"


158 
(fn _ => [ (REPEAT (ares_tac [iffI] 1)) ]);


159 


160 
val iff_sym = prove_goal IFOL.thy "Q <> P ==> P <> Q"


161 
(fn [major] =>


162 
[ (rtac (major RS iffE) 1),


163 
(rtac iffI 1),


164 
(REPEAT (eresolve_tac [asm_rl,mp] 1)) ]);


165 


166 
val iff_trans = prove_goal IFOL.thy


167 
"!!P Q R. [ P <> Q; Q<> R ] ==> P <> R"


168 
(fn _ =>


169 
[ (rtac iffI 1),


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


171 


172 


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


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


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


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


177 
***)


178 


179 
val ex1I = prove_goalw IFOL.thy [ex1_def]


180 
"[ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x)"


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


182 


183 
val ex1E = prove_goalw IFOL.thy [ex1_def]


184 
"[ EX! x.P(x); !!x. [ P(x); ALL y. P(y) > y=x ] ==> R ] ==> R"


185 
(fn prems =>


186 
[ (cut_facts_tac prems 1),


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


188 


189 


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


191 


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


193 
fun iff_tac prems i =


194 
resolve_tac (prems RL [iffE]) i THEN


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


196 


197 
val conj_cong = prove_goal IFOL.thy


198 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P&Q) <> (P'&Q')"


199 
(fn prems =>


200 
[ (cut_facts_tac prems 1),


201 
(REPEAT (ares_tac [iffI,conjI] 1


202 
ORELSE eresolve_tac [iffE,conjE,mp] 1


203 
ORELSE iff_tac prems 1)) ]);


204 


205 
val disj_cong = prove_goal IFOL.thy


206 
"[ P <> P'; Q <> Q' ] ==> (PQ) <> (P'Q')"


207 
(fn prems =>


208 
[ (cut_facts_tac prems 1),


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


210 
ORELSE ares_tac [iffI] 1


211 
ORELSE mp_tac 1)) ]);


212 


213 
val imp_cong = prove_goal IFOL.thy


214 
"[ P <> P'; P' ==> Q <> Q' ] ==> (P>Q) <> (P'>Q')"


215 
(fn prems =>


216 
[ (cut_facts_tac prems 1),


217 
(REPEAT (ares_tac [iffI,impI] 1


218 
ORELSE eresolve_tac [iffE] 1


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


220 


221 
val iff_cong = prove_goal IFOL.thy


222 
"[ P <> P'; Q <> Q' ] ==> (P<>Q) <> (P'<>Q')"


223 
(fn prems =>


224 
[ (cut_facts_tac prems 1),


225 
(REPEAT (eresolve_tac [iffE] 1


226 
ORELSE ares_tac [iffI] 1


227 
ORELSE mp_tac 1)) ]);


228 


229 
val not_cong = prove_goal IFOL.thy


230 
"P <> P' ==> ~P <> ~P'"


231 
(fn prems =>


232 
[ (cut_facts_tac prems 1),


233 
(REPEAT (ares_tac [iffI,notI] 1


234 
ORELSE mp_tac 1


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


236 


237 
val all_cong = prove_goal IFOL.thy


238 
"(!!x.P(x) <> Q(x)) ==> (ALL x.P(x)) <> (ALL x.Q(x))"


239 
(fn prems =>


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


241 
ORELSE mp_tac 1


242 
ORELSE eresolve_tac [allE] 1 ORELSE iff_tac prems 1)) ]);


243 


244 
val ex_cong = prove_goal IFOL.thy


245 
"(!!x.P(x) <> Q(x)) ==> (EX x.P(x)) <> (EX x.Q(x))"


246 
(fn prems =>


247 
[ (REPEAT (eresolve_tac [exE] 1 ORELSE ares_tac [iffI,exI] 1


248 
ORELSE mp_tac 1


249 
ORELSE iff_tac prems 1)) ]);


250 


251 
val ex1_cong = prove_goal IFOL.thy


252 
"(!!x.P(x) <> Q(x)) ==> (EX! x.P(x)) <> (EX! x.Q(x))"


253 
(fn prems =>


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


255 
ORELSE mp_tac 1


256 
ORELSE iff_tac prems 1)) ]);


257 


258 
(*** Equality rules ***)


259 


260 
val sym = prove_goal IFOL.thy "a=b ==> b=a"


261 
(fn [major] => [ (rtac (major RS subst) 1), (rtac refl 1) ]);


262 


263 
val trans = prove_goal IFOL.thy "[ a=b; b=c ] ==> a=c"


264 
(fn [prem1,prem2] => [ (rtac (prem2 RS subst) 1), (rtac prem1 1) ]);


265 


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


267 
val [not_sym] = compose(sym,2,contrapos);


268 


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


270 
val ssubst = standard (sym RS subst);


271 


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


273 
val ex1_equalsE = prove_goal IFOL.thy


274 
"[ EX! x.P(x); P(a); P(b) ] ==> a=b"


275 
(fn prems =>


276 
[ (cut_facts_tac prems 1),


277 
(etac ex1E 1),


278 
(rtac trans 1),


279 
(rtac sym 2),


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


281 


282 
(** Polymorphic congruence rules **)


283 


284 
val subst_context = prove_goal IFOL.thy


285 
"[ a=b ] ==> t(a)=t(b)"


286 
(fn prems=>


287 
[ (resolve_tac (prems RL [ssubst]) 1),


288 
(resolve_tac [refl] 1) ]);


289 


290 
val subst_context2 = prove_goal IFOL.thy


291 
"[ a=b; c=d ] ==> t(a,c)=t(b,d)"


292 
(fn prems=>


293 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);


294 


295 
val subst_context3 = prove_goal IFOL.thy


296 
"[ a=b; c=d; e=f ] ==> t(a,c,e)=t(b,d,f)"


297 
(fn prems=>


298 
[ (EVERY1 (map rtac ((prems RL [ssubst]) @ [refl]))) ]);


299 


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


301 
a = b


302 
 


303 
c = d *)


304 
val box_equals = prove_goal IFOL.thy


305 
"[ a=b; a=c; b=d ] ==> c=d"


306 
(fn prems=>


307 
[ (resolve_tac [trans] 1),


308 
(resolve_tac [trans] 1),


309 
(resolve_tac [sym] 1),


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


311 


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


313 
val simp_equals = prove_goal IFOL.thy


314 
"[ a=c; b=d; c=d ] ==> a=b"


315 
(fn prems=>


316 
[ (resolve_tac [trans] 1),


317 
(resolve_tac [trans] 1),


318 
(REPEAT (resolve_tac (prems @ (prems RL [sym])) 1)) ]);


319 


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


321 


322 
val pred1_cong = prove_goal IFOL.thy


323 
"a=a' ==> P(a) <> P(a')"


324 
(fn prems =>


325 
[ (cut_facts_tac prems 1),


326 
(rtac iffI 1),


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


328 


329 
val pred2_cong = prove_goal IFOL.thy


330 
"[ a=a'; b=b' ] ==> P(a,b) <> P(a',b')"


331 
(fn prems =>


332 
[ (cut_facts_tac prems 1),


333 
(rtac iffI 1),


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


335 


336 
val pred3_cong = prove_goal IFOL.thy


337 
"[ a=a'; b=b'; c=c' ] ==> P(a,b,c) <> P(a',b',c')"


338 
(fn prems =>


339 
[ (cut_facts_tac prems 1),


340 
(rtac iffI 1),


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


342 


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


344 


345 
val pred_congs =


346 
flat (map (fn c =>


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


348 
[pred1_cong,pred2_cong,pred3_cong])


349 
(explode"PQRS"));


350 


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


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


353 


354 


355 
(*** Simplifications of assumed implications.


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


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


358 
intuitionistic propositional logic. See


359 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic


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


361 


362 
val conj_impE = prove_goal IFOL.thy


363 
"[ (P&Q)>S; P>(Q>S) ==> R ] ==> R"


364 
(fn major::prems=>


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


366 


367 
val disj_impE = prove_goal IFOL.thy


368 
"[ (PQ)>S; [ P>S; Q>S ] ==> R ] ==> R"


369 
(fn major::prems=>


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


371 


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


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


374 
val imp_impE = prove_goal IFOL.thy


375 
"[ (P>Q)>S; [ P; Q>S ] ==> Q; S ==> R ] ==> R"


376 
(fn major::prems=>


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


378 


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


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


381 
val not_impE = prove_goal IFOL.thy


382 
"[ ~P > S; P ==> False; S ==> R ] ==> R"


383 
(fn major::prems=>


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


385 


386 
(*Simplifies the implication. UNSAFE. *)


387 
val iff_impE = prove_goal IFOL.thy


388 
"[ (P<>Q)>S; [ P; Q>S ] ==> Q; [ Q; P>S ] ==> P; \


389 
\ S ==> R ] ==> R"


390 
(fn major::prems=>


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


392 


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


394 
val all_impE = prove_goal IFOL.thy


395 
"[ (ALL x.P(x))>S; !!x.P(x); S ==> R ] ==> R"


396 
(fn major::prems=>


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


398 


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


400 
val ex_impE = prove_goal IFOL.thy


401 
"[ (EX x.P(x))>S; P(x)>S ==> R ] ==> R"


402 
(fn major::prems=>


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


404 


405 
end;


406 


407 
open IFOL_Lemmas;


408 
