src/HOLCF/domain/axioms.ML
changeset 16778 2162c0de4673
parent 16394 495dbcd4f4c9
child 16842 5979c46853d1
     1.1 --- a/src/HOLCF/domain/axioms.ML	Tue Jul 12 18:26:44 2005 +0200
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Tue Jul 12 18:28:36 2005 +0200
     1.3 @@ -35,14 +35,14 @@
     1.4  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
     1.5  
     1.6    fun con_def outer recu m n (_,args) = let
     1.7 -     fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id)
     1.8 +     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id)
     1.9  			(if recu andalso is_rec arg then (cproj (Bound z) eqs
    1.10  				  (rec_of arg))`Bound(z-x) else Bound(z-x));
    1.11 -     fun parms [] = %%:"ONE"
    1.12 -     |   parms vs = foldr'(fn(x,t)=> %%:"spair"`x`t)(mapn (idxs(length vs))1 vs);
    1.13 +     fun parms [] = %%:ONE_N
    1.14 +     |   parms vs = foldr'(fn(x,t)=> %%:spairN`x`t)(mapn (idxs(length vs))1 vs);
    1.15       fun inj y 1 _ = y
    1.16 -     |   inj y _ 0 = %%:"sinl"`y
    1.17 -     |   inj y i j = %%:"sinr"`(inj y (i-1) (j-1));
    1.18 +     |   inj y _ 0 = %%:sinlN`y
    1.19 +     |   inj y i j = %%:sinrN`(inj y (i-1) (j-1));
    1.20    in foldr /\# (outer (inj (parms args) m n)) args end;
    1.21  
    1.22    val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo 
    1.23 @@ -58,30 +58,32 @@
    1.24  	fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
    1.25  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.26  			(fn (con',args) => (foldr /\#
    1.27 -			   (if con'=con then %%:"TT" else %%:"FF") args)) cons))
    1.28 +			   (if con'=con then %%:TT_N else %%:FF_N) args)) cons))
    1.29  	in map ddef cons end;
    1.30  
    1.31    val mat_defs = let
    1.32  	fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == 
    1.33  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.34  			(fn (con',args) => (foldr /\#
    1.35 -			   (if con'=con then (%%:"return")`(mk_ctuple (map (bound_arg args) args)) else %%:"fail") args)) cons))
    1.36 +			   (if con'=con
    1.37 +                               then %%:returnN`(mk_ctuple (map (bound_arg args) args))
    1.38 +                               else %%:failN) args)) cons))
    1.39  	in map mdef cons end;
    1.40  
    1.41    val sel_defs = let
    1.42  	fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
    1.43  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.44 -			(fn (con',args) => if con'<>con then %%:"UU" else
    1.45 +			(fn (con',args) => if con'<>con then UU else
    1.46  			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    1.47  	in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    1.48  
    1.49  
    1.50  (* ----- axiom and definitions concerning induction ------------------------- *)
    1.51  
    1.52 -  val reach_ax = ("reach", mk_trp(cproj (%%:"fix"`%%(comp_dname^"_copy")) eqs n
    1.53 +  val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
    1.54  					`%x_name === %:x_name));
    1.55    val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj' 
    1.56 -	     (%%:"iterate" $ Bound 0 $ %%:(comp_dname^"_copy") $ %%:"UU") eqs n));
    1.57 +	     (%%:iterateN $ Bound 0 $ %%:(comp_dname^"_copy") $ UU) eqs n));
    1.58    val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
    1.59  	mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    1.60