formally integrated typecopy layer into record package

--- a/src/HOL/Tools/record.ML	Tue Aug 17 15:13:16 2010 +0200
+++ b/src/HOL/Tools/record.ML	Tue Aug 17 15:17:44 2010 +0200
@@ -93,21 +93,90 @@
   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
 
+fun add_default_code tyco { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } thy =
+  let
+    val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
+    val ty = Type (tyco, map TFree vs);
+    val proj = Const (proj, ty --> ty_rep);
+    val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
+    val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
+      $ t_x $ t_y;
+    val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
+    val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
+    fun tac eq_thm = Class.intro_classes_tac []
+      THEN (Simplifier.rewrite_goals_tac
+        (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
+          THEN ALLGOALS (rtac @{thm refl});
+    fun mk_eq_refl thy = @{thm HOL.eq_refl}
+      |> Thm.instantiate
+         ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
+      |> AxClass.unoverload thy;
+  in
+    thy
+    |> Code.add_datatype [constr]
+    |> Code.add_eqn proj_constr
+    |> Class.instantiation ([tyco], vs, [HOLogic.class_eq])
+    |> `(fn lthy => Syntax.check_term lthy eq)
+    |-> (fn eq => Specification.definition
+         (NONE, (Attrib.empty_binding, eq)))
+    |-> (fn (_, (_, eq_thm)) =>
+       Class.prove_instantiation_exit_result Morphism.thm
+         (fn _ => fn eq_thm => tac eq_thm) eq_thm)
+    |-> (fn eq_thm => Code.add_eqn eq_thm)
+    |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
+  end;
+
+fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
+    { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
+  let
+    val exists_thm =
+      UNIV_I
+      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
+    val constr_inject = Abs_inject OF [exists_thm, exists_thm];
+    val proj_constr = Abs_inverse OF [exists_thm];
+    val info = {
+      vs = vs,
+      typ = rep_type,
+      constr = Abs_name,
+      proj = Rep_name,
+      constr_inject = constr_inject,
+      proj_inject = Rep_inject,
+      constr_proj = Rep_inverse,
+      proj_constr = proj_constr
+    };
+  in
+    thy
+    |> add_default_code tyco info
+    |> Quickcheck_Record.ensure_random_typecopy tyco vs Abs_name rep_type
+    |> pair (tyco, info)
+  end
+
+fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
+  let
+    val ty = Sign.certify_typ thy raw_ty;
+    val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
+    val vs = map (ProofContext.check_tfree ctxt) raw_vs;
+    val tac = Tactic.rtac UNIV_witness 1;
+  in
+    thy
+    |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
+      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
+    |-> (fn (tyco, info) => add_info tyco vs info)
+  end;
+
 fun do_typedef b repT alphas thy =
   let
     val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
-    fun get_thms thy tyco =
+    fun get_info thy tyco { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
       let
-        val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
-          Typecopy.get_info thy tyco;
         val absT = Type (tyco, map TFree vs);
       in
         ((proj_inject, proj_constr), Const (constr, repT --> absT), absT)
       end;
   in
     thy
-    |> Typecopy.typecopy (b, alphas) repT b_constr b_proj
-    |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
+    |> typecopy (b, alphas) repT b_constr b_proj
+    |-> (fn (tyco, info) => `(fn thy => get_info thy tyco info))
   end;
 
 fun mk_cons_tuple (left, right) =