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 


40 
qed_goal "sym" (the_context ()) "s=t ==> t=s"


41 
(fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);


42 


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


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


45 


46 
qed_goal "trans" (the_context ()) "[ r=s; s=t ] ==> r=t"


47 
(fn prems =>


48 
[rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);


49 


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


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 


66 


67 
(** Congruence rules for metaapplication **)


68 
section "Congruence";


69 


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


71 
qed_goal "fun_cong" (the_context ()) "(f::'a=>'b) = g ==> f(x)=g(x)"


72 
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);


73 


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


75 
qed_goal "arg_cong" (the_context ()) "x=y ==> f(x)=f(y)"


76 
(fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);


77 


78 
qed_goal "cong" (the_context ())


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


80 
(fn [prem1,prem2] =>


81 
[rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);


82 


83 


84 
(** Equality of booleans  iff **)


85 
section "iff";


86 


87 
val prems = Goal


88 
"[ P ==> Q; Q ==> P ] ==> P=Q";


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


90 
qed "iffI";


91 


92 
qed_goal "iffD2" (the_context ()) "[ P=Q; Q ] ==> P"


93 
(fn prems =>


94 
[rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);


95 


96 
qed_goal "rev_iffD2" (the_context ()) "!!P. [ Q; P=Q ] ==> P"


97 
(fn _ => [etac iffD2 1, assume_tac 1]);


98 


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


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


101 


102 
qed_goal "iffE" (the_context ())


103 
"[ P=Q; [ P > Q; Q > P ] ==> R ] ==> R"


104 
(fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);


105 


106 


107 
(** True **)


108 
section "True";


109 


110 
qed_goalw "TrueI" (the_context ()) [True_def] "True"


111 
(fn _ => [(rtac refl 1)]);


112 


113 
qed_goal "eqTrueI" (the_context ()) "P ==> P=True"


114 
(fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);


115 


116 
qed_goal "eqTrueE" (the_context ()) "P=True ==> P"


117 
(fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);


118 


119 


120 
(** Universal quantifier **)


121 
section "!";


122 


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


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


125 


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


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


128 


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


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


131 
qed "allE";


132 


133 
val prems = goal (the_context ())


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


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


136 
qed "all_dupE";


137 


138 


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


140 
before quantifiers! **)


141 
section "False";


142 


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


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


145 


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


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


148 


149 


150 
(** Negation **)


151 
section "~";


152 


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


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


155 


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


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


158 


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


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


161 


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


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


164 


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


166 


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


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


169 


170 


171 
(** Implication **)


172 
section ">";


173 


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


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


176 
qed "impE";


177 


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


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


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


181 
qed "rev_mp";


182 


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


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


185 
by (etac minor 1) ;


186 
qed "contrapos";


187 


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


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


190 
by (etac major 1) ;


191 
qed "rev_contrapos";


192 


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


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


195 


196 


197 
(** Existential quantifier **)


198 
section "?";


199 


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


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


202 


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


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


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


206 


207 


208 
(** Conjunction **)


209 
section "&";


210 


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


212 
(fn prems =>


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


214 


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


216 
(fn prems =>


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


218 


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


220 
(fn prems =>


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


222 


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


224 
(fn prems =>


225 
[cut_facts_tac prems 1, resolve_tac prems 1,


226 
etac conjunct1 1, etac conjunct2 1]);


227 


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


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


230 


231 


232 
(** Disjunction *)


233 
section "";


234 


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


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


237 


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


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


240 


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


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


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


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


245 


246 


247 
(** CCONTR  classical logic **)


248 
section "classical logic";


249 


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


251 
(fn [prem] =>


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


253 
rtac (impI RS prem RS eqTrueI) 1,


254 
etac subst 1, assume_tac 1]);


255 


256 
val ccontr = FalseE RS classical;


257 


258 
(*Double negation law*)


259 
Goal "~~P ==> P";


260 
by (rtac classical 1);


261 
by (etac notE 1);


262 
by (assume_tac 1);


263 
qed "notnotD";


264 


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


266 
by (rtac classical 1);


267 
by (dtac p2 1);


268 
by (etac notE 1);


269 
by (rtac p1 1);


270 
qed "contrapos2";


271 


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


273 
by (rtac notI 1);


274 
by (dtac p2 1);


275 
by (etac notE 1);


276 
by (rtac p1 1);


277 
qed "swap2";


278 


279 
(** Unique existence **)


280 
section "?!";


281 


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


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


284 
(fn prems =>


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


286 


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


288 
val [ex,eq] = Goal


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


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


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


292 
qed "ex_ex1I";


293 


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


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


296 
(fn major::prems =>


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


298 


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


300 
by (etac ex1E 1);


301 
by (rtac exI 1);


302 
by (assume_tac 1);


303 
qed "ex1_implies_ex";


304 


305 


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


307 
section "@";


308 


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


310 
val prems = Goal


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


312 
by (resolve_tac prems 1);


313 
by (rtac selectI 1);


314 
by (resolve_tac prems 1) ;


315 
qed "selectI2";


316 


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


318 
qed_goal "selectI2EX" (the_context ())


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


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


321 


322 
val prems = Goal


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


324 
by (rtac selectI2 1);


325 
by (REPEAT (ares_tac prems 1)) ;


326 
qed "select_equality";


327 


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


329 
by (rtac select_equality 1);


330 
by (atac 1);


331 
by (etac exE 1);


332 
by (etac conjE 1);


333 
by (rtac allE 1);


334 
by (atac 1);


335 
by (etac impE 1);


336 
by (atac 1);


337 
by (etac ssubst 1);


338 
by (etac allE 1);


339 
by (etac mp 1);


340 
by (atac 1);


341 
qed "select1_equality";


342 


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


344 
by (rtac iffI 1);


345 
by (etac exI 1);


346 
by (etac exE 1);


347 
by (etac selectI 1);


348 
qed "select_eq_Ex";


349 


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


351 
by (rtac select_equality 1);


352 
by (rtac refl 1);


353 
by (atac 1);


354 
qed "Eps_eq";


355 


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


357 
by (rtac select_equality 1);


358 
by (rtac refl 1);


359 
by (etac sym 1);


360 
qed "Eps_sym_eq";


361 


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


363 
section "classical intro rules";


364 


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


366 
by (rtac classical 1);


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


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


369 
qed "disjCI";


370 


371 
Goal "~P  P";


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


373 
qed "excluded_middle";


374 


375 
(*For disjunctive case analysis*)


376 
fun excluded_middle_tac sP =


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


378 


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


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


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


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


383 
qed "impCE";


384 


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


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


387 
default: would break old proofs.*)


388 
val major::prems = Goal


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


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


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


392 
qed "impCE'";


393 


394 
(*Classical <> elimination. *)


395 
val major::prems = Goal


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


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


398 
by (REPEAT (DEPTH_SOLVE_1


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


400 
qed "iffCE";


401 


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


403 
by (rtac ccontr 1);


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


405 
qed "exCI";


406 


407 


408 
(* case distinction *)


409 


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


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


412 
etac p2 1, etac p1 1]);


413 


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


415 


416 


417 
(** Standard abbreviations **)


418 


419 
(*Apply an equality or definition ONCE.


420 
Fails unless the substitution has an effect*)


421 
fun stac th =


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


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


424 
end;


425 


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


427 


428 


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


430 


431 
local


432 


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


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


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


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


437 
val aspec = forall_intr cvx myspec;


438 


439 
in


440 


441 
fun RSspec th =


442 
(case concl_of th of


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


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


445 
in th RS forall_elim ca aspec end


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


447 


448 
fun RSmp th =


449 
(case concl_of th of


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


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


452 


453 
fun normalize_thm funs =


454 
let fun trans [] th = th


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


456 
in zero_var_indexes o trans funs end;


457 


458 
fun qed_spec_mp name =


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


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


461 


462 
fun qed_goal_spec_mp name thy s p =


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


464 


465 
fun qed_goalw_spec_mp name thy defs s p =


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


467 


468 
end;


469 


470 


471 
(* attributes *)


472 


473 
local


474 


475 
fun gen_rulify x =


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


477 


478 
in


479 


480 
val attrib_setup =


481 
[Attrib.add_attributes


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


483 


484 
end;
