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 

8529

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


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


136 
qed "allI";

7357

137 

8529

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


139 
by (rtac eqTrueE 1);


140 
by (etac fun_cong 1);


141 
qed "spec";

7357

142 

8529

143 
val major::prems= goal (the_context ()) "[ ! 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 ())


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


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 


190 
bind_thm ("classical2", notE RS notI);


191 

8529

192 
Goal "[ P; ~P ] ==> R";


193 
by (etac notE 1);


194 
by (assume_tac 1);


195 
qed "rev_notE";

7357

196 


197 


198 
(** Implication **)


199 
section ">";


200 


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


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


203 
qed "impE";


204 


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


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


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


208 
qed "rev_mp";


209 


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


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


212 
by (etac minor 1) ;


213 
qed "contrapos";


214 


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


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


217 
by (etac major 1) ;


218 
qed "rev_contrapos";


219 


220 
(* ~(?t = ?s) ==> ~(?s = ?t) *)


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


222 


223 


224 
(** Existential quantifier **)


225 
section "?";


226 

8529

227 
Goalw [Ex_def] "P x ==> ? x::'a. P x";


228 
by (etac selectI 1) ;


229 
qed "exI";

7357

230 

8529

231 
val [major,minor] =


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


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


234 
qed "exE";

7357

235 


236 


237 
(** Conjunction **)


238 
section "&";


239 

8529

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


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


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


243 
by (REPEAT (assume_tac 1));


244 
qed "conjI";

7357

245 

8529

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


247 
by (dtac spec 1) ;


248 
by (etac mp 1);


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


250 
qed "conjunct1";

7357

251 

8529

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


253 
by (dtac spec 1) ;


254 
by (etac mp 1);


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


256 
qed "conjunct2";

7357

257 

8529

258 
val [major,minor] =


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


260 
by (rtac minor 1);


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


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


263 
qed "conjE";

7357

264 

8529

265 
val prems =


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


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


268 
qed "context_conjI";

7357

269 


270 


271 
(** Disjunction *)


272 
section "";


273 

8529

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


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


276 
by (etac mp 1 THEN assume_tac 1);


277 
qed "disjI1";

7357

278 

8529

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


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


281 
by (etac mp 1 THEN assume_tac 1);


282 
qed "disjI2";

7357

283 

8529

284 
val [major,minorP,minorQ] =


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


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


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


288 
qed "disjE";

7357

289 


290 


291 
(** CCONTR  classical logic **)


292 
section "classical logic";


293 

8529

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


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


296 
by (assume_tac 1);


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


298 
by (etac subst 1);


299 
by (assume_tac 1);


300 
qed "classical";

7357

301 

7832

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

7357

303 


304 
(*Double negation law*)


305 
Goal "~~P ==> P";


306 
by (rtac classical 1);


307 
by (etac notE 1);


308 
by (assume_tac 1);


309 
qed "notnotD";


310 


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


312 
by (rtac classical 1);


313 
by (dtac p2 1);


314 
by (etac notE 1);


315 
by (rtac p1 1);


316 
qed "contrapos2";


317 


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


319 
by (rtac notI 1);


320 
by (dtac p2 1);


321 
by (etac notE 1);


322 
by (rtac p1 1);


323 
qed "swap2";


324 


325 
(** Unique existence **)


326 
section "?!";


327 

8529

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


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


330 
qed "ex1I";

7357

331 


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

8529

333 
val [ex_prem,eq] = Goal

7357

334 
"[ ? x. P(x); !!x y. [ P(x); P(y) ] ==> x=y ] ==> ?! x. P(x)";

8529

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

7357

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


337 
qed "ex_ex1I";


338 

8529

339 
val major::prems = Goalw [Ex1_def]


340 
"[ ?! x. P(x); !!x. [ P(x); ! y. P(y) > y=x ] ==> R ] ==> R";


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


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


343 
qed "ex1E";

7357

344 


345 
Goal "?! x. P x ==> ? x. P x";


346 
by (etac ex1E 1);


347 
by (rtac exI 1);


348 
by (assume_tac 1);


349 
qed "ex1_implies_ex";


350 


351 


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


353 
section "@";


354 


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


356 
val prems = Goal


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


358 
by (resolve_tac prems 1);


359 
by (rtac selectI 1);


360 
by (resolve_tac prems 1) ;


361 
qed "selectI2";


362 


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

8529

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


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


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


367 
qed "selectI2EX";

7357

368 


369 
val prems = Goal


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


371 
by (rtac selectI2 1);


372 
by (REPEAT (ares_tac prems 1)) ;


373 
qed "select_equality";


374 


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


376 
by (rtac select_equality 1);


377 
by (atac 1);


378 
by (etac exE 1);


379 
by (etac conjE 1);


380 
by (rtac allE 1);


381 
by (atac 1);


382 
by (etac impE 1);


383 
by (atac 1);


384 
by (etac ssubst 1);


385 
by (etac allE 1);


386 
by (etac mp 1);


387 
by (atac 1);


388 
qed "select1_equality";


389 


390 
Goal "P (@ x. P x) = (? x. P x)";


391 
by (rtac iffI 1);


392 
by (etac exI 1);


393 
by (etac exE 1);


394 
by (etac selectI 1);


395 
qed "select_eq_Ex";


396 


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


398 
by (rtac select_equality 1);


399 
by (rtac refl 1);


400 
by (atac 1);


401 
qed "Eps_eq";


402 


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


404 
by (rtac select_equality 1);


405 
by (rtac refl 1);


406 
by (etac sym 1);


407 
qed "Eps_sym_eq";


408 


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


410 
section "classical intro rules";


411 


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


413 
by (rtac classical 1);


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


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


416 
qed "disjCI";


417 


418 
Goal "~P  P";


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


420 
qed "excluded_middle";


421 


422 
(*For disjunctive case analysis*)


423 
fun excluded_middle_tac sP =


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


425 


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


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


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


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


430 
qed "impCE";


431 


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


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


434 
default: would break old proofs.*)


435 
val major::prems = Goal


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


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


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


439 
qed "impCE'";


440 


441 
(*Classical <> elimination. *)


442 
val major::prems = Goal


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


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


445 
by (REPEAT (DEPTH_SOLVE_1


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


447 
qed "iffCE";


448 


449 
val prems = Goal "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)";


450 
by (rtac ccontr 1);


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


452 
qed "exCI";


453 

8964

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


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


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


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


458 
qed "plus_ac0_left_commute";


459 


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


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


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


463 
qed "plus_ac0_zero_right";


464 


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


466 
plus_ac0_left_commute,


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

7357

468 


469 
(* case distinction *)


470 

8529

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


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


473 
by (etac prem2 1);


474 
by (etac prem1 1);


475 
qed "case_split_thm";

7357

476 


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


478 


479 


480 
(** Standard abbreviations **)


481 


482 
(*Apply an equality or definition ONCE.


483 
Fails unless the substitution has an effect*)


484 
fun stac th =


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


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


487 
end;


488 

7490

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


490 
local


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


492 
 wrong_prem (Bound _) = true


493 
 wrong_prem _ = false;

7533

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

7490

495 
in


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


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


498 
end;


499 


500 

7357

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


502 


503 
(** strip ! and > from proved goal while preserving !bound var names **)


504 

7884

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


506 

7357

507 
local


508 


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


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


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


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


513 
val aspec = forall_intr cvx myspec;


514 


515 
in


516 


517 
fun RSspec th =


518 
(case concl_of th of


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


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


521 
in th RS forall_elim ca aspec end


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


523 


524 
fun RSmp th =


525 
(case concl_of th of


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


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


528 


529 
fun normalize_thm funs =


530 
let fun trans [] th = th


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


532 
in zero_var_indexes o trans funs end;


533 


534 
fun qed_spec_mp name =


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


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


537 


538 
fun qed_goal_spec_mp name thy s p =


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


540 


541 
fun qed_goalw_spec_mp name thy defs s p =


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


543 


544 
end;


545 


546 


547 
(* attributes *)


548 


549 
local


550 


551 
fun gen_rulify x =


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


553 


554 
in


555 


556 
val attrib_setup =


557 
[Attrib.add_attributes


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


559 


560 
end;
