src/HOL/Tools/typedef.ML
author wenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261 ddb2da7cb2e4
parent 61260 e6f03fae14d5
child 62513 702085ca8564
permissions -rw-r--r--
more explicit Defs.context: use proper name spaces as far as possible;
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@49833
    12
   {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm,
wenzelm@49833
    13
    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@58662
    18
  val interpretation: (string -> local_theory -> local_theory) -> theory -> theory
wenzelm@61110
    19
  type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding}
wenzelm@61110
    20
  val default_bindings: binding -> bindings
wenzelm@61110
    21
  val make_bindings: binding -> bindings option -> bindings
wenzelm@61110
    22
  val make_morphisms: binding -> (binding * binding) option -> bindings
wenzelm@61260
    23
  val overloaded: bool Config.T
wenzelm@61260
    24
  val add_typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
wenzelm@61110
    25
    term -> bindings option -> (Proof.context -> tactic) -> local_theory ->
wenzelm@58959
    26
    (string * info) * local_theory
wenzelm@61260
    27
  val add_typedef_global: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
wenzelm@61110
    28
    term -> bindings option -> (Proof.context -> tactic) -> theory ->
wenzelm@58959
    29
    (string * info) * theory
wenzelm@61260
    30
  val typedef: {overloaded: bool} -> binding * (string * sort) list * mixfix ->
wenzelm@61260
    31
    term -> bindings option -> local_theory -> Proof.state
wenzelm@61260
    32
  val typedef_cmd: {overloaded: bool} -> binding * (string * string option) list * mixfix ->
wenzelm@61260
    33
    string -> bindings option -> local_theory -> Proof.state
wenzelm@4866
    34
end;
wenzelm@4866
    35
haftmann@31723
    36
structure Typedef: TYPEDEF =
wenzelm@4866
    37
struct
wenzelm@4866
    38
wenzelm@17922
    39
(** type definitions **)
wenzelm@17922
    40
wenzelm@17922
    41
(* theory data *)
berghofe@15259
    42
wenzelm@19705
    43
type info =
wenzelm@35994
    44
  (*global part*)
wenzelm@36107
    45
  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
wenzelm@35741
    46
  (*local part*)
wenzelm@49833
    47
  {inhabited: thm, type_definition: thm, Rep: thm, Rep_inverse: thm, Abs_inverse: thm,
wenzelm@49833
    48
    Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
wenzelm@35994
    49
    Rep_induct: thm, Abs_induct: thm};
haftmann@19459
    50
wenzelm@35741
    51
fun transform_info phi (info: info) =
wenzelm@35741
    52
  let
wenzelm@35741
    53
    val thm = Morphism.thm phi;
wenzelm@49833
    54
    val (global_info, {inhabited, type_definition, Rep, Rep_inverse, Abs_inverse,
wenzelm@49833
    55
      Rep_inject, Abs_inject, Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
wenzelm@35741
    56
  in
wenzelm@35994
    57
    (global_info,
wenzelm@35994
    58
     {inhabited = thm inhabited, type_definition = thm type_definition,
wenzelm@49833
    59
      Rep = thm Rep, Rep_inverse = thm Rep_inverse, Abs_inverse = thm Abs_inverse,
wenzelm@49833
    60
      Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
wenzelm@49833
    61
      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases,
wenzelm@49833
    62
      Rep_induct = thm Rep_induct, Abs_induct = thm Abs_induct})
wenzelm@35741
    63
  end;
wenzelm@35741
    64
wenzelm@35741
    65
structure Data = Generic_Data
wenzelm@22846
    66
(
wenzelm@35741
    67
  type T = info list Symtab.table;
berghofe@15259
    68
  val empty = Symtab.empty;
wenzelm@16458
    69
  val extend = I;
wenzelm@35741
    70
  fun merge data = Symtab.merge_list (K true) data;
wenzelm@22846
    71
);
berghofe@15259
    72
wenzelm@61103
    73
fun get_info_generic context =
wenzelm@61103
    74
  Symtab.lookup_list (Data.get context) #>
wenzelm@61103
    75
  map (transform_info (Morphism.transfer_morphism (Context.theory_of context)));
wenzelm@35741
    76
wenzelm@61103
    77
val get_info = get_info_generic o Context.Proof;
wenzelm@61103
    78
val get_info_global = get_info_generic o Context.Theory;
wenzelm@61103
    79
wenzelm@61103
    80
fun put_info name info =
wenzelm@61103
    81
  Data.map (Symtab.cons_list (name, transform_info Morphism.trim_context_morphism info));
wenzelm@35741
    82
wenzelm@35741
    83
wenzelm@35741
    84
(* global interpretation *)
wenzelm@35741
    85
wenzelm@58662
    86
structure Typedef_Plugin = Plugin(type T = string);
wenzelm@58662
    87
wenzelm@58662
    88
val typedef_plugin = Plugin_Name.declare_setup @{binding typedef};
blanchet@56375
    89
wenzelm@58662
    90
fun interpretation f =
wenzelm@58662
    91
  Typedef_Plugin.interpretation typedef_plugin
wenzelm@58662
    92
    (fn name => fn lthy =>
wenzelm@58662
    93
      lthy
wenzelm@59880
    94
      |> Local_Theory.map_background_naming
wenzelm@58662
    95
          (Name_Space.root_path #> Name_Space.add_path (Long_Name.qualifier name))
wenzelm@58662
    96
      |> f name
wenzelm@59880
    97
      |> Local_Theory.restore_background_naming lthy);
wenzelm@35741
    98
wenzelm@35741
    99
wenzelm@35741
   100
(* primitive typedef axiomatization -- for fresh typedecl *)
wenzelm@35741
   101
wenzelm@61260
   102
val typedef_overloaded = Attrib.setup_config_bool @{binding typedef_overloaded} (K false);
wenzelm@61260
   103
wenzelm@35741
   104
fun mk_inhabited A =
wenzelm@35741
   105
  let val T = HOLogic.dest_setT (Term.fastype_of A)
wenzelm@35741
   106
  in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
wenzelm@35741
   107
wenzelm@35741
   108
fun mk_typedef newT oldT RepC AbsC A =
wenzelm@35741
   109
  let
wenzelm@35741
   110
    val typedefC =
wenzelm@35741
   111
      Const (@{const_name type_definition},
wenzelm@35741
   112
        (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
wenzelm@35741
   113
  in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
wenzelm@35134
   114
wenzelm@61260
   115
fun primitive_typedef {overloaded} type_definition_name newT oldT Rep_name Abs_name A lthy =
wenzelm@35741
   116
  let
wenzelm@35741
   117
    (* errors *)
wenzelm@35741
   118
wenzelm@35741
   119
    fun show_names pairs = commas_quote (map fst pairs);
wenzelm@35741
   120
wenzelm@35741
   121
    val lhs_tfrees = Term.add_tfreesT newT [];
wenzelm@35741
   122
    val rhs_tfrees = Term.add_tfreesT oldT [];
wenzelm@35741
   123
    val _ =
wenzelm@61260
   124
      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of
wenzelm@61260
   125
        [] => ()
wenzelm@35741
   126
      | extras => error ("Extra type variables in representing set: " ^ show_names extras));
wenzelm@35741
   127
wenzelm@35741
   128
    val _ =
wenzelm@61260
   129
      (case Term.add_frees A [] of [] =>
wenzelm@61260
   130
        []
wenzelm@35741
   131
      | xs => error ("Illegal variables in representing set: " ^ show_names xs));
wenzelm@35134
   132
wenzelm@35741
   133
wenzelm@35741
   134
    (* axiomatization *)
wenzelm@35741
   135
wenzelm@42375
   136
    val ((RepC, AbsC), consts_lthy) = lthy
wenzelm@42375
   137
      |> Local_Theory.background_theory_result
wenzelm@42375
   138
        (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
wenzelm@42375
   139
          Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
wenzelm@61255
   140
    val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy);
wenzelm@61261
   141
    val defs_context = Proof_Context.defs_context consts_lthy;
wenzelm@61247
   142
wenzelm@61255
   143
    val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A [];
wenzelm@61248
   144
    val A_types =
wenzelm@61255
   145
      (fold_types o fold_subtypes) (fn Type t => insert (op =) (Theory.type_dep t) | _ => I) A [];
wenzelm@61246
   146
    val typedef_deps = A_consts @ A_types;
wenzelm@61247
   147
wenzelm@61255
   148
    val newT_dep = Theory.type_dep (dest_Type newT);
wenzelm@35741
   149
wenzelm@42375
   150
    val ((axiom_name, axiom), axiom_lthy) = consts_lthy
wenzelm@42375
   151
      |> Local_Theory.background_theory_result
wenzelm@61110
   152
        (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
wenzelm@61261
   153
          Theory.add_deps defs_context "" newT_dep typedef_deps ##>
wenzelm@61261
   154
          Theory.add_deps defs_context "" (const_dep (dest_Const RepC)) [newT_dep] ##>
wenzelm@61261
   155
          Theory.add_deps defs_context "" (const_dep (dest_Const AbsC)) [newT_dep]);
wenzelm@35741
   156
wenzelm@61260
   157
    val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy);
wenzelm@61260
   158
    val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep));
wenzelm@61260
   159
    val _ =
wenzelm@61260
   160
      if null newT_deps orelse overloaded orelse Config.get lthy typedef_overloaded then ()
wenzelm@61260
   161
      else
wenzelm@61260
   162
        error (Pretty.string_of (Pretty.chunks
wenzelm@61260
   163
          [Pretty.paragraph
wenzelm@61260
   164
            (Pretty.text "Type definition with open dependencies, use" @
wenzelm@61260
   165
             [Pretty.brk 1, Pretty.str "\"", Pretty.keyword1 "typedef", Pretty.brk 1,
wenzelm@61260
   166
              Pretty.str "(", Pretty.keyword2 "overloaded", Pretty.str ")\"", Pretty.brk 1] @
wenzelm@61260
   167
             Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."),
wenzelm@61260
   168
           Pretty.block [Pretty.str "  Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT],
wenzelm@61260
   169
           Pretty.block (Pretty.str "  Deps:" :: Pretty.brk 2 ::
wenzelm@61261
   170
             Pretty.commas
wenzelm@61261
   171
              (map (Defs.pretty_entry (Proof_Context.defs_context axiom_lthy)) newT_deps))]))
wenzelm@42375
   172
  in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
berghofe@15259
   173
berghofe@15259
   174
wenzelm@61110
   175
(* derived bindings *)
wenzelm@61110
   176
wenzelm@61110
   177
type bindings = {Rep_name: binding, Abs_name: binding, type_definition_name: binding};
wenzelm@61110
   178
wenzelm@61110
   179
fun default_bindings name =
wenzelm@61110
   180
 {Rep_name = Binding.prefix_name "Rep_" name,
wenzelm@61110
   181
  Abs_name = Binding.prefix_name "Abs_" name,
wenzelm@61110
   182
  type_definition_name = Binding.prefix_name "type_definition_" name};
wenzelm@61110
   183
wenzelm@61110
   184
fun make_bindings name NONE = default_bindings name
wenzelm@61110
   185
  | make_bindings _ (SOME bindings) = bindings;
wenzelm@61110
   186
wenzelm@61110
   187
fun make_morphisms name NONE = default_bindings name
wenzelm@61110
   188
  | make_morphisms name (SOME (Rep_name, Abs_name)) =
wenzelm@61110
   189
      {Rep_name = Rep_name, Abs_name = Abs_name,
wenzelm@61110
   190
        type_definition_name = #type_definition_name (default_bindings name)};
wenzelm@61110
   191
wenzelm@61110
   192
wenzelm@6383
   193
(* prepare_typedef *)
wenzelm@6383
   194
wenzelm@61260
   195
fun prepare_typedef prep_term overloaded (name, raw_args, mx) raw_set opt_bindings lthy =
wenzelm@4866
   196
  let
wenzelm@30345
   197
    val bname = Binding.name_of name;
wenzelm@4866
   198
wenzelm@35741
   199
wenzelm@35741
   200
    (* rhs *)
wenzelm@35741
   201
wenzelm@36153
   202
    val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
wenzelm@36153
   203
    val set = prep_term tmp_ctxt raw_set;
wenzelm@36153
   204
    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
wenzelm@35836
   205
wenzelm@21352
   206
    val setT = Term.fastype_of set;
wenzelm@35741
   207
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
wenzelm@35741
   208
      error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
wenzelm@35741
   209
wenzelm@35741
   210
    val goal = mk_inhabited set;
wenzelm@42290
   211
    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Lexicon.read_variable bname), setT));
wenzelm@35741
   212
wenzelm@35741
   213
wenzelm@35741
   214
    (* lhs *)
wenzelm@35741
   215
wenzelm@42361
   216
    val args = map (Proof_Context.check_tfree tmp_ctxt') raw_args;
wenzelm@35741
   217
    val (newT, typedecl_lthy) = lthy
wenzelm@61259
   218
      |> Typedecl.typedecl {final = false} (name, args, mx)
wenzelm@35741
   219
      ||> Variable.declare_term set;
wenzelm@35741
   220
blanchet@56375
   221
    val Type (full_name, _) = newT;
wenzelm@35741
   222
wenzelm@35741
   223
wenzelm@35741
   224
    (* axiomatization *)
wenzelm@4866
   225
wenzelm@61110
   226
    val {Rep_name, Abs_name, type_definition_name} = make_bindings name opt_bindings;
wenzelm@4866
   227
wenzelm@49833
   228
    val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) = typedecl_lthy
wenzelm@61260
   229
      |> primitive_typedef overloaded type_definition_name newT oldT Rep_name Abs_name set;
wenzelm@35741
   230
wenzelm@35741
   231
    val alias_lthy = typedef_lthy
wenzelm@35741
   232
      |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
wenzelm@35741
   233
      |> Local_Theory.const_alias Abs_name (#1 (Term.dest_Const AbsC));
wenzelm@6383
   234
wenzelm@29056
   235
wenzelm@35741
   236
    (* result *)
wenzelm@4866
   237
wenzelm@35741
   238
    fun note_qualify ((b, atts), th) =
wenzelm@35741
   239
      Local_Theory.note ((Binding.qualify false bname b, map (Attrib.internal o K) atts), [th])
wenzelm@35741
   240
      #>> (fn (_, [th']) => th');
wenzelm@4866
   241
wenzelm@35741
   242
    fun typedef_result inhabited lthy1 =
wenzelm@35741
   243
      let
wenzelm@49833
   244
        val typedef' = inhabited RS typedef;
wenzelm@54883
   245
        fun make th = Goal.norm_result lthy1 (typedef' RS th);
wenzelm@35741
   246
        val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
wenzelm@35741
   247
            Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
wenzelm@61110
   248
          |> Local_Theory.note ((type_definition_name, []), [typedef'])
wenzelm@35741
   249
          ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
wenzelm@35741
   250
          ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
wenzelm@35741
   251
              make @{thm type_definition.Rep_inverse})
wenzelm@35741
   252
          ||>> note_qualify ((Binding.suffix_name "_inverse" Abs_name, []),
wenzelm@35741
   253
              make @{thm type_definition.Abs_inverse})
wenzelm@35741
   254
          ||>> note_qualify ((Binding.suffix_name "_inject" Rep_name, []),
wenzelm@35741
   255
              make @{thm type_definition.Rep_inject})
wenzelm@35741
   256
          ||>> note_qualify ((Binding.suffix_name "_inject" Abs_name, []),
wenzelm@35741
   257
              make @{thm type_definition.Abs_inject})
wenzelm@35741
   258
          ||>> note_qualify ((Binding.suffix_name "_cases" Rep_name,
wenzelm@35741
   259
                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
wenzelm@35741
   260
              make @{thm type_definition.Rep_cases})
wenzelm@35741
   261
          ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
wenzelm@49835
   262
                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_name]),
wenzelm@35741
   263
              make @{thm type_definition.Abs_cases})
wenzelm@35741
   264
          ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
wenzelm@35741
   265
                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
wenzelm@35741
   266
              make @{thm type_definition.Rep_induct})
wenzelm@35741
   267
          ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
wenzelm@49835
   268
                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_name]),
wenzelm@35741
   269
              make @{thm type_definition.Abs_induct});
wenzelm@4866
   270
wenzelm@35994
   271
        val info =
wenzelm@36107
   272
          ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
wenzelm@36107
   273
            Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
wenzelm@49833
   274
           {inhabited = inhabited, type_definition = type_definition,
wenzelm@35741
   275
            Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
wenzelm@35741
   276
            Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
wenzelm@35994
   277
          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
wenzelm@35741
   278
      in
wenzelm@35741
   279
        lthy2
wenzelm@45291
   280
        |> Local_Theory.declaration {syntax = false, pervasive = true}
wenzelm@49835
   281
          (fn phi => put_info full_name (transform_info phi info))
wenzelm@58662
   282
        |> Typedef_Plugin.data Plugin_Name.default_filter full_name
wenzelm@49835
   283
        |> pair (full_name, info)
wenzelm@35741
   284
      end;
wenzelm@11426
   285
wenzelm@35741
   286
  in ((goal, goal_pat, typedef_result), alias_lthy) end
wenzelm@30345
   287
  handle ERROR msg =>
wenzelm@42381
   288
    cat_error msg ("The error(s) above occurred in typedef " ^ Binding.print name);
wenzelm@4866
   289
wenzelm@4866
   290
wenzelm@29056
   291
(* add_typedef: tactic interface *)
wenzelm@4866
   292
wenzelm@61260
   293
fun add_typedef overloaded typ set opt_bindings tac lthy =
wenzelm@6383
   294
  let
wenzelm@35741
   295
    val ((goal, _, typedef_result), lthy') =
wenzelm@61260
   296
      prepare_typedef Syntax.check_term overloaded typ set opt_bindings lthy;
wenzelm@35741
   297
    val inhabited =
wenzelm@58959
   298
      Goal.prove lthy' [] [] goal (tac o #context)
wenzelm@54883
   299
      |> Goal.norm_result lthy' |> Thm.close_derivation;
wenzelm@35741
   300
  in typedef_result inhabited lthy' end;
wenzelm@35741
   301
wenzelm@61260
   302
fun add_typedef_global overloaded typ set opt_bindings tac =
haftmann@38388
   303
  Named_Target.theory_init
wenzelm@61260
   304
  #> add_typedef overloaded typ set opt_bindings tac
wenzelm@35741
   305
  #> Local_Theory.exit_result_global (apsnd o transform_info);
wenzelm@4866
   306
wenzelm@17339
   307
wenzelm@29056
   308
(* typedef: proof interface *)
wenzelm@6383
   309
wenzelm@17339
   310
local
wenzelm@17339
   311
wenzelm@61260
   312
fun gen_typedef prep_term prep_constraint overloaded (b, raw_args, mx) set opt_bindings lthy =
wenzelm@11822
   313
  let
wenzelm@35840
   314
    val args = map (apsnd (prep_constraint lthy)) raw_args;
wenzelm@35741
   315
    val ((goal, goal_pat, typedef_result), lthy') =
wenzelm@61260
   316
      prepare_typedef prep_term overloaded (b, args, mx) set opt_bindings lthy;
wenzelm@35741
   317
    fun after_qed [[th]] = snd o typedef_result th;
wenzelm@36323
   318
  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
wenzelm@17339
   319
wenzelm@17339
   320
in
wenzelm@6383
   321
wenzelm@35840
   322
val typedef = gen_typedef Syntax.check_term (K I);
wenzelm@35840
   323
val typedef_cmd = gen_typedef Syntax.read_term Typedecl.read_constraint;
wenzelm@17339
   324
wenzelm@19705
   325
end;
berghofe@15259
   326
berghofe@15259
   327
berghofe@15259
   328
wenzelm@6383
   329
(** outer syntax **)
wenzelm@6383
   330
wenzelm@24867
   331
val _ =
wenzelm@59936
   332
  Outer_Syntax.local_theory_to_proof @{command_keyword typedef}
wenzelm@46961
   333
    "HOL type definition (requires non-emptiness proof)"
wenzelm@61260
   334
    (Parse_Spec.overloaded -- Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
wenzelm@49835
   335
      (@{keyword "="} |-- Parse.term) --
wenzelm@49835
   336
      Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
wenzelm@61260
   337
    >> (fn (((((overloaded, vs), t), mx), A), opt_morphs) => fn lthy =>
wenzelm@61260
   338
        typedef_cmd {overloaded = overloaded} (t, vs, mx) A
wenzelm@61260
   339
          (SOME (make_morphisms t opt_morphs)) lthy));
wenzelm@61260
   340
wenzelm@61260
   341
wenzelm@61260
   342
val overloaded = typedef_overloaded;
wenzelm@6357
   343
wenzelm@29056
   344
end;