src/HOL/HOL.ML
author berghofe
Fri Oct 23 22:36:15 1998 +0200 (1998-10-23)
changeset 5760 7e2cf2820684
parent 5447 df03d330aeab
child 5809 bacf85370ce0
permissions -rw-r--r--
Added theorems True_not_False and False_not_True
(for rep_datatype).
     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_goal "False_not_True" HOL.thy "False ~= True"
   133   (K [rtac notI 1, etac False_neq_True 1]);
   134 
   135 qed_goal "True_not_False" HOL.thy "True ~= False"
   136   (K [rtac notI 1, dtac sym 1, etac False_neq_True 1]);
   137 
   138 qed_goalw "notE" HOL.thy [not_def] "[| ~P;  P |] ==> R"
   139  (fn prems => [rtac (prems MRS mp RS FalseE) 1]);
   140 
   141 bind_thm ("classical2", notE RS notI);
   142 
   143 qed_goal "rev_notE" HOL.thy "!!P R. [| P; ~P |] ==> R"
   144  (fn _ => [REPEAT (ares_tac [notE] 1)]);
   145 
   146 
   147 (** Implication **)
   148 section "-->";
   149 
   150 qed_goal "impE" HOL.thy "[| P-->Q;  P;  Q ==> R |] ==> R"
   151  (fn prems=> [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   152 
   153 (* Reduces Q to P-->Q, allowing substitution in P. *)
   154 qed_goal "rev_mp" HOL.thy "[| P;  P --> Q |] ==> Q"
   155  (fn prems=>  [ (REPEAT (resolve_tac (prems@[mp]) 1)) ]);
   156 
   157 qed_goal "contrapos" HOL.thy "[| ~Q;  P==>Q |] ==> ~P"
   158  (fn [major,minor]=> 
   159   [ (rtac (major RS notE RS notI) 1), 
   160     (etac minor 1) ]);
   161 
   162 qed_goal "rev_contrapos" HOL.thy "[| P==>Q; ~Q |] ==> ~P"
   163  (fn [major,minor]=> 
   164   [ (rtac (minor RS contrapos) 1), (etac major 1) ]);
   165 
   166 (* ~(?t = ?s) ==> ~(?s = ?t) *)
   167 bind_thm("not_sym", sym COMP rev_contrapos);
   168 
   169 
   170 (** Existential quantifier **)
   171 section "?";
   172 
   173 qed_goalw "exI" HOL.thy [Ex_def] "P x ==> ? x::'a. P x"
   174  (fn prems => [rtac selectI 1, resolve_tac prems 1]);
   175 
   176 qed_goalw "exE" HOL.thy [Ex_def]
   177   "[| ? x::'a. P(x); !!x. P(x) ==> Q |] ==> Q"
   178   (fn prems => [REPEAT(resolve_tac prems 1)]);
   179 
   180 
   181 (** Conjunction **)
   182 section "&";
   183 
   184 qed_goalw "conjI" HOL.thy [and_def] "[| P; Q |] ==> P&Q"
   185  (fn prems =>
   186   [REPEAT (resolve_tac (prems@[allI,impI]) 1 ORELSE etac (mp RS mp) 1)]);
   187 
   188 qed_goalw "conjunct1" HOL.thy [and_def] "[| P & Q |] ==> P"
   189  (fn prems =>
   190    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   191 
   192 qed_goalw "conjunct2" HOL.thy [and_def] "[| P & Q |] ==> Q"
   193  (fn prems =>
   194    [resolve_tac (prems RL [spec] RL [mp]) 1, REPEAT(ares_tac [impI] 1)]);
   195 
   196 qed_goal "conjE" HOL.thy "[| P&Q;  [| P; Q |] ==> R |] ==> R"
   197  (fn prems =>
   198          [cut_facts_tac prems 1, resolve_tac prems 1,
   199           etac conjunct1 1, etac conjunct2 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 _ => 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 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;