src/HOL/HOL_lemmas.ML
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 14430 5cb24165a2e1
permissions -rw-r--r--
import -> imports
wenzelm@7357
     1
(*  Title:      HOL/HOL_lemmas.ML
wenzelm@7357
     2
    ID:         $Id$
wenzelm@7357
     3
    Author:     Tobias Nipkow
wenzelm@7357
     4
    Copyright   1991  University of Cambridge
wenzelm@7357
     5
wenzelm@7357
     6
Derived rules from Appendix of Mike Gordons HOL Report, Cambridge TR 68.
wenzelm@7357
     7
*)
wenzelm@7357
     8
wenzelm@11973
     9
(* legacy ML bindings *)
wenzelm@7357
    10
wenzelm@7357
    11
val plusI = thm "plusI";
wenzelm@7357
    12
val minusI = thm "minusI";
wenzelm@7357
    13
val timesI = thm "timesI";
wenzelm@7357
    14
val eq_reflection = thm "eq_reflection";
wenzelm@7357
    15
val refl = thm "refl";
wenzelm@7357
    16
val subst = thm "subst";
wenzelm@7357
    17
val ext = thm "ext";
wenzelm@7357
    18
val impI = thm "impI";
wenzelm@7357
    19
val mp = thm "mp";
wenzelm@7357
    20
val True_def = thm "True_def";
wenzelm@7357
    21
val All_def = thm "All_def";
wenzelm@7357
    22
val Ex_def = thm "Ex_def";
wenzelm@7357
    23
val False_def = thm "False_def";
wenzelm@7357
    24
val not_def = thm "not_def";
wenzelm@7357
    25
val and_def = thm "and_def";
wenzelm@7357
    26
val or_def = thm "or_def";
wenzelm@7357
    27
val Ex1_def = thm "Ex1_def";
wenzelm@7357
    28
val iff = thm "iff";
wenzelm@7357
    29
val True_or_False = thm "True_or_False";
wenzelm@7357
    30
val Let_def = thm "Let_def";
wenzelm@7357
    31
val if_def = thm "if_def";
wenzelm@7357
    32
wenzelm@7357
    33
wenzelm@10063
    34
section "Equality";
wenzelm@7357
    35
paulson@7618
    36
Goal "s=t ==> t=s";
paulson@7618
    37
by (etac subst 1);
paulson@7618
    38
by (rtac refl 1);
paulson@7618
    39
qed "sym";
wenzelm@7357
    40
wenzelm@7357
    41
(*calling "standard" reduces maxidx to 0*)
paulson@7618
    42
bind_thm ("ssubst", sym RS subst);
wenzelm@7357
    43
paulson@7618
    44
Goal "[| r=s; s=t |] ==> r=t";
paulson@7618
    45
by (etac subst 1 THEN assume_tac 1);
paulson@7618
    46
qed "trans";
wenzelm@7357
    47
paulson@9969
    48
val prems = goal (the_context()) "(A == B) ==> A = B";
wenzelm@7357
    49
by (rewrite_goals_tac prems);
wenzelm@7357
    50
by (rtac refl 1);
wenzelm@7357
    51
qed "def_imp_eq";
wenzelm@7357
    52
wenzelm@7357
    53
(*Useful with eresolve_tac for proving equalties from known equalities.
wenzelm@7357
    54
        a = b
wenzelm@7357
    55
        |   |
wenzelm@7357
    56
        c = d   *)
wenzelm@7357
    57
Goal "[| a=b;  a=c;  b=d |] ==> c=d";
wenzelm@7357
    58
by (rtac trans 1);
wenzelm@7357
    59
by (rtac trans 1);
wenzelm@7357
    60
by (rtac sym 1);
wenzelm@7357
    61
by (REPEAT (assume_tac 1)) ;
wenzelm@7357
    62
qed "box_equals";
wenzelm@7357
    63
wenzelm@10063
    64
wenzelm@10063
    65
section "Congruence rules for application";
wenzelm@7357
    66
wenzelm@7357
    67
(*similar to AP_THM in Gordon's HOL*)
paulson@7618
    68
Goal "(f::'a=>'b) = g ==> f(x)=g(x)";
paulson@7618
    69
by (etac subst 1);
paulson@7618
    70
by (rtac refl 1);
paulson@7618
    71
qed "fun_cong";
wenzelm@7357
    72
wenzelm@7357
    73
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
paulson@7618
    74
Goal "x=y ==> f(x)=f(y)";
paulson@7618
    75
by (etac subst 1);
paulson@7618
    76
by (rtac refl 1);
paulson@7618
    77
qed "arg_cong";
wenzelm@7357
    78
paulson@7618
    79
Goal "[| f = g; (x::'a) = y |] ==> f(x) = g(y)";
paulson@7618
    80
by (etac subst 1);
paulson@7618
    81
by (etac subst 1);
paulson@7618
    82
by (rtac refl 1);
paulson@7618
    83
qed "cong";
wenzelm@7357
    84
wenzelm@10063
    85
wenzelm@10063
    86
section "Equality of booleans -- iff";
wenzelm@7357
    87
paulson@7618
    88
val prems = Goal "[| P ==> Q;  Q ==> P |] ==> P=Q";
wenzelm@7357
    89
by (REPEAT (ares_tac (prems@[impI, iff RS mp RS mp]) 1));
wenzelm@7357
    90
qed "iffI";
wenzelm@7357
    91
paulson@7618
    92
Goal "[| P=Q; Q |] ==> P";
paulson@7618
    93
by (etac ssubst 1);
paulson@7618
    94
by (assume_tac 1);
paulson@7618
    95
qed "iffD2";
wenzelm@7357
    96
paulson@7618
    97
Goal "[| Q; P=Q |] ==> P";
paulson@7618
    98
by (etac iffD2 1);
paulson@7618
    99
by (assume_tac 1);
paulson@7618
   100
qed "rev_iffD2";
wenzelm@7357
   101
wenzelm@7357
   102
bind_thm ("iffD1", sym RS iffD2);
wenzelm@7357
   103
bind_thm ("rev_iffD1", sym RSN (2, rev_iffD2));
wenzelm@7357
   104
paulson@7618
   105
val [p1,p2] = Goal "[| P=Q; [| P --> Q; Q --> P |] ==> R |] ==> R";
paulson@7618
   106
by (REPEAT (ares_tac [p1 RS iffD2, p1 RS iffD1, p2, impI] 1));
paulson@7618
   107
qed "iffE";
wenzelm@7357
   108
wenzelm@7357
   109
wenzelm@7357
   110
section "True";
wenzelm@7357
   111
paulson@7618
   112
Goalw [True_def] "True";
paulson@7618
   113
by (rtac refl 1);
paulson@7618
   114
qed "TrueI";
wenzelm@7357
   115
paulson@7618
   116
Goal "P ==> P=True";
paulson@7618
   117
by (REPEAT (ares_tac [iffI,TrueI] 1));
paulson@7618
   118
qed "eqTrueI";
wenzelm@7357
   119
paulson@7618
   120
Goal "P=True ==> P";
paulson@7618
   121
by (etac iffD2 1);
paulson@7618
   122
by (rtac TrueI 1);
paulson@7618
   123
qed "eqTrueE";
wenzelm@7357
   124
wenzelm@7357
   125
wenzelm@10063
   126
section "Universal quantifier";
wenzelm@7357
   127
paulson@9159
   128
val prems = Goalw [All_def] "(!!x::'a. P(x)) ==> ALL x. P(x)";
paulson@8529
   129
by (resolve_tac (prems RL [eqTrueI RS ext]) 1);
paulson@8529
   130
qed "allI";
wenzelm@7357
   131
paulson@9159
   132
Goalw [All_def] "ALL x::'a. P(x) ==> P(x)";
paulson@8529
   133
by (rtac eqTrueE 1);
paulson@8529
   134
by (etac fun_cong 1);
paulson@8529
   135
qed "spec";
wenzelm@7357
   136
paulson@9969
   137
val major::prems = Goal "[| ALL x. P(x);  P(x) ==> R |] ==> R";
wenzelm@7357
   138
by (REPEAT (resolve_tac (prems @ [major RS spec]) 1)) ;
wenzelm@7357
   139
qed "allE";
wenzelm@7357
   140
paulson@9969
   141
val prems = Goal
paulson@9159
   142
    "[| ALL x. P(x);  [| P(x); ALL x. P(x) |] ==> R |] ==> R";
wenzelm@7357
   143
by (REPEAT (resolve_tac (prems @ (prems RL [spec])) 1)) ;
wenzelm@7357
   144
qed "all_dupE";
wenzelm@7357
   145
wenzelm@7357
   146
wenzelm@7357
   147
section "False";
wenzelm@10063
   148
(*Depends upon spec; it is impossible to do propositional logic before quantifiers!*)
wenzelm@7357
   149
paulson@8529
   150
Goalw [False_def] "False ==> P";
paulson@8529
   151
by (etac spec 1);
paulson@8529
   152
qed "FalseE";
wenzelm@7357
   153
paulson@8529
   154
Goal "False=True ==> P";
paulson@8529
   155
by (etac (eqTrueE RS FalseE) 1);
paulson@8529
   156
qed "False_neq_True";
wenzelm@7357
   157
wenzelm@7357
   158
wenzelm@10063
   159
section "Negation";
wenzelm@7357
   160
paulson@8529
   161
val prems = Goalw [not_def] "(P ==> False) ==> ~P";
paulson@8529
   162
by (rtac impI 1);
paulson@8529
   163
by (eresolve_tac prems 1);
paulson@8529
   164
qed "notI";
wenzelm@7357
   165
paulson@8529
   166
Goal "False ~= True";
paulson@8529
   167
by (rtac notI 1);
paulson@8529
   168
by (etac False_neq_True 1);
paulson@8529
   169
qed "False_not_True";
wenzelm@7357
   170
paulson@8529
   171
Goal "True ~= False";
paulson@8529
   172
by (rtac notI 1);
paulson@8529
   173
by (dtac sym 1);
paulson@8529
   174
by (etac False_neq_True 1);
paulson@8529
   175
qed "True_not_False";
wenzelm@7357
   176
paulson@8529
   177
Goalw [not_def] "[| ~P;  P |] ==> R";
paulson@8529
   178
by (etac (mp RS FalseE) 1);
paulson@8529
   179
by (assume_tac 1);
paulson@8529
   180
qed "notE";
wenzelm@7357
   181
paulson@9159
   182
(* Alternative ~ introduction rule: [| P ==> ~ Pa; P ==> Pa |] ==> ~ P *)
paulson@9159
   183
bind_thm ("notI2", notE RS notI);
wenzelm@7357
   184
wenzelm@7357
   185
wenzelm@10063
   186
section "Implication";
wenzelm@7357
   187
wenzelm@7357
   188
val prems = Goal "[| P-->Q;  P;  Q ==> R |] ==> R";
wenzelm@7357
   189
by (REPEAT (resolve_tac (prems@[mp]) 1));
wenzelm@7357
   190
qed "impE";
wenzelm@7357
   191
wenzelm@7357
   192
(* Reduces Q to P-->Q, allowing substitution in P. *)
wenzelm@7357
   193
Goal "[| P;  P --> Q |] ==> Q";
wenzelm@7357
   194
by (REPEAT (ares_tac [mp] 1)) ;
wenzelm@7357
   195
qed "rev_mp";
wenzelm@7357
   196
wenzelm@7357
   197
val [major,minor] = Goal "[| ~Q;  P==>Q |] ==> ~P";
wenzelm@7357
   198
by (rtac (major RS notE RS notI) 1);
wenzelm@7357
   199
by (etac minor 1) ;
paulson@10231
   200
qed "contrapos_nn";
wenzelm@7357
   201
paulson@11415
   202
(*not used at all, but we already have the other 3 combinations *)
paulson@11415
   203
val [major,minor] = Goal "[| Q;  P ==> ~Q |] ==> ~P";
paulson@11415
   204
by (rtac (minor RS notE RS notI) 1);
paulson@11415
   205
by (assume_tac 1);
paulson@11415
   206
by (rtac major 1) ;
paulson@11415
   207
qed "contrapos_pn";
paulson@11415
   208
paulson@10231
   209
Goal "t ~= s ==> s ~= t";
paulson@10231
   210
by (etac contrapos_nn 1); 
paulson@10231
   211
by (etac sym 1); 
paulson@10231
   212
qed "not_sym";
paulson@10231
   213
paulson@10231
   214
(*still used in HOLCF*)
wenzelm@7357
   215
val [major,minor] = Goal "[| P==>Q; ~Q |] ==> ~P";
paulson@10231
   216
by (rtac (minor RS contrapos_nn) 1);
wenzelm@7357
   217
by (etac major 1) ;
wenzelm@7357
   218
qed "rev_contrapos";
wenzelm@7357
   219
wenzelm@10063
   220
section "Existential quantifier";
wenzelm@7357
   221
paulson@9159
   222
Goalw [Ex_def] "P x ==> EX x::'a. P x";
paulson@11451
   223
by (rtac allI 1); 
paulson@11451
   224
by (rtac impI 1); 
paulson@11451
   225
by (etac allE 1); 
paulson@11451
   226
by (etac mp 1) ;
paulson@11451
   227
by (assume_tac 1); 
paulson@8529
   228
qed "exI";
wenzelm@7357
   229
wenzelm@9869
   230
val [major,minor] =
paulson@9159
   231
Goalw [Ex_def] "[| EX x::'a. P(x); !!x. P(x) ==> Q |] ==> Q";
paulson@11451
   232
by (rtac (major RS spec RS mp) 1); 
paulson@11451
   233
by (rtac (impI RS allI) 1); 
paulson@11451
   234
by (etac minor 1); 
paulson@8529
   235
qed "exE";
wenzelm@7357
   236
wenzelm@7357
   237
wenzelm@10063
   238
section "Conjunction";
wenzelm@7357
   239
paulson@8529
   240
Goalw [and_def] "[| P; Q |] ==> P&Q";
paulson@8529
   241
by (rtac (impI RS allI) 1);
paulson@8529
   242
by (etac (mp RS mp) 1);
paulson@8529
   243
by (REPEAT (assume_tac 1));
paulson@8529
   244
qed "conjI";
wenzelm@7357
   245
paulson@8529
   246
Goalw [and_def] "[| P & Q |] ==> P";
paulson@8529
   247
by (dtac spec 1) ;
paulson@8529
   248
by (etac mp 1);
paulson@8529
   249
by (REPEAT (ares_tac [impI] 1));
paulson@8529
   250
qed "conjunct1";
wenzelm@7357
   251
paulson@8529
   252
Goalw [and_def] "[| P & Q |] ==> Q";
paulson@8529
   253
by (dtac spec 1) ;
paulson@8529
   254
by (etac mp 1);
paulson@8529
   255
by (REPEAT (ares_tac [impI] 1));
paulson@8529
   256
qed "conjunct2";
wenzelm@7357
   257
paulson@8529
   258
val [major,minor] =
paulson@8529
   259
Goal "[| P&Q;  [| P; Q |] ==> R |] ==> R";
paulson@8529
   260
by (rtac minor 1);
paulson@8529
   261
by (rtac (major RS conjunct1) 1);
paulson@8529
   262
by (rtac (major RS conjunct2) 1);
paulson@8529
   263
qed "conjE";
wenzelm@7357
   264
paulson@8529
   265
val prems =
paulson@8529
   266
Goal "[| P; P ==> Q |] ==> P & Q";
paulson@8529
   267
by (REPEAT (resolve_tac (conjI::prems) 1));
paulson@8529
   268
qed "context_conjI";
wenzelm@7357
   269
wenzelm@7357
   270
wenzelm@10063
   271
section "Disjunction";
wenzelm@7357
   272
paulson@8529
   273
Goalw [or_def] "P ==> P|Q";
paulson@8529
   274
by (REPEAT (resolve_tac [allI,impI] 1));
paulson@8529
   275
by (etac mp 1 THEN assume_tac 1);
paulson@8529
   276
qed "disjI1";
wenzelm@7357
   277
paulson@8529
   278
Goalw [or_def] "Q ==> P|Q";
paulson@8529
   279
by (REPEAT (resolve_tac [allI,impI] 1));
paulson@8529
   280
by (etac mp 1 THEN assume_tac 1);
paulson@8529
   281
qed "disjI2";
wenzelm@7357
   282
paulson@8529
   283
val [major,minorP,minorQ] =
paulson@8529
   284
Goalw [or_def]  "[| P | Q; P ==> R; Q ==> R |] ==> R";
paulson@8529
   285
by (rtac (major RS spec RS mp RS mp) 1);
paulson@8529
   286
by (DEPTH_SOLVE (ares_tac [impI,minorP,minorQ] 1));
paulson@8529
   287
qed "disjE";
wenzelm@7357
   288
wenzelm@7357
   289
wenzelm@10063
   290
section "Classical logic";
wenzelm@10063
   291
(*CCONTR -- classical logic*)
wenzelm@7357
   292
paulson@8529
   293
val [prem] = Goal  "(~P ==> P) ==> P";
paulson@8529
   294
by (rtac (True_or_False RS disjE RS eqTrueE) 1);
paulson@8529
   295
by (assume_tac 1);
paulson@8529
   296
by (rtac (notI RS prem RS eqTrueI) 1);
paulson@8529
   297
by (etac subst 1);
paulson@8529
   298
by (assume_tac 1);
paulson@8529
   299
qed "classical";
wenzelm@7357
   300
wenzelm@7832
   301
bind_thm ("ccontr", FalseE RS classical);
wenzelm@7357
   302
paulson@9159
   303
(*notE with premises exchanged; it discharges ~R so that it can be used to
paulson@9159
   304
  make elimination rules*)
paulson@9159
   305
val [premp,premnot] = Goal "[| P; ~R ==> ~P |] ==> R";
paulson@9159
   306
by (rtac ccontr 1);
paulson@9159
   307
by (etac ([premnot,premp] MRS notE) 1);
paulson@9159
   308
qed "rev_notE";
paulson@9159
   309
wenzelm@7357
   310
(*Double negation law*)
wenzelm@7357
   311
Goal "~~P ==> P";
wenzelm@7357
   312
by (rtac classical 1);
wenzelm@7357
   313
by (etac notE 1);
wenzelm@7357
   314
by (assume_tac 1);
wenzelm@7357
   315
qed "notnotD";
wenzelm@7357
   316
wenzelm@7357
   317
val [p1,p2] = Goal "[| Q; ~ P ==> ~ Q |] ==> P";
wenzelm@7357
   318
by (rtac classical 1);
wenzelm@7357
   319
by (dtac p2 1);
wenzelm@7357
   320
by (etac notE 1);
wenzelm@7357
   321
by (rtac p1 1);
paulson@10231
   322
qed "contrapos_pp";
wenzelm@7357
   323
wenzelm@10063
   324
wenzelm@10063
   325
section "Unique existence";
wenzelm@7357
   326
paulson@9159
   327
val prems = Goalw [Ex1_def] "[| P(a);  !!x. P(x) ==> x=a |] ==> EX! x. P(x)";
paulson@8529
   328
by (REPEAT (ares_tac (prems@[exI,conjI,allI,impI]) 1));
paulson@8529
   329
qed "ex1I";
wenzelm@7357
   330
wenzelm@7357
   331
(*Sometimes easier to use: the premises have no shared variables.  Safe!*)
paulson@8529
   332
val [ex_prem,eq] = Goal
paulson@9159
   333
    "[| EX x. P(x);  !!x y. [| P(x); P(y) |] ==> x=y |] ==> EX! x. P(x)";
paulson@8529
   334
by (rtac (ex_prem RS exE) 1);
wenzelm@7357
   335
by (REPEAT (ares_tac [ex1I,eq] 1)) ;
wenzelm@7357
   336
qed "ex_ex1I";
wenzelm@7357
   337
paulson@8529
   338
val major::prems = Goalw [Ex1_def]
paulson@9159
   339
    "[| EX! x. P(x);  !!x. [| P(x);  ALL y. P(y) --> y=x |] ==> R |] ==> R";
paulson@8529
   340
by (rtac (major RS exE) 1);
paulson@8529
   341
by (REPEAT (etac conjE 1 ORELSE ares_tac prems 1));
paulson@8529
   342
qed "ex1E";
wenzelm@7357
   343
paulson@9159
   344
Goal "EX! x. P x ==> EX x. P x";
wenzelm@7357
   345
by (etac ex1E 1);
wenzelm@7357
   346
by (rtac exI 1);
wenzelm@7357
   347
by (assume_tac 1);
wenzelm@7357
   348
qed "ex1_implies_ex";
wenzelm@7357
   349
wenzelm@7357
   350
wenzelm@11432
   351
section "THE: definite description operator";
wenzelm@11432
   352
wenzelm@11432
   353
val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> (THE x. P x) = a";
wenzelm@11432
   354
by (rtac trans 1); 
wenzelm@11432
   355
 by (rtac (thm "the_eq_trivial") 2);
wenzelm@11432
   356
by (res_inst_tac [("f","The")] arg_cong 1); 
wenzelm@11432
   357
by (rtac ext 1); 
wenzelm@11432
   358
 by (rtac iffI 1); 
wenzelm@11432
   359
by (etac premx 1); 
wenzelm@11432
   360
by (etac ssubst 1 THEN rtac prema 1);
wenzelm@11432
   361
qed "the_equality";
wenzelm@11432
   362
wenzelm@11432
   363
val [prema,premx] = Goal "[| P a;  !!x. P x ==> x=a |] ==> P (THE x. P x)";
wenzelm@11432
   364
by (rtac (the_equality RS ssubst) 1);
wenzelm@11432
   365
by (REPEAT (ares_tac [prema,premx] 1));
wenzelm@11432
   366
qed "theI";
wenzelm@11432
   367
wenzelm@11433
   368
Goal "EX! x. P x ==> P (THE x. P x)";
wenzelm@11432
   369
by (etac ex1E 1);
wenzelm@11432
   370
by (etac theI 1);
wenzelm@11432
   371
by (etac allE 1);
wenzelm@11432
   372
by (etac mp 1);
wenzelm@11432
   373
by (atac 1);
wenzelm@11432
   374
qed "theI'";
wenzelm@11432
   375
wenzelm@11432
   376
(*Easier to apply than theI: only one occurrence of P*)
wenzelm@11432
   377
val [prema,premx,premq] = Goal
wenzelm@11432
   378
     "[| P a;  !!x. P x ==> x=a;  !!x. P x ==> Q x |] \
wenzelm@11432
   379
\     ==> Q (THE x. P x)";
wenzelm@11432
   380
by (rtac premq 1); 
wenzelm@11432
   381
by (rtac theI 1); 
wenzelm@11432
   382
by (REPEAT (ares_tac [prema,premx] 1));
wenzelm@11432
   383
qed "theI2";
wenzelm@11432
   384
wenzelm@11432
   385
Goal "[| EX!x. P x; P a |] ==> (THE x. P x) = a";
wenzelm@11432
   386
by (rtac the_equality 1);
wenzelm@11432
   387
by  (atac 1);
wenzelm@11432
   388
by (etac ex1E 1);
wenzelm@11432
   389
by (etac all_dupE 1);
wenzelm@11432
   390
by (dtac mp 1);
wenzelm@11432
   391
by  (atac 1);
wenzelm@11432
   392
by (etac ssubst 1);
wenzelm@11432
   393
by (etac allE 1);
wenzelm@11432
   394
by (etac mp 1);
wenzelm@11432
   395
by (atac 1);
wenzelm@11432
   396
qed "the1_equality";
wenzelm@11432
   397
wenzelm@11432
   398
Goal "(THE y. x=y) = x";
wenzelm@11432
   399
by (rtac the_equality 1);
wenzelm@11432
   400
by (rtac refl 1);
wenzelm@11432
   401
by (etac sym 1);
wenzelm@11432
   402
qed "the_sym_eq_trivial";
wenzelm@11432
   403
wenzelm@11432
   404
wenzelm@10063
   405
section "Classical intro rules for disjunction and existential quantifiers";
wenzelm@7357
   406
paulson@9969
   407
val prems = Goal "(~Q ==> P) ==> P|Q";
wenzelm@7357
   408
by (rtac classical 1);
wenzelm@7357
   409
by (REPEAT (ares_tac (prems@[disjI1,notI]) 1));
wenzelm@7357
   410
by (REPEAT (ares_tac (prems@[disjI2,notE]) 1)) ;
wenzelm@7357
   411
qed "disjCI";
wenzelm@7357
   412
wenzelm@7357
   413
Goal "~P | P";
wenzelm@7357
   414
by (REPEAT (ares_tac [disjCI] 1)) ;
wenzelm@7357
   415
qed "excluded_middle";
wenzelm@7357
   416
wenzelm@7357
   417
(*For disjunctive case analysis*)
wenzelm@7357
   418
fun excluded_middle_tac sP =
wenzelm@7357
   419
    res_inst_tac [("Q",sP)] (excluded_middle RS disjE);
wenzelm@7357
   420
wenzelm@7357
   421
(*Classical implies (-->) elimination. *)
wenzelm@7357
   422
val major::prems = Goal "[| P-->Q; ~P ==> R; Q ==> R |] ==> R";
wenzelm@7357
   423
by (rtac (excluded_middle RS disjE) 1);
wenzelm@7357
   424
by (REPEAT (DEPTH_SOLVE_1 (ares_tac (prems @ [major RS mp]) 1)));
wenzelm@7357
   425
qed "impCE";
wenzelm@7357
   426
wenzelm@7357
   427
(*This version of --> elimination works on Q before P.  It works best for
wenzelm@7357
   428
  those cases in which P holds "almost everywhere".  Can't install as
wenzelm@7357
   429
  default: would break old proofs.*)
wenzelm@7357
   430
val major::prems = Goal
wenzelm@7357
   431
    "[| P-->Q;  Q ==> R;  ~P ==> R |] ==> R";
wenzelm@7357
   432
by (resolve_tac [excluded_middle RS disjE] 1);
wenzelm@7357
   433
by (DEPTH_SOLVE (ares_tac (prems@[major RS mp]) 1)) ;
wenzelm@7357
   434
qed "impCE'";
wenzelm@7357
   435
wenzelm@7357
   436
(*Classical <-> elimination. *)
wenzelm@7357
   437
val major::prems = Goal
wenzelm@7357
   438
    "[| P=Q;  [| P; Q |] ==> R;  [| ~P; ~Q |] ==> R |] ==> R";
wenzelm@7357
   439
by (rtac (major RS iffE) 1);
wenzelm@9869
   440
by (REPEAT (DEPTH_SOLVE_1
wenzelm@9869
   441
            (eresolve_tac ([asm_rl,impCE,notE]@prems) 1)));
wenzelm@7357
   442
qed "iffCE";
wenzelm@7357
   443
paulson@9159
   444
val prems = Goal "(ALL x. ~P(x) ==> P(a)) ==> EX x. P(x)";
wenzelm@7357
   445
by (rtac ccontr 1);
wenzelm@7357
   446
by (REPEAT (ares_tac (prems@[exI,allI,notI,notE]) 1))  ;
wenzelm@7357
   447
qed "exCI";
wenzelm@7357
   448
wenzelm@7357
   449
(* case distinction *)
wenzelm@7357
   450
paulson@8529
   451
val [prem1,prem2] = Goal "[| P ==> Q; ~P ==> Q |] ==> Q";
paulson@8529
   452
by (rtac (excluded_middle RS disjE) 1);
paulson@8529
   453
by (etac prem2 1);
paulson@8529
   454
by (etac prem1 1);
paulson@8529
   455
qed "case_split_thm";
wenzelm@7357
   456
wenzelm@7357
   457
fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
wenzelm@7357
   458
wenzelm@7357
   459
wenzelm@7357
   460
(** Standard abbreviations **)
wenzelm@7357
   461
wenzelm@10731
   462
(* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
oheimb@7490
   463
local
oheimb@7490
   464
  fun wrong_prem (Const ("All", _) $ (Abs (_, _, t))) = wrong_prem t
oheimb@7490
   465
  |   wrong_prem (Bound _) = true
oheimb@7490
   466
  |   wrong_prem _ = false;
oheimb@7533
   467
  val filter_right = filter (fn t => not (wrong_prem (HOLogic.dest_Trueprop (hd (Thm.prems_of t)))));
oheimb@7490
   468
in
oheimb@7490
   469
  fun smp i = funpow i (fn m => filter_right ([spec] RL m)) ([mp]);
oheimb@7490
   470
  fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]
oheimb@7490
   471
end;
oheimb@7490
   472
oheimb@7490
   473
wenzelm@9869
   474
fun strip_tac i = REPEAT(resolve_tac [impI,allI] i);
oheimb@11006
   475