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