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