src/HOL/HOL.ML
author nipkow
Wed Sep 09 17:34:58 1998 +0200 (1998-09-09)
changeset 5447 df03d330aeab
parent 5346 bc9748ad8491
child 5760 7e2cf2820684
permissions -rw-r--r--
Proved and added rewrite rule (@x. x=y) = y to simpset.
Strange that only the symetric version was present!
     1 (*  Title:      HOL/HOL.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1991  University of Cambridge
     5 
     6 For HOL.thy
     7 Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68 
     8 *)
     9 
    10 open HOL;
    11 
    12 
    13 (** Equality **)
    14 section "=";
    15 
    16 qed_goal "sym" HOL.thy "s=t ==> t=s"
    17  (fn prems => [cut_facts_tac prems 1, etac subst 1, rtac refl 1]);
    18 
    19 (*calling "standard" reduces maxidx to 0*)
    20 bind_thm ("ssubst", (sym RS subst));
    21 
    22 qed_goal "trans" HOL.thy "[| r=s; s=t |] ==> r=t"
    23  (fn prems =>
    24         [rtac subst 1, resolve_tac prems 1, resolve_tac prems 1]);
    25 
    26 val prems = goal thy "(A == B) ==> A = B";
    27 by (rewrite_goals_tac prems);
    28 by (rtac refl 1);
    29 qed "def_imp_eq";
    30 
    31 (*Useful with eresolve_tac for proving equalties from known equalities.
    32         a = b
    33         |   |
    34         c = d   *)
    35 qed_goal "box_equals" HOL.thy
    36     "[| a=b;  a=c;  b=d |] ==> c=d"  
    37  (fn prems=>
    38   [ (rtac trans 1),
    39     (rtac trans 1),
    40     (rtac sym 1),
    41     (REPEAT (resolve_tac prems 1)) ]);
    42 
    43 
    44 (** Congruence rules for meta-application **)
    45 section "Congruence";
    46 
    47 (*similar to AP_THM in Gordon's HOL*)
    48 qed_goal "fun_cong" HOL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
    49   (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    50 
    51 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
    52 qed_goal "arg_cong" HOL.thy "x=y ==> f(x)=f(y)"
    53  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
    54 
    55 qed_goal "cong" HOL.thy
    56    "[| f = g; (x::'a) = y |] ==> f(x) = g(y)"
    57  (fn [prem1,prem2] =>
    58    [rtac (prem1 RS subst) 1, rtac (prem2 RS subst) 1, rtac refl 1]);
    59 
    60 
    61 (** Equality of booleans -- iff **)
    62 section "iff";
    63 
    64 qed_goal "iffI" HOL.thy
    65    "[| P ==> Q;  Q ==> P |] ==> P=Q"
    66  (fn prems=> [ (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1)) ]);
    67 
    68 qed_goal "iffD2" HOL.thy "[| P=Q; Q |] ==> P"
    69  (fn prems =>
    70         [rtac ssubst 1, resolve_tac prems 1, resolve_tac prems 1]);
    71 
    72 qed_goal "rev_iffD2" HOL.thy "!!P. [| Q; P=Q |] ==> P"
    73  (fn _ => [etac iffD2 1, assume_tac 1]);
    74 
    75 bind_thm ("iffD1", sym RS iffD2);
    76 bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
    77 
    78 qed_goal "iffE" HOL.thy
    79     "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R"
    80  (fn [p1,p2] => [REPEAT(ares_tac([p1 RS iffD2, p1 RS iffD1, p2, impI])1)]);
    81 
    82 
    83 (** True **)
    84 section "True";
    85 
    86 qed_goalw "TrueI" HOL.thy [True_def] "True"
    87   (fn _ => [rtac refl 1]);
    88 
    89 qed_goal "eqTrueI" HOL.thy "P ==> P=True" 
    90  (fn prems => [REPEAT(resolve_tac ([iffI,TrueI]@prems) 1)]);
    91 
    92 qed_goal "eqTrueE" HOL.thy "P=True ==> P" 
    93  (fn prems => [REPEAT(resolve_tac (prems@[TrueI,iffD2]) 1)]);
    94 
    95 
    96 (** Universal quantifier **)
    97 section "!";
    98 
    99 qed_goalw "allI" HOL.thy [All_def] "(!!x::'a. P(x)) ==> !x. P(x)"
   100  (fn prems => [resolve_tac (prems RL [eqTrueI RS ext]) 1]);
   101 
   102 qed_goalw "spec" HOL.thy [All_def] "! x::'a. P(x) ==> P(x)"
   103  (fn prems => [rtac eqTrueE 1, resolve_tac (prems RL [fun_cong]) 1]);
   104 
   105 qed_goal "allE" HOL.thy "[| !x. P(x);  P(x) ==> R |] ==> R"
   106  (fn major::prems=>
   107   [ (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ]);
   108 
   109 qed_goal "all_dupE" HOL.thy 
   110     "[| ! x. P(x);  [| P(x); ! x. P(x) |] ==> R |] ==> R"
   111  (fn prems =>
   112   [ (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ]);
   113 
   114 
   115 (** False ** Depends upon spec; it is impossible to do propositional logic
   116              before quantifiers! **)
   117 section "False";
   118 
   119 qed_goalw "FalseE" HOL.thy [False_def] "False ==> P"
   120  (fn [major] => [rtac (major RS spec) 1]);
   121 
   122 qed_goal "False_neq_True" HOL.thy "False=True ==> P"
   123  (fn [prem] => [rtac (prem RS eqTrueE RS FalseE) 1]);
   124 
   125 
   126 (** Negation **)
   127 section "~";
   128 
   129 qed_goalw "notI" HOL.thy [not_def] "(P ==> False) ==> ~P"
   130  (fn prems=> [rtac impI 1, eresolve_tac prems 1]);
   131 
   132 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
   133  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
   134 
   135 bind_thm ("classical2", notE RS notI);
   136 
   137 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
   138  (fn _ => [REPEAT (ares_tac [notE] 1)]);
   139 
   140 
   141 (** Implication **)
   142 section "-->";
   143 
   144 qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
   145  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   146 
   147 (* Reduces Q to P-->Q, allowing substitution in P. *)
   148 qed_goal "rev_mp" HOL.thy "[| P;  P --> Q |] ==> Q"
   149  (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   150 
   151 qed_goal "contrapos" HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
   152  (fn [major,minor]=> 
   153   [ (rtac (major RS notE RS notI) 1), 
   154     (etac minor 1) ]);
   155 
   156 qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
   157  (fn [major,minor]=> 
   158   [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
   159 
   160 (* ~(?t = ?s) ==> ~(?s = ?t) *)
   161 bind_thm("not_sym", sym COMP rev_contrapos);
   162 
   163 
   164 (** Existential quantifier **)
   165 section "?";
   166 
   167 qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
   168  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
   169 
   170 qed_goalw "exE" HOL.thy [Ex_def]
   171   "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
   172   (fn prems => [REPEAT(resolve_tac prems 1)]);
   173 
   174 
   175 (** Conjunction **)
   176 section "&";
   177 
   178 qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
   179  (fn prems =>
   180   [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
   181 
   182 qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
   183  (fn prems =>
   184    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   185 
   186 qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
   187  (fn prems =>
   188    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   189 
   190 qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
   191  (fn prems =>
   192          [cut_facts_tac prems 1, resolve_tac prems 1,
   193           etac conjunct1 1, etac conjunct2 1]);
   194 
   195 
   196 (** Disjunction *)
   197 section "|";
   198 
   199 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
   200  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   201 
   202 qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
   203  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   204 
   205 qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
   206  (fn [a1,a2,a3] =>
   207         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
   208          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
   209 
   210 
   211 (** CCONTR -- classical logic **)
   212 section "classical logic";
   213 
   214 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
   215  (fn [prem] =>
   216    [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
   217     rtac (impI RS prem RS eqTrueI) 1,
   218     etac subst 1,  assume_tac 1]);
   219 
   220 val ccontr = FalseE RS classical;
   221 
   222 (*Double negation law*)
   223 qed_goal "notnotD" HOL.thy "~~P ==> P"
   224  (fn [major]=>
   225   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
   226 
   227 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
   228         rtac classical 1,
   229         dtac p2 1,
   230         etac notE 1,
   231         rtac p1 1]);
   232 
   233 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
   234         rtac notI 1,
   235         dtac p2 1,
   236         etac notE 1,
   237         rtac p1 1]);
   238 
   239 (** Unique existence **)
   240 section "?!";
   241 
   242 qed_goalw "ex1I" HOL.thy [Ex1_def]
   243             "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
   244  (fn prems =>
   245   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
   246 
   247 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   248 qed_goal "ex_ex1I" HOL.thy
   249     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
   250  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   251                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   252 
   253 qed_goalw "ex1E" HOL.thy [Ex1_def]
   254     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   255  (fn major::prems =>
   256   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
   257 
   258 Goal "?! x. P x ==> ? x. P x";
   259 by (etac ex1E 1);
   260 by (rtac exI 1);
   261 by (assume_tac 1);
   262 qed "ex1_implies_ex";
   263 
   264 
   265 (** Select: Hilbert's Epsilon-operator **)
   266 section "@";
   267 
   268 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
   269 qed_goal "selectI2" HOL.thy
   270     "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
   271  (fn prems => [ resolve_tac prems 1, 
   272                 rtac selectI 1, 
   273                 resolve_tac prems 1 ]);
   274 
   275 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
   276 qed_goal "selectI2EX" HOL.thy
   277   "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
   278 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
   279 
   280 qed_goal "select_equality" HOL.thy
   281     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
   282  (fn prems => [ rtac selectI2 1, 
   283                 REPEAT (ares_tac prems 1) ]);
   284 
   285 qed_goalw "select1_equality" HOL.thy [Ex1_def]
   286   "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
   287 	  rtac select_equality 1, atac 1,
   288           etac exE 1, etac conjE 1,
   289           rtac allE 1, atac 1,
   290           etac impE 1, atac 1, etac ssubst 1,
   291           etac allE 1, etac impE 1, atac 1, etac ssubst 1,
   292           rtac refl 1]);
   293 
   294 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
   295         rtac iffI 1,
   296         etac exI 1,
   297         etac exE 1,
   298         etac selectI 1]);
   299 
   300 qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
   301 	rtac select_equality 1,
   302 	rtac refl 1,
   303 	atac 1]);
   304 
   305 qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
   306 	rtac select_equality 1,
   307 	rtac refl 1,
   308 	etac sym 1]);
   309 
   310 (** Classical intro rules for disjunction and existential quantifiers *)
   311 section "classical intro rules";
   312 
   313 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
   314  (fn prems=>
   315   [ (rtac classical 1),
   316     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   317     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   318 
   319 qed_goal "excluded_middle" HOL.thy "~P | P"
   320  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
   321 
   322 (*For disjunctive case analysis*)
   323 fun excluded_middle_tac sP =
   324     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   325 
   326 (*Classical implies (-->) elimination. *)
   327 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" 
   328  (fn major::prems=>
   329   [ rtac (excluded_middle RS disjE) 1,
   330     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
   331 
   332 (*This version of --> elimination works on Q before P.  It works best for
   333   those cases in which P holds "almost everywhere".  Can't install as
   334   default: would break old proofs.*)
   335 qed_goal "impCE'" thy 
   336     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
   337  (fn major::prems=>
   338   [ (resolve_tac [excluded_middle RS disjE] 1),
   339     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
   340 
   341 (*Classical <-> elimination. *)
   342 qed_goal "iffCE" HOL.thy
   343     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
   344  (fn major::prems =>
   345   [ (rtac (major RS iffE) 1),
   346     (REPEAT (DEPTH_SOLVE_1 
   347         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
   348 
   349 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
   350  (fn prems=>
   351   [ (rtac ccontr 1),
   352     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
   353 
   354 
   355 (* case distinction *)
   356 
   357 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
   358   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
   359                   etac p2 1, etac p1 1]);
   360 
   361 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   362 
   363 
   364 (** Standard abbreviations **)
   365 
   366 (*Apply an equality or definition ONCE.
   367   Fails unless the substitution has an effect*)
   368 fun stac th = 
   369   let val th' = th RS def_imp_eq handle _ => th
   370   in  CHANGED_GOAL (rtac (th' RS ssubst))
   371   end;
   372 
   373 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   374 
   375 
   376 (** strip ! and --> from proved goal while preserving !-bound var names **)
   377 
   378 local
   379 
   380 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   381 val myspec = read_instantiate [("P","?XXX")] spec;
   382 val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   383 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
   384 val aspec = forall_intr cvx myspec;
   385 
   386 in
   387 
   388 fun RSspec th =
   389   (case concl_of th of
   390      _ $ (Const("All",_) $ Abs(a,_,_)) =>
   391          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
   392          in th RS forall_elim ca aspec end
   393   | _ => raise THM("RSspec",0,[th]));
   394 
   395 fun RSmp th =
   396   (case concl_of th of
   397      _ $ (Const("op -->",_)$_$_) => th RS mp
   398   | _ => raise THM("RSmp",0,[th]));
   399 
   400 fun normalize_thm funs =
   401   let fun trans [] th = th
   402 	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   403   in zero_var_indexes o trans funs end;
   404 
   405 fun qed_spec_mp name =
   406   let val thm = normalize_thm [RSspec,RSmp] (result())
   407   in ml_store_thm(name, thm) end;
   408 
   409 fun qed_goal_spec_mp name thy s p = 
   410 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   411 
   412 fun qed_goalw_spec_mp name thy defs s p = 
   413 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   414 
   415 end;