domain_isomorphism package defines combined copy function

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 20:09:56 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 21:06:22 2009 -0800
@@ -241,10 +241,11 @@
     val thy = thy'
       |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
 
+    val use_copy_def = length eqs>1 andalso not definitional;
   in
     thy
     |> Sign.add_path comp_dnam  
-    |> add_defs_infer (bisim_def::(if length eqs>1 then [copy_def] else []))
+    |> add_defs_infer (bisim_def::(if use_copy_def then [copy_def] else []))
     |> Sign.parent_path
     |> fold add_matchers eqs
   end; (* let (add_axioms) *)

--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 20:09:56 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 21:06:22 2009 -0800
@@ -563,12 +563,13 @@
     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_arg = Free ("f", copy_arg_type);
     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;
+      in mk_copy_args doms copy_arg end;
     fun copy_of_dtyp (T, dt) =
         if DatatypeAux.is_rec_type dt
         then copy_of_dtyp' (T, dt)
@@ -591,7 +592,7 @@
         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 rhs = big_lambda copy_arg comp;
         val eqn = Logic.mk_equals (copy_const, rhs);
         val ([copy_def], thy) =
           thy
@@ -604,6 +605,29 @@
       |> fold_map define_copy (dom_binds ~~ rep_abs_consts ~~ dom_eqns)
       |>> ListPair.unzip;
 
+    (* define combined copy combinator *)
+    val ((c_const, c_def_thms), thy) =
+      if length doms = 1
+      then ((hd copy_consts, []), thy)
+      else
+        let
+          val c_type = copy_arg_type ->> copy_arg_type;
+          val c_name = space_implode "_" (map Binding.name_of dom_binds);
+          val c_bind = Binding.name (c_name ^ "_copy");
+          val c_body =
+              mk_tuple (map (mk_capply o rpair copy_arg) copy_consts);
+          val c_rhs = big_lambda copy_arg c_body;
+          val (c_const, thy) =
+            Sign.declare_const ((c_bind, c_type), NoSyn) thy;
+          val c_eqn = Logic.mk_equals (c_const, c_rhs);
+          val (c_def_thms, thy) =
+            thy
+            |> Sign.add_path c_name
+            |> (PureThy.add_defs false o map Thm.no_attributes)
+                [(Binding.name "copy_def", c_eqn)]
+            ||> Sign.parent_path;
+        in ((c_const, c_def_thms), thy) end;
+
   in
     thy
   end;

--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Nov 19 20:09:56 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Thu Nov 19 21:06:22 2009 -0800
@@ -196,7 +196,8 @@
   in thy''
        |> ContConsts.add_consts_i
            (maps fst ctt @ 
-            (if length eqs'>1 then [const_copy] else[])@
+            (if length eqs'>1 andalso not definitional
+             then [const_copy] else []) @
             [const_bisim])
        |> Sign.add_trrules_i (maps snd ctt)
   end; (* let *)