src/HOL/HOL.ML
author nipkow
Sun Aug 10 12:28:34 1997 +0200 (1997-08-10)
changeset 3646 a11338a5d2d4
parent 3621 d3e248853428
child 3842 b55686a7b22c
permissions -rw-r--r--
Added select1_equality
     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"
   272 (fn _ => [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)" (fn prems => [
   280         rtac iffI 1,
   281         etac exI 1,
   282         etac exE 1,
   283         etac selectI 1]);
   284 
   285 
   286 (** Classical intro rules for disjunction and existential quantifiers *)
   287 section "classical intro rules";
   288 
   289 qed_goal "disjCI" HOL.thy "(~Q ==> P) ==> P|Q"
   290  (fn prems=>
   291   [ (rtac classical 1),
   292     (REPEAT (ares_tac (prems@[disjI1,notI]) 1)),
   293     (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ]);
   294 
   295 qed_goal "excluded_middle" HOL.thy "~P | P"
   296  (fn _ => [ (REPEAT (ares_tac [disjCI] 1)) ]);
   297 
   298 (*For disjunctive case analysis*)
   299 fun excluded_middle_tac sP =
   300     res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
   301 
   302 (*Classical implies (-->) elimination. *)
   303 qed_goal "impCE" HOL.thy "[| P-->Q; ~P ==> R; Q ==> R |] ==> R" 
   304  (fn major::prems=>
   305   [ rtac (excluded_middle RS disjE) 1,
   306     REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1))]);
   307 
   308 (*Classical <-> elimination. *)
   309 qed_goal "iffCE" HOL.thy
   310     "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R"
   311  (fn major::prems =>
   312   [ (rtac (major RS iffE) 1),
   313     (REPEAT (DEPTH_SOLVE_1 
   314         (eresolve_tac ([asm_rl,impCE,notE]@prems) 1))) ]);
   315 
   316 qed_goal "exCI" HOL.thy "(! x. ~P(x) ==> P(a)) ==> ? x.P(x)"
   317  (fn prems=>
   318   [ (rtac ccontr 1),
   319     (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ]);
   320 
   321 
   322 (* case distinction *)
   323 
   324 qed_goal "case_split_thm" HOL.thy "[| P ==> Q; ~P ==> Q |] ==> Q"
   325   (fn [p1,p2] => [cut_facts_tac [excluded_middle] 1, etac disjE 1,
   326                   etac p2 1, etac p1 1]);
   327 
   328 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
   329 
   330 
   331 (** Standard abbreviations **)
   332 
   333 fun stac th = CHANGED o rtac (th RS ssubst);
   334 fun strip_tac i = REPEAT(resolve_tac [impI,allI] i); 
   335 
   336 
   337 (** strip ! and --> from proved goal while preserving !-bound var names **)
   338 
   339 local
   340 
   341 (* Use XXX to avoid forall_intr failing because of duplicate variable name *)
   342 val myspec = read_instantiate [("P","?XXX")] spec;
   343 val _ $ (_ $ (vx as Var(_,vxT))) = concl_of myspec;
   344 val cvx = cterm_of (#sign(rep_thm myspec)) vx;
   345 val aspec = forall_intr cvx myspec;
   346 
   347 in
   348 
   349 fun RSspec th =
   350   (case concl_of th of
   351      _ $ (Const("All",_) $ Abs(a,_,_)) =>
   352          let val ca = cterm_of (#sign(rep_thm th)) (Var((a,0),vxT))
   353          in th RS forall_elim ca aspec end
   354   | _ => raise THM("RSspec",0,[th]));
   355 
   356 fun RSmp th =
   357   (case concl_of th of
   358      _ $ (Const("op -->",_)$_$_) => th RS mp
   359   | _ => raise THM("RSmp",0,[th]));
   360 
   361 fun normalize_thm funs =
   362 let fun trans [] th = th
   363       | trans (f::fs) th = (trans funs (f th)) handle THM _ => trans fs th
   364 in trans funs end;
   365 
   366 fun qed_spec_mp name =
   367   let val thm = normalize_thm [RSspec,RSmp] (result())
   368   in bind_thm(name, thm) end;
   369 
   370 fun qed_goal_spec_mp name thy s p = 
   371 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goal thy s p));
   372 
   373 fun qed_goalw_spec_mp name thy defs s p = 
   374 	bind_thm (name, normalize_thm [RSspec,RSmp] (prove_goalw thy defs s p));
   375 
   376 end;
   377 
   378 
   379 (*Thus, assignments to the references claset and simpset are recorded
   380   with theory "HOL".  These files cannot be loaded directly in ROOT.ML.*)
   381 use "hologic.ML";
   382 use "cladata.ML";
   383 use "simpdata.ML";