# HG changeset patch # User huffman # Date 1128909339 -7200 # Node ID 10ebcd7032c19ea4f7777eb19d7bfe56c658ab90 # Parent 3bdf516d93d81986a5a73b6b6ab1466235eb751a replaced foldr' with foldr1 diff -r 3bdf516d93d8 -r 10ebcd7032c1 src/HOLCF/domain/axioms.ML --- 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*) diff -r 3bdf516d93d8 -r 10ebcd7032c1 src/HOLCF/domain/library.ML --- 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 *) diff -r 3bdf516d93d8 -r 10ebcd7032c1 src/HOLCF/domain/syntax.ML --- 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'; diff -r 3bdf516d93d8 -r 10ebcd7032c1 src/HOLCF/domain/theorems.ML --- 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,