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