src/HOL/Tools/typecopy.ML
author boehmes
Sat Mar 27 02:10:00 2010 +0100 (2010-03-27)
changeset 35983 27e2fa7d4ce7
parent 35845 e5980f0ad025
child 35994 9cc3df9a606e
permissions -rw-r--r--
slightly more general simproc (avoids errors of linarith)
     1 (*  Title:      HOL/Tools/typecopy.ML
     2     Author:     Florian Haftmann, TU Muenchen
     3 
     4 Introducing copies of types using trivial typedefs; datatype-like abstraction.
     5 *)
     6 
     7 signature TYPECOPY =
     8 sig
     9   type info = { vs: (string * sort) list, constr: string, typ: typ,
    10     inject: thm, proj: string * typ, proj_def: thm }
    11   val typecopy: binding * string list -> typ -> (binding * binding) option
    12     -> theory -> (string * info) * theory
    13   val get_info: theory -> string -> info option
    14   val interpretation: (string -> theory -> theory) -> theory -> theory
    15   val add_default_code: string -> theory -> theory
    16   val setup: theory -> theory
    17 end;
    18 
    19 structure Typecopy: TYPECOPY =
    20 struct
    21 
    22 (* theory data *)
    23 
    24 type info = {
    25   vs: (string * sort) list,
    26   constr: string,
    27   typ: typ,
    28   inject: thm,
    29   proj: string * typ,
    30   proj_def: thm
    31 };
    32 
    33 structure TypecopyData = Theory_Data
    34 (
    35   type T = info Symtab.table;
    36   val empty = Symtab.empty;
    37   val extend = I;
    38   fun merge data = Symtab.merge (K true) data;
    39 );
    40 
    41 val get_info = Symtab.lookup o TypecopyData.get;
    42 
    43 
    44 (* interpretation of type copies *)
    45 
    46 structure Typecopy_Interpretation = Interpretation(type T = string val eq = op =);
    47 val interpretation = Typecopy_Interpretation.interpretation;
    48 
    49 
    50 (* introducing typecopies *)
    51 
    52 fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy =
    53   let
    54     val ty = Sign.certify_typ thy raw_ty;
    55     val vs =
    56       AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs;
    57     val tac = Tactic.rtac UNIV_witness 1;
    58     fun add_info tyco ( { abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs,
    59       Rep_name = c_rep, Abs_inject = inject,
    60       Abs_inverse = inverse, ... } : Typedef.info ) thy =
    61         let
    62           val exists_thm =
    63             UNIV_I
    64             |> Drule.instantiate' [SOME (ctyp_of thy (Logic.varifyT_global ty_rep))] [];
    65           val inject' = inject OF [exists_thm, exists_thm];
    66           val proj_def = inverse OF [exists_thm];
    67           val info = {
    68             vs = vs,
    69             constr = c_abs,
    70             typ = ty_rep,
    71             inject = inject',
    72             proj = (c_rep, ty_abs --> ty_rep),
    73             proj_def = proj_def
    74           };
    75         in
    76           thy
    77           |> (TypecopyData.map o Symtab.update_new) (tyco, info)
    78           |> Typecopy_Interpretation.data tyco
    79           |> pair (tyco, info)
    80         end
    81   in
    82     thy
    83     |> Typedef.add_typedef_global false (SOME raw_tyco)
    84       (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn)   (* FIXME keep constraints!? *)
    85       (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac
    86     |-> (fn (tyco, info) => add_info tyco info)
    87   end;
    88 
    89 
    90 (* default code setup *)
    91 
    92 fun add_default_code tyco thy =
    93   let
    94     val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
    95       typ = ty_rep, ... } = get_info thy tyco;
    96     (* FIXME handle multiple typedef interpretations (!??) *)
    97     val [{ Rep_inject = proj_inject, ... }] = Typedef.get_info_global thy tyco;
    98     val constr = (c, Logic.unvarifyT_global (Sign.the_const_type thy c));
    99     val ty = Type (tyco, map TFree vs);
   100     val proj = Const (proj, ty --> ty_rep);
   101     val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));
   102     val eq_lhs = Const (@{const_name eq_class.eq}, ty --> ty --> HOLogic.boolT)
   103       $ t_x $ t_y;
   104     val eq_rhs = HOLogic.mk_eq (proj $ t_x, proj $ t_y);
   105     val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) (eq_lhs, eq_rhs);
   106     fun tac eq_thm = Class.intro_classes_tac []
   107       THEN (Simplifier.rewrite_goals_tac
   108         (map Simpdata.mk_eq [eq_thm, @{thm eq}, proj_inject]))
   109           THEN ALLGOALS (rtac @{thm refl});
   110     fun mk_eq_refl thy = @{thm HOL.eq_refl}
   111       |> Thm.instantiate
   112          ([pairself (Thm.ctyp_of thy) (TVar (("'a", 0), @{sort eq}), Logic.varifyT_global ty)], [])
   113       |> AxClass.unoverload thy;
   114   in
   115     thy
   116     |> Code.add_datatype [constr]
   117     |> Code.add_eqn proj_eq
   118     |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq])
   119     |> `(fn lthy => Syntax.check_term lthy eq)
   120     |-> (fn eq => Specification.definition
   121          (NONE, (Attrib.empty_binding, eq)))
   122     |-> (fn (_, (_, eq_thm)) =>
   123        Class.prove_instantiation_exit_result Morphism.thm
   124          (fn _ => fn eq_thm => tac eq_thm) eq_thm)
   125     |-> (fn eq_thm => Code.add_eqn eq_thm)
   126     |> (fn thy => Code.add_nbe_eqn (mk_eq_refl thy) thy)
   127   end;
   128 
   129 val setup =
   130   Typecopy_Interpretation.init
   131   #> interpretation add_default_code
   132 
   133 end;