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