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 eq_reflection = thm "eq_reflection";


15 
val refl = thm "refl";


16 
val subst = thm "subst";


17 
val ext = thm "ext";

9970

18 
val someI = thm "someI";

7357

19 
val impI = thm "impI";


20 
val mp = thm "mp";


21 
val True_def = thm "True_def";


22 
val All_def = thm "All_def";


23 
val Ex_def = thm "Ex_def";


24 
val False_def = thm "False_def";


25 
val not_def = thm "not_def";


26 
val and_def = thm "and_def";


27 
val or_def = thm "or_def";


28 
val Ex1_def = thm "Ex1_def";


29 
val iff = thm "iff";


30 
val True_or_False = thm "True_or_False";


31 
val Let_def = thm "Let_def";


32 
val if_def = thm "if_def";


33 
val arbitrary_def = thm "arbitrary_def";


34 


35 

10063

36 
section "Equality";

7357

37 

7618

38 
Goal "s=t ==> t=s";


39 
by (etac subst 1);


40 
by (rtac refl 1);


41 
qed "sym";

7357

42 


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

7618

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

7357

45 

7618

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


47 
by (etac subst 1 THEN assume_tac 1);


48 
qed "trans";

7357

49 

9969

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

7357

51 
by (rewrite_goals_tac prems);


52 
by (rtac refl 1);


53 
qed "def_imp_eq";


54 


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


56 
a = b


57 
 


58 
c = d *)


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


60 
by (rtac trans 1);


61 
by (rtac trans 1);


62 
by (rtac sym 1);


63 
by (REPEAT (assume_tac 1)) ;


64 
qed "box_equals";


65 

10063

66 


67 
section "Congruence rules for application";

7357

68 


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

7618

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


71 
by (etac subst 1);


72 
by (rtac refl 1);


73 
qed "fun_cong";

7357

74 


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

7618

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


77 
by (etac subst 1);


78 
by (rtac refl 1);


79 
qed "arg_cong";

7357

80 

7618

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


82 
by (etac subst 1);


83 
by (etac subst 1);


84 
by (rtac refl 1);


85 
qed "cong";

7357

86 

10063

87 


88 
section "Equality of booleans  iff";

7357

89 

7618

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

7357

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


92 
qed "iffI";


93 

7618

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


95 
by (etac ssubst 1);


96 
by (assume_tac 1);


97 
qed "iffD2";

7357

98 

7618

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


100 
by (etac iffD2 1);


101 
by (assume_tac 1);


102 
qed "rev_iffD2";

7357

103 


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


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


106 

7618

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


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


109 
qed "iffE";

7357

110 


111 


112 
section "True";


113 

7618

114 
Goalw [True_def] "True";


115 
by (rtac refl 1);


116 
qed "TrueI";

7357

117 

7618

118 
Goal "P ==> P=True";


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


120 
qed "eqTrueI";

7357

121 

7618

122 
Goal "P=True ==> P";


123 
by (etac iffD2 1);


124 
by (rtac TrueI 1);


125 
qed "eqTrueE";

7357

126 


127 

10063

128 
section "Universal quantifier";

7357

129 

9159

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

8529

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


132 
qed "allI";

7357

133 

9159

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

8529

135 
by (rtac eqTrueE 1);


136 
by (etac fun_cong 1);


137 
qed "spec";

7357

138 

9969

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

7357

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


141 
qed "allE";


142 

9969

143 
val prems = Goal

9159

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

7357

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


146 
qed "all_dupE";


147 


148 


149 
section "False";

10063

150 
(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)

7357

151 

8529

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


153 
by (etac spec 1);


154 
qed "FalseE";

7357

155 

8529

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


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


158 
qed "False_neq_True";

7357

159 


160 

10063

161 
section "Negation";

7357

162 

8529

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


164 
by (rtac impI 1);


165 
by (eresolve_tac prems 1);


166 
qed "notI";

7357

167 

8529

168 
Goal "False ~= True";


169 
by (rtac notI 1);


170 
by (etac False_neq_True 1);


171 
qed "False_not_True";

7357

172 

8529

173 
Goal "True ~= False";


174 
by (rtac notI 1);


175 
by (dtac sym 1);


176 
by (etac False_neq_True 1);


177 
qed "True_not_False";

7357

178 

8529

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


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


181 
by (assume_tac 1);


182 
qed "notE";

7357

183 

9159

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


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

7357

186 


187 

10063

188 
section "Implication";

7357

189 


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


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


192 
qed "impE";


193 


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


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


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


197 
qed "rev_mp";


198 


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


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


201 
by (etac minor 1) ;

10231

202 
qed "contrapos_nn";

7357

203 

10231

204 
Goal "t ~= s ==> s ~= t";


205 
by (etac contrapos_nn 1);


206 
by (etac sym 1);


207 
qed "not_sym";


208 


209 
(*still used in HOLCF*)

7357

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

10231

211 
by (rtac (minor RS contrapos_nn) 1);

7357

212 
by (etac major 1) ;


213 
qed "rev_contrapos";


214 

10063

215 
section "Existential quantifier";

7357

216 

9159

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

9970

218 
by (etac someI 1) ;

8529

219 
qed "exI";

7357

220 

9869

221 
val [major,minor] =

9159

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

8529

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


224 
qed "exE";

7357

225 


226 

10063

227 
section "Conjunction";

7357

228 

8529

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


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


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


232 
by (REPEAT (assume_tac 1));


233 
qed "conjI";

7357

234 

8529

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


236 
by (dtac spec 1) ;


237 
by (etac mp 1);


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


239 
qed "conjunct1";

7357

240 

8529

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


242 
by (dtac spec 1) ;


243 
by (etac mp 1);


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


245 
qed "conjunct2";

7357

246 

8529

247 
val [major,minor] =


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


249 
by (rtac minor 1);


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


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


252 
qed "conjE";

7357

253 

8529

254 
val prems =


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


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


257 
qed "context_conjI";

7357

258 


259 

10063

260 
section "Disjunction";

7357

261 

8529

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


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


264 
by (etac mp 1 THEN assume_tac 1);


265 
qed "disjI1";

7357

266 

8529

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


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


269 
by (etac mp 1 THEN assume_tac 1);


270 
qed "disjI2";

7357

271 

8529

272 
val [major,minorP,minorQ] =


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


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


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


276 
qed "disjE";

7357

277 


278 

10063

279 
section "Classical logic";


280 
(*CCONTR  classical logic*)

7357

281 

8529

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


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


284 
by (assume_tac 1);


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


286 
by (etac subst 1);


287 
by (assume_tac 1);


288 
qed "classical";

7357

289 

7832

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

7357

291 

9159

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


293 
make elimination rules*)


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


295 
by (rtac ccontr 1);


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


297 
qed "rev_notE";


298 

7357

299 
(*Double negation law*)


300 
Goal "~~P ==> P";


301 
by (rtac classical 1);


302 
by (etac notE 1);


303 
by (assume_tac 1);


304 
qed "notnotD";


305 


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


307 
by (rtac classical 1);


308 
by (dtac p2 1);


309 
by (etac notE 1);


310 
by (rtac p1 1);

10231

311 
qed "contrapos_pp";

7357

312 

10063

313 


314 
section "Unique existence";

7357

315 

9159

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

8529

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


318 
qed "ex1I";

7357

319 


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

8529

321 
val [ex_prem,eq] = Goal

9159

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

8529

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

7357

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


325 
qed "ex_ex1I";


326 

8529

327 
val major::prems = Goalw [Ex1_def]

9159

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

8529

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


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


331 
qed "ex1E";

7357

332 

9159

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

7357

334 
by (etac ex1E 1);


335 
by (rtac exI 1);


336 
by (assume_tac 1);


337 
qed "ex1_implies_ex";


338 


339 

10063

340 
section "SOME: Hilbert's Epsilonoperator";

7357

341 

9970

342 
(*Easier to apply than someI if witness ?a comes from an EXformula*)

9969

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

9404

344 
by (etac exE 1);

9970

345 
by (etac someI 1);

10175

346 
qed "someI_ex";

9404

347 

9970

348 
(*Easier to apply than someI: conclusion has only one occurrence of P*)

7357

349 
val prems = Goal

10170

350 
"[ P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)";

7357

351 
by (resolve_tac prems 1);

9970

352 
by (rtac someI 1);

7357

353 
by (resolve_tac prems 1) ;

9969

354 
qed "someI2";

7357

355 

9969

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

10170

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

8529

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

9969

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

9998

360 
qed "someI2_ex";

7357

361 


362 
val prems = Goal

10175

363 
"[ P a; !!x. P x ==> x=a ] ==> (SOME x. P x) = a";

9969

364 
by (rtac someI2 1);

7357

365 
by (REPEAT (ares_tac prems 1)) ;

9969

366 
qed "some_equality";

7357

367 

10175

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

9969

369 
by (rtac some_equality 1);

7357

370 
by (atac 1);


371 
by (etac exE 1);


372 
by (etac conjE 1);


373 
by (rtac allE 1);


374 
by (atac 1);


375 
by (etac impE 1);


376 
by (atac 1);


377 
by (etac ssubst 1);


378 
by (etac allE 1);


379 
by (etac mp 1);


380 
by (atac 1);

9969

381 
qed "some1_equality";

7357

382 

10175

383 
Goal "P (SOME x. P x) = (EX x. P x)";

7357

384 
by (rtac iffI 1);


385 
by (etac exI 1);


386 
by (etac exE 1);

9970

387 
by (etac someI 1);

9969

388 
qed "some_eq_ex";

7357

389 

10175

390 
Goal "(SOME y. y=x) = x";

9969

391 
by (rtac some_equality 1);

7357

392 
by (rtac refl 1);


393 
by (atac 1);

9969

394 
qed "some_eq_trivial";

7357

395 

10175

396 
Goal "(SOME y. x=y) = x";

9969

397 
by (rtac some_equality 1);

7357

398 
by (rtac refl 1);


399 
by (etac sym 1);

9969

400 
qed "some_sym_eq_trivial";

7357

401 

10063

402 


403 
section "Classical intro rules for disjunction and existential quantifiers";

7357

404 

9969

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

7357

406 
by (rtac classical 1);


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


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


409 
qed "disjCI";


410 


411 
Goal "~P  P";


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


413 
qed "excluded_middle";


414 


415 
(*For disjunctive case analysis*)


416 
fun excluded_middle_tac sP =


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


418 


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


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


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


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


423 
qed "impCE";


424 


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


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


427 
default: would break old proofs.*)


428 
val major::prems = Goal


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


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


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


432 
qed "impCE'";


433 


434 
(*Classical <> elimination. *)


435 
val major::prems = Goal


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


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

9869

438 
by (REPEAT (DEPTH_SOLVE_1


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

7357

440 
qed "iffCE";


441 

9159

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

7357

443 
by (rtac ccontr 1);


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


445 
qed "exCI";


446 

8964

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


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


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


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


451 
qed "plus_ac0_left_commute";


452 


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


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


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


456 
qed "plus_ac0_zero_right";


457 

9869

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


459 
plus_ac0_left_commute,


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

7357

461 


462 
(* case distinction *)


463 

8529

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


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


466 
by (etac prem2 1);


467 
by (etac prem1 1);


468 
qed "case_split_thm";

7357

469 


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


471 


472 


473 
(** Standard abbreviations **)


474 

9869

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

7490

476 
local


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


478 
 wrong_prem (Bound _) = true


479 
 wrong_prem _ = false;

7533

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

7490

481 
in


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


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


484 
end;


485 


486 

9869

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