1.1 --- a/src/HOL/Tools/record.ML	Sat Jun 19 06:43:33 2010 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Jun 19 09:14:06 2010 +0200
     1.3 @@ -101,21 +101,21 @@
     1.4    fun merge data = Symtab.merge Thm.eq_thm_prop data;   (* FIXME handle Symtab.DUP ?? *)
     1.5  );
     1.6  
     1.7 -fun do_typedef name repT alphas thy =
     1.8 +fun do_typedef tyco repT alphas thy =
     1.9    let
    1.10 -    fun get_thms thy name =
    1.11 +    val (b_constr, b_proj) = pairself Binding.name ("Abs_" ^  tyco, "Rep_" ^  tyco); (*FIXME*)
    1.12 +    fun get_thms thy tyco =
    1.13        let
    1.14 -        val [({Abs_name, abs_type = absT, ...}, {Rep_inject, Abs_inverse, ...})] =
    1.15 -          Typedef.get_info_global thy name;
    1.16 -        val rewrite_rule =
    1.17 -          MetaSimplifier.rewrite_rule [@{thm iso_tuple_UNIV_I}, @{thm iso_tuple_True_simp}];
    1.18 +        val SOME { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
    1.19 +          Typecopy.get_info thy tyco;
    1.20 +        val absT = Type (tyco, map TFree vs);
    1.21        in
    1.22 -        (map rewrite_rule [Rep_inject, Abs_inverse], Const (Abs_name, repT --> absT), absT)
    1.23 +        ((proj_inject, proj_constr), Const (constr, repT --> absT), absT)
    1.24        end;
    1.25    in
    1.26      thy
    1.27 -    |> Typecopy.typecopy (Binding.name name, alphas) repT NONE
    1.28 -    |-> (fn (name, _) => `(fn thy => get_thms thy name))
    1.29 +    |> Typecopy.typecopy (Binding.name tyco, alphas) repT b_constr b_proj
    1.30 +    |-> (fn (tyco, _) => `(fn thy => get_thms thy tyco))
    1.31    end;
    1.32  
    1.33  fun mk_cons_tuple (left, right) =
    1.34 @@ -135,7 +135,7 @@
    1.35    let
    1.36      val repT = HOLogic.mk_prodT (leftT, rightT);
    1.37  
    1.38 -    val (([rep_inject, abs_inverse], absC, absT), typ_thy) =
    1.39 +    val (((rep_inject, abs_inverse), absC, absT), typ_thy) =
    1.40        thy
    1.41        |> do_typedef name repT alphas
    1.42        ||> Sign.add_path name;

     2.1 --- a/src/HOL/Tools/typecopy.ML	Sat Jun 19 06:43:33 2010 +0200
     2.2 +++ b/src/HOL/Tools/typecopy.ML	Sat Jun 19 09:14:06 2010 +0200
     2.3 @@ -6,9 +6,9 @@
     2.4  
     2.5  signature TYPECOPY =
     2.6  sig
     2.7 -  type info = { vs: (string * sort) list, constr: string, typ: typ,
     2.8 -    inject: thm, proj: string * typ, proj_def: thm }
     2.9 -  val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option
    2.10 +  type info = { vs: (string * sort) list, typ: typ, constr: string, proj: string,
    2.11 +    constr_inject: thm, proj_inject: thm, constr_proj: thm, proj_constr: thm }
    2.12 +  val typecopy: binding * (string * sort) list -> typ -> binding -> binding
    2.13      -> theory -> (string * info) * theory
    2.14    val get_info: theory -> string -> info option
    2.15    val interpretation: (string -> theory -> theory) -> theory -> theory
    2.16 @@ -23,14 +23,16 @@
    2.17  
    2.18  type info = {
    2.19    vs: (string * sort) list,
    2.20 +  typ: typ,
    2.21    constr: string,
    2.22 -  typ: typ,
    2.23 -  inject: thm,
    2.24 -  proj: string * typ,
    2.25 -  proj_def: thm
    2.26 +  proj: string,
    2.27 +  constr_inject: thm,
    2.28 +  proj_inject: thm,
    2.29 +  constr_proj: thm,
    2.30 +  proj_constr: thm
    2.31  };
    2.32  
    2.33 -structure TypecopyData = Theory_Data
    2.34 +structure Typecopy_Data = Theory_Data
    2.35  (
    2.36    type T = info Symtab.table;
    2.37    val empty = Symtab.empty;
    2.38 @@ -38,7 +40,7 @@
    2.39    fun merge data = Symtab.merge (K true) data;
    2.40  );
    2.41  
    2.42 -val get_info = Symtab.lookup o TypecopyData.get;
    2.43 +val get_info = Symtab.lookup o Typecopy_Data.get;
    2.44  
    2.45  
    2.46  (* interpretation of type copies *)
    2.47 @@ -49,40 +51,42 @@
    2.48  
    2.49  (* introducing typecopies *)
    2.50  
    2.51 -fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
    2.52 +fun add_info tyco vs (({ rep_type, Abs_name, Rep_name, ...},
    2.53 +    { Abs_inject, Rep_inject, Abs_inverse, Rep_inverse, ... }) : Typedef.info) thy =
    2.54 +  let
    2.55 +    val exists_thm =
    2.56 +      UNIV_I
    2.57 +      |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global rep_type))] [];
    2.58 +    val constr_inject = Abs_inject OF [exists_thm, exists_thm];
    2.59 +    val proj_constr = Abs_inverse OF [exists_thm];
    2.60 +    val info = {
    2.61 +      vs = vs,
    2.62 +      typ = rep_type,
    2.63 +      constr = Abs_name,
    2.64 +      proj = Rep_name,
    2.65 +      constr_inject = constr_inject,
    2.66 +      proj_inject = Rep_inject,
    2.67 +      constr_proj = Rep_inverse,
    2.68 +      proj_constr = proj_constr
    2.69 +    };
    2.70 +  in
    2.71 +    thy
    2.72 +    |> (Typecopy_Data.map o Symtab.update_new) (tyco, info)
    2.73 +    |> Typecopy_Interpretation.data tyco
    2.74 +    |> pair (tyco, info)
    2.75 +  end
    2.76 +
    2.77 +fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
    2.78    let
    2.79      val ty = Sign.certify_typ thy raw_ty;
    2.80      val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
    2.81      val vs = map (ProofContext.check_tfree ctxt) raw_vs;
    2.82      val tac = Tactic.rtac UNIV_witness 1;
    2.83 -    fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    2.84 -          Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... })
    2.85 -          : Typedef.info) thy =
    2.86 -        let
    2.87 -          val exists_thm =
    2.88 -            UNIV_I
    2.89 -            |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
    2.90 -          val inject' = inject OF [exists_thm, exists_thm];
    2.91 -          val proj_def = inverse OF [exists_thm];
    2.92 -          val info = {
    2.93 -            vs = vs,
    2.94 -            constr = c_abs,
    2.95 -            typ = ty_rep,
    2.96 -            inject = inject',
    2.97 -            proj = (c_rep, ty_abs --> ty_rep),
    2.98 -            proj_def = proj_def
    2.99 -          };
   2.100 -        in
   2.101 -          thy
   2.102 -          |> (TypecopyData.map o Symtab.update_new) (tyco, info)
   2.103 -          |> Typecopy_Interpretation.data tyco
   2.104 -          |> pair (tyco, info)
   2.105 -        end
   2.106    in
   2.107      thy
   2.108      |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
   2.109 -      (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
   2.110 -    |-> (fn (tyco, info) => add_info tyco info)
   2.111 +      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
   2.112 +    |-> (fn (tyco, info) => add_info tyco vs info)
   2.113    end;
   2.114  
   2.115  
   2.116 @@ -90,10 +94,8 @@
   2.117  
   2.118  fun add_default_code tyco thy =
   2.119    let
   2.120 -    val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
   2.121 -      typ = ty_rep, ... } = get_info thy tyco;
   2.122 -    (* FIXME handle multiple typedef interpretations (!??) *)
   2.123 -    val [(_, { Rep_inject = proj_inject, ... })] = Typedef.get_info_global thy tyco;
   2.124 +    val SOME { vs, typ = ty_rep, constr = c, proj, proj_constr, proj_inject, ... } =
   2.125 +      get_info thy tyco;
   2.126      val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
   2.127      val ty = Type (tyco, map TFree vs);
   2.128      val proj = Const (proj, ty --> ty_rep);
   2.129 @@ -113,7 +115,7 @@
   2.130    in
   2.131      thy
   2.132      |> Code.add_datatype [constr]
   2.133 -    |> Code.add_eqn proj_eq
   2.134 +    |> Code.add_eqn proj_constr
   2.135      |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
   2.136      |> `(fn lthy => Syntax.check_term lthy eq)
   2.137      |-> (fn eq => Specification.definition