src/HOL/HOL.ML
author paulson
Thu Aug 13 17:28:52 1998 +0200 (1998-08-13)
changeset 5309 01c2b317da88
parent 5299 d15a4155b96b
child 5346 bc9748ad8491
permissions -rw-r--r--
stac now handles definitions as well as equalities
     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 "(Eps (op = x)) = x" (K [
   301 	rtac select_equality 1,
   302 	rtac refl 1,
   303 	etac sym 1]);
   304 
   305 (** Classical intro rules for disjunction and existential quantifiers *)
   306 section "classical intro rules";
   307 
   308 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
   309  (fn prems=>
   310   [ (rtac classical 1),
   311     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   312     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   313 
   314 qed_goal "excluded_middle" HOL.thy "~P | P"
   315  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
   316 
   317 (*For disjunctive case analysis*)
   318 fun excluded_middle_tac sP =
   319     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   320 
   321 (*Classical implies (-->) elimination. *)
   322 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" 
   323  (fn major::prems=>
   324   [ rtac (excluded_middle RS disjE) 1,
   325     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
   326 
   327 (*This version of --> elimination works on Q before P.  It works best for
   328   those cases in which P holds "almost everywhere".  Can't install as
   329   default: would break old proofs.*)
   330 qed_goal "impCE'" thy 
   331     "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R"
   332  (fn major::prems=>
   333   [ (resolve_tac [excluded_middle RS disjE] 1),
   334     (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ]);
   335 
   336 (*Classical <-> elimination. *)
   337 qed_goal "iffCE" HOL.thy
   338     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
   339  (fn major::prems =>
   340   [ (rtac (major RS iffE) 1),
   341     (REPEAT (DEPTH_SOLVE_1 
   342         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
   343 
   344 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x. P(x)"
   345  (fn prems=>
   346   [ (rtac ccontr 1),
   347     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
   348 
   349 
   350 (* case distinction *)
   351 
   352 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
   353   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
   354                   etac p2 1, etac p1 1]);
   355 
   356 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   357 
   358 
   359 (** Standard abbreviations **)
   360 
   361 (*Apply an equality or definition ONCE.
   362   Fails unless the substitution has an effect*)
   363 fun stac th = 
   364   let val th' = th RS def_imp_eq handle _ => th
   365   in  CHANGED_GOAL (rtac (th' RS ssubst))
   366   end;
   367 
   368 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   369 
   370 
   371 (** strip ! and --> from proved goal while preserving !-bound var names **)
   372 
   373 local
   374 
   375 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   376 val myspec = read_instantiate [("P","?XXX")] spec;
   377 val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   378 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
   379 val aspec = forall_intr cvx myspec;
   380 
   381 in
   382 
   383 fun RSspec th =
   384   (case concl_of th of
   385      _ $ (Const("All",_) $ Abs(a,_,_)) =>
   386          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
   387          in th RS forall_elim ca aspec end
   388   | _ => raise THM("RSspec",0,[th]));
   389 
   390 fun RSmp th =
   391   (case concl_of th of
   392      _ $ (Const("op -->",_)$_$_) => th RS mp
   393   | _ => raise THM("RSmp",0,[th]));
   394 
   395 fun normalize_thm funs =
   396 let fun trans [] th = th
   397       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   398 in trans funs end;
   399 
   400 fun qed_spec_mp name =
   401   let val thm = normalize_thm [RSspec,RSmp] (result())
   402   in bind_thm(name, thm) end;
   403 
   404 fun qed_goal_spec_mp name thy s p = 
   405 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   406 
   407 fun qed_goalw_spec_mp name thy defs s p = 
   408 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   409 
   410 end;