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.156                              simp_tac(iterate_Cprod_ss addsimps copy_con_rews) 1,
   1.157                                  asm_full_simp_tac (HOLCF_ss addsimps 
   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.165                                  asm_full_simp_tac (HOLCF_ss addsimps copy_rews)1
   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.238                          TRY(safe_tac(empty_cs addSEs[conjE] addSIs[conjI]))] @
   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])