(*  Title:      HOL/Tools/typecopy_package.ML

     ID:         $Id$

     Author:     Florian Haftmann, TU Muenchen

 Introducing copies of types using trivial typedefs; datatype-like abstraction.

 *)

 signature TYPECOPY_PACKAGE =

 sig

   type info = {

     vs: (string * sort) list,

     constr: string,

     typ: typ,

     inject: thm,

     proj: string * typ,

     proj_def: thm

   }

   val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option

     -> theory -> (string * info) * theory

   val get_typecopies: theory -> string list

   val get_info: theory -> string -> info option

   val interpretation: (string -> theory -> theory) -> theory -> theory

   val print_typecopies: theory -> unit

   val setup: theory -> theory

 end;

 structure TypecopyPackage: TYPECOPY_PACKAGE =

 struct

 (* theory data *)

 type info = {

   vs: (string * sort) list,

   constr: string,

   typ: typ,

   inject: thm,

   proj: string * typ,

   proj_def: thm

 };

 structure TypecopyData = TheoryDataFun

 (

   type T = info Symtab.table;

   val empty = Symtab.empty;

   val copy = I;

   val extend = I;

   fun merge _ = Symtab.merge (K true);

 );

 fun print_typecopies thy =

   let

     val tab = TypecopyData.get thy;

     fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =

       (Pretty.block o Pretty.breaks) [

         Syntax.pretty_typ_global thy (Type (tyco, map TFree vs)),

         Pretty.str "=",

         (Pretty.str o Sign.extern_const thy) constr,

         Syntax.pretty_typ_global thy typ,

         Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]];

     in

       (Pretty.writeln o Pretty.block o Pretty.fbreaks)

         (Pretty.str "type copies:" :: map mk (Symtab.dest tab))

     end;

 val get_typecopies = Symtab.keys o TypecopyData.get;

 val get_info = Symtab.lookup o TypecopyData.get;

 (* interpretation of type copies *)

 structure TypecopyInterpretation = InterpretationFun(type T = string val eq = op =);

 val interpretation = TypecopyInterpretation.interpretation;

 (* add a type copy *)

 local

 fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =

   let

     val ty = prep_typ thy raw_ty;

     val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) 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, ... } : TypedefPackage.info ) thy =

         let

           val exists_thm =

             UNIV_I

             |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT 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)

           |> TypecopyInterpretation.data tyco

           |> pair (tyco, info)

         end

   in

     thy

     |> TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)

       (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac

     |-> (fn (tyco, info) => add_info tyco info)

   end;

 in

 val add_typecopy = gen_add_typecopy Sign.certify_typ;

 end;

 (* code generator setup *)

 fun add_typecopy_spec tyco thy =

   let

     val SOME { constr, proj_def, inject, vs, ... } = get_info thy tyco;

     val vs' = (map o apsnd) (curry (Sorts.inter_sort (Sign.classes_of thy)) [HOLogic.class_eq]) vs;

     val ty = Logic.unvarifyT (Sign.the_const_type thy constr);

     fun add_def tyco lthy =

       let

         val ty = Type (tyco, map TFree vs');

         fun mk_side const_name = Const (const_name, ty --> ty --> HOLogic.boolT)

           $ Free ("x", ty) $ Free ("y", ty);

         val def = HOLogic.mk_Trueprop (HOLogic.mk_eq

           (mk_side @{const_name eq_class.eq}, mk_side @{const_name "op ="}));

         val def' = Syntax.check_term lthy def;

         val ((_, (_, thm)), lthy') = Specification.definition

           (NONE, ((Name.no_binding, []), def')) lthy;

         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy);

         val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm;

       in (thm', lthy') end;

     fun tac thms = Class.intro_classes_tac []

       THEN ALLGOALS (ProofContext.fact_tac thms);

     fun add_eq_thm thy = 

       let

         val eq = inject

           |> Code_Unit.constrain_thm [HOLogic.class_eq]

           |> Simpdata.mk_eq

           |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];

       in Code.add_func eq thy end;

   in

     thy

     |> Code.add_datatype [(constr, ty)]

     |> Code.add_func proj_def

     |> TheoryTarget.instantiation ([tyco], vs', [HOLogic.class_eq])

     |> add_def tyco

     |-> (fn thm => Class.prove_instantiation_instance (K (tac [thm]))

     #> LocalTheory.exit

     #> ProofContext.theory_of

     #> Code.del_func thm

     #> add_eq_thm)

   end;

 val setup =

   TypecopyInterpretation.init

   #> interpretation add_typecopy_spec

 end;