eliminated fabs,fapp.
changed all theorem names and functions into Rep_CFun, Abs_CFun
--- 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),
--- 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\\<Lambda>_./ _)" [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
--- 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<<y"
(fn prems =>
[
- (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<<g|]==>fabs(f)<<fabs(g)"
+qed_goal "semi_monofun_Abs_CFun" thy
+ "[|cont(f);cont(g);f<<g|]==>Abs_CFun(f)<<Abs_CFun(g)"
(fn prems =>
[
(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)
--- 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),
--- 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]);
--- 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";
--- 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;
--- 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 *)
--- 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)
]);
--- 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),
--- 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]
--- 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(
--- 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)
--- 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;
--- 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;
--- 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),
--- 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))
]);