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 


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


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 

9159

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

7357

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


145 
qed "allE";


146 


147 
val prems = goal (the_context ())

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 

8529

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 


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


359 
val prems = Goal


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


361 
by (resolve_tac prems 1);


362 
by (rtac selectI 1);


363 
by (resolve_tac prems 1) ;


364 
qed "selectI2";


365 


366 
(*Easier to apply than selectI2 if witness ?a comes from an EXformula*)

9159

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

8529

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


369 
by (etac selectI2 1 THEN etac minor 1);


370 
qed "selectI2EX";

7357

371 


372 
val prems = Goal


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


374 
by (rtac selectI2 1);


375 
by (REPEAT (ares_tac prems 1)) ;


376 
qed "select_equality";


377 

9159

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

7357

379 
by (rtac select_equality 1);


380 
by (atac 1);


381 
by (etac exE 1);


382 
by (etac conjE 1);


383 
by (rtac allE 1);


384 
by (atac 1);


385 
by (etac impE 1);


386 
by (atac 1);


387 
by (etac ssubst 1);


388 
by (etac allE 1);


389 
by (etac mp 1);


390 
by (atac 1);


391 
qed "select1_equality";


392 

9159

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

7357

394 
by (rtac iffI 1);


395 
by (etac exI 1);


396 
by (etac exE 1);


397 
by (etac selectI 1);


398 
qed "select_eq_Ex";


399 


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


401 
by (rtac select_equality 1);


402 
by (rtac refl 1);


403 
by (atac 1);


404 
qed "Eps_eq";


405 


406 
Goal "(Eps (op = x)) = x";


407 
by (rtac select_equality 1);


408 
by (rtac refl 1);


409 
by (etac sym 1);


410 
qed "Eps_sym_eq";


411 


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


413 
section "classical intro rules";


414 


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


416 
by (rtac classical 1);


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


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


419 
qed "disjCI";


420 


421 
Goal "~P  P";


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


423 
qed "excluded_middle";


424 


425 
(*For disjunctive case analysis*)


426 
fun excluded_middle_tac sP =


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


428 


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


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


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


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


433 
qed "impCE";


434 


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


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


437 
default: would break old proofs.*)


438 
val major::prems = Goal


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


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


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


442 
qed "impCE'";


443 


444 
(*Classical <> elimination. *)


445 
val major::prems = Goal


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


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


448 
by (REPEAT (DEPTH_SOLVE_1


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


450 
qed "iffCE";


451 

9159

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

7357

453 
by (rtac ccontr 1);


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


455 
qed "exCI";


456 

8964

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


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


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


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


461 
qed "plus_ac0_left_commute";


462 


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


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


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


466 
qed "plus_ac0_zero_right";


467 


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


469 
plus_ac0_left_commute,


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

7357

471 


472 
(* case distinction *)


473 

8529

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


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


476 
by (etac prem2 1);


477 
by (etac prem1 1);


478 
qed "case_split_thm";

7357

479 


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


481 


482 


483 
(** Standard abbreviations **)


484 


485 
(*Apply an equality or definition ONCE.


486 
Fails unless the substitution has an effect*)


487 
fun stac th =


488 
let val th' = th RS def_imp_eq handle THM _ => th


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


490 
end;


491 

7490

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


493 
local


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


495 
 wrong_prem (Bound _) = true


496 
 wrong_prem _ = false;

7533

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

7490

498 
in


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


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


501 
end;


502 


503 

7357

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


505 

9159

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

7357

507 

7884

508 
(** THIS CODE IS A MESS!!! **)


509 

7357

510 
local


511 


512 
(* Use XXX to avoid forall_intr failing because of duplicate variable name *)


513 
val myspec = read_instantiate [("P","?XXX")] spec;


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


515 
val cvx = cterm_of (#sign(rep_thm myspec)) vx;


516 
val aspec = forall_intr cvx myspec;


517 


518 
in


519 


520 
fun RSspec th =


521 
(case concl_of th of


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


523 
let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))


524 
in th RS forall_elim ca aspec end


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


526 


527 
fun RSmp th =


528 
(case concl_of th of


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


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


531 


532 
fun normalize_thm funs =


533 
let fun trans [] th = th


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

9058

535 
in zero_var_indexes o strip_shyps_warning o trans funs end;

7357

536 


537 
fun qed_spec_mp name =


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


539 
in ThmDatabase.ml_store_thm(name, thm) end;


540 


541 
fun qed_goal_spec_mp name thy s p =


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


543 


544 
fun qed_goalw_spec_mp name thy defs s p =


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


546 


547 
end;


548 


549 


550 
(* attributes *)


551 


552 
local


553 


554 
fun gen_rulify x =


555 
Attrib.no_args (Drule.rule_attribute (fn _ => (normalize_thm [RSspec, RSmp]))) x;


556 


557 
in


558 


559 
val attrib_setup =


560 
[Attrib.add_attributes


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


562 


563 
end;
