# HG changeset patch
# User haftmann
# Date 1276931646 -7200
# Node ID 1436d6f28f175e9fa1f307b7fd50831cd5346a80
# Parent  a2a3b62fc819b9a19104fc6e8fba18cf572f02b5
cleanup of typecopy package

diff -r a2a3b62fc819 -r 1436d6f28f17 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Jun 19 06:43:33 2010 +0200
+++ b/src/HOL/Tools/record.ML	Sat Jun 19 09:14:06 2010 +0200
@@ -101,21 +101,21 @@
   fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
 );
 
-fun do_typedef name repT alphas thy =
+fun do_typedef tyco repT alphas thy =
   let
-    fun get_thms thy name =
+    val (b_constr, b_proj) = pairself Binding.name ("Abs_" ^  tyco, "Rep_" ^  tyco); (*FIXME*)
+    fun get_thms thy tyco =
       let
-        val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
-          Typedef.get_info_global thy name;
-        val rewrite_rule =
-          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
+        val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
+          Typecopy.get_info thy tyco;
+        val absT = Type (tyco, map TFree vs);
       in
-        (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
+        ((proj_inject, proj_constr), Const (constr, repT --> absT), absT)
       end;
   in
     thy
-    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
-    |-> (fn (name, _) => `(fn thy => get_thms thy name))
+    |> Typecopy.typecopy (Binding.name tyco, alphas) repT b_constr b_proj
+    |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
   end;
 
 fun mk_cons_tuple (left, right) =
@@ -135,7 +135,7 @@
   let
     val repT = HOLogic.mk_prodT (leftT, rightT);
 
-    val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
+    val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
       thy
       |> do_typedef name repT alphas
       ||> Sign.add_path name;
diff -r a2a3b62fc819 -r 1436d6f28f17 src/HOL/Tools/typecopy.ML
--- a/src/HOL/Tools/typecopy.ML	Sat Jun 19 06:43:33 2010 +0200
+++ b/src/HOL/Tools/typecopy.ML	Sat Jun 19 09:14:06 2010 +0200
@@ -6,9 +6,9 @@
 
 signature TYPECOPY =
 sig
-  type info = { vs: (string * sort) list, constr: string, typ: typ,
-    inject: thm, proj: string * typ, proj_def: thm }
-  val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
+  type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
+    constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
+  val typecopy: binding * (string * sort) list -> typ -> binding -> binding
     -> theory -> (string * info) * theory
   val get_info: theory -> string -> info option
   val interpretation: (string -> theory -> theory) -> theory -> theory
@@ -23,14 +23,16 @@
 
 type info = {
   vs: (string * sort) list,
+  typ: typ,
   constr: string,
-  typ: typ,
-  inject: thm,
-  proj: string * typ,
-  proj_def: thm
+  proj: string,
+  constr_inject: thm,
+  proj_inject: thm,
+  constr_proj: thm,
+  proj_constr: thm
 };
 
-structure TypecopyData = Theory_Data
+structure Typecopy_Data = Theory_Data
 (
   type T = info Symtab.table;
   val empty = Symtab.empty;
@@ -38,7 +40,7 @@
   fun merge data = Symtab.merge (K true) data;
 );
 
-val get_info = Symtab.lookup o TypecopyData.get;
+val get_info = Symtab.lookup o Typecopy_Data.get;
 
 
 (* interpretation of type copies *)
@@ -49,40 +51,42 @@
 
 (* introducing typecopies *)
 
-fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
+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
+    |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
+    |> Typecopy_Interpretation.data tyco
+    |> 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;
-    fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
-          Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
-          : Typedef.info) thy =
-        let
-          val exists_thm =
-            UNIV_I
-            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
-          val inject' = inject OF [exists_thm, exists_thm];
-          val proj_def = inverse OF [exists_thm];
-          val info = {
-            vs = vs,
-            constr = c_abs,
-            typ = ty_rep,
-            inject = inject',
-            proj = (c_rep, ty_abs --> ty_rep),
-            proj_def = proj_def
-          };
-        in
-          thy
-          |> (TypecopyData.map o Symtab.update_new) (tyco, info)
-          |> Typecopy_Interpretation.data tyco
-          |> pair (tyco, info)
-        end
   in
     thy
     |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
-      (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
-    |-> (fn (tyco, info) => add_info tyco info)
+      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
+    |-> (fn (tyco, info) => add_info tyco vs info)
   end;
 
 
@@ -90,10 +94,8 @@
 
 fun add_default_code tyco thy =
   let
-    val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
-      typ = ty_rep, ... } = get_info thy tyco;
-    (* FIXME handle multiple typedef interpretations (!??) *)
-    val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
+    val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
+      get_info thy tyco;
     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);
@@ -113,7 +115,7 @@
   in
     thy
     |> Code.add_datatype [constr]
-    |> Code.add_eqn proj_eq
+    |> Code.add_eqn proj_constr
     |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
     |> `(fn lthy => Syntax.check_term lthy eq)
     |-> (fn eq => Specification.definition