src/HOL/HOL.ML
author wenzelm
Sat Jul 10 21:48:27 1999 +0200 (1999-07-10)
changeset 6968 7f2977e96a5c
parent 6513 e0a9459e99fc
child 7030 53934985426a
permissions -rw-r--r--
handle THM/TERM exn;
     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 qed_goal "context_conjI" HOL.thy  "[| P; P ==> Q |] ==> P & Q"
   199  (fn prems => [REPEAT(resolve_tac (conjI::prems) 1)]);
   200 
   201 
   202 (** Disjunction *)
   203 section "|";
   204 
   205 qed_goalw "disjI1" HOL.thy [or_def] "P ==> P|Q"
   206  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   207 
   208 qed_goalw "disjI2" HOL.thy [or_def] "Q ==> P|Q"
   209  (fn [prem] => [REPEAT(ares_tac [allI,impI, prem RSN (2,mp)] 1)]);
   210 
   211 qed_goalw "disjE" HOL.thy [or_def] "[| P | Q; P ==> R; Q ==> R |] ==> R"
   212  (fn [a1,a2,a3] =>
   213         [rtac (mp RS mp) 1, rtac spec 1, rtac a1 1,
   214          rtac (a2 RS impI) 1, assume_tac 1, rtac (a3 RS impI) 1, assume_tac 1]);
   215 
   216 
   217 (** CCONTR -- classical logic **)
   218 section "classical logic";
   219 
   220 qed_goalw "classical" HOL.thy [not_def]  "(~P ==> P) ==> P"
   221  (fn [prem] =>
   222    [rtac (True_or_False RS (disjE RS eqTrueE)) 1,  assume_tac 1,
   223     rtac (impI RS prem RS eqTrueI) 1,
   224     etac subst 1,  assume_tac 1]);
   225 
   226 val ccontr = FalseE RS classical;
   227 
   228 (*Double negation law*)
   229 qed_goal "notnotD" HOL.thy "~~P ==> P"
   230  (fn [major]=>
   231   [ (rtac classical 1), (eresolve_tac [major RS notE] 1) ]);
   232 
   233 qed_goal "contrapos2" HOL.thy "[| Q; ~ P ==> ~ Q |] ==> P" (fn [p1,p2] => [
   234         rtac classical 1,
   235         dtac p2 1,
   236         etac notE 1,
   237         rtac p1 1]);
   238 
   239 qed_goal "swap2" HOL.thy "[| P;  Q ==> ~ P |] ==> ~ Q" (fn [p1,p2] => [
   240         rtac notI 1,
   241         dtac p2 1,
   242         etac notE 1,
   243         rtac p1 1]);
   244 
   245 (** Unique existence **)
   246 section "?!";
   247 
   248 qed_goalw "ex1I" HOL.thy [Ex1_def]
   249             "[| P(a);  !!x. P(x) ==> x=a |] ==> ?! x. P(x)"
   250  (fn prems =>
   251   [REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1)]);
   252 
   253 (*Sometimes easier to use: the premises have no shared variables.  Safe!*)
   254 qed_goal "ex_ex1I" HOL.thy
   255     "[| ? x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> ?! x. P(x)"
   256  (fn [ex,eq] => [ (rtac (ex RS exE) 1),
   257                   (REPEAT (ares_tac [ex1I,eq] 1)) ]);
   258 
   259 qed_goalw "ex1E" HOL.thy [Ex1_def]
   260     "[| ?! x. P(x);  !!x. [| P(x);  ! y. P(y) --> y=x |] ==> R |] ==> R"
   261  (fn major::prems =>
   262   [rtac (major RS exE) 1, REPEAT (etac conjE 1 ORELSE ares_tac prems 1)]);
   263 
   264 Goal "?! x. P x ==> ? x. P x";
   265 by (etac ex1E 1);
   266 by (rtac exI 1);
   267 by (assume_tac 1);
   268 qed "ex1_implies_ex";
   269 
   270 
   271 (** Select: Hilbert's Epsilon-operator **)
   272 section "@";
   273 
   274 (*Easier to apply than selectI: conclusion has only one occurrence of P*)
   275 qed_goal "selectI2" HOL.thy
   276     "[| P a;  !!x. P x ==> Q x |] ==> Q (@x. P x)"
   277  (fn prems => [ resolve_tac prems 1, 
   278                 rtac selectI 1, 
   279                 resolve_tac prems 1 ]);
   280 
   281 (*Easier to apply than selectI2 if witness ?a comes from an EX-formula*)
   282 qed_goal "selectI2EX" HOL.thy
   283   "[| ? a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"
   284 (fn [major,minor] => [rtac (major RS exE) 1, etac selectI2 1, etac minor 1]);
   285 
   286 qed_goal "select_equality" HOL.thy
   287     "[| P a;  !!x. P x ==> x=a |] ==> (@x. P x) = a"
   288  (fn prems => [ rtac selectI2 1, 
   289                 REPEAT (ares_tac prems 1) ]);
   290 
   291 qed_goalw "select1_equality" HOL.thy [Ex1_def]
   292   "!!P. [| ?!x. P x; P a |] ==> (@x. P x) = a" (K [
   293 	  rtac select_equality 1, atac 1,
   294           etac exE 1, etac conjE 1,
   295           rtac allE 1, atac 1,
   296           etac impE 1, atac 1, etac ssubst 1,
   297           etac allE 1, etac impE 1, atac 1, etac ssubst 1,
   298           rtac refl 1]);
   299 
   300 qed_goal "select_eq_Ex" HOL.thy "P (@ x. P x) =  (? x. P x)" (K [
   301         rtac iffI 1,
   302         etac exI 1,
   303         etac exE 1,
   304         etac selectI 1]);
   305 
   306 qed_goal "Eps_eq" HOL.thy "(@y. y=x) = x" (K [
   307 	rtac select_equality 1,
   308 	rtac refl 1,
   309 	atac 1]);
   310 
   311 qed_goal "Eps_sym_eq" HOL.thy "(Eps (op = x)) = x" (K [
   312 	rtac select_equality 1,
   313 	rtac refl 1,
   314 	etac sym 1]);
   315 
   316 (** Classical intro rules for disjunction and existential quantifiers *)
   317 section "classical intro rules";
   318 
   319 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
   320  (fn prems=>
   321   [ (rtac classical 1),
   322     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   323     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   324 
   325 qed_goal "excluded_middle" HOL.thy "~P | P"
   326  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
   327 
   328 (*For disjunctive case analysis*)
   329 fun excluded_middle_tac sP =
   330     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   331 
   332 (*Classical implies (-->) elimination. *)
   333 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" 
   334  (fn major::prems=>
   335   [ rtac (excluded_middle RS disjE) 1,
   336     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
   337 
   338 (*This version of --> elimination works on Q before P.  It works best for
   339   those cases in which P holds "almost everywhere".  Can't install as
   340   default: would break old proofs.*)
   341 qed_goal "impCE'" thy 
   342     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
   343  (fn major::prems=>
   344   [ (resolve_tac [excluded_middle RS disjE] 1),
   345     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
   346 
   347 (*Classical <-> elimination. *)
   348 qed_goal "iffCE" HOL.thy
   349     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
   350  (fn major::prems =>
   351   [ (rtac (major RS iffE) 1),
   352     (REPEAT (DEPTH_SOLVE_1 
   353         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
   354 
   355 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
   356  (fn prems=>
   357   [ (rtac ccontr 1),
   358     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
   359 
   360 
   361 (* case distinction *)
   362 
   363 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
   364   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
   365                   etac p2 1, etac p1 1]);
   366 
   367 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   368 
   369 
   370 (** Standard abbreviations **)
   371 
   372 (*Apply an equality or definition ONCE.
   373   Fails unless the substitution has an effect*)
   374 fun stac th = 
   375   let val th' = th RS def_imp_eq handle THM _ => th
   376   in  CHANGED_GOAL (rtac (th' RS ssubst))
   377   end;
   378 
   379 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   380 
   381 
   382 (** strip ! and --> from proved goal while preserving !-bound var names **)
   383 
   384 local
   385 
   386 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   387 val myspec = read_instantiate [("P","?XXX")] spec;
   388 val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   389 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
   390 val aspec = forall_intr cvx myspec;
   391 
   392 in
   393 
   394 fun RSspec th =
   395   (case concl_of th of
   396      _ $ (Const("All",_) $ Abs(a,_,_)) =>
   397          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
   398          in th RS forall_elim ca aspec end
   399   | _ => raise THM("RSspec",0,[th]));
   400 
   401 fun RSmp th =
   402   (case concl_of th of
   403      _ $ (Const("op -->",_)$_$_) => th RS mp
   404   | _ => raise THM("RSmp",0,[th]));
   405 
   406 fun normalize_thm funs =
   407   let fun trans [] th = th
   408 	| trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   409   in zero_var_indexes o trans funs end;
   410 
   411 fun qed_spec_mp name =
   412   let val thm = normalize_thm [RSspec,RSmp] (result())
   413   in ThmDatabase.ml_store_thm(name, thm) end;
   414 
   415 fun qed_goal_spec_mp name thy s p = 
   416 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   417 
   418 fun qed_goalw_spec_mp name thy defs s p = 
   419 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   420 
   421 end;
   422 
   423 
   424 (* attributes *)
   425 
   426 local
   427 
   428 fun gen_rulify x = Attrib.no_args (Drule.rule_attribute (K (normalize_thm [RSspec, RSmp]))) x;
   429 
   430 in
   431 
   432 val hol_setup =
   433  [Attrib.add_attributes
   434   [("rulify", (gen_rulify, gen_rulify), "put theorem into standard rule form")]];
   435 
   436 end;