src/CCL/CCL.ML
author oheimb
Fri Jun 02 20:38:28 2000 +0200 (2000-06-02)
changeset 9028 8a1ec8f05f14
parent 5062 fbdb0b541314
child 15531 08c8dad8e399
permissions -rw-r--r--
added HOL/Prolog
clasohm@1459
     1
(*  Title:      CCL/ccl
clasohm@0
     2
    ID:         $Id$
clasohm@1459
     3
    Author:     Martin Coen, Cambridge University Computer Laboratory
clasohm@0
     4
    Copyright   1993  University of Cambridge
clasohm@0
     5
clasohm@0
     6
For ccl.thy.
clasohm@0
     7
*)
clasohm@0
     8
clasohm@0
     9
open CCL;
clasohm@0
    10
clasohm@0
    11
val ccl_data_defs = [apply_def,fix_def];
clasohm@0
    12
paulson@4347
    13
val CCL_ss = set_ss addsimps [po_refl];
clasohm@0
    14
clasohm@0
    15
(*** Congruence Rules ***)
clasohm@0
    16
clasohm@0
    17
(*similar to AP_THM in Gordon's HOL*)
clasohm@757
    18
qed_goal "fun_cong" CCL.thy "(f::'a=>'b) = g ==> f(x)=g(x)"
clasohm@0
    19
  (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
clasohm@0
    20
clasohm@0
    21
(*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
clasohm@757
    22
qed_goal "arg_cong" CCL.thy "x=y ==> f(x)=f(y)"
clasohm@0
    23
 (fn [prem] => [rtac (prem RS subst) 1, rtac refl 1]);
clasohm@0
    24
wenzelm@5062
    25
Goal  "(ALL x. f(x) = g(x)) --> (%x. f(x)) = (%x. g(x))";
lcp@8
    26
by (simp_tac (CCL_ss addsimps [eq_iff]) 1);
clasohm@0
    27
by (fast_tac (set_cs addIs [po_abstractn]) 1);
clasohm@1087
    28
bind_thm("abstractn", standard (allI RS (result() RS mp)));
clasohm@0
    29
clasohm@0
    30
fun type_of_terms (Const("Trueprop",_) $ 
clasohm@0
    31
                   (Const("op =",(Type ("fun", [t,_]))) $ _ $ _)) = t;
clasohm@0
    32
clasohm@0
    33
fun abs_prems thm = 
clasohm@0
    34
   let fun do_abs n thm (Type ("fun", [_,t])) = do_abs n (abstractn RSN (n,thm)) t
clasohm@0
    35
         | do_abs n thm _                     = thm
clasohm@0
    36
       fun do_prems n      [] thm = thm
clasohm@0
    37
         | do_prems n (x::xs) thm = do_prems (n+1) xs (do_abs n thm (type_of_terms x));
clasohm@0
    38
   in do_prems 1 (prems_of thm) thm
clasohm@0
    39
   end;
clasohm@0
    40
clasohm@0
    41
val caseBs = [caseBtrue,caseBfalse,caseBpair,caseBlam,caseBbot];
clasohm@0
    42
clasohm@0
    43
(*** Termination and Divergence ***)
clasohm@0
    44
wenzelm@5062
    45
Goalw [Trm_def,Dvg_def] "Trm(t) <-> ~ t = bot";
lcp@642
    46
by (rtac iff_refl 1);
clasohm@757
    47
qed "Trm_iff";
clasohm@0
    48
wenzelm@5062
    49
Goalw [Trm_def,Dvg_def] "Dvg(t) <-> t = bot";
lcp@642
    50
by (rtac iff_refl 1);
clasohm@757
    51
qed "Dvg_iff";
clasohm@0
    52
clasohm@0
    53
(*** Constructors are injective ***)
clasohm@0
    54
clasohm@0
    55
val prems = goal CCL.thy
clasohm@0
    56
    "[| x=a;  y=b;  x=y |] ==> a=b";
clasohm@0
    57
by  (REPEAT (SOMEGOAL (ares_tac (prems@[box_equals]))));
clasohm@757
    58
qed "eq_lemma";
clasohm@0
    59
lcp@8
    60
fun mk_inj_rl thy rews s = 
clasohm@0
    61
      let fun mk_inj_lemmas r = ([arg_cong] RL [(r RS (r RS eq_lemma))]);
clasohm@0
    62
          val inj_lemmas = flat (map mk_inj_lemmas rews);
clasohm@0
    63
          val tac = REPEAT (ares_tac [iffI,allI,conjI] 1 ORELSE
clasohm@0
    64
                            eresolve_tac inj_lemmas 1 ORELSE
lcp@8
    65
                            asm_simp_tac (CCL_ss addsimps rews) 1)
clasohm@0
    66
      in prove_goal thy s (fn _ => [tac])
clasohm@0
    67
      end;
clasohm@0
    68
lcp@8
    69
val ccl_injs = map (mk_inj_rl CCL.thy caseBs)
clasohm@0
    70
               ["<a,b> = <a',b'> <-> (a=a' & b=b')",
wenzelm@3837
    71
                "(lam x. b(x) = lam x. b'(x)) <-> ((ALL z. b(z)=b'(z)))"];
clasohm@0
    72
clasohm@0
    73
val pair_inject = ((hd ccl_injs) RS iffD1) RS conjE;
clasohm@0
    74
clasohm@0
    75
(*** Constructors are distinct ***)
clasohm@0
    76
clasohm@0
    77
local
clasohm@0
    78
  fun pairs_of f x [] = []
clasohm@0
    79
    | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys);
clasohm@0
    80
clasohm@0
    81
  fun mk_combs ff [] = []
clasohm@0
    82
    | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs;
clasohm@0
    83
clasohm@0
    84
(* Doesn't handle binder types correctly *)
clasohm@0
    85
  fun saturate thy sy name = 
clasohm@0
    86
       let fun arg_str 0 a s = s
clasohm@0
    87
         | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
clasohm@0
    88
         | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s);
clasohm@0
    89
           val sg = sign_of thy;
wenzelm@3935
    90
           val T = case Sign.const_type sg (Sign.intern_const (sign_of thy) sy) of
clasohm@1459
    91
                            None => error(sy^" not declared") | Some(T) => T;
clasohm@0
    92
           val arity = length (fst (strip_type T));
clasohm@0
    93
       in sy ^ (arg_str arity name "") end;
clasohm@0
    94
clasohm@0
    95
  fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b");
clasohm@0
    96
clasohm@0
    97
  val lemma = prove_goal CCL.thy "t=t' --> case(t,b,c,d,e) = case(t',b,c,d,e)"
lcp@8
    98
                   (fn _ => [simp_tac CCL_ss 1]) RS mp;
clasohm@0
    99
  fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL 
clasohm@0
   100
                           [distinctness RS notE,sym RS (distinctness RS notE)];
clasohm@0
   101
in
clasohm@0
   102
  fun mk_lemmas rls = flat (map mk_lemma (mk_combs pair rls));
clasohm@0
   103
  fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs;
clasohm@0
   104
end;
clasohm@0
   105
clasohm@0
   106
clasohm@0
   107
val caseB_lemmas = mk_lemmas caseBs;
clasohm@0
   108
clasohm@0
   109
val ccl_dstncts = 
clasohm@0
   110
        let fun mk_raw_dstnct_thm rls s = 
clasohm@0
   111
                  prove_goal CCL.thy s (fn _=> [rtac notI 1,eresolve_tac rls 1])
clasohm@0
   112
        in map (mk_raw_dstnct_thm caseB_lemmas) 
clasohm@0
   113
                (mk_dstnct_rls CCL.thy ["bot","true","false","pair","lambda"]) end;
clasohm@0
   114
clasohm@0
   115
fun mk_dstnct_thms thy defs inj_rls xs = 
clasohm@0
   116
          let fun mk_dstnct_thm rls s = prove_goalw thy defs s 
lcp@8
   117
                               (fn _ => [simp_tac (CCL_ss addsimps (rls@inj_rls)) 1])
clasohm@0
   118
          in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end;
clasohm@0
   119
clasohm@0
   120
fun mkall_dstnct_thms thy defs i_rls xss = flat (map (mk_dstnct_thms thy defs i_rls) xss);
clasohm@0
   121
clasohm@0
   122
(*** Rewriting and Proving ***)
clasohm@0
   123
clasohm@0
   124
fun XH_to_I rl = rl RS iffD2;
clasohm@0
   125
fun XH_to_D rl = rl RS iffD1;
clasohm@0
   126
val XH_to_E = make_elim o XH_to_D;
clasohm@0
   127
val XH_to_Is = map XH_to_I;
clasohm@0
   128
val XH_to_Ds = map XH_to_D;
clasohm@0
   129
val XH_to_Es = map XH_to_E;
clasohm@0
   130
clasohm@0
   131
val ccl_rews = caseBs @ ccl_injs @ ccl_dstncts;
lcp@8
   132
val ccl_ss = CCL_ss addsimps ccl_rews;
clasohm@0
   133
clasohm@0
   134
val ccl_cs = set_cs addSEs (pair_inject::(ccl_dstncts RL [notE])) 
clasohm@0
   135
                    addSDs (XH_to_Ds ccl_injs);
clasohm@0
   136
clasohm@0
   137
(****** Facts from gfp Definition of [= and = ******)
clasohm@0
   138
clasohm@0
   139
val major::prems = goal Set.thy "[| A=B;  a:B <-> P |] ==> a:A <-> P";
lcp@642
   140
by (resolve_tac (prems RL [major RS ssubst]) 1);
clasohm@757
   141
qed "XHlemma1";
clasohm@0
   142
wenzelm@5062
   143
Goal "(P(t,t') <-> Q) --> (<t,t'> : {p. EX t t'. p=<t,t'> &  P(t,t')} <-> Q)";
clasohm@0
   144
by (fast_tac ccl_cs 1);
clasohm@1087
   145
bind_thm("XHlemma2", result() RS mp);
clasohm@0
   146
clasohm@0
   147
(*** Pre-Order ***)
clasohm@0
   148
wenzelm@5062
   149
Goalw [POgen_def,SIM_def]  "mono(%X. POgen(X))";
lcp@642
   150
by (rtac monoI 1);
clasohm@0
   151
by (safe_tac ccl_cs);
clasohm@0
   152
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
lcp@8
   153
by (ALLGOALS (simp_tac ccl_ss));
clasohm@0
   154
by (ALLGOALS (fast_tac set_cs));
clasohm@757
   155
qed "POgen_mono";
clasohm@0
   156
wenzelm@5062
   157
Goalw [POgen_def,SIM_def]
paulson@4347
   158
 "<t,t'> : POgen(R) <-> t= bot | (t=true & t'=true)  | (t=false & t'=false) | \
paulson@4347
   159
\          (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
paulson@4347
   160
\          (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : R))";
lcp@642
   161
by (rtac (iff_refl RS XHlemma2) 1);
clasohm@757
   162
qed "POgenXH";
clasohm@0
   163
wenzelm@5062
   164
Goal
clasohm@0
   165
  "t [= t' <-> t=bot | (t=true & t'=true) | (t=false & t'=false) | \
paulson@4347
   166
\                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
paulson@4347
   167
\                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
paulson@4347
   168
by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1);
wenzelm@4423
   169
by (rtac (rewrite_rule [POgen_def,SIM_def] 
wenzelm@4423
   170
                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1);
lcp@642
   171
by (rtac (iff_refl RS XHlemma2) 1);
clasohm@757
   172
qed "poXH";
clasohm@0
   173
wenzelm@5062
   174
Goal "bot [= b";
lcp@642
   175
by (rtac (poXH RS iffD2) 1);
lcp@8
   176
by (simp_tac ccl_ss 1);
clasohm@757
   177
qed "po_bot";
clasohm@0
   178
wenzelm@5062
   179
Goal "a [= bot --> a=bot";
lcp@642
   180
by (rtac impI 1);
lcp@642
   181
by (dtac (poXH RS iffD1) 1);
lcp@642
   182
by (etac rev_mp 1);
lcp@8
   183
by (simp_tac ccl_ss 1);
clasohm@1087
   184
bind_thm("bot_poleast", result() RS mp);
clasohm@0
   185
wenzelm@5062
   186
Goal "<a,b> [= <a',b'> <->  a [= a' & b [= b'";
lcp@642
   187
by (rtac (poXH RS iff_trans) 1);
lcp@8
   188
by (simp_tac ccl_ss 1);
clasohm@757
   189
qed "po_pair";
clasohm@0
   190
wenzelm@5062
   191
Goal "lam x. f(x) [= lam x. f'(x) <-> (ALL x. f(x) [= f'(x))";
lcp@642
   192
by (rtac (poXH RS iff_trans) 1);
lcp@8
   193
by (simp_tac ccl_ss 1);
clasohm@0
   194
by (REPEAT (ares_tac [iffI,allI] 1 ORELSE eresolve_tac [exE,conjE] 1));
lcp@8
   195
by (asm_simp_tac ccl_ss 1);
clasohm@0
   196
by (fast_tac ccl_cs 1);
clasohm@757
   197
qed "po_lam";
clasohm@0
   198
clasohm@0
   199
val ccl_porews = [po_bot,po_pair,po_lam];
clasohm@0
   200
clasohm@0
   201
val [p1,p2,p3,p4,p5] = goal CCL.thy
wenzelm@3837
   202
    "[| t [= t';  a [= a';  b [= b';  !!x y. c(x,y) [= c'(x,y); \
wenzelm@3837
   203
\       !!u. d(u) [= d'(u) |] ==> case(t,a,b,c,d) [= case(t',a',b',c',d')";
lcp@642
   204
by (rtac (p1 RS po_cong RS po_trans) 1);
lcp@642
   205
by (rtac (p2 RS po_cong RS po_trans) 1);
lcp@642
   206
by (rtac (p3 RS po_cong RS po_trans) 1);
lcp@642
   207
by (rtac (p4 RS po_abstractn RS po_abstractn RS po_cong RS po_trans) 1);
wenzelm@3837
   208
by (res_inst_tac [("f1","%d. case(t',a',b',c',d)")] 
clasohm@0
   209
               (p5 RS po_abstractn RS po_cong RS po_trans) 1);
lcp@642
   210
by (rtac po_refl 1);
clasohm@757
   211
qed "case_pocong";
clasohm@0
   212
clasohm@0
   213
val [p1,p2] = goalw CCL.thy ccl_data_defs
clasohm@0
   214
    "[| f [= f';  a [= a' |] ==> f ` a [= f' ` a'";
clasohm@0
   215
by (REPEAT (ares_tac [po_refl,case_pocong,p1,p2 RS po_cong] 1));
clasohm@757
   216
qed "apply_pocong";
clasohm@0
   217
clasohm@0
   218
wenzelm@3837
   219
val prems = goal CCL.thy "~ lam x. b(x) [= bot";
lcp@642
   220
by (rtac notI 1);
lcp@642
   221
by (dtac bot_poleast 1);
lcp@642
   222
by (etac (distinctness RS notE) 1);
clasohm@757
   223
qed "npo_lam_bot";
clasohm@0
   224
clasohm@0
   225
val eq1::eq2::prems = goal CCL.thy
clasohm@0
   226
    "[| x=a;  y=b;  x[=y |] ==> a[=b";
lcp@642
   227
by (rtac (eq1 RS subst) 1);
lcp@642
   228
by (rtac (eq2 RS subst) 1);
lcp@642
   229
by (resolve_tac prems 1);
clasohm@757
   230
qed "po_lemma";
clasohm@0
   231
wenzelm@5062
   232
Goal "~ <a,b> [= lam x. f(x)";
lcp@642
   233
by (rtac notI 1);
lcp@642
   234
by (rtac (npo_lam_bot RS notE) 1);
lcp@642
   235
by (etac (case_pocong RS (caseBlam RS (caseBpair RS po_lemma))) 1);
clasohm@0
   236
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
clasohm@757
   237
qed "npo_pair_lam";
clasohm@0
   238
wenzelm@5062
   239
Goal "~ lam x. f(x) [= <a,b>";
lcp@642
   240
by (rtac notI 1);
lcp@642
   241
by (rtac (npo_lam_bot RS notE) 1);
lcp@642
   242
by (etac (case_pocong RS (caseBpair RS (caseBlam RS po_lemma))) 1);
clasohm@0
   243
by (REPEAT (resolve_tac [po_refl,npo_lam_bot] 1));
clasohm@757
   244
qed "npo_lam_pair";
clasohm@0
   245
clasohm@0
   246
fun mk_thm s = prove_goal CCL.thy s (fn _ => 
clasohm@0
   247
                          [rtac notI 1,dtac case_pocong 1,etac rev_mp 5,
lcp@8
   248
                           ALLGOALS (simp_tac ccl_ss),
clasohm@0
   249
                           REPEAT (resolve_tac [po_refl,npo_lam_bot] 1)]);
clasohm@0
   250
clasohm@0
   251
val npo_rls = [npo_pair_lam,npo_lam_pair] @ map mk_thm
clasohm@0
   252
            ["~ true [= false",          "~ false [= true",
clasohm@0
   253
             "~ true [= <a,b>",          "~ <a,b> [= true",
wenzelm@3837
   254
             "~ true [= lam x. f(x)","~ lam x. f(x) [= true",
clasohm@0
   255
            "~ false [= <a,b>",          "~ <a,b> [= false",
wenzelm@3837
   256
            "~ false [= lam x. f(x)","~ lam x. f(x) [= false"];
clasohm@0
   257
clasohm@0
   258
(* Coinduction for [= *)
clasohm@0
   259
clasohm@0
   260
val prems = goal CCL.thy "[|  <t,u> : R;  R <= POgen(R) |] ==> t [= u";
lcp@642
   261
by (rtac (PO_def RS def_coinduct RS (PO_iff RS iffD2)) 1);
clasohm@0
   262
by (REPEAT (ares_tac prems 1));
clasohm@757
   263
qed "po_coinduct";
clasohm@0
   264
clasohm@0
   265
fun po_coinduct_tac s i = res_inst_tac [("R",s)] po_coinduct i;
clasohm@0
   266
clasohm@0
   267
(*************** EQUALITY *******************)
clasohm@0
   268
wenzelm@5062
   269
Goalw [EQgen_def,SIM_def]  "mono(%X. EQgen(X))";
lcp@642
   270
by (rtac monoI 1);
clasohm@0
   271
by (safe_tac set_cs);
clasohm@0
   272
by (REPEAT_SOME (resolve_tac [exI,conjI,refl]));
lcp@8
   273
by (ALLGOALS (simp_tac ccl_ss));
clasohm@0
   274
by (ALLGOALS (fast_tac set_cs));
clasohm@757
   275
qed "EQgen_mono";
clasohm@0
   276
wenzelm@5062
   277
Goalw [EQgen_def,SIM_def]
clasohm@0
   278
  "<t,t'> : EQgen(R) <-> (t=bot & t'=bot)  | (t=true & t'=true)  | \
clasohm@0
   279
\                                            (t=false & t'=false) | \
wenzelm@3837
   280
\                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : R & <b,b'> : R) | \
wenzelm@3837
   281
\                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x.<f(x),f'(x)> : R))";
lcp@642
   282
by (rtac (iff_refl RS XHlemma2) 1);
clasohm@757
   283
qed "EQgenXH";
clasohm@0
   284
wenzelm@5062
   285
Goal
clasohm@0
   286
  "t=t' <-> (t=bot & t'=bot)  | (t=true & t'=true)  | (t=false & t'=false) | \
wenzelm@3837
   287
\                    (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a=a' & b=b') | \
wenzelm@3837
   288
\                    (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x)=f'(x)))";
clasohm@0
   289
by (subgoal_tac
clasohm@0
   290
  "<t,t'> : EQ <-> (t=bot & t'=bot)  | (t=true & t'=true) | (t=false & t'=false) | \
wenzelm@3837
   291
\             (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & <a,a'> : EQ & <b,b'> : EQ) | \
wenzelm@3837
   292
\             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
lcp@642
   293
by (etac rev_mp 1);
lcp@8
   294
by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
wenzelm@4423
   295
by (rtac (rewrite_rule [EQgen_def,SIM_def]
wenzelm@4423
   296
                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1);
lcp@642
   297
by (rtac (iff_refl RS XHlemma2) 1);
clasohm@757
   298
qed "eqXH";
clasohm@0
   299
clasohm@0
   300
val prems = goal CCL.thy "[|  <t,u> : R;  R <= EQgen(R) |] ==> t = u";
lcp@642
   301
by (rtac (EQ_def RS def_coinduct RS (EQ_iff RS iffD2)) 1);
clasohm@0
   302
by (REPEAT (ares_tac prems 1));
clasohm@757
   303
qed "eq_coinduct";
clasohm@0
   304
clasohm@0
   305
val prems = goal CCL.thy 
wenzelm@3837
   306
    "[|  <t,u> : R;  R <= EQgen(lfp(%x. EQgen(x) Un R Un EQ)) |] ==> t = u";
lcp@642
   307
by (rtac (EQ_def RS def_coinduct3 RS (EQ_iff RS iffD2)) 1);
clasohm@0
   308
by (REPEAT (ares_tac (EQgen_mono::prems) 1));
clasohm@757
   309
qed "eq_coinduct3";
clasohm@0
   310
clasohm@0
   311
fun eq_coinduct_tac s i = res_inst_tac [("R",s)] eq_coinduct i;
clasohm@0
   312
fun eq_coinduct3_tac s i = res_inst_tac [("R",s)] eq_coinduct3 i;
clasohm@0
   313
clasohm@0
   314
(*** Untyped Case Analysis and Other Facts ***)
clasohm@0
   315
wenzelm@5062
   316
Goalw [apply_def]  "(EX f. t=lam x. f(x)) --> t = lam x.(t ` x)";
clasohm@0
   317
by (safe_tac ccl_cs);
lcp@8
   318
by (simp_tac ccl_ss 1);
clasohm@1087
   319
bind_thm("cond_eta", result() RS mp);
clasohm@0
   320
wenzelm@5062
   321
Goal "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))";
clasohm@0
   322
by (cut_facts_tac [refl RS (eqXH RS iffD1)] 1);
clasohm@0
   323
by (fast_tac set_cs 1);
clasohm@757
   324
qed "exhaustion";
clasohm@0
   325
clasohm@0
   326
val prems = goal CCL.thy 
wenzelm@3837
   327
    "[| P(bot);  P(true);  P(false);  !!x y. P(<x,y>);  !!b. P(lam x. b(x)) |] ==> P(t)";
clasohm@0
   328
by (cut_facts_tac [exhaustion] 1);
clasohm@0
   329
by (REPEAT_SOME (ares_tac prems ORELSE' eresolve_tac [disjE,exE,ssubst]));
clasohm@757
   330
qed "term_case";
clasohm@0
   331
clasohm@0
   332
fun term_case_tac a i = res_inst_tac [("t",a)] term_case i;