7357

1 
(* Title: HOL/HOL_lemmas.ML


2 
ID: $Id$


3 
Author: Tobias Nipkow


4 
Copyright 1991 University of Cambridge


5 


6 
Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.


7 
*)


8 


9 
(* ML bindings *)


10 


11 
val plusI = thm "plusI";


12 
val minusI = thm "minusI";


13 
val timesI = thm "timesI";


14 
val powerI = thm "powerI";


15 
val eq_reflection = thm "eq_reflection";


16 
val refl = thm "refl";


17 
val subst = thm "subst";


18 
val ext = thm "ext";


19 
val selectI = thm "selectI";


20 
val impI = thm "impI";


21 
val mp = thm "mp";


22 
val True_def = thm "True_def";


23 
val All_def = thm "All_def";


24 
val Ex_def = thm "Ex_def";


25 
val False_def = thm "False_def";


26 
val not_def = thm "not_def";


27 
val and_def = thm "and_def";


28 
val or_def = thm "or_def";


29 
val Ex1_def = thm "Ex1_def";


30 
val iff = thm "iff";


31 
val True_or_False = thm "True_or_False";


32 
val Let_def = thm "Let_def";


33 
val if_def = thm "if_def";


34 
val arbitrary_def = thm "arbitrary_def";


35 


36 


37 
(** Equality **)


38 
section "=";


39 

7618

40 
Goal "s=t ==> t=s";


41 
by (etac subst 1);


42 
by (rtac refl 1);


43 
qed "sym";

7357

44 


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

7618

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

7357

47 

7618

48 
Goal "[ r=s; s=t ] ==> r=t";


49 
by (etac subst 1 THEN assume_tac 1);


50 
qed "trans";

7357

51 

9969

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

7357

53 
by (rewrite_goals_tac prems);


54 
by (rtac refl 1);


55 
qed "def_imp_eq";


56 


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


58 
a = b


59 
 


60 
c = d *)


61 
Goal "[ a=b; a=c; b=d ] ==> c=d";


62 
by (rtac trans 1);


63 
by (rtac trans 1);


64 
by (rtac sym 1);


65 
by (REPEAT (assume_tac 1)) ;


66 
qed "box_equals";


67 


68 
(** Congruence rules for metaapplication **)


69 
section "Congruence";


70 


71 
(*similar to AP_THM in Gordon's HOL*)

7618

72 
Goal "(f::'a=>'b) = g ==> f(x)=g(x)";


73 
by (etac subst 1);


74 
by (rtac refl 1);


75 
qed "fun_cong";

7357

76 


77 
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)

7618

78 
Goal "x=y ==> f(x)=f(y)";


79 
by (etac subst 1);


80 
by (rtac refl 1);


81 
qed "arg_cong";

7357

82 

7618

83 
Goal "[ f = g; (x::'a) = y ] ==> f(x) = g(y)";


84 
by (etac subst 1);


85 
by (etac subst 1);


86 
by (rtac refl 1);


87 
qed "cong";

7357

88 


89 
(** Equality of booleans  iff **)


90 
section "iff";


91 

7618

92 
val prems = Goal "[ P ==> Q; Q ==> P ] ==> P=Q";

7357

93 
by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));


94 
qed "iffI";


95 

7618

96 
Goal "[ P=Q; Q ] ==> P";


97 
by (etac ssubst 1);


98 
by (assume_tac 1);


99 
qed "iffD2";

7357

100 

7618

101 
Goal "[ Q; P=Q ] ==> P";


102 
by (etac iffD2 1);


103 
by (assume_tac 1);


104 
qed "rev_iffD2";

7357

105 


106 
bind_thm ("iffD1", sym RS iffD2);


107 
bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));


108 

7618

109 
val [p1,p2] = Goal "[ P=Q; [ P > Q; Q > P ] ==> R ] ==> R";


110 
by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1));


111 
qed "iffE";

7357

112 


113 


114 
(** True **)


115 
section "True";


116 

7618

117 
Goalw [True_def] "True";


118 
by (rtac refl 1);


119 
qed "TrueI";

7357

120 

7618

121 
Goal "P ==> P=True";


122 
by (REPEAT (ares_tac [iffI,TrueI] 1));


123 
qed "eqTrueI";

7357

124 

7618

125 
Goal "P=True ==> P";


126 
by (etac iffD2 1);


127 
by (rtac TrueI 1);


128 
qed "eqTrueE";

7357

129 


130 


131 
(** Universal quantifier **)


132 
section "!";


133 

9159

134 
val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)";

8529

135 
by (resolve_tac (prems RL [eqTrueI RS ext]) 1);


136 
qed "allI";

7357

137 

9159

138 
Goalw [All_def] "ALL x::'a. P(x) ==> P(x)";

8529

139 
by (rtac eqTrueE 1);


140 
by (etac fun_cong 1);


141 
qed "spec";

7357

142 

9969

143 
val major::prems = Goal "[ ALL x. P(x); P(x) ==> R ] ==> R";

7357

144 
by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;


145 
qed "allE";


146 

9969

147 
val prems = Goal

9159

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

7357

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


150 
qed "all_dupE";


151 


152 


153 
(** False ** Depends upon spec; it is impossible to do propositional logic


154 
before quantifiers! **)


155 
section "False";


156 

8529

157 
Goalw [False_def] "False ==> P";


158 
by (etac spec 1);


159 
qed "FalseE";

7357

160 

8529

161 
Goal "False=True ==> P";


162 
by (etac (eqTrueE RS FalseE) 1);


163 
qed "False_neq_True";

7357

164 


165 


166 
(** Negation **)


167 
section "~";


168 

8529

169 
val prems = Goalw [not_def] "(P ==> False) ==> ~P";


170 
by (rtac impI 1);


171 
by (eresolve_tac prems 1);


172 
qed "notI";

7357

173 

8529

174 
Goal "False ~= True";


175 
by (rtac notI 1);


176 
by (etac False_neq_True 1);


177 
qed "False_not_True";

7357

178 

8529

179 
Goal "True ~= False";


180 
by (rtac notI 1);


181 
by (dtac sym 1);


182 
by (etac False_neq_True 1);


183 
qed "True_not_False";

7357

184 

8529

185 
Goalw [not_def] "[ ~P; P ] ==> R";


186 
by (etac (mp RS FalseE) 1);


187 
by (assume_tac 1);


188 
qed "notE";

7357

189 

9159

190 
(* Alternative ~ introduction rule: [ P ==> ~ Pa; P ==> Pa ] ==> ~ P *)


191 
bind_thm ("notI2", notE RS notI);

7357

192 


193 


194 
(** Implication **)


195 
section ">";


196 


197 
val prems = Goal "[ P>Q; P; Q ==> R ] ==> R";


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


199 
qed "impE";


200 


201 
(* Reduces Q to P>Q, allowing substitution in P. *)


202 
Goal "[ P; P > Q ] ==> Q";


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


204 
qed "rev_mp";


205 


206 
val [major,minor] = Goal "[ ~Q; P==>Q ] ==> ~P";


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


208 
by (etac minor 1) ;


209 
qed "contrapos";


210 


211 
val [major,minor] = Goal "[ P==>Q; ~Q ] ==> ~P";


212 
by (rtac (minor RS contrapos) 1);


213 
by (etac major 1) ;


214 
qed "rev_contrapos";


215 

9159

216 
(* t ~= s ==> s ~= t *)

7357

217 
bind_thm("not_sym", sym COMP rev_contrapos);


218 


219 


220 
(** Existential quantifier **)

9159

221 
section "EX ";

7357

222 

9159

223 
Goalw [Ex_def] "P x ==> EX x::'a. P x";

8529

224 
by (etac selectI 1) ;


225 
qed "exI";

7357

226 

9869

227 
val [major,minor] =

9159

228 
Goalw [Ex_def] "[ EX x::'a. P(x); !!x. P(x) ==> Q ] ==> Q";

8529

229 
by (rtac (major RS minor) 1);


230 
qed "exE";

7357

231 


232 


233 
(** Conjunction **)


234 
section "&";


235 

8529

236 
Goalw [and_def] "[ P; Q ] ==> P&Q";


237 
by (rtac (impI RS allI) 1);


238 
by (etac (mp RS mp) 1);


239 
by (REPEAT (assume_tac 1));


240 
qed "conjI";

7357

241 

8529

242 
Goalw [and_def] "[ P & Q ] ==> P";


243 
by (dtac spec 1) ;


244 
by (etac mp 1);


245 
by (REPEAT (ares_tac [impI] 1));


246 
qed "conjunct1";

7357

247 

8529

248 
Goalw [and_def] "[ P & Q ] ==> Q";


249 
by (dtac spec 1) ;


250 
by (etac mp 1);


251 
by (REPEAT (ares_tac [impI] 1));


252 
qed "conjunct2";

7357

253 

8529

254 
val [major,minor] =


255 
Goal "[ P&Q; [ P; Q ] ==> R ] ==> R";


256 
by (rtac minor 1);


257 
by (rtac (major RS conjunct1) 1);


258 
by (rtac (major RS conjunct2) 1);


259 
qed "conjE";

7357

260 

8529

261 
val prems =


262 
Goal "[ P; P ==> Q ] ==> P & Q";


263 
by (REPEAT (resolve_tac (conjI::prems) 1));


264 
qed "context_conjI";

7357

265 


266 


267 
(** Disjunction *)


268 
section "";


269 

8529

270 
Goalw [or_def] "P ==> PQ";


271 
by (REPEAT (resolve_tac [allI,impI] 1));


272 
by (etac mp 1 THEN assume_tac 1);


273 
qed "disjI1";

7357

274 

8529

275 
Goalw [or_def] "Q ==> PQ";


276 
by (REPEAT (resolve_tac [allI,impI] 1));


277 
by (etac mp 1 THEN assume_tac 1);


278 
qed "disjI2";

7357

279 

8529

280 
val [major,minorP,minorQ] =


281 
Goalw [or_def] "[ P  Q; P ==> R; Q ==> R ] ==> R";


282 
by (rtac (major RS spec RS mp RS mp) 1);


283 
by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1));


284 
qed "disjE";

7357

285 


286 


287 
(** CCONTR  classical logic **)


288 
section "classical logic";


289 

8529

290 
val [prem] = Goal "(~P ==> P) ==> P";


291 
by (rtac (True_or_False RS disjE RS eqTrueE) 1);


292 
by (assume_tac 1);


293 
by (rtac (notI RS prem RS eqTrueI) 1);


294 
by (etac subst 1);


295 
by (assume_tac 1);


296 
qed "classical";

7357

297 

7832

298 
bind_thm ("ccontr", FalseE RS classical);

7357

299 

9159

300 
(*notE with premises exchanged; it discharges ~R so that it can be used to


301 
make elimination rules*)


302 
val [premp,premnot] = Goal "[ P; ~R ==> ~P ] ==> R";


303 
by (rtac ccontr 1);


304 
by (etac ([premnot,premp] MRS notE) 1);


305 
qed "rev_notE";


306 

7357

307 
(*Double negation law*)


308 
Goal "~~P ==> P";


309 
by (rtac classical 1);


310 
by (etac notE 1);


311 
by (assume_tac 1);


312 
qed "notnotD";


313 


314 
val [p1,p2] = Goal "[ Q; ~ P ==> ~ Q ] ==> P";


315 
by (rtac classical 1);


316 
by (dtac p2 1);


317 
by (etac notE 1);


318 
by (rtac p1 1);


319 
qed "contrapos2";


320 


321 
val [p1,p2] = Goal "[ P; Q ==> ~ P ] ==> ~ Q";


322 
by (rtac notI 1);


323 
by (dtac p2 1);


324 
by (etac notE 1);


325 
by (rtac p1 1);


326 
qed "swap2";


327 


328 
(** Unique existence **)

9159

329 
section "EX!";

7357

330 

9159

331 
val prems = Goalw [Ex1_def] "[ P(a); !!x. P(x) ==> x=a ] ==> EX! x. P(x)";

8529

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


333 
qed "ex1I";

7357

334 


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

8529

336 
val [ex_prem,eq] = Goal

9159

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

8529

338 
by (rtac (ex_prem RS exE) 1);

7357

339 
by (REPEAT (ares_tac [ex1I,eq] 1)) ;


340 
qed "ex_ex1I";


341 

8529

342 
val major::prems = Goalw [Ex1_def]

9159

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

8529

344 
by (rtac (major RS exE) 1);


345 
by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));


346 
qed "ex1E";

7357

347 

9159

348 
Goal "EX! x. P x ==> EX x. P x";

7357

349 
by (etac ex1E 1);


350 
by (rtac exI 1);


351 
by (assume_tac 1);


352 
qed "ex1_implies_ex";


353 


354 


355 
(** Select: Hilbert's Epsilonoperator **)


356 
section "@";


357 

9404

358 
(*Easier to apply than selectI if witness ?a comes from an EXformula*)

9969

359 
Goal "EX x. P x ==> P (SOME x. P x)";

9404

360 
by (etac exE 1);


361 
by (etac selectI 1);


362 
qed "ex_someI";


363 

7357

364 
(*Easier to apply than selectI: conclusion has only one occurrence of P*)


365 
val prems = Goal


366 
"[ P a; !!x. P x ==> Q x ] ==> Q (@x. P x)";


367 
by (resolve_tac prems 1);


368 
by (rtac selectI 1);


369 
by (resolve_tac prems 1) ;

9969

370 
qed "someI2";

7357

371 

9969

372 
(*Easier to apply than someI2 if witness ?a comes from an EXformula*)

9159

373 
val [major,minor] = Goal "[ EX a. P a; !!x. P x ==> Q x ] ==> Q (Eps P)";

8529

374 
by (rtac (major RS exE) 1);

9969

375 
by (etac someI2 1 THEN etac minor 1);


376 
qed "someI2EX";

7357

377 


378 
val prems = Goal


379 
"[ P a; !!x. P x ==> x=a ] ==> (@x. P x) = a";

9969

380 
by (rtac someI2 1);

7357

381 
by (REPEAT (ares_tac prems 1)) ;

9969

382 
qed "some_equality";

7357

383 

9159

384 
Goalw [Ex1_def] "[ EX!x. P x; P a ] ==> (@x. P x) = a";

9969

385 
by (rtac some_equality 1);

7357

386 
by (atac 1);


387 
by (etac exE 1);


388 
by (etac conjE 1);


389 
by (rtac allE 1);


390 
by (atac 1);


391 
by (etac impE 1);


392 
by (atac 1);


393 
by (etac ssubst 1);


394 
by (etac allE 1);


395 
by (etac mp 1);


396 
by (atac 1);

9969

397 
qed "some1_equality";

7357

398 

9159

399 
Goal "P (@ x. P x) = (EX x. P x)";

7357

400 
by (rtac iffI 1);


401 
by (etac exI 1);


402 
by (etac exE 1);


403 
by (etac selectI 1);

9969

404 
qed "some_eq_ex";

7357

405 


406 
Goal "(@y. y=x) = x";

9969

407 
by (rtac some_equality 1);

7357

408 
by (rtac refl 1);


409 
by (atac 1);

9969

410 
qed "some_eq_trivial";

7357

411 

9969

412 
Goal "(@y. x=y) = x";


413 
by (rtac some_equality 1);

7357

414 
by (rtac refl 1);


415 
by (etac sym 1);

9969

416 
qed "some_sym_eq_trivial";

7357

417 


418 
(** Classical intro rules for disjunction and existential quantifiers *)


419 
section "classical intro rules";


420 

9969

421 
val prems = Goal "(~Q ==> P) ==> PQ";

7357

422 
by (rtac classical 1);


423 
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));


424 
by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;


425 
qed "disjCI";


426 


427 
Goal "~P  P";


428 
by (REPEAT (ares_tac [disjCI] 1)) ;


429 
qed "excluded_middle";


430 


431 
(*For disjunctive case analysis*)


432 
fun excluded_middle_tac sP =


433 
res_inst_tac [("Q",sP)] (excluded_middle RS disjE);


434 


435 
(*Classical implies (>) elimination. *)


436 
val major::prems = Goal "[ P>Q; ~P ==> R; Q ==> R ] ==> R";


437 
by (rtac (excluded_middle RS disjE) 1);


438 
by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));


439 
qed "impCE";


440 


441 
(*This version of > elimination works on Q before P. It works best for


442 
those cases in which P holds "almost everywhere". Can't install as


443 
default: would break old proofs.*)


444 
val major::prems = Goal


445 
"[ P>Q; Q ==> R; ~P ==> R ] ==> R";


446 
by (resolve_tac [excluded_middle RS disjE] 1);


447 
by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;


448 
qed "impCE'";


449 


450 
(*Classical <> elimination. *)


451 
val major::prems = Goal


452 
"[ P=Q; [ P; Q ] ==> R; [ ~P; ~Q ] ==> R ] ==> R";


453 
by (rtac (major RS iffE) 1);

9869

454 
by (REPEAT (DEPTH_SOLVE_1


455 
(eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));

7357

456 
qed "iffCE";


457 

9159

458 
val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";

7357

459 
by (rtac ccontr 1);


460 
by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1)) ;


461 
qed "exCI";


462 

8964

463 
Goal "x + (y+z) = y + ((x+z)::'a::plus_ac0)";


464 
by (rtac (thm"plus_ac0.commute" RS trans) 1);


465 
by (rtac (thm"plus_ac0.assoc" RS trans) 1);


466 
by (rtac (thm"plus_ac0.commute" RS arg_cong) 1);


467 
qed "plus_ac0_left_commute";


468 


469 
Goal "x + 0 = (x ::'a::plus_ac0)";


470 
by (rtac (thm"plus_ac0.commute" RS trans) 1);


471 
by (rtac (thm"plus_ac0.zero") 1);


472 
qed "plus_ac0_zero_right";


473 

9869

474 
bind_thms ("plus_ac0", [thm"plus_ac0.assoc", thm"plus_ac0.commute",


475 
plus_ac0_left_commute,


476 
thm"plus_ac0.zero", plus_ac0_zero_right]);

7357

477 


478 
(* case distinction *)


479 

8529

480 
val [prem1,prem2] = Goal "[ P ==> Q; ~P ==> Q ] ==> Q";


481 
by (rtac (excluded_middle RS disjE) 1);


482 
by (etac prem2 1);


483 
by (etac prem1 1);


484 
qed "case_split_thm";

7357

485 


486 
fun case_tac a = res_inst_tac [("P",a)] case_split_thm;


487 


488 


489 
(** Standard abbreviations **)


490 

9869

491 
(* combination of (spec RS spec RS ...(j times) ... spec RS mp *)

7490

492 
local


493 
fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t


494 
 wrong_prem (Bound _) = true


495 
 wrong_prem _ = false;

7533

496 
val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))));

7490

497 
in


498 
fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);


499 
fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]


500 
end;


501 


502 

9869

503 
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
