domain_isomorphism package defines copy functions

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 16:50:25 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 17:53:22 2009 -0800
@@ -150,8 +150,8 @@
                    mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
 
   in (dnam,
-      if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax],
-      [when_def, copy_def] @
+      (if definitional then [reach_ax] else [abs_iso_ax, rep_iso_ax, reach_ax]),
+      (if definitional then [when_def] else [when_def, copy_def]) @
       con_defs @ dis_defs @ mat_defs @ pat_defs @ sel_defs @
       [take_def, finite_def])
   end; (* let (calc_axioms) *)

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 16:50:25 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 17:53:22 2009 -0800
@@ -558,6 +558,52 @@
     val (_, thy) = thy |>
       (PureThy.add_thms o map Thm.no_attributes)
         (map_ID_binds ~~ map_ID_thms);
+
+    (* define copy combinators *)
+    val new_dts =
+      map (apsnd (map (fst o dest_TFree)) o dest_Type o fst) dom_eqns;
+    val copy_arg_type = tupleT (map (fn (T, _) => T ->> T) dom_eqns);
+    val copy_args =
+      let fun mk_copy_args [] t = []
+            | mk_copy_args (_::[]) t = [t]
+            | mk_copy_args (_::xs) t =
+              HOLogic.mk_fst t :: mk_copy_args xs (HOLogic.mk_snd t);
+      in mk_copy_args doms (Free ("f", copy_arg_type)) end;
+    fun copy_of_dtyp (T, dt) =
+        if DatatypeAux.is_rec_type dt
+        then copy_of_dtyp' (T, dt)
+        else ID_const T
+    and copy_of_dtyp' (T, DatatypeAux.DtRec i) = nth copy_args i
+      | copy_of_dtyp' (T, DatatypeAux.DtTFree a) = ID_const T
+      | copy_of_dtyp' (T as Type (_, Ts), DatatypeAux.DtType (c, ds)) =
+        case Symtab.lookup map_tab' c of
+          SOME f =>
+          Library.foldl mk_capply
+            (Const (f, mapT T), map copy_of_dtyp (Ts ~~ ds))
+        | NONE =>
+          (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID_const T);
+    fun define_copy ((tbind, (rep_const, abs_const)), (lhsT, rhsT)) thy =
+      let
+        val copy_type = copy_arg_type ->> (lhsT ->> lhsT);
+        val copy_bind = Binding.suffix_name "_copy" tbind;
+        val (copy_const, thy) = thy |>
+          Sign.declare_const ((copy_bind, copy_type), NoSyn);
+        val dtyp = DatatypeAux.dtyp_of_typ new_dts rhsT;
+        val body = copy_of_dtyp (rhsT, dtyp);
+        val comp = mk_cfcomp (abs_const, mk_cfcomp (body, rep_const));
+        val rhs = big_lambda (Free ("f", copy_arg_type)) comp;
+        val eqn = Logic.mk_equals (copy_const, rhs);
+        val ([copy_def], thy) =
+          thy
+          |> Sign.add_path (Binding.name_of tbind)
+          |> (PureThy.add_defs false o map Thm.no_attributes)
+              [(Binding.name "copy_def", eqn)]
+          ||> Sign.parent_path;
+      in ((copy_const, copy_def), thy) end;
+    val ((copy_consts, copy_defs), thy) = thy
+      |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
+      |>> ListPair.unzip;
+
   in
     thy
   end;

--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Nov 19 16:50:25 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Nov 19 17:53:22 2009 -0800
@@ -163,10 +163,10 @@
     val Case_trans = maps one_case_trans cons';
     end;
     end;
-    val rep_abs_consts =
-        if definitional then [] else [const_rep, const_abs];
+    val optional_consts =
+        if definitional then [] else [const_rep, const_abs, const_copy];
 
-  in (rep_abs_consts @ [const_when, const_copy] @ 
+  in (optional_consts @ [const_when] @ 
       consts_con @ consts_dis @ consts_mat @ consts_pat @ consts_sel @
       [const_take, const_finite],
       (case_trans::(abscon_trans @ Case_trans)))