--- 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 =