src/HOLCF/Cfun3.ML

 *)
 
 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                       *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "contlub_fapp1" thy "contlub(fapp)"
+(* the contlub property for Rep_CFun its 'first' argument                       *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "contlub_Rep_CFun1" thy "contlub(Rep_CFun)"
 (fn prems =>
         [
         (rtac contlubI 1),
         (strip_tac 1),
         (rtac (expand_fun_eq RS iffD2) 1),

         (stac thelub_cfun 1),
         (atac 1),
         (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                        *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "cont_fapp1" thy "cont(fapp)"
+(* the cont property for Rep_CFun in its first argument                        *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "cont_Rep_CFun1" thy "cont(Rep_CFun)"
 (fn prems =>
         [
         (rtac monocontlub2cont 1),
-        (rtac monofun_fapp1 1),
-        (rtac contlub_fapp1 1)
-        ]);
-
-
-(* ------------------------------------------------------------------------ *)
-(* contlub, cont properties of fapp in its first argument in mixfix _[_]   *)
+        (rtac monofun_Rep_CFun1 1),
+        (rtac contlub_Rep_CFun1 1)
+        ]);
+
+
+(* ------------------------------------------------------------------------ *)
+(* contlub, cont properties of Rep_CFun in its first argument in mixfix _[_]   *)
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "contlub_cfun_fun" thy 
 "chain(FY) ==>\
 \ lub(range FY)`x = lub(range (%i. FY(i)`x))"
 (fn prems =>
         [
         (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)
         ]);
 
 
 qed_goal "cont_cfun_fun" thy 

 \ range(%i. FY(i)`x) <<| lub(range FY)`x"
 (fn prems =>
         [
         (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 
 "[|chain(FY);chain(TY)|] ==>\
 \ (lub(range FY))`(lub(range TY)) = lub(range(%i. FY(i)`(TY i)))"
 (fn prems =>
         [
         (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)
         ]);
 
 qed_goal "cont_cfun" thy 

 \ range(%i.(FY i)`(TY i)) <<| (lub (range FY))`(lub(range TY))"
 (fn prems =>
         [
         (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),
         (atac 1)
         ]);
 
 
 (* ------------------------------------------------------------------------ *)
-(* cont2cont lemma for fapp                                               *)
-(* ------------------------------------------------------------------------ *)
-
-qed_goal "cont2cont_fapp" thy 
+(* cont2cont lemma for Rep_CFun                                               *)
+(* ------------------------------------------------------------------------ *)
+
+qed_goal "cont2cont_Rep_CFun" thy 
         "[|cont(%x. ft x);cont(%x. tt x)|] ==> cont(%x. (ft x)`(tt x))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac cont2cont_app2 1),
         (rtac cont2cont_app2 1),
         (rtac cont_const 1),
-        (rtac cont_fapp1 1),
-        (atac 1),
-        (rtac cont_fapp2 1),
+        (rtac cont_Rep_CFun1 1),
+        (atac 1),
+        (rtac cont_Rep_CFun2 1),
         (atac 1)
         ]);
 
 
 

         (strip_tac 1),
         (stac thelub_cfun 1),
         (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)
         ]);
 
 (* ------------------------------------------------------------------------ *)
 (* 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;
 
 (* HINT: cont_tac is now installed in simplifier in Lift.ML ! *)
 

 
 (* ------------------------------------------------------------------------ *)
 (* 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),
         (stac beta_cfun 1),
         (Simp_tac 1),

         (rtac exI 1),
         (strip_tac 1),
         (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),
         (atac 1)
         ]);

 
 (* ------------------------------------------------------------------------ *)
 (* Instantiate the simplifier                                               *)
 (* ------------------------------------------------------------------------ *)
 
-Addsimps [minimal,refl_less,beta_cfun,strict_fapp1,strictify1, strictify2];
+Addsimps [minimal,refl_less,beta_cfun,strict_Rep_CFun1,strictify1, strictify2];
 
 
 (* ------------------------------------------------------------------------ *)
 (* use cont_tac as autotac.                                                *)
 (* ------------------------------------------------------------------------ *)

 
 (* ------------------------------------------------------------------------ *)
 (* 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 => 
 	[
 	cut_facts_tac prems 1,
 	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
 	]);
 
 (* ------------------------------------------------------------------------ *)
 (* continuous isomorphisms are strict                                       *)
 (* a prove for embedding projection pairs is similar                        *)

         (rewtac max_in_chain_def),
         (strip_tac 1),
         (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),
         (etac spec 1),
         (res_inst_tac [("s","f`(g`(Y j))"),("t","Y(j)")] subst 1),