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