new term-building combinators
authorhuffman
Tue Jan 29 18:00:12 2008 +0100 (2008-01-29)
changeset 26012f6917792f8a4
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
     1.1 --- a/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jan 29 10:20:00 2008 +0100
     1.2 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Tue Jan 29 18:00:12 2008 +0100
     1.3 @@ -44,11 +44,11 @@
     1.4  (* -- definitions concerning the constructors, discriminators and selectors - *)
     1.5  
     1.6    fun con_def m n (_,args) = let
     1.7 -    fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x));
     1.8 +    fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x));
     1.9      fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs);
    1.10      fun inj y 1 _ = y
    1.11 -    |   inj y _ 0 = %%:sinlN`y
    1.12 -    |   inj y i j = %%:sinrN`(inj y (i-1) (j-1));
    1.13 +    |   inj y _ 0 = mk_sinl y
    1.14 +    |   inj y i j = mk_sinr (inj y (i-1) (j-1));
    1.15    in foldr /\# (dc_abs`(inj (parms args) m n)) args end;
    1.16    
    1.17    val con_defs = mapn (fn n => fn (con,args) =>
    1.18 @@ -58,7 +58,7 @@
    1.19  	fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
    1.20  		 list_ccomb(%%:(dname^"_when"),map 
    1.21  			(fn (con',args) => (foldr /\#
    1.22 -			   (if con'=con then %%:TT_N else %%:FF_N) args)) cons))
    1.23 +			   (if con'=con then TT else FF) args)) cons))
    1.24  	in map ddef cons end;
    1.25  
    1.26    val mat_defs = let
    1.27 @@ -66,8 +66,8 @@
    1.28  		 list_ccomb(%%:(dname^"_when"),map 
    1.29  			(fn (con',args) => (foldr /\#
    1.30  			   (if con'=con
    1.31 -                               then %%:returnN`(mk_ctuple (map (bound_arg args) args))
    1.32 -                               else %%:failN) args)) cons))
    1.33 +                               then mk_return (mk_ctuple (map (bound_arg args) args))
    1.34 +                               else mk_fail) args)) cons))
    1.35  	in map mdef cons end;
    1.36  
    1.37    val pat_defs =
    1.38 @@ -77,9 +77,9 @@
    1.39            val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
    1.40            val xs = map (bound_arg args) args;
    1.41            val r = Bound (length args);
    1.42 -          val rhs = case args of [] => %%:returnN ` HOLogic.unit
    1.43 -                                | _ => foldr1 cpair_pat ps ` mk_ctuple xs;
    1.44 -          fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args';
    1.45 +          val rhs = case args of [] => mk_return HOLogic.unit
    1.46 +                                | _ => mk_ctuple_pat ps ` mk_ctuple xs;
    1.47 +          fun one_con (con',args') = foldr /\# (if con'=con then rhs else mk_fail) args';
    1.48          in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
    1.49                 list_ccomb(%%:(dname^"_when"), map one_con cons))
    1.50          end
    1.51 @@ -95,10 +95,10 @@
    1.52  
    1.53  (* ----- axiom and definitions concerning induction ------------------------- *)
    1.54  
    1.55 -  val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
    1.56 +  val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n
    1.57  					`%x_name === %:x_name));
    1.58    val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj
    1.59 -	     (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
    1.60 +	     (mk_iterate (Bound 0, %%:(comp_dname^"_copy"), UU)) eqs n));
    1.61    val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
    1.62  	mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    1.63  
    1.64 @@ -125,7 +125,7 @@
    1.65    val x_name = idx_name dnames "x"; 
    1.66    fun copy_app dname = %%:(dname^"_copy")`Bound 0;
    1.67    val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
    1.68 -				    /\"f"(foldr1 cpair (map copy_app dnames)));
    1.69 +				    /\"f"(mk_ctuple (map copy_app dnames)));
    1.70    val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
    1.71      let
    1.72        fun one_con (con,args) = let
     2.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Tue Jan 29 10:20:00 2008 +0100
     2.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Tue Jan 29 18:00:12 2008 +0100
     2.3 @@ -97,44 +97,6 @@
     2.4  fun nonlazy     args   = map vname (filter_out is_lazy    args);
     2.5  fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
     2.6  
     2.7 -(* ----- qualified names of HOLCF constants ----- *)
     2.8 -
     2.9 -val lessN      = @{const_name Porder.sq_le};
    2.10 -val UU_N       = "Pcpo.UU";
    2.11 -val admN       = "Adm.adm";
    2.12 -val compactN   = "Adm.compact";
    2.13 -val Rep_CFunN  = "Cfun.Rep_CFun";
    2.14 -val Abs_CFunN  = "Cfun.Abs_CFun";
    2.15 -val ID_N       = "Cfun.ID";
    2.16 -val cfcompN    = "Cfun.cfcomp";
    2.17 -val strictifyN = "Cfun.strictify";
    2.18 -val cpairN     = "Cprod.cpair";
    2.19 -val cfstN      = "Cprod.cfst";
    2.20 -val csndN      = "Cprod.csnd";
    2.21 -val csplitN    = "Cprod.csplit";
    2.22 -val spairN     = "Sprod.spair";
    2.23 -val sfstN      = "Sprod.sfst";
    2.24 -val ssndN      = "Sprod.ssnd";
    2.25 -val ssplitN    = "Sprod.ssplit";
    2.26 -val sinlN      = "Ssum.sinl";
    2.27 -val sinrN      = "Ssum.sinr";
    2.28 -val sscaseN    = "Ssum.sscase";
    2.29 -val upN        = "Up.up";
    2.30 -val fupN       = "Up.fup";
    2.31 -val ONE_N      = "One.ONE";
    2.32 -val TT_N       = "Tr.TT";
    2.33 -val FF_N       = "Tr.FF";
    2.34 -val iterateN   = "Fix.iterate";
    2.35 -val fixN       = "Fix.fix";
    2.36 -val returnN    = "Fixrec.return";
    2.37 -val failN      = "Fixrec.fail";
    2.38 -val cpair_patN = "Fixrec.cpair_pat";
    2.39 -val branchN    = "Fixrec.branch";
    2.40 -
    2.41 -val pcpoN      = "Pcpo.pcpo"
    2.42 -val pcpoS      = [pcpoN];
    2.43 -
    2.44 -
    2.45  (* ----- support for type and mixfix expressions ----- *)
    2.46  
    2.47  infixr 5 -->;
    2.48 @@ -164,12 +126,40 @@
    2.49  infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    2.50  infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
    2.51  infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
    2.52 -infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
    2.53 +infix 1 <<;     fun S <<  T = %%:@{const_name Porder.sq_le} $ S $ T;
    2.54  infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
    2.55  
    2.56 -infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
    2.57 +infix 9 `  ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x;
    2.58  infix 9 `% ; fun f`% s = f` %: s;
    2.59  infix 9 `%%; fun f`%%s = f` %%:s;
    2.60 +
    2.61 +fun mk_adm t = %%:@{const_name adm} $ t;
    2.62 +fun mk_compact t = %%:@{const_name compact} $ t;
    2.63 +val ID = %%:@{const_name ID};
    2.64 +fun mk_strictify t = %%:@{const_name strictify}`t;
    2.65 +fun mk_cfst t = %%:@{const_name cfst}`t;
    2.66 +fun mk_csnd t = %%:@{const_name csnd}`t;
    2.67 +(*val csplitN    = "Cprod.csplit";*)
    2.68 +(*val sfstN      = "Sprod.sfst";*)
    2.69 +(*val ssndN      = "Sprod.ssnd";*)
    2.70 +fun mk_ssplit t = %%:@{const_name ssplit}`t;
    2.71 +fun mk_sinl t = %%:@{const_name sinl}`t;
    2.72 +fun mk_sinr t = %%:@{const_name sinr}`t;
    2.73 +fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y;
    2.74 +fun mk_up t = %%:@{const_name up}`t;
    2.75 +fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u;
    2.76 +val ONE = @{term ONE};
    2.77 +val TT = @{term TT};
    2.78 +val FF = @{term FF};
    2.79 +fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z;
    2.80 +fun mk_fix t = %%:@{const_name fix}`t;
    2.81 +fun mk_return t = %%:@{const_name Fixrec.return}`t;
    2.82 +val mk_fail = %%:@{const_name Fixrec.fail};
    2.83 +
    2.84 +fun mk_branch t = %%:@{const_name Fixrec.branch} $ t;
    2.85 +
    2.86 +val pcpoS = @{sort pcpo};
    2.87 +
    2.88  val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
    2.89  fun con_app2 con f args = list_ccomb(%%:con,map f args);
    2.90  fun con_app con = con_app2 con %#;
    2.91 @@ -179,25 +169,26 @@
    2.92  |   prj f1 _  x (_::y::ys) 0 = f1 x y
    2.93  |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
    2.94  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
    2.95 -fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
    2.96 +fun cproj x      = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
    2.97  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
    2.98  
    2.99 -fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
   2.100 +fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T);
   2.101  fun /\# (arg,T) = /\ (vname arg) T;
   2.102 -infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
   2.103 -val UU = %%:UU_N;
   2.104 +infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T;
   2.105 +val UU = %%:@{const_name UU};
   2.106  fun strict f = f`UU === UU;
   2.107  fun defined t = t ~= UU;
   2.108 -fun cpair (t,u) = %%:cpairN`t`u;
   2.109 -fun spair (t,u) = %%:spairN`t`u;
   2.110 +fun cpair (t,u) = %%:@{const_name cpair}`t`u;
   2.111 +fun spair (t,u) = %%:@{const_name spair}`t`u;
   2.112  fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
   2.113  |   mk_ctuple ts = foldr1 cpair ts;
   2.114 -fun mk_stuple [] = %%:ONE_N
   2.115 +fun mk_stuple [] = ONE
   2.116  |   mk_stuple ts = foldr1 spair ts;
   2.117  fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
   2.118  |   mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
   2.119  fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
   2.120 -fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2;
   2.121 +fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2;
   2.122 +val mk_ctuple_pat = foldr1 cpair_pat;
   2.123  fun lift_defined f = lift (fn x => defined (f x));
   2.124  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
   2.125  
   2.126 @@ -217,14 +208,14 @@
   2.127  	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   2.128  	|   one_fun n (_,args) = let
   2.129  		val l2 = length args;
   2.130 -		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
   2.131 +		fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
   2.132  					         else I) (Bound(l2-m));
   2.133  		in cont_eta_contract (foldr'' 
   2.134 -			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
   2.135 +			(fn (a,t) => mk_ssplit (/\# (a,t)))
   2.136  			(args,
   2.137  			fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
   2.138  			) end;
   2.139  in (if length cons = 1 andalso length(snd(hd cons)) <= 1
   2.140 -    then fn t => %%:strictifyN`t else I)
   2.141 -     (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
   2.142 +    then mk_strictify else I)
   2.143 +     (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
   2.144  end; (* struct *)
     3.1 --- a/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 29 10:20:00 2008 +0100
     3.2 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Tue Jan 29 18:00:12 2008 +0100
     3.3 @@ -276,7 +276,7 @@
     3.4    fun dis_app c (con, args) =
     3.5      let
     3.6        val lhs = %%:(dis_name c) ` con_app con args;
     3.7 -      val rhs = %%:(if con = c then TT_N else FF_N);
     3.8 +      val rhs = if con = c then TT else FF;
     3.9        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    3.10        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.11      in pg axs_dis_def goal tacs end;
    3.12 @@ -313,8 +313,8 @@
    3.13        val lhs = %%:(mat_name c) ` con_app con args;
    3.14        val rhs =
    3.15          if con = c
    3.16 -        then %%:returnN ` mk_ctuple (map %# args)
    3.17 -        else %%:failN;
    3.18 +        then mk_return (mk_ctuple (map %# args))
    3.19 +        else mk_fail;
    3.20        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    3.21        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.22      in pg axs_mat_def goal tacs end;
    3.23 @@ -328,11 +328,11 @@
    3.24  local
    3.25    fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
    3.26  
    3.27 -  fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args);
    3.28 +  fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
    3.29  
    3.30 -  fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit)
    3.31 +  fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
    3.32      | pat_rhs (con,args) =
    3.33 -        (%%:branchN $ foldr1 cpair_pat (ps args))
    3.34 +        (mk_branch (mk_ctuple_pat (ps args)))
    3.35            `(%:"rhs")`(mk_ctuple (map %# args));
    3.36  
    3.37    fun pat_strict c =
    3.38 @@ -346,7 +346,7 @@
    3.39      let
    3.40        val axs = @{thm branch_def} :: axs_pat_def;
    3.41        val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
    3.42 -      val rhs = if con = fst c then pat_rhs c else %%:failN;
    3.43 +      val rhs = if con = fst c then pat_rhs c else mk_fail;
    3.44        val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
    3.45        val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.46      in pg axs goal tacs end;
    3.47 @@ -389,8 +389,8 @@
    3.48      [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
    3.49    fun con_compact (con, args) =
    3.50      let
    3.51 -      val concl = mk_trp (%%:compactN $ con_app con args);
    3.52 -      val goal = lift (fn x => %%:compactN $ %#x) (args, concl);
    3.53 +      val concl = mk_trp (mk_compact (con_app con args));
    3.54 +      val goal = lift (fn x => mk_compact (%#x)) (args, concl);
    3.55        val tacs = [
    3.56          rtac (iso_locale RS iso_compact_abs) 1,
    3.57          REPEAT (resolve_tac rules 1 ORELSE atac 1)];
    3.58 @@ -890,7 +890,7 @@
    3.59  
    3.60          val goal =
    3.61            let
    3.62 -            fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n));
    3.63 +            fun one_adm n _ = mk_trp (mk_adm (%:(P_name n)));
    3.64              fun concf n dn = %:(P_name n) $ %:(x_name n);
    3.65            in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end;
    3.66          fun tacf prems =