new term-building combinators
authorhuffman
Tue, 29 Jan 2008 18:00:12 +0100
changeset 26012 f6917792f8a4
parent 26011 d55224947082
child 26013 8764a1f1253b
new term-building combinators
src/HOLCF/Tools/domain/domain_axioms.ML
src/HOLCF/Tools/domain/domain_library.ML
src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jan 29 10:20:00 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jan 29 18:00:12 2008 +0100
@@ -44,11 +44,11 @@
 (* -- definitions concerning the constructors, discriminators and selectors - *)
 
   fun con_def m n (_,args) = let
-    fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x));
+    fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
     fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
     fun inj y 1 _ = y
-    |   inj y _ 0 = %%:sinlN`y
-    |   inj y i j = %%:sinrN`(inj y (i-1) (j-1));
+    |   inj y _ 0 = mk_sinl y
+    |   inj y i j = mk_sinr (inj y (i-1) (j-1));
   in foldr /\# (dc_abs`(inj (parms args) m n)) args end;
   
   val con_defs = mapn (fn n => fn (con,args) =>
@@ -58,7 +58,7 @@
 	fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
 		 list_ccomb(%%:(dname^"_when"),map 
 			(fn (con',args) => (foldr /\#
-			   (if con'=con then %%:TT_N else %%:FF_N) args)) cons))
+			   (if con'=con then TT else FF) args)) cons))
 	in map ddef cons end;
 
   val mat_defs = let
@@ -66,8 +66,8 @@
 		 list_ccomb(%%:(dname^"_when"),map 
 			(fn (con',args) => (foldr /\#
 			   (if con'=con
-                               then %%:returnN`(mk_ctuple (map (bound_arg args) args))
-                               else %%:failN) args)) cons))
+                               then mk_return (mk_ctuple (map (bound_arg args) args))
+                               else mk_fail) args)) cons))
 	in map mdef cons end;
 
   val pat_defs =
@@ -77,9 +77,9 @@
           val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
           val xs = map (bound_arg args) args;
           val r = Bound (length args);
-          val rhs = case args of [] => %%:returnN ` HOLogic.unit
-                                | _ => foldr1 cpair_pat ps ` mk_ctuple xs;
-          fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args';
+          val rhs = case args of [] => mk_return HOLogic.unit
+                                | _ => mk_ctuple_pat ps ` mk_ctuple xs;
+          fun one_con (con',args') = foldr /\# (if con'=con then rhs else mk_fail) args';
         in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
                list_ccomb(%%:(dname^"_when"), map one_con cons))
         end
@@ -95,10 +95,10 @@
 
 (* ----- axiom and definitions concerning induction ------------------------- *)
 
-  val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
+  val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
 					`%x_name === %:x_name));
   val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj
-	     (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
+	     (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
   val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
 	mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
@@ -125,7 +125,7 @@
   val x_name = idx_name dnames "x"; 
   fun copy_app dname = %%:(dname^"_copy")`Bound 0;
   val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
-				    /\"f"(foldr1 cpair (map copy_app dnames)));
+				    /\"f"(mk_ctuple (map copy_app dnames)));
   val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
     let
       fun one_con (con,args) = let
--- a/src/HOLCF/Tools/domain/domain_library.ML	Tue Jan 29 10:20:00 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_library.ML	Tue Jan 29 18:00:12 2008 +0100
@@ -97,44 +97,6 @@
 fun nonlazy     args   = map vname (filter_out is_lazy    args);
 fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
 
-(* ----- qualified names of HOLCF constants ----- *)
-
-val lessN      = @{const_name Porder.sq_le};
-val UU_N       = "Pcpo.UU";
-val admN       = "Adm.adm";
-val compactN   = "Adm.compact";
-val Rep_CFunN  = "Cfun.Rep_CFun";
-val Abs_CFunN  = "Cfun.Abs_CFun";
-val ID_N       = "Cfun.ID";
-val cfcompN    = "Cfun.cfcomp";
-val strictifyN = "Cfun.strictify";
-val cpairN     = "Cprod.cpair";
-val cfstN      = "Cprod.cfst";
-val csndN      = "Cprod.csnd";
-val csplitN    = "Cprod.csplit";
-val spairN     = "Sprod.spair";
-val sfstN      = "Sprod.sfst";
-val ssndN      = "Sprod.ssnd";
-val ssplitN    = "Sprod.ssplit";
-val sinlN      = "Ssum.sinl";
-val sinrN      = "Ssum.sinr";
-val sscaseN    = "Ssum.sscase";
-val upN        = "Up.up";
-val fupN       = "Up.fup";
-val ONE_N      = "One.ONE";
-val TT_N       = "Tr.TT";
-val FF_N       = "Tr.FF";
-val iterateN   = "Fix.iterate";
-val fixN       = "Fix.fix";
-val returnN    = "Fixrec.return";
-val failN      = "Fixrec.fail";
-val cpair_patN = "Fixrec.cpair_pat";
-val branchN    = "Fixrec.branch";
-
-val pcpoN      = "Pcpo.pcpo"
-val pcpoS      = [pcpoN];
-
-
 (* ----- support for type and mixfix expressions ----- *)
 
 infixr 5 -->;
@@ -164,12 +126,40 @@
 infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
 infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
 infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
-infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
+infix 1 <<;     fun S <<  T = %%:@{const_name Porder.sq_le} $ S $ T;
 infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
 
-infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
+infix 9 `  ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x;
 infix 9 `% ; fun f`% s = f` %: s;
 infix 9 `%%; fun f`%%s = f` %%:s;
+
+fun mk_adm t = %%:@{const_name adm} $ t;
+fun mk_compact t = %%:@{const_name compact} $ t;
+val ID = %%:@{const_name ID};
+fun mk_strictify t = %%:@{const_name strictify}`t;
+fun mk_cfst t = %%:@{const_name cfst}`t;
+fun mk_csnd t = %%:@{const_name csnd}`t;
+(*val csplitN    = "Cprod.csplit";*)
+(*val sfstN      = "Sprod.sfst";*)
+(*val ssndN      = "Sprod.ssnd";*)
+fun mk_ssplit t = %%:@{const_name ssplit}`t;
+fun mk_sinl t = %%:@{const_name sinl}`t;
+fun mk_sinr t = %%:@{const_name sinr}`t;
+fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y;
+fun mk_up t = %%:@{const_name up}`t;
+fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u;
+val ONE = @{term ONE};
+val TT = @{term TT};
+val FF = @{term FF};
+fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z;
+fun mk_fix t = %%:@{const_name fix}`t;
+fun mk_return t = %%:@{const_name Fixrec.return}`t;
+val mk_fail = %%:@{const_name Fixrec.fail};
+
+fun mk_branch t = %%:@{const_name Fixrec.branch} $ t;
+
+val pcpoS = @{sort pcpo};
+
 val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
 fun con_app2 con f args = list_ccomb(%%:con,map f args);
 fun con_app con = con_app2 con %#;
@@ -179,25 +169,26 @@
 |   prj f1 _  x (_::y::ys) 0 = f1 x y
 |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
-fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
+fun cproj x      = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
 fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
-fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
+fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T);
 fun /\# (arg,T) = /\ (vname arg) T;
-infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
-val UU = %%:UU_N;
+infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T;
+val UU = %%:@{const_name UU};
 fun strict f = f`UU === UU;
 fun defined t = t ~= UU;
-fun cpair (t,u) = %%:cpairN`t`u;
-fun spair (t,u) = %%:spairN`t`u;
+fun cpair (t,u) = %%:@{const_name cpair}`t`u;
+fun spair (t,u) = %%:@{const_name spair}`t`u;
 fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
 |   mk_ctuple ts = foldr1 cpair ts;
-fun mk_stuple [] = %%:ONE_N
+fun mk_stuple [] = ONE
 |   mk_stuple ts = foldr1 spair ts;
 fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
 |   mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
 fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
-fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2;
+fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2;
+val mk_ctuple_pat = foldr1 cpair_pat;
 fun lift_defined f = lift (fn x => defined (f x));
 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
 
@@ -217,14 +208,14 @@
 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
 	|   one_fun n (_,args) = let
 		val l2 = length args;
-		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
+		fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
 					         else I) (Bound(l2-m));
 		in cont_eta_contract (foldr'' 
-			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
+			(fn (a,t) => mk_ssplit (/\# (a,t)))
 			(args,
 			fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
 			) end;
 in (if length cons = 1 andalso length(snd(hd cons)) <= 1
-    then fn t => %%:strictifyN`t else I)
-     (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
+    then mk_strictify else I)
+     (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
 end; (* struct *)
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 29 10:20:00 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 29 18:00:12 2008 +0100
@@ -276,7 +276,7 @@
   fun dis_app c (con, args) =
     let
       val lhs = %%:(dis_name c) ` con_app con args;
-      val rhs = %%:(if con = c then TT_N else FF_N);
+      val rhs = if con = c then TT else FF;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_dis_def goal tacs end;
@@ -313,8 +313,8 @@
       val lhs = %%:(mat_name c) ` con_app con args;
       val rhs =
         if con = c
-        then %%:returnN ` mk_ctuple (map %# args)
-        else %%:failN;
+        then mk_return (mk_ctuple (map %# args))
+        else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_mat_def goal tacs end;
@@ -328,11 +328,11 @@
 local
   fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
 
-  fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
+  fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
 
-  fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
+  fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
     | pat_rhs (con,args) =
-        (%%:branchN $ foldr1 cpair_pat (ps args))
+        (mk_branch (mk_ctuple_pat (ps args)))
           `(%:"rhs")`(mk_ctuple (map %# args));
 
   fun pat_strict c =
@@ -346,7 +346,7 @@
     let
       val axs = @{thm branch_def} :: axs_pat_def;
       val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
-      val rhs = if con = fst c then pat_rhs c else %%:failN;
+      val rhs = if con = fst c then pat_rhs c else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs goal tacs end;
@@ -389,8 +389,8 @@
     [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
   fun con_compact (con, args) =
     let
-      val concl = mk_trp (%%:compactN $ con_app con args);
-      val goal = lift (fn x => %%:compactN $ %#x) (args, concl);
+      val concl = mk_trp (mk_compact (con_app con args));
+      val goal = lift (fn x => mk_compact (%#x)) (args, concl);
       val tacs = [
         rtac (iso_locale RS iso_compact_abs) 1,
         REPEAT (resolve_tac rules 1 ORELSE atac 1)];
@@ -890,7 +890,7 @@
 
         val goal =
           let
-            fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n));
+            fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
             fun concf n dn = %:(P_name n) $ %:(x_name n);
           in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
         fun tacf prems =