src/HOLCF/domain/theorems.ML
 changeset 15570 8d8c70b41bab parent 15531 08c8dad8e399 child 15742 64eae3513064
```     1.1 --- a/src/HOLCF/domain/theorems.ML	Thu Mar 03 09:22:35 2005 +0100
1.2 +++ b/src/HOLCF/domain/theorems.ML	Thu Mar 03 12:43:01 2005 +0100
1.3 @@ -71,7 +71,7 @@
1.4  val ax_when_def   = ga "when_def" dname;
1.5  val axs_con_def   = map (fn (con,_) => ga (extern_name con^"_def") dname) cons;
1.6  val axs_dis_def   = map (fn (con,_) => ga (   dis_name con^"_def") dname) cons;
1.7 -val axs_sel_def   = flat(map (fn (_,args) =>
1.8 +val axs_sel_def   = List.concat(map (fn (_,args) =>
1.9                      map (fn     arg => ga (sel_of arg     ^"_def") dname) args)
1.10  									  cons);
1.11  val ax_copy_def   = ga "copy_def" dname;
1.12 @@ -101,7 +101,7 @@
1.13                              etac (ax_rep_iso RS subst) 1];
1.14  fun exh foldr1 cn quant foldr2 var = let
1.15    fun one_con (con,args) = let val vns = map vname args in
1.16 -    foldr quant (vns, foldr2 ((%:x_name === con_app2 con (var vns) vns)::
1.17 +    Library.foldr quant (vns, foldr2 ((%:x_name === con_app2 con (var vns) vns)::
1.18                                map (defined o (var vns)) (nonlazy args))) end
1.19    in foldr1 ((cn(%:x_name===UU))::map one_con cons) end;
1.20  in
1.21 @@ -130,9 +130,9 @@
1.22                                  prod_tac args THEN sum_rest_tac p) THEN
1.23                                  sum_tac cons' prems
1.24              |   sum_tac _ _ = Imposs "theorems:sum_tac";
1.25 -          in pg'' thy [] (exh (fn l => foldr (op ===>) (l,mk_trp(%:"P")))
1.26 +          in pg'' thy [] (exh (fn l => Library.foldr (op ===>) (l,mk_trp(%:"P")))
1.27                                (fn T => T ==> %:"P") mk_All
1.28 -                              (fn l => foldr (op ===>) (map mk_trp l,
1.29 +                              (fn l => Library.foldr (op ===>) (map mk_trp l,
1.30                                                              mk_trp(%:"P")))
1.31                                bound_arg)
1.32                               (fn prems => [
1.33 @@ -153,9 +153,9 @@
1.34  end;
1.35
1.36  local
1.37 -  fun bind_fun t = foldr mk_All (when_funs cons,t);
1.38 +  fun bind_fun t = Library.foldr mk_All (when_funs cons,t);
1.39    fun bound_fun i _ = Bound (length cons - i);
1.40 -  val when_app  = foldl (op `) (%%:(dname^"_when"), mapn bound_fun 1 cons);
1.41 +  val when_app  = Library.foldl (op `) (%%:(dname^"_when"), mapn bound_fun 1 cons);
1.42    val when_appl = pg [ax_when_def] (bind_fun(mk_trp(when_app`%x_name ===
1.43               when_body cons (fn (m,n)=> bound_fun (n-m) 0)`(dc_rep`%x_name))))[
1.44                                  simp_tac HOLCF_ss 1];
1.45 @@ -182,7 +182,7 @@
1.46                          (mk_trp((%%:(dis_name c))`(con_app con args) ===
1.47                                %%:(if con=c then "TT" else "FF"))))) [
1.48                                  asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
1.49 -        in flat(map (fn (c,_) => map (one_dis c) cons) cons) end;
1.50 +        in List.concat(map (fn (c,_) => map (one_dis c) cons) cons) end;
1.51    val dis_defins = map (fn (con,args) => pg [] (defined(%:x_name) ==>
1.52                        defined(%%:(dis_name con)`%x_name)) [
1.53                                  rtac casedist 1,
1.54 @@ -191,7 +191,7 @@
1.55                                          (HOLCF_ss addsimps dis_apps) 1))]) cons;
1.56  in dis_stricts @ dis_defins @ dis_apps end;
1.57
1.58 -val con_stricts = flat(map (fn (con,args) => map (fn vn =>
1.59 +val con_stricts = List.concat(map (fn (con,args) => map (fn vn =>
1.60                          pg (axs_con_def)
1.61                             (mk_trp(con_app2 con (fn arg => if vname arg = vn
1.62                                          then UU else %# arg) args === UU))[
1.63 @@ -207,22 +207,22 @@
1.64
1.65  val sel_stricts = let fun one_sel sel = pg axs_sel_def (mk_trp(strict(%%:sel))) [
1.66                                  simp_tac (HOLCF_ss addsimps when_rews) 1];
1.67 -in flat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
1.68 +in List.concat(map (fn (_,args) =>map (fn arg => one_sel (sel_of arg)) args) cons) end;
1.69  val sel_apps = let fun one_sel c n sel = map (fn (con,args) =>
1.70                  let val nlas = nonlazy args;
1.71                      val vns  = map vname args;
1.72                  in pg axs_sel_def (lift_defined %:
1.73 -                   (filter (fn v => con=c andalso (v<>nth_elem(n,vns))) nlas,
1.74 +                   (List.filter (fn v => con=c andalso (v<>List.nth(vns,n))) nlas,
1.75                                  mk_trp((%%:sel)`(con_app con args) ===
1.76 -                                (if con=c then %:(nth_elem(n,vns)) else UU))))
1.77 +                                (if con=c then %:(List.nth(vns,n)) else UU))))
1.78                              ( (if con=c then []
1.79                         else map(case_UU_tac(when_rews@con_stricts)1) nlas)
1.80 -                     @(if con=c andalso ((nth_elem(n,vns)) mem nlas)
1.81 +                     @(if con=c andalso ((List.nth(vns,n)) mem nlas)
1.82                                   then[case_UU_tac (when_rews @ con_stricts) 1
1.83 -                                                  (nth_elem(n,vns))] else [])
1.84 +                                                  (List.nth(vns,n))] else [])
1.85                       @ [asm_simp_tac(HOLCF_ss addsimps when_rews)1])end) cons;
1.86 -in flat(map  (fn (c,args) =>
1.87 -     flat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
1.88 +in List.concat(map  (fn (c,args) =>
1.89 +     List.concat(mapn (fn n => fn arg => one_sel c n (sel_of arg)) 0 args)) cons) end;
1.90  val sel_defins = if length cons=1 then map (fn arg => pg [](defined(%:x_name)==>
1.91                          defined(%%:(sel_of arg)`%x_name)) [
1.92                                  rtac casedist 1,
1.93 @@ -249,7 +249,7 @@
1.94      fun distincts []      = []
1.95      |   distincts (c::cs) = (map (distinct c) cs) :: distincts cs;
1.96  in distincts cons end;
1.97 -val dist_les = flat (flat distincts_le);
1.98 +val dist_les = List.concat (List.concat distincts_le);
1.99  val dist_eqs = let
1.100      fun distinct (_,args1) ((_,args2),leqs) = let
1.101          val (le1,le2) = (hd leqs, hd(tl leqs));
1.102 @@ -273,10 +273,10 @@
1.103                              mk_trp (foldr' mk_conj
1.104                                  (ListPair.map rel
1.105  				 (map %# largs, map %# rargs)))))) end;
1.106 -  val cons' = filter (fn (_,args) => args<>[]) cons;
1.107 +  val cons' = List.filter (fn (_,args) => args<>[]) cons;
1.108  in
1.109  val inverts = map (fn (con,args) =>
1.110 -                pgterm (op <<) con args (flat(map (fn arg => [
1.111 +                pgterm (op <<) con args (List.concat(map (fn arg => [
1.112                                  TRY(rtac conjI 1),
1.113                                  dres_inst_tac [("fo",sel_of arg)] monofun_cfun_arg 1,
1.114                                  asm_full_simp_tac (HOLCF_ss addsimps sel_apps) 1]
1.115 @@ -302,7 +302,7 @@
1.116                  (con_app2 con (app_rec_arg (cproj (%:"f") eqs)) args))))
1.117                          (map (case_UU_tac (abs_strict::when_strict::con_stricts)
1.118                                   1 o vname)
1.119 -                         (filter (fn a => not (is_rec a orelse is_lazy a)) args)
1.120 +                         (List.filter (fn a => not (is_rec a orelse is_lazy a)) args)
1.121                          @[asm_simp_tac (HOLCF_ss addsimps when_apps) 1,
1.122                            simp_tac (HOLCF_ss addsimps axs_con_def) 1]))cons;
1.123  val copy_stricts = map (fn (con,args) => pg [] (mk_trp(dc_copy`UU`
1.124 @@ -310,7 +310,7 @@
1.125       (let val rews = cfst_strict::csnd_strict::copy_strict::copy_apps@con_rews
1.126                           in map (case_UU_tac rews 1) (nonlazy args) @ [
1.127                               asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
1.128 -                        (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
1.129 +                        (List.filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
1.130  val copy_rews = copy_strict::copy_apps @ copy_stricts;
1.131  in thy |> Theory.add_path (Sign.base_name dname)
1.132         |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
1.133 @@ -352,8 +352,8 @@
1.134  local fun gt  s dn = get_thm  thy (dn ^ "." ^ s, NONE);
1.135        fun gts s dn = get_thms thy (dn ^ "." ^ s, NONE) in
1.136  val cases     =       map (gt  "casedist" ) dnames;
1.137 -val con_rews  = flat (map (gts "con_rews" ) dnames);
1.138 -val copy_rews = flat (map (gts "copy_rews") dnames);
1.139 +val con_rews  = List.concat (map (gts "con_rews" ) dnames);
1.140 +val copy_rews = List.concat (map (gts "copy_rews") dnames);
1.141  end; (* local *)
1.142
1.143  fun dc_take dn = %%:(dn^"_take");
1.144 @@ -379,17 +379,17 @@
1.145                                  simp_tac iterate_Cprod_ss 1]) 1 dnames;
1.146    val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;
1.147    val take_apps = pg copy_take_defs (mk_trp(foldr' mk_conj
1.148 -            (flat(map (fn ((dn,_),cons) => map (fn (con,args) => foldr mk_all
1.149 +            (List.concat(map (fn ((dn,_),cons) => map (fn (con,args) => Library.foldr mk_all
1.150          (map vname args,(dc_take dn \$ (%%:"Suc" \$ %:"n"))`(con_app con args) ===
1.151 -         con_app2 con (app_rec_arg (fn n=>dc_take (nth_elem(n,dnames))\$ %:"n"))
1.152 +         con_app2 con (app_rec_arg (fn n=>dc_take (List.nth(dnames,n))\$ %:"n"))
1.153                                args)) cons) eqs)))) ([
1.154                                  simp_tac iterate_Cprod_ss 1,
1.155                                  induct_tac "n" 1,
1.158 -                                      (filter (has_fewer_prems 1) copy_rews)) 1,
1.159 +                                      (List.filter (has_fewer_prems 1) copy_rews)) 1,
1.160                                  TRY(safe_tac HOL_cs)] @
1.161 -                        (flat(map (fn ((dn,_),cons) => map (fn (con,args) =>
1.162 +                        (List.concat(map (fn ((dn,_),cons) => map (fn (con,args) =>
1.163                                  if nonlazy_rec args = [] then all_tac else
1.164                                  EVERY(map c_UU_tac (nonlazy_rec args)) THEN
1.166 @@ -399,23 +399,23 @@
1.167  end; (* local *)
1.168
1.169  local
1.170 -  fun one_con p (con,args) = foldr mk_All (map vname args,
1.171 +  fun one_con p (con,args) = Library.foldr mk_All (map vname args,
1.172          lift_defined (bound_arg (map vname args)) (nonlazy args,
1.173          lift (fn arg => %:(P_name (1+rec_of arg)) \$ bound_arg args arg)
1.174 -         (filter is_rec args,mk_trp(%:p \$ con_app2 con (bound_arg args) args))));
1.175 +         (List.filter is_rec args,mk_trp(%:p \$ con_app2 con (bound_arg args) args))));
1.176    fun one_eq ((p,cons),concl) = (mk_trp(%:p \$ UU) ===>
1.177 -                           foldr (op ===>) (map (one_con p) cons,concl));
1.178 -  fun ind_term concf = foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
1.179 +                           Library.foldr (op ===>) (map (one_con p) cons,concl));
1.180 +  fun ind_term concf = Library.foldr one_eq (mapn (fn n => fn x => (P_name n, x))1conss,
1.181                          mk_trp(foldr' mk_conj (mapn concf 1 dnames)));
1.182    val take_ss = HOL_ss addsimps take_rews;
1.183    fun quant_tac i = EVERY(mapn(fn n=> fn _=> res_inst_tac[("x",x_name n)]spec i)
1.184                                 1 dnames);
1.185 -  fun ind_prems_tac prems = EVERY(flat (map (fn cons => (
1.186 +  fun ind_prems_tac prems = EVERY(List.concat (map (fn cons => (
1.187                                       resolve_tac prems 1 ::
1.188 -                                     flat (map (fn (_,args) =>
1.189 +                                     List.concat (map (fn (_,args) =>
1.190                                         resolve_tac prems 1 ::
1.191                                         map (K(atac 1)) (nonlazy args) @
1.192 -                                       map (K(atac 1)) (filter is_rec args))
1.193 +                                       map (K(atac 1)) (List.filter is_rec args))
1.194                                       cons))) conss));
1.195    local
1.196      (* check whether every/exists constructor of the n-th part of the equation:
1.197 @@ -425,11 +425,11 @@
1.198            is_rec arg andalso not(rec_of arg mem ns) andalso
1.199            ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse
1.200              rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns)
1.201 -              (lazy_rec orelse is_lazy arg) (n, (nth_elem(rec_of arg,conss))))
1.202 +              (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
1.203            ) o snd) cons;
1.204      fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
1.205      fun warn (n,cons)  = if all_rec_to [] false (n,cons) then (warning
1.206 -        ("domain "^nth_elem(n,dnames)^" is empty!"); true) else false;
1.207 +        ("domain "^List.nth(dnames,n)^" is empty!"); true) else false;
1.208      fun lazy_rec_to ns = rec_to exists Id  lazy_rec_to ns;
1.209
1.210    in val n__eqs     = mapn (fn n => fn (_,cons) => (n,cons)) 0 eqs;
1.211 @@ -444,18 +444,18 @@
1.212                                  induct_tac "n" 1,
1.213                                  simp_tac (take_ss addsimps prems) 1,
1.214                                  TRY(safe_tac HOL_cs)]
1.215 -                                @ flat(map (fn (cons,cases) => [
1.216 +                                @ List.concat(map (fn (cons,cases) => [
1.217                                   res_inst_tac [("x","x")] cases 1,
1.218                                   asm_simp_tac (take_ss addsimps prems) 1]
1.219 -                                 @ flat(map (fn (con,args) =>
1.220 +                                 @ List.concat(map (fn (con,args) =>
1.221                                    asm_simp_tac take_ss 1 ::
1.222                                    map (fn arg =>
1.223                                     case_UU_tac (prems@con_rews) 1 (
1.224 -                           nth_elem(rec_of arg,dnames)^"_take n\$"^vname arg))
1.225 -                                  (filter is_nonlazy_rec args) @ [
1.226 +                           List.nth(dnames,rec_of arg)^"_take n\$"^vname arg))
1.227 +                                  (List.filter is_nonlazy_rec args) @ [
1.228                                    resolve_tac prems 1] @
1.229                                    map (K (atac 1))      (nonlazy args) @
1.230 -                                  map (K (etac spec 1)) (filter is_rec args))
1.231 +                                  map (K (etac spec 1)) (List.filter is_rec args))
1.232                                   cons))
1.233                                  (conss~~cases)));
1.234
1.235 @@ -496,14 +496,14 @@
1.236                                  induct_tac "n" 1,
1.237                                  simp_tac take_ss 1,
1.239 -                                flat(mapn (fn n => fn (cons,cases) => [
1.240 +                                List.concat(mapn (fn n => fn (cons,cases) => [
1.241                                    simp_tac take_ss 1,
1.242                                    rtac allI 1,
1.243                                    res_inst_tac [("x",x_name n)] cases 1,
1.244                                    asm_simp_tac take_ss 1] @
1.245 -                                  flat(map (fn (con,args) =>
1.246 +                                  List.concat(map (fn (con,args) =>
1.247                                      asm_simp_tac take_ss 1 ::
1.248 -                                    flat(map (fn vn => [
1.249 +                                    List.concat(map (fn vn => [
1.250                                        eres_inst_tac [("x",vn)] all_dupE 1,
1.251                                        etac disjE 1,
1.252                                        asm_simp_tac (HOL_ss addsimps con_rews) 1,
1.253 @@ -523,7 +523,7 @@
1.254    (finites,
1.255     pg'' thy[](ind_term (fn n => fn dn => %:(P_name n) \$ %:(x_name n)))(fn prems =>
1.256                                  TRY(safe_tac HOL_cs) ::
1.257 -                         flat (map (fn (finite,fin_ind) => [
1.258 +                         List.concat (map (fn (finite,fin_ind) => [
1.259                                 rtac(rewrite_rule axs_finite_def finite RS exE)1,
1.260                                  etac subst 1,
1.261                                  rtac fin_ind 1,
1.262 @@ -532,7 +532,7 @@
1.263  ) end (* let *) else
1.264    (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy)
1.265                      [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
1.266 -   pg'' thy [] (foldr (op ===>) (mapn (fn n => K(mk_trp(%%:"adm" \$ %:(P_name n))))
1.267 +   pg'' thy [] (Library.foldr (op ===>) (mapn (fn n => K(mk_trp(%%:"adm" \$ %:(P_name n))))
1.268                 1 dnames, ind_term (fn n => fn dn => %:(P_name n) \$ %:(x_name n))))
1.269                     (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1)
1.270                                      axs_reach @ [
1.271 @@ -556,8 +556,8 @@
1.272    val take_ss = HOL_ss addsimps take_rews;
1.273    val sproj   = prj (fn s => K("fst("^s^")")) (fn s => K("snd("^s^")"));
1.274    val coind_lemma=pg[ax_bisim_def](mk_trp(mk_imp(%%:(comp_dname^"_bisim") \$ %:"R",
1.275 -                foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
1.276 -                  foldr mk_imp (mapn (fn n => K(proj (%:"R") eqs n \$
1.277 +                Library.foldr (fn (x,t)=> mk_all(x,mk_all(x^"'",t))) (xs,
1.278 +                  Library.foldr mk_imp (mapn (fn n => K(proj (%:"R") eqs n \$
1.279                                        bnd_arg n 0 \$ bnd_arg n 1)) 0 dnames,
1.280                      foldr' mk_conj (mapn (fn n => fn dn =>
1.281                                  (dc_take dn \$ %:"n" `bnd_arg n 0 ===
1.282 @@ -566,7 +566,7 @@
1.283                                  induct_tac "n" 1,
1.284                                  simp_tac take_ss 1,
1.285                                  safe_tac HOL_cs] @
1.286 -                                flat(mapn (fn n => fn x => [
1.287 +                                List.concat(mapn (fn n => fn x => [
1.288                                    rotate_tac (n+1) 1,
1.289                                    etac all2E 1,
1.290                                    eres_inst_tac [("P1", sproj "R" eqs n^
1.291 @@ -576,11 +576,11 @@
1.292                                  0 xs));
1.293  in
1.294  val coind = pg [] (mk_trp(%%:(comp_dname^"_bisim") \$ %:"R") ===>
1.295 -                foldr (op ===>) (mapn (fn n => fn x =>
1.296 +                Library.foldr (op ===>) (mapn (fn n => fn x =>
1.297                    mk_trp(proj (%:"R") eqs n \$ %:x \$ %:(x^"'"))) 0 xs,
1.298                    mk_trp(foldr' mk_conj (map (fn x => %:x === %:(x^"'")) xs)))) ([
1.299                                  TRY(safe_tac HOL_cs)] @
1.300 -                                flat(map (fn take_lemma => [
1.301 +                                List.concat(map (fn take_lemma => [
1.302                                    rtac take_lemma 1,
1.303                                    cut_facts_tac [coind_lemma] 1,
1.304                                    fast_tac HOL_cs 1])
```