src/HOL/HOL_lemmas.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14430 5cb24165a2e1
permissions -rw-r--r--
import -> imports
     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 (* legacy 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";
    18 val impI = thm "impI";
    19 val mp = thm "mp";
    20 val True_def = thm "True_def";
    21 val All_def = thm "All_def";
    22 val Ex_def = thm "Ex_def";
    23 val False_def = thm "False_def";
    24 val not_def = thm "not_def";
    25 val and_def = thm "and_def";
    26 val or_def = thm "or_def";
    27 val Ex1_def = thm "Ex1_def";
    28 val iff = thm "iff";
    29 val True_or_False = thm "True_or_False";
    30 val Let_def = thm "Let_def";
    31 val if_def = thm "if_def";
    32 
    33 
    34 section "Equality";
    35 
    36 Goal "s=t ==> t=s";
    37 by (etac subst 1);
    38 by (rtac refl 1);
    39 qed "sym";
    40 
    41 (*calling "standard" reduces maxidx to 0*)
    42 bind_thm ("ssubst", sym RS subst);
    43 
    44 Goal "[| r=s; s=t |] ==> r=t";
    45 by (etac subst 1 THEN assume_tac 1);
    46 qed "trans";
    47 
    48 val prems = goal (the_context()) "(A == B) ==> A = B";
    49 by (rewrite_goals_tac prems);
    50 by (rtac refl 1);
    51 qed "def_imp_eq";
    52 
    53 (*Useful with eresolve_tac for proving equalties from known equalities.
    54         a = b
    55         |   |
    56         c = d   *)
    57 Goal "[| a=b;  a=c;  b=d |] ==> c=d";
    58 by (rtac trans 1);
    59 by (rtac trans 1);
    60 by (rtac sym 1);
    61 by (REPEAT (assume_tac 1)) ;
    62 qed "box_equals";
    63 
    64 
    65 section "Congruence rules for application";
    66 
    67 (*similar to AP_THM in Gordon's HOL*)
    68 Goal "(f::'a=>'b) = g ==> f(x)=g(x)";
    69 by (etac subst 1);
    70 by (rtac refl 1);
    71 qed "fun_cong";
    72 
    73 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    74 Goal "x=y ==> f(x)=f(y)";
    75 by (etac subst 1);
    76 by (rtac refl 1);
    77 qed "arg_cong";
    78 
    79 Goal "[| f = g; (x::'a) = y |] ==> f(x) = g(y)";
    80 by (etac subst 1);
    81 by (etac subst 1);
    82 by (rtac refl 1);
    83 qed "cong";
    84 
    85 
    86 section "Equality of booleans -- iff";
    87 
    88 val prems = Goal "[| P ==> Q;  Q ==> P |] ==> P=Q";
    89 by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
    90 qed "iffI";
    91 
    92 Goal "[| P=Q; Q |] ==> P";
    93 by (etac ssubst 1);
    94 by (assume_tac 1);
    95 qed "iffD2";
    96 
    97 Goal "[| Q; P=Q |] ==> P";
    98 by (etac iffD2 1);
    99 by (assume_tac 1);
   100 qed "rev_iffD2";
   101 
   102 bind_thm ("iffD1", sym RS iffD2);
   103 bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
   104 
   105 val [p1,p2] = Goal "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R";
   106 by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1));
   107 qed "iffE";
   108 
   109 
   110 section "True";
   111 
   112 Goalw [True_def] "True";
   113 by (rtac refl 1);
   114 qed "TrueI";
   115 
   116 Goal "P ==> P=True";
   117 by (REPEAT (ares_tac [iffI,TrueI] 1));
   118 qed "eqTrueI";
   119 
   120 Goal "P=True ==> P";
   121 by (etac iffD2 1);
   122 by (rtac TrueI 1);
   123 qed "eqTrueE";
   124 
   125 
   126 section "Universal quantifier";
   127 
   128 val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)";
   129 by (resolve_tac (prems RL [eqTrueI RS ext]) 1);
   130 qed "allI";
   131 
   132 Goalw [All_def] "ALL x::'a. P(x) ==> P(x)";
   133 by (rtac eqTrueE 1);
   134 by (etac fun_cong 1);
   135 qed "spec";
   136 
   137 val major::prems = Goal "[| ALL x. P(x);  P(x) ==> R |] ==> R";
   138 by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
   139 qed "allE";
   140 
   141 val prems = Goal
   142     "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
   143 by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
   144 qed "all_dupE";
   145 
   146 
   147 section "False";
   148 (*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
   149 
   150 Goalw [False_def] "False ==> P";
   151 by (etac spec 1);
   152 qed "FalseE";
   153 
   154 Goal "False=True ==> P";
   155 by (etac (eqTrueE RS FalseE) 1);
   156 qed "False_neq_True";
   157 
   158 
   159 section "Negation";
   160 
   161 val prems = Goalw [not_def] "(P ==> False) ==> ~P";
   162 by (rtac impI 1);
   163 by (eresolve_tac prems 1);
   164 qed "notI";
   165 
   166 Goal "False ~= True";
   167 by (rtac notI 1);
   168 by (etac False_neq_True 1);
   169 qed "False_not_True";
   170 
   171 Goal "True ~= False";
   172 by (rtac notI 1);
   173 by (dtac sym 1);
   174 by (etac False_neq_True 1);
   175 qed "True_not_False";
   176 
   177 Goalw [not_def] "[| ~P;  P |] ==> R";
   178 by (etac (mp RS FalseE) 1);
   179 by (assume_tac 1);
   180 qed "notE";
   181 
   182 (* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
   183 bind_thm ("notI2", notE RS notI);
   184 
   185 
   186 section "Implication";
   187 
   188 val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
   189 by (REPEAT (resolve_tac (prems@[mp]) 1));
   190 qed "impE";
   191 
   192 (* Reduces Q to P-->Q, allowing substitution in P. *)
   193 Goal "[| P;  P --> Q |] ==> Q";
   194 by (REPEAT (ares_tac [mp] 1)) ;
   195 qed "rev_mp";
   196 
   197 val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
   198 by (rtac (major RS notE RS notI) 1);
   199 by (etac minor 1) ;
   200 qed "contrapos_nn";
   201 
   202 (*not used at all, but we already have the other 3 combinations *)
   203 val [major,minor] = Goal "[| Q;  P ==> ~Q |] ==> ~P";
   204 by (rtac (minor RS notE RS notI) 1);
   205 by (assume_tac 1);
   206 by (rtac major 1) ;
   207 qed "contrapos_pn";
   208 
   209 Goal "t ~= s ==> s ~= t";
   210 by (etac contrapos_nn 1); 
   211 by (etac sym 1); 
   212 qed "not_sym";
   213 
   214 (*still used in HOLCF*)
   215 val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
   216 by (rtac (minor RS contrapos_nn) 1);
   217 by (etac major 1) ;
   218 qed "rev_contrapos";
   219 
   220 section "Existential quantifier";
   221 
   222 Goalw [Ex_def] "P x ==> EX x::'a. P x";
   223 by (rtac allI 1); 
   224 by (rtac impI 1); 
   225 by (etac allE 1); 
   226 by (etac mp 1) ;
   227 by (assume_tac 1); 
   228 qed "exI";
   229 
   230 val [major,minor] =
   231 Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
   232 by (rtac (major RS spec RS mp) 1); 
   233 by (rtac (impI RS allI) 1); 
   234 by (etac minor 1); 
   235 qed "exE";
   236 
   237 
   238 section "Conjunction";
   239 
   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";
   245 
   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";
   251 
   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";
   257 
   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";
   264 
   265 val prems =
   266 Goal "[| P; P ==> Q |] ==> P & Q";
   267 by (REPEAT (resolve_tac (conjI::prems) 1));
   268 qed "context_conjI";
   269 
   270 
   271 section "Disjunction";
   272 
   273 Goalw [or_def] "P ==> P|Q";
   274 by (REPEAT (resolve_tac [allI,impI] 1));
   275 by (etac mp 1 THEN assume_tac 1);
   276 qed "disjI1";
   277 
   278 Goalw [or_def] "Q ==> P|Q";
   279 by (REPEAT (resolve_tac [allI,impI] 1));
   280 by (etac mp 1 THEN assume_tac 1);
   281 qed "disjI2";
   282 
   283 val [major,minorP,minorQ] =
   284 Goalw [or_def]  "[| P | Q; P ==> R; Q ==> R |] ==> R";
   285 by (rtac (major RS spec RS mp RS mp) 1);
   286 by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1));
   287 qed "disjE";
   288 
   289 
   290 section "Classical logic";
   291 (*CCONTR -- classical logic*)
   292 
   293 val [prem] = Goal  "(~P ==> P) ==> P";
   294 by (rtac (True_or_False RS disjE RS eqTrueE) 1);
   295 by (assume_tac 1);
   296 by (rtac (notI RS prem RS eqTrueI) 1);
   297 by (etac subst 1);
   298 by (assume_tac 1);
   299 qed "classical";
   300 
   301 bind_thm ("ccontr", FalseE RS classical);
   302 
   303 (*notE with premises exchanged; it discharges ~R so that it can be used to
   304   make elimination rules*)
   305 val [premp,premnot] = Goal "[| P; ~R ==> ~P |] ==> R";
   306 by (rtac ccontr 1);
   307 by (etac ([premnot,premp] MRS notE) 1);
   308 qed "rev_notE";
   309 
   310 (*Double negation law*)
   311 Goal "~~P ==> P";
   312 by (rtac classical 1);
   313 by (etac notE 1);
   314 by (assume_tac 1);
   315 qed "notnotD";
   316 
   317 val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
   318 by (rtac classical 1);
   319 by (dtac p2 1);
   320 by (etac notE 1);
   321 by (rtac p1 1);
   322 qed "contrapos_pp";
   323 
   324 
   325 section "Unique existence";
   326 
   327 val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)";
   328 by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1));
   329 qed "ex1I";
   330 
   331 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   332 val [ex_prem,eq] = Goal
   333     "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
   334 by (rtac (ex_prem RS exE) 1);
   335 by (REPEAT (ares_tac [ex1I,eq] 1)) ;
   336 qed "ex_ex1I";
   337 
   338 val major::prems = Goalw [Ex1_def]
   339     "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R";
   340 by (rtac (major RS exE) 1);
   341 by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));
   342 qed "ex1E";
   343 
   344 Goal "EX! x. P x ==> EX x. P x";
   345 by (etac ex1E 1);
   346 by (rtac exI 1);
   347 by (assume_tac 1);
   348 qed "ex1_implies_ex";
   349 
   350 
   351 section "THE: definite description operator";
   352 
   353 val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";
   354 by (rtac trans 1); 
   355  by (rtac (thm "the_eq_trivial") 2);
   356 by (res_inst_tac [("f","The")] arg_cong 1); 
   357 by (rtac ext 1); 
   358  by (rtac iffI 1); 
   359 by (etac premx 1); 
   360 by (etac ssubst 1 THEN rtac prema 1);
   361 qed "the_equality";
   362 
   363 val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> P (THE x. P x)";
   364 by (rtac (the_equality RS ssubst) 1);
   365 by (REPEAT (ares_tac [prema,premx] 1));
   366 qed "theI";
   367 
   368 Goal "EX! x. P x ==> P (THE x. P x)";
   369 by (etac ex1E 1);
   370 by (etac theI 1);
   371 by (etac allE 1);
   372 by (etac mp 1);
   373 by (atac 1);
   374 qed "theI'";
   375 
   376 (*Easier to apply than theI: only one occurrence of P*)
   377 val [prema,premx,premq] = Goal
   378      "[| P a;  !!x. P x ==> x=a;  !!x. P x ==> Q x |] \
   379 \     ==> Q (THE x. P x)";
   380 by (rtac premq 1); 
   381 by (rtac theI 1); 
   382 by (REPEAT (ares_tac [prema,premx] 1));
   383 qed "theI2";
   384 
   385 Goal "[| EX!x. P x; P a |] ==> (THE x. P x) = a";
   386 by (rtac the_equality 1);
   387 by  (atac 1);
   388 by (etac ex1E 1);
   389 by (etac all_dupE 1);
   390 by (dtac mp 1);
   391 by  (atac 1);
   392 by (etac ssubst 1);
   393 by (etac allE 1);
   394 by (etac mp 1);
   395 by (atac 1);
   396 qed "the1_equality";
   397 
   398 Goal "(THE y. x=y) = x";
   399 by (rtac the_equality 1);
   400 by (rtac refl 1);
   401 by (etac sym 1);
   402 qed "the_sym_eq_trivial";
   403 
   404 
   405 section "Classical intro rules for disjunction and existential quantifiers";
   406 
   407 val prems = Goal "(~Q ==> P) ==> P|Q";
   408 by (rtac classical 1);
   409 by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
   410 by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
   411 qed "disjCI";
   412 
   413 Goal "~P | P";
   414 by (REPEAT (ares_tac [disjCI] 1)) ;
   415 qed "excluded_middle";
   416 
   417 (*For disjunctive case analysis*)
   418 fun excluded_middle_tac sP =
   419     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   420 
   421 (*Classical implies (-->) elimination. *)
   422 val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
   423 by (rtac (excluded_middle RS disjE) 1);
   424 by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
   425 qed "impCE";
   426 
   427 (*This version of --> elimination works on Q before P.  It works best for
   428   those cases in which P holds "almost everywhere".  Can't install as
   429   default: would break old proofs.*)
   430 val major::prems = Goal
   431     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
   432 by (resolve_tac [excluded_middle RS disjE] 1);
   433 by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
   434 qed "impCE'";
   435 
   436 (*Classical <-> elimination. *)
   437 val major::prems = Goal
   438     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
   439 by (rtac (major RS iffE) 1);
   440 by (REPEAT (DEPTH_SOLVE_1
   441             (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
   442 qed "iffCE";
   443 
   444 val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";
   445 by (rtac ccontr 1);
   446 by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
   447 qed "exCI";
   448 
   449 (* case distinction *)
   450 
   451 val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
   452 by (rtac (excluded_middle RS disjE) 1);
   453 by (etac prem2 1);
   454 by (etac prem1 1);
   455 qed "case_split_thm";
   456 
   457 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   458 
   459 
   460 (** Standard abbreviations **)
   461 
   462 (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   463 local
   464   fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
   465   |   wrong_prem (Bound _) = true
   466   |   wrong_prem _ = false;
   467   val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))));
   468 in
   469   fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
   470   fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
   471 end;
   472 
   473 
   474 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
   475