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