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