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 


134 
qed_goalw "allI" (the_context ()) [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"


135 
(fn prems => [(resolve_tac (prems RL [eqTrueI RS ext]) 1)]);


136 


137 
qed_goalw "spec" (the_context ()) [All_def] "! x::'a. P(x) ==> P(x)"


138 
(fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);


139 


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


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


142 
qed "allE";


143 


144 
val prems = goal (the_context ())


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


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


147 
qed "all_dupE";


148 


149 


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


151 
before quantifiers! **)


152 
section "False";


153 


154 
qed_goalw "FalseE" (the_context ()) [False_def] "False ==> P"


155 
(fn [major] => [rtac (major RS spec) 1]);


156 


157 
qed_goal "False_neq_True" (the_context ()) "False=True ==> P"


158 
(fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);


159 


160 


161 
(** Negation **)


162 
section "~";


163 


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


165 
(fn prems=> [rtac impI 1, eresolve_tac prems 1]);


166 


167 
qed_goal "False_not_True" (the_context ()) "False ~= True"


168 
(fn _ => [rtac notI 1, etac False_neq_True 1]);


169 


170 
qed_goal "True_not_False" (the_context ()) "True ~= False"


171 
(fn _ => [rtac notI 1, dtac sym 1, etac False_neq_True 1]);


172 


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


174 
(fn prems => [rtac (prems MRS mp RS FalseE) 1]);


175 


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


177 


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


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


180 


181 


182 
(** Implication **)


183 
section ">";


184 


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


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


187 
qed "impE";


188 


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


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


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


192 
qed "rev_mp";


193 


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


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


196 
by (etac minor 1) ;


197 
qed "contrapos";


198 


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


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


201 
by (etac major 1) ;


202 
qed "rev_contrapos";


203 


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


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


206 


207 


208 
(** Existential quantifier **)


209 
section "?";


210 


211 
qed_goalw "exI" (the_context ()) [Ex_def] "P x ==> ? x::'a. P x"


212 
(fn prems => [rtac selectI 1, resolve_tac prems 1]);


213 


214 
qed_goalw "exE" (the_context ()) [Ex_def]


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


216 
(fn prems => [REPEAT(resolve_tac prems 1)]);


217 


218 


219 
(** Conjunction **)


220 
section "&";


221 


222 
qed_goalw "conjI" (the_context ()) [and_def] "[ P; Q ] ==> P&Q"


223 
(fn prems =>


224 
[REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);


225 


226 
qed_goalw "conjunct1" (the_context ()) [and_def] "[ P & Q ] ==> P"


227 
(fn prems =>


228 
[resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);


229 


230 
qed_goalw "conjunct2" (the_context ()) [and_def] "[ P & Q ] ==> Q"


231 
(fn prems =>


232 
[resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);


233 


234 
qed_goal "conjE" (the_context ()) "[ P&Q; [ P; Q ] ==> R ] ==> R"


235 
(fn prems =>


236 
[cut_facts_tac prems 1, resolve_tac prems 1,


237 
etac conjunct1 1, etac conjunct2 1]);


238 


239 
qed_goal "context_conjI" (the_context ()) "[ P; P ==> Q ] ==> P & Q"


240 
(fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);


241 


242 


243 
(** Disjunction *)


244 
section "";


245 


246 
qed_goalw "disjI1" (the_context ()) [or_def] "P ==> PQ"


247 
(fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);


248 


249 
qed_goalw "disjI2" (the_context ()) [or_def] "Q ==> PQ"


250 
(fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);


251 


252 
qed_goalw "disjE" (the_context ()) [or_def] "[ P  Q; P ==> R; Q ==> R ] ==> R"


253 
(fn [a1,a2,a3] =>


254 
[rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,


255 
rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);


256 


257 


258 
(** CCONTR  classical logic **)


259 
section "classical logic";


260 


261 
qed_goalw "classical" (the_context ()) [not_def] "(~P ==> P) ==> P"


262 
(fn [prem] =>


263 
[rtac (True_or_False RS (disjE RS eqTrueE)) 1, assume_tac 1,


264 
rtac (impI RS prem RS eqTrueI) 1,


265 
etac subst 1, assume_tac 1]);


266 


267 
val ccontr = FalseE RS classical;


268 


269 
(*Double negation law*)


270 
Goal "~~P ==> P";


271 
by (rtac classical 1);


272 
by (etac notE 1);


273 
by (assume_tac 1);


274 
qed "notnotD";


275 


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


277 
by (rtac classical 1);


278 
by (dtac p2 1);


279 
by (etac notE 1);


280 
by (rtac p1 1);


281 
qed "contrapos2";


282 


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


284 
by (rtac notI 1);


285 
by (dtac p2 1);


286 
by (etac notE 1);


287 
by (rtac p1 1);


288 
qed "swap2";


289 


290 
(** Unique existence **)


291 
section "?!";


292 


293 
qed_goalw "ex1I" (the_context ()) [Ex1_def]


294 
"[ P(a); !!x. P(x) ==> x=a ] ==> ?! x. P(x)"


295 
(fn prems =>


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


297 


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


299 
val [ex,eq] = Goal


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


301 
by (rtac (ex RS exE) 1);


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


303 
qed "ex_ex1I";


304 


305 
qed_goalw "ex1E" (the_context ()) [Ex1_def]


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


307 
(fn major::prems =>


308 
[rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);


309 


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


311 
by (etac ex1E 1);


312 
by (rtac exI 1);


313 
by (assume_tac 1);


314 
qed "ex1_implies_ex";


315 


316 


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


318 
section "@";


319 


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


321 
val prems = Goal


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


323 
by (resolve_tac prems 1);


324 
by (rtac selectI 1);


325 
by (resolve_tac prems 1) ;


326 
qed "selectI2";


327 


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


329 
qed_goal "selectI2EX" (the_context ())


330 
"[ ? a. P a; !!x. P x ==> Q x ] ==> Q (Eps P)"


331 
(fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);


332 


333 
val prems = Goal


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


335 
by (rtac selectI2 1);


336 
by (REPEAT (ares_tac prems 1)) ;


337 
qed "select_equality";


338 


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


340 
by (rtac select_equality 1);


341 
by (atac 1);


342 
by (etac exE 1);


343 
by (etac conjE 1);


344 
by (rtac allE 1);


345 
by (atac 1);


346 
by (etac impE 1);


347 
by (atac 1);


348 
by (etac ssubst 1);


349 
by (etac allE 1);


350 
by (etac mp 1);


351 
by (atac 1);


352 
qed "select1_equality";


353 


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


355 
by (rtac iffI 1);


356 
by (etac exI 1);


357 
by (etac exE 1);


358 
by (etac selectI 1);


359 
qed "select_eq_Ex";


360 


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


362 
by (rtac select_equality 1);


363 
by (rtac refl 1);


364 
by (atac 1);


365 
qed "Eps_eq";


366 


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


368 
by (rtac select_equality 1);


369 
by (rtac refl 1);


370 
by (etac sym 1);


371 
qed "Eps_sym_eq";


372 


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


374 
section "classical intro rules";


375 


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


377 
by (rtac classical 1);


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


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


380 
qed "disjCI";


381 


382 
Goal "~P  P";


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


384 
qed "excluded_middle";


385 


386 
(*For disjunctive case analysis*)


387 
fun excluded_middle_tac sP =


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


389 


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


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


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


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


394 
qed "impCE";


395 


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


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


398 
default: would break old proofs.*)


399 
val major::prems = Goal


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


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


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


403 
qed "impCE'";


404 


405 
(*Classical <> elimination. *)


406 
val major::prems = Goal


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


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


409 
by (REPEAT (DEPTH_SOLVE_1


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


411 
qed "iffCE";


412 


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


414 
by (rtac ccontr 1);


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


416 
qed "exCI";


417 


418 


419 
(* case distinction *)


420 


421 
qed_goal "case_split_thm" (the_context ()) "[ P ==> Q; ~P ==> Q ] ==> Q"


422 
(fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,


423 
etac p2 1, etac p1 1]);


424 


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


426 


427 


428 
(** Standard abbreviations **)


429 


430 
(*Apply an equality or definition ONCE.


431 
Fails unless the substitution has an effect*)


432 
fun stac th =


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


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


435 
end;


436 

7490

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


438 
local


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


440 
 wrong_prem (Bound _) = true


441 
 wrong_prem _ = false;

7533

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

7490

443 
in


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


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


446 
end;


447 


448 

7357

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


450 


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


452 


453 
local


454 


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


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


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


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


459 
val aspec = forall_intr cvx myspec;


460 


461 
in


462 


463 
fun RSspec th =


464 
(case concl_of th of


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


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


467 
in th RS forall_elim ca aspec end


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


469 


470 
fun RSmp th =


471 
(case concl_of th of


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


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


474 


475 
fun normalize_thm funs =


476 
let fun trans [] th = th


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


478 
in zero_var_indexes o trans funs end;


479 


480 
fun qed_spec_mp name =


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


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


483 


484 
fun qed_goal_spec_mp name thy s p =


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


486 


487 
fun qed_goalw_spec_mp name thy defs s p =


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


489 


490 
end;


491 


492 


493 
(* attributes *)


494 


495 
local


496 


497 
fun gen_rulify x =


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


499 


500 
in


501 


502 
val attrib_setup =


503 
[Attrib.add_attributes


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


505 


506 
end;
