7355

1 
(* Title: FOL/IFOL_lemmas.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 theory IFOL (intuitionistic firstorder logic).


7 
*)


8 


9 
(* ML bindings *)


10 


11 
val refl = thm "refl";


12 
val subst = thm "subst";


13 
val conjI = thm "conjI";


14 
val conjunct1 = thm "conjunct1";


15 
val conjunct2 = thm "conjunct2";


16 
val disjI1 = thm "disjI1";


17 
val disjI2 = thm "disjI2";


18 
val disjE = thm "disjE";


19 
val impI = thm "impI";


20 
val mp = thm "mp";


21 
val FalseE = thm "FalseE";


22 
val True_def = thm "True_def";


23 
val not_def = thm "not_def";


24 
val iff_def = thm "iff_def";


25 
val ex1_def = thm "ex1_def";


26 
val allI = thm "allI";


27 
val spec = thm "spec";


28 
val exI = thm "exI";


29 
val exE = thm "exE";


30 
val eq_reflection = thm "eq_reflection";


31 
val iff_reflection = thm "iff_reflection";


32 


33 


34 


35 
qed_goalw "TrueI" (the_context ()) [True_def] "True"


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


37 


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


39 


40 
qed_goal "conjE" (the_context ())


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


42 
(fn prems=>


43 
[ (REPEAT (resolve_tac prems 1


44 
ORELSE (resolve_tac [conjunct1, conjunct2] 1 THEN


45 
resolve_tac prems 1))) ]);


46 


47 
qed_goal "impE" (the_context ())


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


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


50 


51 
qed_goal "allE" (the_context ())


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


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


54 


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


56 
qed_goal "all_dupE" (the_context ())


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


58 
\ ] ==> R"


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


60 


61 


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


63 


64 
qed_goalw "notI" (the_context ()) [not_def] "(P ==> False) ==> ~P"


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


66 


67 
qed_goalw "notE" (the_context ()) [not_def] "[ ~P; P ] ==> R"


68 
(fn prems=>


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


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


71 


72 
qed_goal "rev_notE" (the_context ()) "!!P R. [ P; ~P ] ==> R"


73 
(fn _ => [REPEAT (ares_tac [notE] 1)]);


74 


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


76 
qed_goal "not_to_imp" (the_context ())


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


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


79 


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


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


82 
To specify P use something like


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


84 
qed_goal "rev_mp" (the_context ()) "[ P; P > Q ] ==> Q"


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


86 


87 
(*Contrapositive of an inference rule*)


88 
qed_goal "contrapos" (the_context ()) "[ ~Q; P==>Q ] ==> ~P"


89 
(fn [major,minor]=>


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


91 
(etac minor 1) ]);


92 


93 


94 
(*** Modus Ponens Tactics ***)


95 


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


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


98 


99 
(*Like mp_tac but instantiates no variables*)


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


101 


102 


103 
(*** Ifandonlyif ***)


104 


105 
qed_goalw "iffI" (the_context ()) [iff_def]


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


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


108 


109 


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


111 
qed_goalw "iffE" (the_context ()) [iff_def]


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


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


114 


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


116 


117 
qed_goalw "iffD1" (the_context ()) [iff_def] "[ P <> Q; P ] ==> Q"


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


119 


120 
qed_goalw "iffD2" (the_context ()) [iff_def] "[ P <> Q; Q ] ==> P"


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


122 


123 
qed_goal "rev_iffD1" (the_context ()) "!!P. [ P; P <> Q ] ==> Q"


124 
(fn _ => [etac iffD1 1, assume_tac 1]);


125 


126 
qed_goal "rev_iffD2" (the_context ()) "!!P. [ Q; P <> Q ] ==> P"


127 
(fn _ => [etac iffD2 1, assume_tac 1]);


128 


129 
qed_goal "iff_refl" (the_context ()) "P <> P"


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


131 


132 
qed_goal "iff_sym" (the_context ()) "Q <> P ==> P <> Q"


133 
(fn [major] =>


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


135 
(rtac iffI 1),


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


137 


138 
qed_goal "iff_trans" (the_context ())


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


140 
(fn _ =>


141 
[ (rtac iffI 1),


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


143 


144 


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


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


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


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


149 
***)


150 


151 
qed_goalw "ex1I" (the_context ()) [ex1_def]


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


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


154 


155 
(*Sometimes easier to use: the premises have no shared variables. Safe!*)


156 
qed_goal "ex_ex1I" (the_context ())


157 
"[ EX x. P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> EX! x. P(x)"


158 
(fn [ex,eq] => [ (rtac (ex RS exE) 1),


159 
(REPEAT (ares_tac [ex1I,eq] 1)) ]);


160 


161 
qed_goalw "ex1E" (the_context ()) [ex1_def]


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


163 
(fn prems =>


164 
[ (cut_facts_tac prems 1),


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


166 


167 


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


169 


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


171 
fun iff_tac prems i =


172 
resolve_tac (prems RL [iffE]) i THEN


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


174 


175 
qed_goal "conj_cong" (the_context ())


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


177 
(fn prems =>


178 
[ (cut_facts_tac prems 1),


179 
(REPEAT (ares_tac [iffI,conjI] 1


180 
ORELSE eresolve_tac [iffE,conjE,mp] 1


181 
ORELSE iff_tac prems 1)) ]);


182 


183 
(*Reversed congruence rule! Used in ZF/Order*)


184 
qed_goal "conj_cong2" (the_context ())


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


186 
(fn prems =>


187 
[ (cut_facts_tac prems 1),


188 
(REPEAT (ares_tac [iffI,conjI] 1


189 
ORELSE eresolve_tac [iffE,conjE,mp] 1


190 
ORELSE iff_tac prems 1)) ]);


191 


192 
qed_goal "disj_cong" (the_context ())


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


194 
(fn prems =>


195 
[ (cut_facts_tac prems 1),


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


197 
ORELSE ares_tac [iffI] 1


198 
ORELSE mp_tac 1)) ]);


199 


200 
qed_goal "imp_cong" (the_context ())


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


202 
(fn prems =>


203 
[ (cut_facts_tac prems 1),


204 
(REPEAT (ares_tac [iffI,impI] 1


205 
ORELSE etac iffE 1


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


207 


208 
qed_goal "iff_cong" (the_context ())


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


210 
(fn prems =>


211 
[ (cut_facts_tac prems 1),


212 
(REPEAT (etac iffE 1


213 
ORELSE ares_tac [iffI] 1


214 
ORELSE mp_tac 1)) ]);


215 


216 
qed_goal "not_cong" (the_context ())


217 
"P <> P' ==> ~P <> ~P'"


218 
(fn prems =>


219 
[ (cut_facts_tac prems 1),


220 
(REPEAT (ares_tac [iffI,notI] 1


221 
ORELSE mp_tac 1


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


223 


224 
qed_goal "all_cong" (the_context ())


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


226 
(fn prems =>


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


228 
ORELSE mp_tac 1


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


230 


231 
qed_goal "ex_cong" (the_context ())


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


233 
(fn prems =>


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


235 
ORELSE mp_tac 1


236 
ORELSE iff_tac prems 1)) ]);


237 


238 
qed_goal "ex1_cong" (the_context ())


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


240 
(fn prems =>


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


242 
ORELSE mp_tac 1


243 
ORELSE iff_tac prems 1)) ]);


244 


245 
(*** Equality rules ***)


246 


247 
qed_goal "sym" (the_context ()) "a=b ==> b=a"


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


249 


250 
qed_goal "trans" (the_context ()) "[ a=b; b=c ] ==> a=c"


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


252 


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

7422

254 
bind_thm ("not_sym", hd (compose(sym,2,contrapos)));

7355

255 


256 


257 
(* Two theorms for rewriting only one instance of a definition:


258 
the first for definitions of formulae and the second for terms *)


259 


260 
val prems = goal (the_context ()) "(A == B) ==> A <> B";


261 
by (rewrite_goals_tac prems);


262 
by (rtac iff_refl 1);


263 
qed "def_imp_iff";


264 


265 
val prems = goal (the_context ()) "(A == B) ==> A = B";


266 
by (rewrite_goals_tac prems);


267 
by (rtac refl 1);


268 
qed "meta_eq_to_obj_eq";


269 


270 


271 
(*Substitution: rule and tactic*)


272 
bind_thm ("ssubst", sym RS subst);


273 


274 
(*Apply an equality or definition ONCE.


275 
Fails unless the substitution has an effect*)


276 
fun stac th =


277 
let val th' = th RS meta_eq_to_obj_eq handle THM _ => th


278 
in CHANGED_GOAL (rtac (th' RS ssubst))


279 
end;


280 


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


282 
qed_goal "ex1_equalsE" (the_context ())


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


284 
(fn prems =>


285 
[ (cut_facts_tac prems 1),


286 
(etac ex1E 1),


287 
(rtac trans 1),


288 
(rtac sym 2),


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


290 


291 
(** Polymorphic congruence rules **)


292 


293 
qed_goal "subst_context" (the_context ())


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


295 
(fn prems=>


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


297 
(rtac refl 1) ]);


298 


299 
qed_goal "subst_context2" (the_context ())


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


301 
(fn prems=>


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


303 


304 
qed_goal "subst_context3" (the_context ())


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


306 
(fn prems=>


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


308 


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


310 
a = b


311 
 


312 
c = d *)


313 
qed_goal "box_equals" (the_context ())


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


315 
(fn prems=>


316 
[ (rtac trans 1),


317 
(rtac trans 1),


318 
(rtac sym 1),


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


320 


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


322 
qed_goal "simp_equals" (the_context ())


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


324 
(fn prems=>


325 
[ (rtac trans 1),


326 
(rtac trans 1),


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


328 


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


330 


331 
qed_goal "pred1_cong" (the_context ())


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


333 
(fn prems =>


334 
[ (cut_facts_tac prems 1),


335 
(rtac iffI 1),


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


337 


338 
qed_goal "pred2_cong" (the_context ())


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


340 
(fn prems =>


341 
[ (cut_facts_tac prems 1),


342 
(rtac iffI 1),


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


344 


345 
qed_goal "pred3_cong" (the_context ())


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


347 
(fn prems =>


348 
[ (cut_facts_tac prems 1),


349 
(rtac iffI 1),


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


351 


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


353 


354 
val pred_congs =


355 
flat (map (fn c =>


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


357 
[pred1_cong,pred2_cong,pred3_cong])


358 
(explode"PQRS"));


359 


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

7422

361 
bind_thm ("eq_cong", read_instantiate [("P","op =")] pred2_cong);

7355

362 


363 


364 
(*** Simplifications of assumed implications.


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


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


367 
intuitionistic propositional logic. See


368 
R. Dyckhoff, Contractionfree sequent calculi for intuitionistic logic


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


370 


371 
qed_goal "conj_impE" (the_context ())


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


373 
(fn major::prems=>


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


375 


376 
qed_goal "disj_impE" (the_context ())


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


378 
(fn major::prems=>


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


380 


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


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


383 
qed_goal "imp_impE" (the_context ())


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


385 
(fn major::prems=>


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


387 


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


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


390 
qed_goal "not_impE" (the_context ())


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


392 
(fn major::prems=>


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


394 


395 
(*Simplifies the implication. UNSAFE. *)


396 
qed_goal "iff_impE" (the_context ())


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


398 
\ S ==> R ] ==> R"


399 
(fn major::prems=>


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


401 


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


403 
qed_goal "all_impE" (the_context ())


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


405 
(fn major::prems=>


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


407 


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


409 
qed_goal "ex_impE" (the_context ())


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


411 
(fn major::prems=>


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


413 


414 
(*** Courtesy of Krzysztof Grabczewski ***)


415 


416 
val major::prems = goal (the_context ()) "[ PQ; P==>R; Q==>S ] ==> RS";


417 
by (rtac (major RS disjE) 1);


418 
by (REPEAT (eresolve_tac (prems RL [disjI1, disjI2]) 1));


419 
qed "disj_imp_disj";


420 


421 


422 
(** strip ALL and > from proved goal while preserving ALLbound var names **)


423 


424 
fun make_new_spec rl =


425 
(* Use a crazy name to avoid forall_intr failing because of


426 
duplicate variable name *)


427 
let val myspec = read_instantiate [("P","?wlzickd")] rl


428 
val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;


429 
val cvx = cterm_of (#sign(rep_thm myspec)) vx


430 
in (vxT, forall_intr cvx myspec) end;


431 


432 
local


433 


434 
val (specT, spec') = make_new_spec spec


435 


436 
in


437 


438 
fun RSspec th =


439 
(case concl_of th of


440 
_ $ (Const("All",_) $ Abs(a,_,_)) =>


441 
let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),specT))


442 
in th RS forall_elim ca spec' end


443 
 _ => raise THM("RSspec",0,[th]));


444 


445 
fun RSmp th =


446 
(case concl_of th of


447 
_ $ (Const("op >",_)$_$_) => th RS mp


448 
 _ => raise THM("RSmp",0,[th]));


449 


450 
fun normalize_thm funs =


451 
let fun trans [] th = th


452 
 trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th


453 
in trans funs end;


454 


455 
fun qed_spec_mp name =


456 
let val thm = normalize_thm [RSspec,RSmp] (result())


457 
in bind_thm(name, thm) end;


458 


459 
fun qed_goal_spec_mp name thy s p =


460 
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));


461 


462 
fun qed_goalw_spec_mp name thy defs s p =


463 
bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));


464 


465 
end;


466 


467 


468 
(* attributes *)


469 


470 
local


471 


472 
fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;


473 


474 
in


475 


476 
val attrib_setup =


477 
[Attrib.add_attributes


478 
[("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];


479 


480 
end;
