# HG changeset patch # User slotosch # Date 902917040 -7200 # Node ID 5706f0ef1d43102ae7f008fb4c3e6103d078adf1 # Parent b755c7240348914ed845e0fa7a7381e73c5a3984 eliminated fabs,fapp. changed all theorem names and functions into Rep_CFun, Abs_CFun diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun1.ML --- a/src/HOLCF/Cfun1.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Cfun1.ML Wed Aug 12 12:17:20 1998 +0200 @@ -9,22 +9,22 @@ open Cfun1; (* ------------------------------------------------------------------------ *) -(* derive old type definition rules for fabs & fapp *) -(* fapp and fabs should be replaced by Rep_Cfun anf Abs_Cfun in future *) +(* derive old type definition rules for Abs_CFun & Rep_CFun *) +(* Rep_CFun and Abs_CFun should be replaced by Rep_Cfun anf Abs_Cfun in future *) (* ------------------------------------------------------------------------ *) -qed_goalw "Rep_Cfun" thy [fapp_def] "fapp fo : CFun" +qed_goal "Rep_Cfun" thy "Rep_CFun fo : CFun" (fn prems => [ (rtac Rep_CFun 1) ]); -qed_goalw "Rep_Cfun_inverse" thy [fapp_def,fabs_def] "fabs (fapp fo) = fo" +qed_goal "Rep_Cfun_inverse" thy "Abs_CFun (Rep_CFun fo) = fo" (fn prems => [ (rtac Rep_CFun_inverse 1) ]); -qed_goalw "Abs_Cfun_inverse" thy [fapp_def,fabs_def] "f:CFun==>fapp(fabs f)=f" +qed_goal "Abs_Cfun_inverse" thy "f:CFun==>Rep_CFun(Abs_CFun f)=f" (fn prems => [ (cut_facts_tac prems 1), @@ -97,7 +97,7 @@ (* additional lemma about the isomorphism between -> and Cfun *) (* ------------------------------------------------------------------------ *) -qed_goal "Abs_Cfun_inverse2" thy "cont f ==> fapp (fabs f) = f" +qed_goal "Abs_Cfun_inverse2" thy "cont f ==> Rep_CFun (Abs_CFun f) = f" (fn prems => [ (cut_facts_tac prems 1), @@ -110,7 +110,7 @@ (* simplification of application *) (* ------------------------------------------------------------------------ *) -qed_goal "Cfunapp2" thy "cont f ==> (fabs f)`x = f x" +qed_goal "Cfunapp2" thy "cont f ==> (Abs_CFun f)`x = f x" (fn prems => [ (cut_facts_tac prems 1), diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun1.thy --- a/src/HOLCF/Cfun1.thy Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Cfun1.thy Wed Aug 12 12:17:20 1998 +0200 @@ -16,12 +16,10 @@ (* to make << defineable *) instance "->" :: (cpo,cpo)sq_ord -consts - fapp :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999) - (* usually Rep_Cfun *) +syntax + Rep_CFun :: "('a -> 'b)=>('a => 'b)" ("_`_" [999,1000] 999) (* application *) - fabs :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10) - (* usually Abs_Cfun *) + Abs_CFun :: "('a => 'b)=>('a -> 'b)" (binder "LAM " 10) (* abstraction *) less_cfun :: "[('a -> 'b),('a -> 'b)]=>bool" @@ -30,9 +28,6 @@ "LAM " :: "[idts, 'a => 'b] => ('a -> 'b)" ("(3\\_./ _)" [0, 10] 10) defs - fabs_def "fabs==Abs_CFun" - fapp_def "fapp==Rep_CFun" - - less_cfun_def "(op <<) == (% fo1 fo2. fapp fo1 << fapp fo2 )" + less_cfun_def "(op <<) == (% fo1 fo2. Rep_CFun fo1 << Rep_CFun fo2 )" end diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun2.ML --- a/src/HOLCF/Cfun2.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Cfun2.ML Wed Aug 12 12:17:20 1998 +0200 @@ -9,7 +9,7 @@ open Cfun2; (* for compatibility with old HOLCF-Version *) -qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. fapp f1 << fapp f2)" +qed_goal "inst_cfun_po" thy "(op <<)=(%f1 f2. Rep_CFun f1 << Rep_CFun f2)" (fn prems => [ (fold_goals_tac [less_cfun_def]), @@ -20,7 +20,7 @@ (* access to less_cfun in class po *) (* ------------------------------------------------------------------------ *) -qed_goal "less_cfun" thy "( f1 << f2 ) = (fapp(f1) << fapp(f2))" +qed_goal "less_cfun" thy "( f1 << f2 ) = (Rep_CFun(f1) << Rep_CFun(f2))" (fn prems => [ (simp_tac (simpset() addsimps [inst_cfun_po]) 1) @@ -30,7 +30,7 @@ (* Type 'a ->'b is pointed *) (* ------------------------------------------------------------------------ *) -qed_goal "minimal_cfun" thy "fabs(% x. UU) << f" +qed_goal "minimal_cfun" thy "Abs_CFun(% x. UU) << f" (fn prems => [ (stac less_cfun 1), @@ -44,17 +44,17 @@ qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y. x< [ - (res_inst_tac [("x","fabs(% x. UU)")] exI 1), + (res_inst_tac [("x","Abs_CFun(% x. UU)")] exI 1), (rtac (minimal_cfun RS allI) 1) ]); (* ------------------------------------------------------------------------ *) -(* fapp yields continuous functions in 'a => 'b *) -(* this is continuity of fapp in its 'second' argument *) -(* cont_fapp2 ==> monofun_fapp2 & contlub_fapp2 *) +(* Rep_CFun yields continuous functions in 'a => 'b *) +(* this is continuity of Rep_CFun in its 'second' argument *) +(* cont_Rep_CFun2 ==> monofun_Rep_CFun2 & contlub_Rep_CFun2 *) (* ------------------------------------------------------------------------ *) -qed_goal "cont_fapp2" thy "cont(fapp(fo))" +qed_goal "cont_Rep_CFun2" thy "cont(Rep_CFun(fo))" (fn prems => [ (res_inst_tac [("P","cont")] CollectD 1), @@ -62,30 +62,30 @@ (rtac Rep_Cfun 1) ]); -bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono); -(* monofun(fapp(?fo1)) *) +bind_thm ("monofun_Rep_CFun2", cont_Rep_CFun2 RS cont2mono); +(* monofun(Rep_CFun(?fo1)) *) -bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub); -(* contlub(fapp(?fo1)) *) +bind_thm ("contlub_Rep_CFun2", cont_Rep_CFun2 RS cont2contlub); +(* contlub(Rep_CFun(?fo1)) *) (* ------------------------------------------------------------------------ *) -(* expanded thms cont_fapp2, contlub_fapp2 *) +(* expanded thms cont_Rep_CFun2, contlub_Rep_CFun2 *) (* looks nice with mixfix syntac *) (* ------------------------------------------------------------------------ *) -bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp)); +bind_thm ("cont_cfun_arg", (cont_Rep_CFun2 RS contE RS spec RS mp)); (* chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1)) *) -bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp)); +bind_thm ("contlub_cfun_arg", (contlub_Rep_CFun2 RS contlubE RS spec RS mp)); (* chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *) (* ------------------------------------------------------------------------ *) -(* fapp is monotone in its 'first' argument *) +(* Rep_CFun is monotone in its 'first' argument *) (* ------------------------------------------------------------------------ *) -qed_goalw "monofun_fapp1" thy [monofun] "monofun(fapp)" +qed_goalw "monofun_Rep_CFun1" thy [monofun] "monofun(Rep_CFun)" (fn prems => [ (strip_tac 1), @@ -94,7 +94,7 @@ (* ------------------------------------------------------------------------ *) -(* monotonicity of application fapp in mixfix syntax [_]_ *) +(* monotonicity of application Rep_CFun in mixfix syntax [_]_ *) (* ------------------------------------------------------------------------ *) qed_goal "monofun_cfun_fun" thy "f1 << f2 ==> f1`x << f2`x" @@ -103,15 +103,15 @@ (cut_facts_tac prems 1), (res_inst_tac [("x","x")] spec 1), (rtac (less_fun RS subst) 1), - (etac (monofun_fapp1 RS monofunE RS spec RS spec RS mp) 1) + (etac (monofun_Rep_CFun1 RS monofunE RS spec RS spec RS mp) 1) ]); -bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp); +bind_thm ("monofun_cfun_arg", monofun_Rep_CFun2 RS monofunE RS spec RS spec RS mp); (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1 *) (* ------------------------------------------------------------------------ *) -(* monotonicity of fapp in both arguments in mixfix syntax [_]_ *) +(* monotonicity of Rep_CFun in both arguments in mixfix syntax [_]_ *) (* ------------------------------------------------------------------------ *) qed_goal "monofun_cfun" thy @@ -137,16 +137,16 @@ (* use MF2 lemmas from Cont.ML *) (* ------------------------------------------------------------------------ *) -qed_goal "ch2ch_fappR" thy +qed_goal "ch2ch_Rep_CFunR" thy "chain(Y) ==> chain(%i. f`(Y i))" (fn prems => [ (cut_facts_tac prems 1), - (etac (monofun_fapp2 RS ch2ch_MF2R) 1) + (etac (monofun_Rep_CFun2 RS ch2ch_MF2R) 1) ]); -bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L); +bind_thm ("ch2ch_Rep_CFunL", monofun_Rep_CFun1 RS ch2ch_MF2L); (* chain(?F) ==> chain (%i. ?F i`?x) *) @@ -161,8 +161,8 @@ [ (cut_facts_tac prems 1), (rtac lub_MF2_mono 1), - (rtac monofun_fapp1 1), - (rtac (monofun_fapp2 RS allI) 1), + (rtac monofun_Rep_CFun1 1), + (rtac (monofun_Rep_CFun2 RS allI) 1), (atac 1) ]); @@ -179,8 +179,8 @@ [ (cut_facts_tac prems 1), (rtac ex_lubMF2 1), - (rtac monofun_fapp1 1), - (rtac (monofun_fapp2 RS allI) 1), + (rtac monofun_Rep_CFun1 1), + (rtac (monofun_Rep_CFun2 RS allI) 1), (atac 1), (atac 1) ]); @@ -221,14 +221,14 @@ (stac Abs_Cfun_inverse2 1), (etac cont_lubcfun 1), (rtac (lub_fun RS is_lubE RS conjunct1 RS ub_rangeE RS spec) 1), - (etac (monofun_fapp1 RS ch2ch_monofun) 1), + (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1), (strip_tac 1), (stac less_cfun 1), (stac Abs_Cfun_inverse2 1), (etac cont_lubcfun 1), (rtac (lub_fun RS is_lubE RS conjunct2 RS spec RS mp) 1), - (etac (monofun_fapp1 RS ch2ch_monofun) 1), - (etac (monofun_fapp1 RS ub2ub_monofun) 1) + (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1), + (etac (monofun_Rep_CFun1 RS ub2ub_monofun) 1) ]); bind_thm ("thelub_cfun", lub_cfun RS thelubI); @@ -255,17 +255,17 @@ [ (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), - (res_inst_tac [("f","fabs")] arg_cong 1), + (res_inst_tac [("f","Abs_CFun")] arg_cong 1), (rtac ext 1), (resolve_tac prems 1) ]); (* ------------------------------------------------------------------------ *) -(* Monotonicity of fabs *) +(* Monotonicity of Abs_CFun *) (* ------------------------------------------------------------------------ *) -qed_goal "semi_monofun_fabs" thy - "[|cont(f);cont(g);f<fabs(f)<Abs_CFun(f)< [ (rtac (less_cfun RS iffD2) 1), @@ -285,9 +285,9 @@ [ (res_inst_tac [("t","f")] (Rep_Cfun_inverse RS subst) 1), (res_inst_tac [("t","g")] (Rep_Cfun_inverse RS subst) 1), - (rtac semi_monofun_fabs 1), - (rtac cont_fapp2 1), - (rtac cont_fapp2 1), + (rtac semi_monofun_Abs_CFun 1), + (rtac cont_Rep_CFun2 1), + (rtac cont_Rep_CFun2 1), (rtac (less_fun RS iffD2) 1), (rtac allI 1), (resolve_tac prems 1) diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Cfun3.ML --- a/src/HOLCF/Cfun3.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Cfun3.ML Wed Aug 12 12:17:20 1998 +0200 @@ -7,17 +7,17 @@ open Cfun3; (* for compatibility with old HOLCF-Version *) -qed_goal "inst_cfun_pcpo" thy "UU = fabs(%x. UU)" +qed_goal "inst_cfun_pcpo" thy "UU = Abs_CFun(%x. UU)" (fn prems => [ (simp_tac (HOL_ss addsimps [UU_def,UU_cfun_def]) 1) ]); (* ------------------------------------------------------------------------ *) -(* the contlub property for fapp its 'first' argument *) +(* the contlub property for Rep_CFun its 'first' argument *) (* ------------------------------------------------------------------------ *) -qed_goal "contlub_fapp1" thy "contlub(fapp)" +qed_goal "contlub_Rep_CFun1" thy "contlub(Rep_CFun)" (fn prems => [ (rtac contlubI 1), @@ -29,26 +29,26 @@ (stac Cfunapp2 1), (etac cont_lubcfun 1), (stac thelub_fun 1), - (etac (monofun_fapp1 RS ch2ch_monofun) 1), + (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1), (rtac refl 1) ]); (* ------------------------------------------------------------------------ *) -(* the cont property for fapp in its first argument *) +(* the cont property for Rep_CFun in its first argument *) (* ------------------------------------------------------------------------ *) -qed_goal "cont_fapp1" thy "cont(fapp)" +qed_goal "cont_Rep_CFun1" thy "cont(Rep_CFun)" (fn prems => [ (rtac monocontlub2cont 1), - (rtac monofun_fapp1 1), - (rtac contlub_fapp1 1) + (rtac monofun_Rep_CFun1 1), + (rtac contlub_Rep_CFun1 1) ]); (* ------------------------------------------------------------------------ *) -(* contlub, cont properties of fapp in its first argument in mixfix _[_] *) +(* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_] *) (* ------------------------------------------------------------------------ *) qed_goal "contlub_cfun_fun" thy @@ -58,9 +58,9 @@ [ (cut_facts_tac prems 1), (rtac trans 1), - (etac (contlub_fapp1 RS contlubE RS spec RS mp RS fun_cong) 1), + (etac (contlub_Rep_CFun1 RS contlubE RS spec RS mp RS fun_cong) 1), (stac thelub_fun 1), - (etac (monofun_fapp1 RS ch2ch_monofun) 1), + (etac (monofun_Rep_CFun1 RS ch2ch_monofun) 1), (rtac refl 1) ]); @@ -72,13 +72,13 @@ [ (cut_facts_tac prems 1), (rtac thelubE 1), - (etac ch2ch_fappL 1), + (etac ch2ch_Rep_CFunL 1), (etac (contlub_cfun_fun RS sym) 1) ]); (* ------------------------------------------------------------------------ *) -(* contlub, cont properties of fapp in both argument in mixfix _[_] *) +(* contlub, cont properties of Rep_CFun in both argument in mixfix _[_] *) (* ------------------------------------------------------------------------ *) qed_goal "contlub_cfun" thy @@ -88,9 +88,9 @@ [ (cut_facts_tac prems 1), (rtac contlub_CF2 1), - (rtac cont_fapp1 1), + (rtac cont_Rep_CFun1 1), (rtac allI 1), - (rtac cont_fapp2 1), + (rtac cont_Rep_CFun2 1), (atac 1), (atac 1) ]); @@ -102,9 +102,9 @@ [ (cut_facts_tac prems 1), (rtac thelubE 1), - (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1), + (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1), (rtac allI 1), - (rtac monofun_fapp2 1), + (rtac monofun_Rep_CFun2 1), (atac 1), (atac 1), (etac (contlub_cfun RS sym) 1), @@ -113,10 +113,10 @@ (* ------------------------------------------------------------------------ *) -(* cont2cont lemma for fapp *) +(* cont2cont lemma for Rep_CFun *) (* ------------------------------------------------------------------------ *) -qed_goal "cont2cont_fapp" thy +qed_goal "cont2cont_Rep_CFun" thy "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))" (fn prems => [ @@ -124,9 +124,9 @@ (rtac cont2cont_app2 1), (rtac cont2cont_app2 1), (rtac cont_const 1), - (rtac cont_fapp1 1), + (rtac cont_Rep_CFun1 1), (atac 1), - (rtac cont_fapp2 1), + (rtac cont_Rep_CFun2 1), (atac 1) ]); @@ -169,7 +169,7 @@ (rtac (p1 RS cont2mono_LAM RS ch2ch_monofun) 1), (rtac (p2 RS cont2mono) 1), (atac 1), - (res_inst_tac [("f","fabs")] arg_cong 1), + (res_inst_tac [("f","Abs_CFun")] arg_cong 1), (rtac ext 1), (stac (p1 RS beta_cfun RS ext) 1), (etac (p2 RS cont2contlub RS contlubE RS spec RS mp) 1) @@ -179,8 +179,8 @@ (* cont2cont tactic *) (* ------------------------------------------------------------------------ *) -val cont_lemmas1 = [cont_const, cont_id, cont_fapp2, - cont2cont_fapp,cont2cont_LAM]; +val cont_lemmas1 = [cont_const, cont_id, cont_Rep_CFun2, + cont2cont_Rep_CFun,cont2cont_LAM]; Addsimps cont_lemmas1; @@ -193,7 +193,7 @@ (* function application _[_] is strict in its first arguments *) (* ------------------------------------------------------------------------ *) -qed_goal "strict_fapp1" thy "(UU::'a::cpo->'b)`x = (UU::'b)" +qed_goal "strict_Rep_CFun1" thy "(UU::'a::cpo->'b)`x = (UU::'b)" (fn prems => [ (stac inst_cfun_pcpo 1), @@ -322,7 +322,7 @@ (rtac (Istrictify2 RS sym) 1), (fast_tac HOL_cs 1), (rtac ch2ch_monofun 1), - (rtac monofun_fapp2 1), + (rtac monofun_Rep_CFun2 1), (atac 1), (rtac ch2ch_monofun 1), (rtac monofun_Istrictify2 1), @@ -362,7 +362,7 @@ (* Instantiate the simplifier *) (* ------------------------------------------------------------------------ *) -Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2]; +Addsimps [minimal,refl_less,beta_cfun,strict_Rep_CFun1,strictify1, strictify2]; (* ------------------------------------------------------------------------ *) @@ -376,7 +376,7 @@ (* some lemmata for functions with flat/chfin domain/range types *) (* ------------------------------------------------------------------------ *) -qed_goal "chfin_fappR" thy +qed_goal "chfin_Rep_CFunR" thy "chain (Y::nat => 'a::cpo->'b::chfin)==> !s. ? n. lub(range(Y))`s = Y n`s" (fn prems => [ @@ -384,7 +384,7 @@ rtac allI 1, stac contlub_cfun_fun 1, atac 1, - fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1 + fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_Rep_CFunL])1 ]); (* ------------------------------------------------------------------------ *) @@ -451,7 +451,7 @@ (rtac exE 1), (res_inst_tac [("P","chain(%i. g`(Y i))")] mp 1), (etac spec 1), - (etac ch2ch_fappR 1), + (etac ch2ch_Rep_CFunR 1), (rtac exI 1), (strip_tac 1), (res_inst_tac [("s","f`(g`(Y x))"),("t","Y(x)")] subst 1), diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Fix.ML --- a/src/HOLCF/Fix.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Fix.ML Wed Aug 12 12:17:20 1998 +0200 @@ -65,13 +65,13 @@ (rtac antisym_less 1), (rtac lub_mono 1), (rtac chain_iterate 1), - (rtac ch2ch_fappR 1), + (rtac ch2ch_Rep_CFunR 1), (rtac chain_iterate 1), (rtac allI 1), (rtac (iterate_Suc RS subst) 1), (rtac (chain_iterate RS chainE RS spec) 1), (rtac is_lub_thelub 1), - (rtac ch2ch_fappR 1), + (rtac ch2ch_Rep_CFunR 1), (rtac chain_iterate 1), (rtac ub_rangeI 1), (rtac allI 1), @@ -120,7 +120,7 @@ (* ------------------------------------------------------------------------ *) (* the following lemma uses contlub_cfun which itself is based on a *) (* diagonalisation lemma for continuous functions with two arguments. *) -(* In this special case it is the application function fapp *) +(* In this special case it is the application function Rep_CFun *) (* ------------------------------------------------------------------------ *) qed_goalw "contlub_iterate" thy [contlub] "contlub(iterate(i))" @@ -138,9 +138,9 @@ (rtac (less_fun RS iffD2) 1), (rtac allI 1), (rtac (chainE RS spec) 1), - (rtac (monofun_fapp1 RS ch2ch_MF2LR) 1), + (rtac (monofun_Rep_CFun1 RS ch2ch_MF2LR) 1), (rtac allI 1), - (rtac monofun_fapp2 1), + (rtac monofun_Rep_CFun2 1), (atac 1), (rtac ch2ch_fun 1), (rtac (monofun_iterate RS ch2ch_monofun) 1), @@ -547,7 +547,7 @@ qed_goalw "adm_chfindom" thy [adm_def] "adm (%(u::'a::cpo->'b::chfin). P(u`s))" (fn _ => [ strip_tac 1, - dtac chfin_fappR 1, + dtac chfin_Rep_CFunR 1, eres_inst_tac [("x","s")] allE 1, fast_tac (HOL_cs addss (simpset() addsimps [chfin])) 1]); diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/IOA/meta_theory/Sequence.ML --- a/src/HOLCF/IOA/meta_theory/Sequence.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML Wed Aug 12 12:17:20 1998 +0200 @@ -924,8 +924,8 @@ by (stac contlub_cfun_fun 1); by (rtac chain_iterate 1); by (rtac lub_mono 1); -by (rtac (chain_iterate RS ch2ch_fappL) 1); -by (rtac (chain_iterate RS ch2ch_fappL) 1); +by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1); +by (rtac (chain_iterate RS ch2ch_Rep_CFunL) 1); by (rtac allI 1); by (resolve_tac prems 1); qed"take_lemma_less1"; diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Lift.ML --- a/src/HOLCF/Lift.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Lift.ML Wed Aug 12 12:17:20 1998 +0200 @@ -58,7 +58,7 @@ val cont_lemmas_ext = [cont_flift1_arg,cont_flift2_arg, cont_flift1_arg_and_not_arg,cont2cont_CF1L_rev2, - cont_fapp_app,cont_fapp_app_app,cont_if]; + cont_Rep_CFun_app,cont_Rep_CFun_app_app,cont_if]; val cont_lemmas2 = cont_lemmas1 @ cont_lemmas_ext; diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Lift3.ML --- a/src/HOLCF/Lift3.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Lift3.ML Wed Aug 12 12:17:20 1998 +0200 @@ -143,13 +143,13 @@ by (rtac cont2cont_CF1L 1); by (REPEAT (resolve_tac cont_lemmas1 1)); by Auto_tac; -qed"cont_fapp_app"; +qed"cont_Rep_CFun_app"; Goal "[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)"; by (rtac cont2cont_CF1L 1); -by (etac cont_fapp_app 1); +by (etac cont_Rep_CFun_app 1); by (assume_tac 1); -qed"cont_fapp_app_app"; +qed"cont_Rep_CFun_app_app"; (* continuity of if then else *) diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Ssum3.ML --- a/src/HOLCF/Ssum3.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Ssum3.ML Wed Aug 12 12:17:20 1998 +0200 @@ -262,7 +262,7 @@ (atac 1), (fast_tac HOL_cs 1), (simp_tac (simpset_of Cfun3.thy) 1), - (rtac (monofun_fapp2 RS ch2ch_monofun) 1), + (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1), (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), (etac (monofun_Iwhen3 RS ch2ch_monofun) 1) ]); @@ -326,7 +326,7 @@ (atac 1), (fast_tac HOL_cs 1), (simp_tac (simpset_of Cfun3.thy) 1), - (rtac (monofun_fapp2 RS ch2ch_monofun) 1), + (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 1), (etac (monofun_Iwhen3 RS ch2ch_monofun) 1), (etac (monofun_Iwhen3 RS ch2ch_monofun) 1) ]); diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/Up3.ML --- a/src/HOLCF/Up3.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/Up3.ML Wed Aug 12 12:17:20 1998 +0200 @@ -110,7 +110,7 @@ (stac contlub_cfun_arg 1), (etac (monofun_Ifup2 RS ch2ch_monofun) 1), (rtac lub_equal2 1), - (rtac (monofun_fapp2 RS ch2ch_monofun) 2), + (rtac (monofun_Rep_CFun2 RS ch2ch_monofun) 2), (etac (monofun_Ifup2 RS ch2ch_monofun) 2), (etac (monofun_Ifup2 RS ch2ch_monofun) 2), (rtac (chain_mono2 RS exE) 1), diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/cont_consts.ML --- a/src/HOLCF/cont_consts.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/cont_consts.ML Wed Aug 12 12:17:20 1998 +0200 @@ -35,7 +35,7 @@ val vnames = argnames (ord "A") n; val extra_parse_rule = Syntax.ParseRule (Constant name2, Constant name1); in [Syntax.ParsePrintRule (Ast.mk_appl (Constant name2) (map Variable vnames), - foldl (fn (t,arg) => (Ast.mk_appl (Constant "fapp") + foldl (fn (t,arg) => (Ast.mk_appl (Constant "Rep_CFun") [t,Variable arg])) (Constant name1,vnames))] @(case mx of InfixlName _ => [extra_parse_rule] diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/domain/axioms.ML Wed Aug 12 12:17:20 1998 +0200 @@ -57,14 +57,14 @@ val dis_defs = let fun ddef (con,_) = (dis_name con ^"_def",%%(dis_name con) == - mk_cfapp(%%(dname^"_when"),map + mk_cRep_CFun(%%(dname^"_when"),map (fn (con',args) => (foldr /\# (args,if con'=con then %%"TT" else %%"FF"))) cons)) in map ddef cons end; val sel_defs = let fun sdef con n arg = (sel_of arg^"_def",%%(sel_of arg) == - mk_cfapp(%%(dname^"_when"),map + mk_cRep_CFun(%%(dname^"_when"),map (fn (con',args) => if con'<>con then %%"UU" else foldr /\# (args,Bound (length args - n))) cons)); in flat(map (fn (con,args) => mapn (sdef con) 1 args) cons) end; @@ -116,8 +116,8 @@ fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); val capps = foldr mk_conj (mapn rel_app 1 rec_args, mk_conj( - Bound(allargs_cnt+1)===mk_cfapp(%%con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===mk_cfapp(%%con,map (bound_arg allvns) vns2))); + Bound(allargs_cnt+1)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===mk_cRep_CFun(%%con,map (bound_arg allvns) vns2))); in foldr mk_ex (allvns, foldr mk_conj (map (defined o Bound) nonlazy_idxs,capps)) end; fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp( diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/domain/library.ML Wed Aug 12 12:17:20 1998 +0200 @@ -145,11 +145,11 @@ infix 1 <<; fun S << T = %%"op <<" $ S $ T; infix 1 ~<<; fun S ~<< T = mk_not (S << T); -infix 9 ` ; fun f` x = %%"fapp" $ f $ x; +infix 9 ` ; fun f` x = %%"Rep_CFun" $ f $ x; infix 9 `% ; fun f`% s = f` % s; infix 9 `%%; fun f`%%s = f` %%s; -fun mk_cfapp (F,As) = foldl (op `) (F,As); -fun con_app2 con f args = mk_cfapp(%%con,map f args); +fun mk_cRep_CFun (F,As) = foldl (op `) (F,As); +fun con_app2 con f args = mk_cRep_CFun(%%con,map f args); fun con_app con = con_app2 con %#; fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg); @@ -166,7 +166,7 @@ T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs); fun lift tfn = foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); -fun /\ v T = %%"fabs" $ mk_lam(v,T); +fun /\ v T = %%"Abs_CFun" $ mk_lam(v,T); fun /\# (arg,T) = /\ (vname arg) T; infixr 9 oo; fun S oo T = %%"cfcomp"`S`T; val UU = %%"UU"; @@ -176,12 +176,12 @@ fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); -fun cont_eta_contract (Const("fabs",TT) $ Abs(a,T,body)) = +fun cont_eta_contract (Const("Abs_CFun",TT) $ Abs(a,T,body)) = (case cont_eta_contract body of - body' as (Const("fapp",Ta) $ f $ Bound 0) => + body' as (Const("Rep_CFun",Ta) $ f $ Bound 0) => if not (0 mem loose_bnos f) then incr_boundvars ~1 f - else Const("fabs",TT) $ Abs(a,T,body') - | body' => Const("fabs",TT) $ Abs(a,T,body')) + else Const("Abs_CFun",TT) $ Abs(a,T,body') + | body' => Const("Abs_CFun",TT) $ Abs(a,T,body')) | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t | cont_eta_contract t = t; @@ -197,7 +197,7 @@ in cont_eta_contract (foldr'' (fn (a,t) => %%"ssplit"`(/\# (a,t))) (args, - fn a=> /\#(a,(mk_cfapp(funarg(l2,n),mapn idxs 1 args)))) + fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args)))) ) end; in (if length cons = 1 andalso length(snd(hd cons)) <= 1 then fn t => %%"strictify"`t else Id) diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/syntax.ML --- a/src/HOLCF/domain/syntax.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/domain/syntax.ML Wed Aug 12 12:17:20 1998 +0200 @@ -71,7 +71,7 @@ (string_of_int m)); fun app s (l,r) = mk_appl (Constant s) [l,r]; fun case1 n (con,mx,args) = mk_appl (Constant "@case1") - [foldl (app "fapp") (c_ast con mx, (mapn (argvar n) 1 args)), + [foldl (app "Rep_CFun") (c_ast con mx, (mapn (argvar n) 1 args)), expvar n]; fun arg1 n (con,_,args) = if args = [] then expvar n else mk_appl (Constant "LAM ") @@ -81,8 +81,8 @@ (mk_appl (Constant "@case") [Variable "x", foldr' (fn (c,cs) => mk_appl (Constant"@case2") [c,cs]) (mapn case1 1 cons')], - mk_appl (Constant "fapp") [foldl - (fn (w,a ) => mk_appl (Constant"fapp" ) [w,a ]) + mk_appl (Constant "Rep_CFun") [foldl + (fn (w,a ) => mk_appl (Constant"Rep_CFun" ) [w,a ]) (Constant (dnam^"_when"),mapn arg1 1 cons'), Variable "x"]) end; diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/domain/theorems.ML Wed Aug 12 12:17:20 1998 +0200 @@ -41,7 +41,7 @@ asm_simp_tac (HOLCF_ss addsimps rews) i; val chain_tac = REPEAT_DETERM o resolve_tac - [chain_iterate, ch2ch_fappR, ch2ch_fappL]; + [chain_iterate, ch2ch_Rep_CFunR, ch2ch_Rep_CFunL]; (* ----- general proofs ----------------------------------------------------- *) @@ -175,7 +175,7 @@ val when_apps = let fun one_when n (con,args) = pg axs_con_def (bind_fun (lift_defined % (nonlazy args, mk_trp(when_app`(con_app con args) === - mk_cfapp(bound_fun n 0,map %# args)))))[ + mk_cRep_CFun(bound_fun n 0,map %# args)))))[ asm_simp_tac (HOLCF_ss addsimps [when_appl,ax_abs_iso]) 1]; in mapn one_when 1 cons end; end; diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/ex/Hoare.ML --- a/src/HOLCF/ex/Hoare.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/ex/Hoare.ML Wed Aug 12 12:17:20 1998 +0200 @@ -262,7 +262,7 @@ (rtac adm_eq 1), (cont_tacR 1), (rtac allI 1), - (stac strict_fapp1 1), + (stac strict_Rep_CFun1 1), (rtac refl 1), (Simp_tac 1), (rtac allI 1), @@ -295,7 +295,7 @@ (rtac adm_eq 1), (cont_tacR 1), (rtac allI 1), - (stac strict_fapp1 1), + (stac strict_Rep_CFun1 1), (rtac refl 1), (rtac allI 1), (Simp_tac 1), @@ -336,7 +336,7 @@ (rtac adm_eq 1), (cont_tacR 1), (rtac allI 1), - (stac strict_fapp1 1), + (stac strict_Rep_CFun1 1), (rtac refl 1), (rtac allI 1), (Simp_tac 1), diff -r b755c7240348 -r 5706f0ef1d43 src/HOLCF/ex/Stream.ML --- a/src/HOLCF/ex/Stream.ML Mon Aug 10 17:06:02 1998 +0200 +++ b/src/HOLCF/ex/Stream.ML Wed Aug 12 12:17:20 1998 +0200 @@ -77,7 +77,7 @@ qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [ stream_case_tac "s" 1, - ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews)) + ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_Rep_CFun1::stream.when_rews)) ]);