--- a/src/HOLCF/domain/axioms.ML Mon Oct 10 03:47:00 2005 +0200
+++ b/src/HOLCF/domain/axioms.ML Mon Oct 10 03:55:39 2005 +0200
@@ -39,7 +39,7 @@
(if recu andalso is_rec arg then (cproj (Bound z) eqs
(rec_of arg))`Bound(z-x) else Bound(z-x));
fun parms [] = %%:ONE_N
- | parms vs = foldr'(fn(x,t)=> %%:spairN`x`t)(mapn (idxs(length vs))1 vs);
+ | parms vs = foldr1(fn(x,t)=> %%:spairN`x`t)(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));
@@ -105,7 +105,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"(foldr' cpair (map copy_app dnames)));
+ /\"f"(foldr1 cpair (map copy_app dnames)));
val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R",
let
fun one_con (con,args) = let
@@ -132,9 +132,9 @@
(map (defined o Bound) nonlazy_idxs,capps)) allvns end;
fun one_comp n (_,cons) =mk_all(x_name(n+1),mk_all(x_name(n+1)^"'",mk_imp(
proj (Bound 2) eqs n $ Bound 1 $ Bound 0,
- foldr' mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
+ foldr1 mk_disj (mk_conj(Bound 1 === UU,Bound 0 === UU)
::map one_con cons))));
- in foldr' mk_conj (mapn one_comp 0 eqs)end ));
+ in foldr1 mk_conj (mapn one_comp 0 eqs)end ));
fun add_one (thy,(dnam,axs,dfs)) = thy
|> Theory.add_path dnam
|> add_axioms_infer dfs(*add_defs_i*)
--- a/src/HOLCF/domain/library.ML Mon Oct 10 03:47:00 2005 +0200
+++ b/src/HOLCF/domain/library.ML Mon Oct 10 03:55:39 2005 +0200
@@ -15,7 +15,6 @@
| itr [a] = f2 a
| itr (a::l) = f(a, itr l)
in itr l end;
-fun foldr' f l = foldr'' f (l,I);
fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
(y::ys,res2)) ([],start) xs;
@@ -193,7 +192,7 @@
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 prj' _ _ x ( _::[]) _ = x
-| prj' f1 _ x (_:: ys) 0 = f1 x (foldr' HOLogic.mk_prodT ys)
+| prj' f1 _ x (_:: ys) 0 = f1 x (foldr1 HOLogic.mk_prodT ys)
| prj' f1 f2 x (y:: ys) j = prj' f1 f2 (f2 x y) ys (j-1);
fun cproj' T eqs = prj'
(fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
@@ -242,5 +241,5 @@
) end;
in (if length cons = 1 andalso length(snd(hd cons)) <= 1
then fn t => %%:strictifyN`t else I)
- (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
+ (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
end; (* struct *)
--- a/src/HOLCF/domain/syntax.ML Mon Oct 10 03:47:00 2005 +0200
+++ b/src/HOLCF/domain/syntax.ML Mon Oct 10 03:55:39 2005 +0200
@@ -19,13 +19,13 @@
local
fun opt_lazy (lazy,_,t) = if lazy then mk_uT t else t
fun prod (_,_,args) = if args = [] then oneT
- else foldr' mk_sprodT (map opt_lazy args);
+ else foldr1 mk_sprodT (map opt_lazy args);
fun freetvar s = let val tvar = mk_TFree s in
if tvar mem typevars then freetvar ("t"^s) else tvar end;
fun when_type (_ ,_,args) = foldr (op ->>) (freetvar "t") (map third args);
in
val dtype = Type(dname,typevars);
- val dtype2 = foldr' mk_ssumT (map prod cons');
+ val dtype2 = foldr1 mk_ssumT (map prod cons');
val dnam = Sign.base_name dname;
val const_rep = (dnam^"_rep" , dtype ->> dtype2, NoSyn);
val const_abs = (dnam^"_abs" , dtype2 ->> dtype , NoSyn);
@@ -77,10 +77,10 @@
expvar n];
fun arg1 n (con,_,args) = if args = [] then expvar n
else mk_appl (Constant "LAM ")
- [foldr' (app "_idts") (mapn (argvar n) 1 args) , expvar n];
+ [foldr1 (app "_idts") (mapn (argvar n) 1 args) , expvar n];
in
ParsePrintRule
- (mk_appl (Constant "_case_syntax") [Variable "x", foldr'
+ (mk_appl (Constant "_case_syntax") [Variable "x", foldr1
(fn (c,cs) => mk_appl (Constant"_case2") [c,cs])
(mapn case1 1 cons')],
mk_appl (Constant "Rep_CFun") [Library.foldl
@@ -105,8 +105,8 @@
let
val dtypes = map (Type o fst) eqs';
val boolT = HOLogic.boolT;
- val funprod = foldr' HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
- val relprod = foldr' HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
+ val funprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp ->> tp ) dtypes);
+ val relprod = foldr1 HOLogic.mk_prodT (map (fn tp => tp --> tp --> boolT) dtypes);
val const_copy = (comp_dnam^"_copy" ,funprod ->> funprod, NoSyn);
val const_bisim = (comp_dnam^"_bisim" ,relprod --> boolT , NoSyn);
val ctt = map (calc_syntax funprod) eqs';
--- a/src/HOLCF/domain/theorems.ML Mon Oct 10 03:47:00 2005 +0200
+++ b/src/HOLCF/domain/theorems.ML Mon Oct 10 03:55:39 2005 +0200
@@ -134,9 +134,9 @@
local
val iso_swap = iso_locale RS iso_iso_swap;
fun one_con (con,args) = let val vns = map vname args in
- Library.foldr mk_ex (vns, foldr' mk_conj ((%:x_name === con_app2 con %: vns)::
+ Library.foldr mk_ex (vns, foldr1 mk_conj ((%:x_name === con_app2 con %: vns)::
map (defined o %:) (nonlazy args))) end;
- val exh = foldr' mk_disj ((%:x_name===UU)::map one_con cons);
+ val exh = foldr1 mk_disj ((%:x_name===UU)::map one_con cons);
val my_ctyp = cons2ctyp cons;
val thm1 = instantiate' [SOME my_ctyp] [] exh_start;
val thm2 = rewrite_rule (map mk_meta_eq ex_defined_iffs) thm1;
@@ -280,7 +280,7 @@
let
fun append s = upd_vname(fn v => v^s);
val (largs,rargs) = (args, map (append "'") args);
- val concl = mk_trp (foldr' mk_conj (ListPair.map rel (map %# largs, map %# rargs)));
+ val concl = mk_trp (foldr1 mk_conj (ListPair.map rel (map %# largs, map %# rargs)));
val prem = mk_trp (rel(con_app con largs,con_app con rargs));
val prop = prem ===> lift_defined %: (nonlazy largs, concl);
in pg con_appls prop end;
@@ -380,7 +380,7 @@
val iterate_Cprod_ss = simpset_of Fix.thy;
val copy_con_rews = copy_rews @ con_rews;
val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
- val take_stricts=pg copy_take_defs(mk_trp(foldr' mk_conj(map(fn((dn,args),_)=>
+ val take_stricts=pg copy_take_defs(mk_trp(foldr1 mk_conj(map(fn((dn,args),_)=>
strict(dc_take dn $ %:"n")) eqs))) ([
induct_tac "n" 1,
simp_tac iterate_Cprod_ss 1,
@@ -390,7 +390,7 @@
`%x_name n === UU))[
simp_tac iterate_Cprod_ss 1]) 1 dnames;
val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
- val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj
+ val take_apps = pg copy_take_defs (mk_trp(foldr1 mk_conj
(List.concat(map (fn ((dn,_),cons) => map (fn (con,args) => Library.foldr mk_all
(map vname args,(dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args) ===
con_app2 con (app_rec_arg (fn n=>dc_take (List.nth(dnames,n))$ %:"n"))
@@ -418,7 +418,7 @@
fun one_eq ((p,cons),concl) = (mk_trp(%:p $ UU) ===>
Library.foldr (op ===>) (map (one_con p) cons,concl));
fun ind_term concf = Library.foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
- mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
+ mk_trp(foldr1 mk_conj (mapn concf 1 dnames)));
val take_ss = HOL_ss addsimps take_rews;
fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i)
1 dnames);
@@ -500,7 +500,7 @@
resolve_tac take_lemmas 1,
asm_simp_tac take_ss 1,
atac 1]) dnames;
- val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr' mk_conj (mapn
+ val finite_lemma1b = pg [] (mk_trp (mk_all("n",foldr1 mk_conj (mapn
(fn n => fn ((dn,args),_) => mk_constrainall(x_name n,Type(dn,args),
mk_disj(dc_take dn $ Bound 1 ` Bound 0 === UU,
dc_take dn $ Bound 1 ` Bound 0 === Bound 0))) 1 eqs)))) ([
@@ -571,7 +571,7 @@
Library.foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
Library.foldr mk_imp (mapn (fn n => K(proj (%:"R") eqs n $
bnd_arg n 0 $ bnd_arg n 1)) 0 dnames,
- foldr' mk_conj (mapn (fn n => fn dn =>
+ foldr1 mk_conj (mapn (fn n => fn dn =>
(dc_take dn $ %:"n" `bnd_arg n 0 ===
(dc_take dn $ %:"n" `bnd_arg n 1)))0 dnames))))))
([ rtac impI 1,
@@ -590,7 +590,7 @@
val coind = pg [] (mk_trp(%%:(comp_dname^"_bisim") $ %:"R") ===>
Library.foldr (op ===>) (mapn (fn n => fn x =>
mk_trp(proj (%:"R") eqs n $ %:x $ %:(x^"'"))) 0 xs,
- mk_trp(foldr' mk_conj (map (fn x => %:x === %:(x^"'")) xs)))) ([
+ mk_trp(foldr1 mk_conj (map (fn x => %:x === %:(x^"'")) xs)))) ([
TRY(safe_tac HOL_cs)] @
List.concat(map (fn take_lemma => [
rtac take_lemma 1,