src/HOL/Tools/typedef.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 38757 2b3e054ae6fc
child 42290 b1f544c84040
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
haftmann@31723
     1
(*  Title:      HOL/Tools/typedef.ML
wenzelm@16458
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
wenzelm@4866
     3
wenzelm@21352
     4
Gordon/HOL-style type definitions: create a new syntactic type
wenzelm@35741
     5
represented by a non-empty set.
wenzelm@4866
     6
*)
wenzelm@4866
     7
haftmann@31723
     8
signature TYPEDEF =
wenzelm@4866
     9
sig
wenzelm@19705
    10
  type info =
wenzelm@36107
    11
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
wenzelm@35994
    12
   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
wenzelm@29061
    13
    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
wenzelm@29061
    14
    Rep_induct: thm, Abs_induct: thm}
wenzelm@35741
    15
  val transform_info: morphism -> info -> info
wenzelm@35741
    16
  val get_info: Proof.context -> string -> info list
wenzelm@35741
    17
  val get_info_global: theory -> string -> info list
wenzelm@35741
    18
  val interpretation: (string -> theory -> theory) -> theory -> theory
wenzelm@35741
    19
  val setup: theory -> theory
wenzelm@35840
    20
  val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix ->
wenzelm@35741
    21
    term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
wenzelm@35840
    22
  val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix ->
wenzelm@30345
    23
    term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
wenzelm@35840
    24
  val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term *
wenzelm@35741
    25
    (binding * binding) option -> local_theory -> Proof.state
wenzelm@35840
    26
  val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string *
wenzelm@35741
    27
    (binding * binding) option -> local_theory -> Proof.state
wenzelm@4866
    28
end;
wenzelm@4866
    29
haftmann@31723
    30
structure Typedef: TYPEDEF =
wenzelm@4866
    31
struct
wenzelm@4866
    32
wenzelm@17922
    33
(** type definitions **)
wenzelm@17922
    34
wenzelm@17922
    35
(* theory data *)
berghofe@15259
    36
wenzelm@19705
    37
type info =
wenzelm@35994
    38
  (*global part*)
wenzelm@36107
    39
  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
wenzelm@35741
    40
  (*local part*)
wenzelm@35994
    41
  {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
wenzelm@35994
    42
    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
wenzelm@35994
    43
    Rep_induct: thm, Abs_induct: thm};
haftmann@19459
    44
wenzelm@35741
    45
fun transform_info phi (info: info) =
wenzelm@35741
    46
  let
wenzelm@35741
    47
    val thm = Morphism.thm phi;
wenzelm@35994
    48
    val (global_info, {inhabited, type_definition,
wenzelm@35741
    49
      set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
wenzelm@35994
    50
      Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
wenzelm@35741
    51
  in
wenzelm@35994
    52
    (global_info,
wenzelm@35994
    53
     {inhabited = thm inhabited, type_definition = thm type_definition,
wenzelm@35994
    54
      set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
wenzelm@35994
    55
      Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
wenzelm@35994
    56
      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
wenzelm@35994
    57
      Abs_induct = thm Abs_induct})
wenzelm@35741
    58
  end;
wenzelm@35741
    59
wenzelm@35741
    60
structure Data = Generic_Data
wenzelm@22846
    61
(
wenzelm@35741
    62
  type T = info list Symtab.table;
berghofe@15259
    63
  val empty = Symtab.empty;
wenzelm@16458
    64
  val extend = I;
wenzelm@35741
    65
  fun merge data = Symtab.merge_list (K true) data;
wenzelm@22846
    66
);
berghofe@15259
    67
wenzelm@35741
    68
val get_info = Symtab.lookup_list o Data.get o Context.Proof;
wenzelm@35741
    69
val get_info_global = Symtab.lookup_list o Data.get o Context.Theory;
wenzelm@35741
    70
wenzelm@35741
    71
fun put_info name info = Data.map (Symtab.cons_list (name, info));
wenzelm@35741
    72
wenzelm@35741
    73
wenzelm@35741
    74
(* global interpretation *)
wenzelm@35741
    75
wenzelm@35741
    76
structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
wenzelm@35741
    77
val interpretation = Typedef_Interpretation.interpretation;
wenzelm@35741
    78
wenzelm@35741
    79
val setup = Typedef_Interpretation.init;
wenzelm@35741
    80
wenzelm@35741
    81
wenzelm@35741
    82
(* primitive typedef axiomatization -- for fresh typedecl *)
wenzelm@35741
    83
wenzelm@35741
    84
fun mk_inhabited A =
wenzelm@35741
    85
  let val T = HOLogic.dest_setT (Term.fastype_of A)
wenzelm@35741
    86
  in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
wenzelm@35741
    87
wenzelm@35741
    88
fun mk_typedef newT oldT RepC AbsC A =
wenzelm@35741
    89
  let
wenzelm@35741
    90
    val typedefC =
wenzelm@35741
    91
      Const (@{const_name type_definition},
wenzelm@35741
    92
        (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
wenzelm@35741
    93
  in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
wenzelm@35134
    94
wenzelm@35741
    95
fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A thy =
wenzelm@35741
    96
  let
wenzelm@35741
    97
    (* errors *)
wenzelm@35741
    98
wenzelm@35741
    99
    fun show_names pairs = commas_quote (map fst pairs);
wenzelm@35741
   100
wenzelm@35741
   101
    val lhs_tfrees = Term.add_tfreesT newT [];
wenzelm@35741
   102
    val rhs_tfrees = Term.add_tfreesT oldT [];
wenzelm@35741
   103
    val _ =
wenzelm@35741
   104
      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
wenzelm@35741
   105
      | extras => error ("Extra type variables in representing set: " ^ show_names extras));
wenzelm@35741
   106
wenzelm@35741
   107
    val _ =
wenzelm@35741
   108
      (case Term.add_frees A [] of [] => []
wenzelm@35741
   109
      | xs => error ("Illegal variables in representing set: " ^ show_names xs));
wenzelm@35134
   110
wenzelm@35741
   111
wenzelm@35741
   112
    (* axiomatization *)
wenzelm@35741
   113
wenzelm@35741
   114
    val ((RepC, AbsC), consts_thy) = thy
wenzelm@35741
   115
      |> Sign.declare_const ((Rep_name, newT --> oldT), NoSyn)
wenzelm@35741
   116
      ||>> Sign.declare_const ((Abs_name, oldT --> newT), NoSyn);
wenzelm@35741
   117
wenzelm@35741
   118
    val typedef_deps = Term.add_consts A [];
wenzelm@35741
   119
wenzelm@36106
   120
    val ((axiom_name, axiom), axiom_thy) = consts_thy
wenzelm@35741
   121
      |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
wenzelm@35741
   122
      ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
wenzelm@35741
   123
      ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
wenzelm@35741
   124
wenzelm@36107
   125
  in ((RepC, AbsC, axiom_name, axiom), axiom_thy) end;
berghofe@15259
   126
berghofe@15259
   127
wenzelm@6383
   128
(* prepare_typedef *)
wenzelm@6383
   129
wenzelm@35840
   130
fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy =
wenzelm@4866
   131
  let
wenzelm@35741
   132
    val full_name = Local_Theory.full_name lthy name;
wenzelm@30345
   133
    val bname = Binding.name_of name;
wenzelm@4866
   134
wenzelm@35741
   135
wenzelm@35741
   136
    (* rhs *)
wenzelm@35741
   137
wenzelm@36153
   138
    val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
wenzelm@36153
   139
    val set = prep_term tmp_ctxt raw_set;
wenzelm@36153
   140
    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
wenzelm@35836
   141
wenzelm@21352
   142
    val setT = Term.fastype_of set;
wenzelm@35741
   143
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
wenzelm@35741
   144
      error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
wenzelm@35741
   145
wenzelm@35741
   146
    val goal = mk_inhabited set;
wenzelm@35741
   147
    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
wenzelm@35741
   148
wenzelm@35741
   149
wenzelm@35741
   150
    (* lhs *)
wenzelm@35741
   151
wenzelm@36153
   152
    val args = map (ProofContext.check_tfree tmp_ctxt') raw_args;
wenzelm@35741
   153
    val (newT, typedecl_lthy) = lthy
wenzelm@35836
   154
      |> Typedecl.typedecl (tname, args, mx)
wenzelm@35741
   155
      ||> Variable.declare_term set;
wenzelm@35741
   156
wenzelm@35741
   157
    val Type (full_tname, type_args) = newT;
wenzelm@35741
   158
    val lhs_tfrees = map Term.dest_TFree type_args;
wenzelm@35741
   159
wenzelm@35741
   160
wenzelm@35741
   161
    (* set definition *)
wenzelm@35741
   162
wenzelm@35741
   163
    val ((set', set_def), set_lthy) =
wenzelm@35741
   164
      if def_set then
wenzelm@35741
   165
        typedecl_lthy
wenzelm@35766
   166
        |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set))
wenzelm@35766
   167
        |>> (fn (set', (_, set_def)) => (set', SOME set_def))
wenzelm@35741
   168
      else ((set, NONE), typedecl_lthy);
wenzelm@35741
   169
wenzelm@35741
   170
wenzelm@35741
   171
    (* axiomatization *)
wenzelm@4866
   172
wenzelm@30345
   173
    val (Rep_name, Abs_name) =
wenzelm@30345
   174
      (case opt_morphs of
wenzelm@30345
   175
        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
wenzelm@30345
   176
      | SOME morphs => morphs);
wenzelm@10280
   177
wenzelm@30345
   178
    val typedef_name = Binding.prefix_name "type_definition_" name;
wenzelm@4866
   179
wenzelm@36107
   180
    val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) =
wenzelm@35741
   181
      let
wenzelm@35741
   182
        val thy = ProofContext.theory_of set_lthy;
wenzelm@35741
   183
        val cert = Thm.cterm_of thy;
wenzelm@35741
   184
        val (defs, A) =
wenzelm@36610
   185
          Local_Defs.export_cterm set_lthy (ProofContext.init_global thy) (cert set')
wenzelm@36610
   186
          ||> Thm.term_of;
haftmann@18358
   187
wenzelm@36107
   188
        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
wenzelm@38757
   189
          Local_Theory.background_theory_result
wenzelm@38757
   190
            (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
wenzelm@35741
   191
wenzelm@35741
   192
        val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
wenzelm@35741
   193
        val typedef =
wenzelm@35741
   194
          Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
wenzelm@36107
   195
      in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
wenzelm@35741
   196
wenzelm@35741
   197
    val alias_lthy = typedef_lthy
wenzelm@35741
   198
      |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
wenzelm@35741
   199
      |> Local_Theory.const_alias Abs_name (#1 (Term.dest_Const AbsC));
wenzelm@6383
   200
wenzelm@29056
   201
wenzelm@35741
   202
    (* result *)
wenzelm@4866
   203
wenzelm@35741
   204
    fun note_qualify ((b, atts), th) =
wenzelm@35741
   205
      Local_Theory.note ((Binding.qualify false bname b, map (Attrib.internal o K) atts), [th])
wenzelm@35741
   206
      #>> (fn (_, [th']) => th');
wenzelm@4866
   207
wenzelm@35741
   208
    fun typedef_result inhabited lthy1 =
wenzelm@35741
   209
      let
wenzelm@35741
   210
        val cert = Thm.cterm_of (ProofContext.theory_of lthy1);
wenzelm@35741
   211
        val inhabited' =
wenzelm@35741
   212
          Local_Defs.contract lthy1 (the_list set_def) (cert (mk_inhabited set')) inhabited;
wenzelm@35741
   213
        val typedef' = inhabited' RS typedef;
wenzelm@35741
   214
        fun make th = Goal.norm_result (typedef' RS th);
wenzelm@35741
   215
        val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
wenzelm@35741
   216
            Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
wenzelm@35741
   217
          |> Local_Theory.note ((typedef_name, []), [typedef'])
wenzelm@35741
   218
          ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
wenzelm@35741
   219
          ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
wenzelm@35741
   220
              make @{thm type_definition.Rep_inverse})
wenzelm@35741
   221
          ||>> note_qualify ((Binding.suffix_name "_inverse" Abs_name, []),
wenzelm@35741
   222
              make @{thm type_definition.Abs_inverse})
wenzelm@35741
   223
          ||>> note_qualify ((Binding.suffix_name "_inject" Rep_name, []),
wenzelm@35741
   224
              make @{thm type_definition.Rep_inject})
wenzelm@35741
   225
          ||>> note_qualify ((Binding.suffix_name "_inject" Abs_name, []),
wenzelm@35741
   226
              make @{thm type_definition.Abs_inject})
wenzelm@35741
   227
          ||>> note_qualify ((Binding.suffix_name "_cases" Rep_name,
wenzelm@35741
   228
                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
wenzelm@35741
   229
              make @{thm type_definition.Rep_cases})
wenzelm@35741
   230
          ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
wenzelm@35741
   231
                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
wenzelm@35741
   232
              make @{thm type_definition.Abs_cases})
wenzelm@35741
   233
          ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
wenzelm@35741
   234
                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
wenzelm@35741
   235
              make @{thm type_definition.Rep_induct})
wenzelm@35741
   236
          ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
wenzelm@35741
   237
                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
wenzelm@35741
   238
              make @{thm type_definition.Abs_induct});
wenzelm@4866
   239
wenzelm@35994
   240
        val info =
wenzelm@36107
   241
          ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
wenzelm@36107
   242
            Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
wenzelm@35994
   243
           {inhabited = inhabited, type_definition = type_definition, set_def = set_def,
wenzelm@35741
   244
            Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
wenzelm@35741
   245
            Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
wenzelm@35994
   246
          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
wenzelm@35741
   247
      in
wenzelm@35741
   248
        lthy2
wenzelm@35741
   249
        |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
wenzelm@38757
   250
        |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
wenzelm@35741
   251
        |> pair (full_tname, info)
wenzelm@35741
   252
      end;
wenzelm@11426
   253
wenzelm@35741
   254
  in ((goal, goal_pat, typedef_result), alias_lthy) end
wenzelm@30345
   255
  handle ERROR msg =>
wenzelm@30345
   256
    cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
wenzelm@4866
   257
wenzelm@4866
   258
wenzelm@29056
   259
(* add_typedef: tactic interface *)
wenzelm@4866
   260
wenzelm@35741
   261
fun add_typedef def opt_name typ set opt_morphs tac lthy =
wenzelm@6383
   262
  let
wenzelm@17922
   263
    val name = the_default (#1 typ) opt_name;
wenzelm@35741
   264
    val ((goal, _, typedef_result), lthy') =
wenzelm@35741
   265
      prepare_typedef Syntax.check_term def name typ set opt_morphs lthy;
wenzelm@35741
   266
    val inhabited =
wenzelm@35741
   267
      Goal.prove lthy' [] [] goal (K tac)
wenzelm@35741
   268
      |> Goal.norm_result |> Thm.close_derivation;
wenzelm@35741
   269
  in typedef_result inhabited lthy' end;
wenzelm@35741
   270
wenzelm@35741
   271
fun add_typedef_global def opt_name typ set opt_morphs tac =
haftmann@38388
   272
  Named_Target.theory_init
wenzelm@35741
   273
  #> add_typedef def opt_name typ set opt_morphs tac
wenzelm@35741
   274
  #> Local_Theory.exit_result_global (apsnd o transform_info);
wenzelm@4866
   275
wenzelm@17339
   276
wenzelm@29056
   277
(* typedef: proof interface *)
wenzelm@6383
   278
wenzelm@17339
   279
local
wenzelm@17339
   280
wenzelm@35840
   281
fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy =
wenzelm@11822
   282
  let
wenzelm@35840
   283
    val args = map (apsnd (prep_constraint lthy)) raw_args;
wenzelm@35741
   284
    val ((goal, goal_pat, typedef_result), lthy') =
wenzelm@35840
   285
      prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
wenzelm@35741
   286
    fun after_qed [[th]] = snd o typedef_result th;
wenzelm@36323
   287
  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
wenzelm@17339
   288
wenzelm@17339
   289
in
wenzelm@6383
   290
wenzelm@35840
   291
val typedef = gen_typedef Syntax.check_term (K I);
wenzelm@35840
   292
val typedef_cmd = gen_typedef Syntax.read_term Typedecl.read_constraint;
wenzelm@17339
   293
wenzelm@19705
   294
end;
berghofe@15259
   295
berghofe@15259
   296
berghofe@15259
   297
wenzelm@6383
   298
(** outer syntax **)
wenzelm@6383
   299
wenzelm@36960
   300
val _ = Keyword.keyword "morphisms";
wenzelm@24867
   301
wenzelm@24867
   302
val _ =
wenzelm@36960
   303
  Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
wenzelm@36960
   304
    Keyword.thy_goal
wenzelm@36960
   305
    (Scan.optional (Parse.$$$ "(" |--
wenzelm@36960
   306
        ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
wenzelm@36960
   307
          Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
wenzelm@36960
   308
      (Parse.type_args_constrained -- Parse.binding) --
wenzelm@36960
   309
        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
wenzelm@36960
   310
        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
wenzelm@35840
   311
    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
wenzelm@35840
   312
        typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
wenzelm@6357
   313
wenzelm@29056
   314
end;
wenzelm@29056
   315