src/HOLCF/Cfun3.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 5291 5706f0ef1d43
child 8820 a1297de19ec7
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/cfun3.ML
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 *)
     6 
     7 open Cfun3;
     8 
     9 (* for compatibility with old HOLCF-Version *)
    10 qed_goal "inst_cfun_pcpo" thy "UU = Abs_CFun(%x. UU)"
    11  (fn prems => 
    12         [
    13         (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1)
    14         ]);
    15 
    16 (* ------------------------------------------------------------------------ *)
    17 (* the contlub property for Rep_CFun its 'first' argument                       *)
    18 (* ------------------------------------------------------------------------ *)
    19 
    20 qed_goal "contlub_Rep_CFun1" thy "contlub(Rep_CFun)"
    21 (fn prems =>
    22         [
    23         (rtac contlubI 1),
    24         (strip_tac 1),
    25         (rtac (expand_fun_eq RS iffD2) 1),
    26         (strip_tac 1),
    27         (stac thelub_cfun 1),
    28         (atac 1),
    29         (stac Cfunapp2 1),
    30         (etac cont_lubcfun 1),
    31         (stac thelub_fun 1),
    32         (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
    33         (rtac refl 1)
    34         ]);
    35 
    36 
    37 (* ------------------------------------------------------------------------ *)
    38 (* the cont property for Rep_CFun in its first argument                        *)
    39 (* ------------------------------------------------------------------------ *)
    40 
    41 qed_goal "cont_Rep_CFun1" thy "cont(Rep_CFun)"
    42 (fn prems =>
    43         [
    44         (rtac monocontlub2cont 1),
    45         (rtac monofun_Rep_CFun1 1),
    46         (rtac contlub_Rep_CFun1 1)
    47         ]);
    48 
    49 
    50 (* ------------------------------------------------------------------------ *)
    51 (* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_]   *)
    52 (* ------------------------------------------------------------------------ *)
    53 
    54 qed_goal "contlub_cfun_fun" thy 
    55 "chain(FY) ==>\
    56 \ lub(range FY)`x = lub(range (%i. FY(i)`x))"
    57 (fn prems =>
    58         [
    59         (cut_facts_tac prems 1),
    60         (rtac trans 1),
    61         (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1),
    62         (stac thelub_fun 1),
    63         (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1),
    64         (rtac refl 1)
    65         ]);
    66 
    67 
    68 qed_goal "cont_cfun_fun" thy 
    69 "chain(FY) ==>\
    70 \ range(%i. FY(i)`x) <<| lub(range FY)`x"
    71 (fn prems =>
    72         [
    73         (cut_facts_tac prems 1),
    74         (rtac thelubE 1),
    75         (etac ch2ch_Rep_CFunL 1),
    76         (etac (contlub_cfun_fun RS sym) 1)
    77         ]);
    78 
    79 
    80 (* ------------------------------------------------------------------------ *)
    81 (* contlub, cont  properties of Rep_CFun in both argument in mixfix _[_]       *)
    82 (* ------------------------------------------------------------------------ *)
    83 
    84 qed_goal "contlub_cfun" thy 
    85 "[|chain(FY);chain(TY)|] ==>\
    86 \ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
    87 (fn prems =>
    88         [
    89         (cut_facts_tac prems 1),
    90         (rtac contlub_CF2 1),
    91         (rtac cont_Rep_CFun1 1),
    92         (rtac allI 1),
    93         (rtac cont_Rep_CFun2 1),
    94         (atac 1),
    95         (atac 1)
    96         ]);
    97 
    98 qed_goal "cont_cfun" thy 
    99 "[|chain(FY);chain(TY)|] ==>\
   100 \ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
   101 (fn prems =>
   102         [
   103         (cut_facts_tac prems 1),
   104         (rtac thelubE 1),
   105         (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1),
   106         (rtac allI 1),
   107         (rtac monofun_Rep_CFun2 1),
   108         (atac 1),
   109         (atac 1),
   110         (etac (contlub_cfun RS sym) 1),
   111         (atac 1)
   112         ]);
   113 
   114 
   115 (* ------------------------------------------------------------------------ *)
   116 (* cont2cont lemma for Rep_CFun                                               *)
   117 (* ------------------------------------------------------------------------ *)
   118 
   119 qed_goal "cont2cont_Rep_CFun" thy 
   120         "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
   121  (fn prems =>
   122         [
   123         (cut_facts_tac prems 1),
   124         (rtac cont2cont_app2 1),
   125         (rtac cont2cont_app2 1),
   126         (rtac cont_const 1),
   127         (rtac cont_Rep_CFun1 1),
   128         (atac 1),
   129         (rtac cont_Rep_CFun2 1),
   130         (atac 1)
   131         ]);
   132 
   133 
   134 
   135 (* ------------------------------------------------------------------------ *)
   136 (* cont2mono Lemma for %x. LAM y. c1(x)(y)                                  *)
   137 (* ------------------------------------------------------------------------ *)
   138 
   139 qed_goal "cont2mono_LAM" thy 
   140  "[| !!x. cont(c1 x); !!y. monofun(%x. c1 x y)|] ==> monofun(%x. LAM y. c1 x y)"
   141 (fn [p1,p2] =>
   142         [
   143         (rtac monofunI 1),
   144         (strip_tac 1),
   145         (stac less_cfun 1),
   146         (stac less_fun 1),
   147         (rtac allI 1),
   148         (stac beta_cfun 1),
   149 	(rtac p1 1),
   150         (stac beta_cfun 1),
   151 	(rtac p1 1),
   152         (etac (p2 RS monofunE RS spec RS spec RS mp) 1)
   153         ]);
   154 
   155 (* ------------------------------------------------------------------------ *)
   156 (* cont2cont Lemma for %x. LAM y. c1 x y)                                 *)
   157 (* ------------------------------------------------------------------------ *)
   158 
   159 qed_goal "cont2cont_LAM" thy 
   160  "[| !!x. cont(c1 x); !!y. cont(%x. c1 x y) |] ==> cont(%x. LAM y. c1 x y)"
   161 (fn [p1,p2] =>
   162         [
   163         (rtac monocontlub2cont 1),
   164         (rtac (p1 RS cont2mono_LAM) 1),
   165         (rtac (p2 RS cont2mono) 1),
   166         (rtac contlubI 1),
   167         (strip_tac 1),
   168         (stac thelub_cfun 1),
   169         (rtac (p1 RS cont2mono_LAM RS ch2ch_monofun) 1),
   170         (rtac (p2 RS cont2mono) 1),
   171         (atac 1),
   172         (res_inst_tac [("f","Abs_CFun")] arg_cong 1),
   173         (rtac ext 1),
   174         (stac (p1 RS beta_cfun RS ext) 1),
   175         (etac (p2 RS cont2contlub RS contlubE RS spec RS mp) 1)
   176         ]);
   177 
   178 (* ------------------------------------------------------------------------ *)
   179 (* cont2cont tactic                                                       *)
   180 (* ------------------------------------------------------------------------ *)
   181 
   182 val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2,
   183                     cont2cont_Rep_CFun,cont2cont_LAM];
   184 
   185 Addsimps cont_lemmas1;
   186 
   187 (* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
   188 
   189 (*val cont_tac = (fn i => (resolve_tac cont_lemmas i));*)
   190 (*val cont_tacR = (fn i => (REPEAT (cont_tac i)));*)
   191 
   192 (* ------------------------------------------------------------------------ *)
   193 (* function application _[_]  is strict in its first arguments              *)
   194 (* ------------------------------------------------------------------------ *)
   195 
   196 qed_goal "strict_Rep_CFun1" thy "(UU::'a::cpo->'b)`x = (UU::'b)"
   197  (fn prems =>
   198         [
   199         (stac inst_cfun_pcpo 1),
   200         (stac beta_cfun 1),
   201         (Simp_tac 1),
   202         (rtac refl 1)
   203         ]);
   204 
   205 
   206 (* ------------------------------------------------------------------------ *)
   207 (* results about strictify                                                  *)
   208 (* ------------------------------------------------------------------------ *)
   209 
   210 qed_goalw "Istrictify1" thy [Istrictify_def]
   211         "Istrictify(f)(UU)= (UU)"
   212  (fn prems =>
   213         [
   214         (Simp_tac 1)
   215         ]);
   216 
   217 qed_goalw "Istrictify2" thy [Istrictify_def]
   218         "~x=UU ==> Istrictify(f)(x)=f`x"
   219  (fn prems =>
   220         [
   221         (cut_facts_tac prems 1),
   222         (Asm_simp_tac 1)
   223         ]);
   224 
   225 qed_goal "monofun_Istrictify1" thy "monofun(Istrictify)"
   226  (fn prems =>
   227         [
   228         (rtac monofunI 1),
   229         (strip_tac 1),
   230         (rtac (less_fun RS iffD2) 1),
   231         (strip_tac 1),
   232         (res_inst_tac [("Q","xa=UU")] (excluded_middle RS disjE) 1),
   233         (stac Istrictify2 1),
   234         (atac 1),
   235         (stac Istrictify2 1),
   236         (atac 1),
   237         (rtac monofun_cfun_fun 1),
   238         (atac 1),
   239         (hyp_subst_tac 1),
   240         (stac Istrictify1 1),
   241         (stac Istrictify1 1),
   242         (rtac refl_less 1)
   243         ]);
   244 
   245 qed_goal "monofun_Istrictify2" thy "monofun(Istrictify(f))"
   246  (fn prems =>
   247         [
   248         (rtac monofunI 1),
   249         (strip_tac 1),
   250         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   251         (stac Istrictify2 1),
   252         (etac notUU_I 1),
   253         (atac 1),
   254         (stac Istrictify2 1),
   255         (atac 1),
   256         (rtac monofun_cfun_arg 1),
   257         (atac 1),
   258         (hyp_subst_tac 1),
   259         (stac Istrictify1 1),
   260         (rtac minimal 1)
   261         ]);
   262 
   263 
   264 qed_goal "contlub_Istrictify1" thy "contlub(Istrictify)"
   265  (fn prems =>
   266         [
   267         (rtac contlubI 1),
   268         (strip_tac 1),
   269         (rtac (expand_fun_eq RS iffD2) 1),
   270         (strip_tac 1),
   271         (stac thelub_fun 1),
   272         (etac (monofun_Istrictify1 RS ch2ch_monofun) 1),
   273         (res_inst_tac [("Q","x=UU")] (excluded_middle RS disjE) 1),
   274         (stac Istrictify2 1),
   275         (atac 1),
   276         (stac (Istrictify2 RS ext) 1),
   277         (atac 1),
   278         (stac thelub_cfun 1),
   279         (atac 1),
   280         (stac beta_cfun 1),
   281         (rtac cont_lubcfun 1),
   282         (atac 1),
   283         (rtac refl 1),
   284         (hyp_subst_tac 1),
   285         (stac Istrictify1 1),
   286         (stac (Istrictify1 RS ext) 1),
   287         (rtac (chain_UU_I_inverse RS sym) 1),
   288         (rtac (refl RS allI) 1)
   289         ]);
   290 
   291 qed_goal "contlub_Istrictify2" thy "contlub(Istrictify(f::'a -> 'b))"
   292  (fn prems =>
   293         [
   294         (rtac contlubI 1),
   295         (strip_tac 1),
   296         (case_tac "lub(range(Y))=(UU::'a)" 1),
   297         (res_inst_tac [("t","lub(range(Y))")] subst 1),
   298         (rtac sym 1),
   299         (atac 1),
   300         (stac Istrictify1 1),
   301         (rtac sym 1),
   302         (rtac chain_UU_I_inverse 1),
   303         (strip_tac 1),
   304         (res_inst_tac [("t","Y(i)"),("s","UU::'a")] subst 1),
   305         (rtac sym 1),
   306         (rtac (chain_UU_I RS spec) 1),
   307         (atac 1),
   308         (atac 1),
   309         (rtac Istrictify1 1),
   310         (stac Istrictify2 1),
   311         (atac 1),
   312         (res_inst_tac [("s","lub(range(%i. f`(Y i)))")] trans 1),
   313         (rtac contlub_cfun_arg 1),
   314         (atac 1),
   315         (rtac lub_equal2 1),
   316         (rtac (chain_mono2 RS exE) 1),
   317         (atac 2),
   318         (rtac chain_UU_I_inverse2 1),
   319         (atac 1),
   320         (rtac exI 1),
   321         (strip_tac 1),
   322         (rtac (Istrictify2 RS sym) 1),
   323         (fast_tac HOL_cs 1),
   324         (rtac ch2ch_monofun 1),
   325         (rtac monofun_Rep_CFun2 1),
   326         (atac 1),
   327         (rtac ch2ch_monofun 1),
   328         (rtac monofun_Istrictify2 1),
   329         (atac 1)
   330         ]);
   331 
   332 
   333 bind_thm ("cont_Istrictify1", contlub_Istrictify1 RS 
   334         (monofun_Istrictify1 RS monocontlub2cont)); 
   335 
   336 bind_thm ("cont_Istrictify2", contlub_Istrictify2 RS 
   337         (monofun_Istrictify2 RS monocontlub2cont)); 
   338 
   339 
   340 qed_goalw "strictify1" thy [strictify_def] "strictify`f`UU=UU" (fn _ => [
   341         (stac beta_cfun 1),
   342          (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
   343 					cont2cont_CF1L]) 1),
   344         (stac beta_cfun 1),
   345         (rtac cont_Istrictify2 1),
   346         (rtac Istrictify1 1)
   347         ]);
   348 
   349 qed_goalw "strictify2" thy [strictify_def]
   350         "~x=UU ==> strictify`f`x=f`x"  (fn prems => [
   351         (stac beta_cfun 1),
   352          (simp_tac (simpset() addsimps [cont_Istrictify2,cont_Istrictify1,
   353 					cont2cont_CF1L]) 1),
   354         (stac beta_cfun 1),
   355         (rtac cont_Istrictify2 1),
   356         (rtac Istrictify2 1),
   357         (resolve_tac prems 1)
   358         ]);
   359 
   360 
   361 (* ------------------------------------------------------------------------ *)
   362 (* Instantiate the simplifier                                               *)
   363 (* ------------------------------------------------------------------------ *)
   364 
   365 Addsimps [minimal,refl_less,beta_cfun,strict_Rep_CFun1,strictify1, strictify2];
   366 
   367 
   368 (* ------------------------------------------------------------------------ *)
   369 (* use cont_tac as autotac.                                                *)
   370 (* ------------------------------------------------------------------------ *)
   371 
   372 (* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
   373 (*simpset_ref() := simpset() addsolver (K (DEPTH_SOLVE_1 o cont_tac));*)
   374 
   375 (* ------------------------------------------------------------------------ *)
   376 (* some lemmata for functions with flat/chfin domain/range types	    *)
   377 (* ------------------------------------------------------------------------ *)
   378 
   379 qed_goal "chfin_Rep_CFunR" thy 
   380     "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" 
   381 (fn prems => 
   382 	[
   383 	cut_facts_tac prems 1,
   384 	rtac allI 1,
   385 	stac contlub_cfun_fun 1,
   386 	 atac 1,
   387 	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_Rep_CFunL])1
   388 	]);
   389 
   390 (* ------------------------------------------------------------------------ *)
   391 (* continuous isomorphisms are strict                                       *)
   392 (* a prove for embedding projection pairs is similar                        *)
   393 (* ------------------------------------------------------------------------ *)
   394 
   395 qed_goal "iso_strict"  thy  
   396 "!!f g.[|!y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a) |] \
   397 \ ==> f`UU=UU & g`UU=UU"
   398  (fn prems =>
   399         [
   400         (rtac conjI 1),
   401         (rtac UU_I 1),
   402         (res_inst_tac [("s","f`(g`(UU::'b))"),("t","UU::'b")] subst 1),
   403         (etac spec 1),
   404         (rtac (minimal RS monofun_cfun_arg) 1),
   405         (rtac UU_I 1),
   406         (res_inst_tac [("s","g`(f`(UU::'a))"),("t","UU::'a")] subst 1),
   407         (etac spec 1),
   408         (rtac (minimal RS monofun_cfun_arg) 1)
   409         ]);
   410 
   411 
   412 qed_goal "isorep_defined" thy 
   413         "[|!x. rep`(abs`x)=x;!y. abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
   414  (fn prems =>
   415         [
   416         (cut_facts_tac prems 1),
   417         (etac swap 1),
   418         (dtac notnotD 1),
   419         (dres_inst_tac [("f","abs")] cfun_arg_cong 1),
   420         (etac box_equals 1),
   421         (fast_tac HOL_cs 1),
   422         (etac (iso_strict RS conjunct1) 1),
   423         (atac 1)
   424         ]);
   425 
   426 qed_goal "isoabs_defined" thy 
   427         "[|!x. rep`(abs`x) = x;!y. abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
   428  (fn prems =>
   429         [
   430         (cut_facts_tac prems 1),
   431         (etac swap 1),
   432         (dtac notnotD 1),
   433         (dres_inst_tac [("f","rep")] cfun_arg_cong 1),
   434         (etac box_equals 1),
   435         (fast_tac HOL_cs 1),
   436         (etac (iso_strict RS conjunct2) 1),
   437         (atac 1)
   438         ]);
   439 
   440 (* ------------------------------------------------------------------------ *)
   441 (* propagation of flatness and chainfiniteness by continuous isomorphisms   *)
   442 (* ------------------------------------------------------------------------ *)
   443 
   444 qed_goal "chfin2chfin" thy "!!f g.[|! Y::nat=>'a. chain Y --> (? n. max_in_chain n Y); \
   445 \ !y. f`(g`y)=(y::'b) ; !x. g`(f`x)=(x::'a::chfin) |] \
   446 \ ==> ! Y::nat=>'b. chain Y --> (? n. max_in_chain n Y)"
   447  (fn prems =>
   448         [
   449         (rewtac max_in_chain_def),
   450         (strip_tac 1),
   451         (rtac exE 1),
   452         (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1),
   453         (etac spec 1),
   454         (etac ch2ch_Rep_CFunR 1),
   455         (rtac exI 1),
   456         (strip_tac 1),
   457         (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1),
   458         (etac spec 1),
   459         (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1),
   460         (etac spec 1),
   461         (rtac cfun_arg_cong 1),
   462         (rtac mp 1),
   463         (etac spec 1),
   464         (atac 1)
   465         ]);
   466 
   467 
   468 qed_goal "flat2flat" thy "!!f g.[|!x y::'a. x<<y --> x=UU | x=y; \
   469 \ !y. f`(g`y)=(y::'b); !x. g`(f`x)=(x::'a)|] ==> !x y::'b. x<<y --> x=UU | x=y"
   470  (fn prems =>
   471         [
   472         (strip_tac 1),
   473         (rtac disjE 1),
   474         (res_inst_tac [("P","g`x<<g`y")] mp 1),
   475         (etac monofun_cfun_arg 2),
   476         (dtac spec 1),
   477         (etac spec 1),
   478         (rtac disjI1 1),
   479         (rtac trans 1),
   480         (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
   481         (etac spec 1),
   482         (etac cfun_arg_cong 1),
   483         (rtac (iso_strict RS conjunct1) 1),
   484         (atac 1),
   485         (atac 1),
   486         (rtac disjI2 1),
   487         (res_inst_tac [("s","f`(g`x)"),("t","x")] subst 1),
   488         (etac spec 1),
   489         (res_inst_tac [("s","f`(g`y)"),("t","y")] subst 1),
   490         (etac spec 1),
   491         (etac cfun_arg_cong 1)
   492         ]);
   493 
   494 (* ------------------------------------------------------------------------- *)
   495 (* a result about functions with flat codomain                               *)
   496 (* ------------------------------------------------------------------------- *)
   497 
   498 qed_goal "flat_codom" thy 
   499 "f`(x::'a)=(c::'b::flat) ==> f`(UU::'a)=(UU::'b) | (!z. f`(z::'a)=c)"
   500  (fn prems =>
   501         [
   502         (cut_facts_tac prems 1),
   503         (case_tac "f`(x::'a)=(UU::'b)" 1),
   504         (rtac disjI1 1),
   505         (rtac UU_I 1),
   506         (res_inst_tac [("s","f`(x)"),("t","UU::'b")] subst 1),
   507         (atac 1),
   508         (rtac (minimal RS monofun_cfun_arg) 1),
   509         (case_tac "f`(UU::'a)=(UU::'b)" 1),
   510         (etac disjI1 1),
   511         (rtac disjI2 1),
   512         (rtac allI 1),
   513         (hyp_subst_tac 1),
   514         (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
   515         (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS 
   516 		(ax_flat RS spec RS spec RS mp) RS disjE) 1),
   517 	(contr_tac 1),(atac 1),
   518         (res_inst_tac [("fo5","f")] ((minimal RS monofun_cfun_arg) RS 
   519 		(ax_flat RS spec RS spec RS mp) RS disjE) 1),
   520 	(contr_tac 1),(atac 1)
   521 ]);
   522 
   523 
   524 (* ------------------------------------------------------------------------ *)
   525 (* Access to definitions                                                    *)
   526 (* ------------------------------------------------------------------------ *)
   527 
   528 
   529 qed_goalw "ID1" thy [ID_def] "ID`x=x"
   530  (fn prems =>
   531         [
   532         (stac beta_cfun 1),
   533         (rtac cont_id 1),
   534         (rtac refl 1)
   535         ]);
   536 
   537 qed_goalw "cfcomp1" thy [oo_def] "(f oo g)=(LAM x. f`(g`x))" (fn _ => [
   538         (stac beta_cfun 1),
   539         (Simp_tac 1),
   540         (stac beta_cfun 1),
   541         (Simp_tac 1),
   542 	(rtac refl 1)
   543         ]);
   544 
   545 qed_goal "cfcomp2" thy  "(f oo g)`x=f`(g`x)" (fn _ => [
   546         (stac cfcomp1 1),
   547         (stac beta_cfun 1),
   548         (Simp_tac 1),
   549 	(rtac refl 1)
   550         ]);
   551 
   552 
   553 (* ------------------------------------------------------------------------ *)
   554 (* Show that interpretation of (pcpo,_->_) is a category                    *)
   555 (* The class of objects is interpretation of syntactical class pcpo         *)
   556 (* The class of arrows  between objects 'a and 'b is interpret. of 'a -> 'b *)
   557 (* The identity arrow is interpretation of ID                               *)
   558 (* The composition of f and g is interpretation of oo                       *)
   559 (* ------------------------------------------------------------------------ *)
   560 
   561 
   562 qed_goal "ID2" thy "f oo ID = f "
   563  (fn prems =>
   564         [
   565         (rtac ext_cfun 1),
   566         (stac cfcomp2 1),
   567         (stac ID1 1),
   568         (rtac refl 1)
   569         ]);
   570 
   571 qed_goal "ID3" thy "ID oo f = f "
   572  (fn prems =>
   573         [
   574         (rtac ext_cfun 1),
   575         (stac cfcomp2 1),
   576         (stac ID1 1),
   577         (rtac refl 1)
   578         ]);
   579 
   580 
   581 qed_goal "assoc_oo" thy "f oo (g oo h) = (f oo g) oo h"
   582  (fn prems =>
   583         [
   584         (rtac ext_cfun 1),
   585         (res_inst_tac [("s","f`(g`(h`x))")] trans  1),
   586         (stac cfcomp2 1),
   587         (stac cfcomp2 1),
   588         (rtac refl 1),
   589         (stac cfcomp2 1),
   590         (stac cfcomp2 1),
   591         (rtac refl 1)
   592         ]);
   593 
   594 (* ------------------------------------------------------------------------ *)
   595 (* Merge the different rewrite rules for the simplifier                     *)
   596 (* ------------------------------------------------------------------------ *)
   597 
   598 Addsimps ([ID1,ID2,ID3,cfcomp2]);
   599 
   600