src/HOL/Tools/typecopy_package.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 20855 9f60d493c8fe
child 21675 38f6cb45ce24
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (*  Title:      HOL/Tools/typecopy_package.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Introducing copies of types using trivial typedefs; datatype-like abstraction.
     6 *)
     7 
     8 signature TYPECOPY_PACKAGE =
     9 sig
    10   type info = {
    11     vs: (string * sort) list,
    12     constr: string,
    13     typ: typ,
    14     inject: thm,
    15     proj: string * typ,
    16     proj_def: thm
    17   }
    18   val add_typecopy: bstring * string list -> typ -> (bstring * bstring) option
    19     -> theory -> (string * info) * theory
    20   val get_typecopies: theory -> string list
    21   val get_typecopy_info: theory -> string -> info option
    22   type hook = string * info -> theory -> theory
    23   val add_hook: hook -> theory -> theory
    24   val get_spec: theory -> string -> (string * sort) list * (string * typ list) list
    25   val get_cert: theory -> string -> thm
    26   val get_eq: theory -> string -> thm
    27   val print: theory -> unit
    28   val setup: theory -> theory
    29 end;
    30 
    31 structure TypecopyPackage: TYPECOPY_PACKAGE =
    32 struct
    33 
    34 (* theory context reference *)
    35 
    36 val univ_witness = thm "Set.UNIV_witness"
    37 
    38 
    39 (* theory data *)
    40 
    41 type info = {
    42   vs: (string * sort) list,
    43   constr: string,
    44   typ: typ,
    45   inject: thm,
    46   proj: string * typ,
    47   proj_def: thm
    48 };
    49 
    50 type hook = string * info -> theory -> theory;
    51 
    52 structure TypecopyData = TheoryDataFun
    53 (struct
    54   val name = "HOL/typecopy_package";
    55   type T = info Symtab.table * (serial * hook) list;
    56   val empty = (Symtab.empty, []);
    57   val copy = I;
    58   val extend = I;
    59   fun merge _ ((tab1, hooks1), (tab2, hooks2) : T) =
    60     (Symtab.merge (K true) (tab1, tab2), AList.merge (op =) (K true) (hooks1, hooks2));
    61   fun print thy (tab, _) =
    62     let
    63       fun mk (tyco, { vs, constr, typ, proj = (proj, _), ... } : info) =
    64         (Pretty.block o Pretty.breaks) [
    65           Sign.pretty_typ thy (Type (tyco, map TFree vs)),
    66           Pretty.str "=",
    67           (Pretty.str o Sign.extern_const thy) constr,
    68           Sign.pretty_typ thy typ,
    69           Pretty.block [Pretty.str "(", (Pretty.str o Sign.extern_const thy) proj, Pretty.str  ")"]
    70         ];
    71     in
    72       (Pretty.writeln o Pretty.block o Pretty.fbreaks) (
    73         Pretty.str "type copies:"
    74         :: map mk (Symtab.dest tab)
    75       )
    76     end;
    77 end);
    78 
    79 val print = TypecopyData.print;
    80 val get_typecopies = Symtab.keys o fst o TypecopyData.get;
    81 val get_typecopy_info = Symtab.lookup o fst o TypecopyData.get;
    82 
    83 
    84 (* hook management *)
    85 
    86 fun add_hook hook =
    87   (TypecopyData.map o apsnd o cons) (serial (), hook);
    88 
    89 fun invoke_hooks tyco_info thy =
    90   fold (fn (_, f) => f tyco_info) ((snd o TypecopyData.get) thy) thy;
    91 
    92 
    93 (* add a type copy *)
    94 
    95 local
    96 
    97 fun gen_add_typecopy prep_typ (raw_tyco, raw_vs) raw_ty constr_proj thy =
    98   let
    99     val ty = prep_typ thy raw_ty;
   100     val vs = AList.make (the_default HOLogic.typeS o AList.lookup (op =) (typ_tfrees ty)) raw_vs;
   101     val tac = Tactic.rtac UNIV_witness 1;
   102     fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
   103       Rep_name = c_rep, Abs_inject = inject,
   104       Abs_inverse = inverse, ... } : TypedefPackage.info ) thy = 
   105         let
   106           val exists_thm =
   107             UNIV_I
   108             |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT ty_rep))] [];
   109           val inject' = inject OF [exists_thm, exists_thm];
   110           val proj_def = inverse OF [exists_thm];
   111           val info = {
   112             vs = vs,
   113             constr = c_abs,
   114             typ = ty_rep,
   115             inject = inject',
   116             proj = (c_rep, ty_abs --> ty_rep),
   117             proj_def = proj_def
   118           };
   119         in
   120           thy
   121           |> (TypecopyData.map o apfst o Symtab.update_new) (tyco, info)
   122           |> invoke_hooks (tyco, info)
   123           |> pair (tyco, info)
   124         end
   125   in
   126     thy
   127     |> setmp TypedefPackage.quiet_mode true
   128         (TypedefPackage.add_typedef_i false (SOME raw_tyco) (raw_tyco, map fst vs, NoSyn)
   129           (HOLogic.mk_UNIV ty) (Option.map swap constr_proj)) tac
   130     |-> (fn (tyco, info) => add_info tyco info)
   131   end;
   132 
   133 in
   134 
   135 val add_typecopy = gen_add_typecopy Sign.certify_typ;
   136 
   137 end; (*local*)
   138 
   139 
   140 (* equality function equation *)
   141 
   142 fun get_eq thy tyco =
   143   (#inject o the o get_typecopy_info thy) tyco;
   144 
   145 
   146 (* datatype specification and certificate *)
   147 
   148 fun get_spec thy tyco =
   149   let
   150     val SOME { vs, constr, typ, ... } = get_typecopy_info thy tyco
   151   in (vs, [(constr, [typ])]) end;
   152 
   153 local
   154   val bool_eq_implies = thm "iffD1";
   155   val rew_eq = thm "HOL.atomize_eq" |> Thm.symmetric;
   156 in fun get_cert thy tyco =
   157   Tactic.rewrite_rule [rew_eq] (bool_eq_implies OF [get_eq thy tyco])
   158 end; (*local*)
   159 
   160 
   161 (* hook for projection function code *)
   162 
   163 fun add_project (_ , { proj_def, ...} : info) =
   164   CodegenData.add_func proj_def;
   165 
   166 val setup =
   167   TypecopyData.init
   168   #> add_hook add_project;
   169 
   170 end; (*struct*)