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