src/HOL/Tools/Quotient/quotient_type.ML
author wenzelm
Fri Oct 12 21:22:35 2012 +0200 (2012-10-12)
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 50177 2006c50172c9
permissions -rw-r--r--
discontinued typedef with alternative name;
wenzelm@45680
     1
(*  Title:      HOL/Tools/Quotient/quotient_type.ML
kaliszyk@35222
     2
    Author:     Cezary Kaliszyk and Christian Urban
kaliszyk@35222
     3
urbanc@35806
     4
Definition of a quotient type.
kaliszyk@35222
     5
*)
kaliszyk@35222
     6
kaliszyk@35222
     7
signature QUOTIENT_TYPE =
kaliszyk@35222
     8
sig
kuncar@45676
     9
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool) * 
kuncar@47937
    10
    ((binding * binding) option * bool)) * thm -> local_theory -> Quotient_Info.quotients * local_theory
kaliszyk@35415
    11
kuncar@47983
    12
  val quotient_type: (string list * binding * mixfix) * (typ * term * bool) * 
kuncar@47983
    13
    ((binding * binding) option * bool) -> Proof.context -> Proof.state
kaliszyk@35222
    14
kuncar@47983
    15
  val quotient_type_cmd: (((((bool * string list) * binding) * mixfix) * string) * (bool * string)) *
kuncar@47983
    16
    (binding * binding) option -> Proof.context -> Proof.state
kaliszyk@35222
    17
end;
kaliszyk@35222
    18
kaliszyk@35222
    19
structure Quotient_Type: QUOTIENT_TYPE =
kaliszyk@35222
    20
struct
kaliszyk@35222
    21
kaliszyk@35222
    22
kaliszyk@35222
    23
(*** definition of quotient types ***)
kaliszyk@35222
    24
kaliszyk@44204
    25
val mem_def1 = @{lemma "y : Collect S ==> S y" by simp}
kaliszyk@44204
    26
val mem_def2 = @{lemma "S y ==> y : Collect S" by simp}
kaliszyk@35222
    27
kuncar@47100
    28
(* constructs the term {c. EX (x::rty). rel x x \<and> c = Collect (rel x)} *)
kaliszyk@35222
    29
fun typedef_term rel rty lthy =
wenzelm@41444
    30
  let
wenzelm@41444
    31
    val [x, c] =
wenzelm@41444
    32
      [("x", rty), ("c", HOLogic.mk_setT rty)]
wenzelm@41444
    33
      |> Variable.variant_frees lthy [rel]
wenzelm@41444
    34
      |> map Free
wenzelm@41444
    35
  in
bulwahn@45312
    36
    HOLogic.Collect_const (HOLogic.mk_setT rty) $ (lambda c (HOLogic.exists_const rty $
kaliszyk@44204
    37
        lambda x (HOLogic.mk_conj (rel $ x $ x,
bulwahn@45312
    38
        HOLogic.mk_eq (c, HOLogic.Collect_const rty $ (rel $ x))))))
wenzelm@41444
    39
  end
kaliszyk@35222
    40
kaliszyk@35222
    41
kaliszyk@35222
    42
(* makes the new type definitions and proves non-emptyness *)
kaliszyk@37493
    43
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
wenzelm@41444
    44
  let
wenzelm@41444
    45
    val typedef_tac =
wenzelm@41444
    46
      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
wenzelm@41444
    47
  in
wenzelm@49835
    48
    Typedef.add_typedef (qty_name, map (rpair dummyS) vs, mx)
wenzelm@41444
    49
      (typedef_term rel rty lthy) NONE typedef_tac lthy
wenzelm@41444
    50
  end
kaliszyk@35222
    51
kaliszyk@35222
    52
kaliszyk@35222
    53
(* tactic to prove the quot_type theorem for the new type *)
wenzelm@35994
    54
fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
wenzelm@41444
    55
  let
wenzelm@41444
    56
    val rep_thm = #Rep typedef_info RS mem_def1
wenzelm@41444
    57
    val rep_inv = #Rep_inverse typedef_info
wenzelm@41444
    58
    val abs_inv = #Abs_inverse typedef_info
wenzelm@41444
    59
    val rep_inj = #Rep_inject typedef_info
wenzelm@41444
    60
  in
wenzelm@41444
    61
    (rtac @{thm quot_type.intro} THEN' RANGE [
wenzelm@41444
    62
      rtac equiv_thm,
wenzelm@41444
    63
      rtac rep_thm,
wenzelm@41444
    64
      rtac rep_inv,
wenzelm@41444
    65
      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
wenzelm@41444
    66
      rtac rep_inj]) 1
wenzelm@41444
    67
  end
kaliszyk@35222
    68
kaliszyk@35222
    69
(* proves the quot_type theorem for the new type *)
kaliszyk@35222
    70
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
wenzelm@41444
    71
  let
bulwahn@45317
    72
    val quot_type_const = Const (@{const_name "quot_type"},
bulwahn@45317
    73
      fastype_of rel --> fastype_of abs --> fastype_of rep --> @{typ bool})
bulwahn@45317
    74
    val goal = HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
wenzelm@41444
    75
  in
wenzelm@41444
    76
    Goal.prove lthy [] [] goal
wenzelm@41444
    77
      (K (typedef_quot_type_tac equiv_thm typedef_info))
wenzelm@41444
    78
  end
kuncar@47096
    79
   
kuncar@47698
    80
open Lifting_Util
kuncar@47362
    81
kuncar@47698
    82
infix 0 MRSL
kuncar@47362
    83
kuncar@47362
    84
fun define_cr_rel equiv_thm abs_fun lthy =
kuncar@47362
    85
  let
kuncar@47362
    86
    fun force_type_of_rel rel forced_ty =
kuncar@47362
    87
      let
kuncar@47362
    88
        val thy = Proof_Context.theory_of lthy
kuncar@47362
    89
        val rel_ty = (domain_type o fastype_of) rel
kuncar@47362
    90
        val ty_inst = Sign.typ_match thy (rel_ty, forced_ty) Vartab.empty
kuncar@47362
    91
      in
kuncar@47362
    92
        Envir.subst_term_types ty_inst rel
kuncar@47362
    93
      end
kuncar@47362
    94
  
kuncar@47362
    95
    val (rty, qty) = (dest_funT o fastype_of) abs_fun
kuncar@47362
    96
    val abs_fun_graph = HOLogic.mk_eq(abs_fun $ Bound 1, Bound 0)
kuncar@47362
    97
    val Abs_body = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
kuncar@47362
    98
      Const (@{const_name equivp}, _) $ _ => abs_fun_graph
kuncar@47362
    99
      | Const (@{const_name part_equivp}, _) $ rel => 
kuncar@47362
   100
        HOLogic.mk_conj (force_type_of_rel rel rty $ Bound 1 $ Bound 1, abs_fun_graph)
kuncar@47362
   101
      | _ => error "unsupported equivalence theorem"
kuncar@47362
   102
      )
kuncar@47362
   103
    val def_term = Abs ("x", rty, Abs ("y", qty, Abs_body));
kuncar@47362
   104
    val qty_name = (fst o dest_Type) qty
kuncar@47362
   105
    val cr_rel_name = Binding.prefix_name "cr_" (Binding.qualified_name qty_name)  
kuncar@47362
   106
    val (fixed_def_term, lthy') = yield_singleton (Variable.importT_terms) def_term lthy
kuncar@47362
   107
    val ((_, (_ , def_thm)), lthy'') =
kuncar@47362
   108
      Local_Theory.define ((cr_rel_name, NoSyn), ((Thm.def_binding cr_rel_name, []), fixed_def_term)) lthy'
kuncar@47362
   109
  in
kuncar@47362
   110
    (def_thm, lthy'')
kuncar@47362
   111
  end;
kuncar@47362
   112
kuncar@47937
   113
fun setup_lifting_package gen_code quot3_thm equiv_thm lthy =
kuncar@47362
   114
  let
kuncar@47362
   115
    val (_ $ _ $ abs_fun $ _) = (HOLogic.dest_Trueprop o prop_of) quot3_thm
kuncar@47362
   116
    val (T_def, lthy') = define_cr_rel equiv_thm abs_fun lthy
kuncar@47502
   117
    val (rty, qty) = (dest_funT o fastype_of) abs_fun
kuncar@47502
   118
    val qty_name = (fst o dest_Type) qty
kuncar@47502
   119
    val quotient_thm_name = Binding.prefix_name "Quotient_" (Binding.qualified_name qty_name) 
kuncar@47521
   120
    val (reflp_thm, quot_thm) = (case (HOLogic.dest_Trueprop o prop_of) equiv_thm of
kuncar@47521
   121
      Const (@{const_name equivp}, _) $ _ =>
kuncar@47521
   122
        (SOME (equiv_thm RS @{thm equivp_reflp2}),
kuncar@47521
   123
         [quot3_thm, T_def, equiv_thm] MRSL @{thm Quotient3_to_Quotient_equivp})
kuncar@47521
   124
      | Const (@{const_name part_equivp}, _) $ _ =>
kuncar@47521
   125
        (NONE,
kuncar@47521
   126
        [quot3_thm, T_def] MRSL @{thm Quotient3_to_Quotient})
kuncar@47362
   127
      | _ => error "unsupported equivalence theorem"
kuncar@47362
   128
      )
kuncar@47362
   129
  in
kuncar@47502
   130
    lthy'
kuncar@47937
   131
      |> Lifting_Setup.setup_by_quotient gen_code quot_thm reflp_thm
kuncar@47502
   132
      |> (snd oo Local_Theory.note) ((quotient_thm_name, []), [quot_thm])
kuncar@47362
   133
  end
kuncar@47362
   134
kuncar@47937
   135
fun init_quotient_infr gen_code quot_thm equiv_thm lthy =
kuncar@47096
   136
  let
kuncar@47096
   137
    val (_ $ rel $ abs $ rep) = (HOLogic.dest_Trueprop o prop_of) quot_thm
kuncar@47096
   138
    val (qtyp, rtyp) = (dest_funT o fastype_of) rep
kuncar@47096
   139
    val qty_full_name = (fst o dest_Type) qtyp
kuncar@47096
   140
    val quotients = {qtyp = qtyp, rtyp = rtyp, equiv_rel = rel, equiv_thm = equiv_thm, 
kuncar@47096
   141
      quot_thm = quot_thm }
kuncar@47096
   142
    fun quot_info phi = Quotient_Info.transform_quotients phi quotients
kuncar@47096
   143
    val abs_rep = {abs = abs, rep = rep}
kuncar@47096
   144
    fun abs_rep_info phi = Quotient_Info.transform_abs_rep phi abs_rep
kuncar@47096
   145
  in
kuncar@47096
   146
    lthy
kuncar@47096
   147
      |> Local_Theory.declaration {syntax = false, pervasive = true}
kuncar@47096
   148
        (fn phi => Quotient_Info.update_quotients qty_full_name (quot_info phi)
kuncar@47096
   149
          #> Quotient_Info.update_abs_rep qty_full_name (abs_rep_info phi))
kuncar@47937
   150
      |> setup_lifting_package gen_code quot_thm equiv_thm
kuncar@47096
   151
  end
kaliszyk@35222
   152
kaliszyk@35222
   153
(* main function for constructing a quotient type *)
kuncar@47937
   154
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), equiv_thm) lthy =
wenzelm@41444
   155
  let
wenzelm@41444
   156
    val part_equiv =
wenzelm@41444
   157
      if partial
wenzelm@41444
   158
      then equiv_thm
wenzelm@41444
   159
      else equiv_thm RS @{thm equivp_implies_part_equivp}
kaliszyk@37493
   160
wenzelm@41444
   161
    (* generates the typedef *)
kuncar@47096
   162
    val ((_, typedef_info), lthy1) =
wenzelm@41444
   163
      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
kaliszyk@35222
   164
wenzelm@41444
   165
    (* abs and rep functions from the typedef *)
wenzelm@41444
   166
    val Abs_ty = #abs_type (#1 typedef_info)
wenzelm@41444
   167
    val Rep_ty = #rep_type (#1 typedef_info)
wenzelm@41444
   168
    val Abs_name = #Abs_name (#1 typedef_info)
wenzelm@41444
   169
    val Rep_name = #Rep_name (#1 typedef_info)
wenzelm@41444
   170
    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
wenzelm@41444
   171
    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
kaliszyk@35222
   172
wenzelm@41444
   173
    (* more useful abs and rep definitions *)
bulwahn@45317
   174
    val abs_const = Const (@{const_name quot_type.abs},
bulwahn@45317
   175
      (rty --> rty --> @{typ bool}) --> (Rep_ty --> Abs_ty) --> rty --> Abs_ty)
bulwahn@45317
   176
    val rep_const = Const (@{const_name quot_type.rep}, (Abs_ty --> Rep_ty) --> Abs_ty --> rty)
bulwahn@45317
   177
    val abs_trm = abs_const $ rel $ Abs_const
bulwahn@45317
   178
    val rep_trm = rep_const $ Rep_const
kuncar@45676
   179
    val (rep_name, abs_name) =
kuncar@45676
   180
      (case opt_morphs of
kuncar@45676
   181
        NONE => (Binding.prefix_name "rep_" qty_name, Binding.prefix_name "abs_" qty_name)
kuncar@45676
   182
      | SOME morphs => morphs)
kaliszyk@35222
   183
kuncar@47096
   184
    val ((_, (_, abs_def)), lthy2) = lthy1
wenzelm@46909
   185
      |> Local_Theory.define ((abs_name, NoSyn), ((Thm.def_binding abs_name, []), abs_trm))
kuncar@47096
   186
    val ((_, (_, rep_def)), lthy3) = lthy2
wenzelm@46909
   187
      |> Local_Theory.define ((rep_name, NoSyn), ((Thm.def_binding rep_name, []), rep_trm))
kaliszyk@35222
   188
wenzelm@41444
   189
    (* quot_type theorem *)
wenzelm@41444
   190
    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
kaliszyk@35222
   191
wenzelm@41444
   192
    (* quotient theorem *)
kuncar@47308
   193
    val quotient_thm_name = Binding.prefix_name "Quotient3_" qty_name
wenzelm@41444
   194
    val quotient_thm =
wenzelm@41444
   195
      (quot_thm RS @{thm quot_type.Quotient})
wenzelm@41444
   196
      |> fold_rule [abs_def, rep_def]
kaliszyk@35222
   197
wenzelm@41444
   198
    (* name equivalence theorem *)
wenzelm@41444
   199
    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
kaliszyk@35222
   200
wenzelm@45279
   201
    (* storing the quotients *)
kuncar@47093
   202
    val quotients = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm, 
kuncar@47093
   203
      quot_thm = quotient_thm}
urbanc@37530
   204
wenzelm@41444
   205
    val lthy4 = lthy3
kuncar@47937
   206
      |> init_quotient_infr gen_code quotient_thm equiv_thm
wenzelm@45282
   207
      |> (snd oo Local_Theory.note)
wenzelm@45282
   208
        ((equiv_thm_name,
wenzelm@45282
   209
          if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
wenzelm@45282
   210
          [equiv_thm])
wenzelm@45282
   211
      |> (snd oo Local_Theory.note)
wenzelm@45282
   212
        ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
wenzelm@45282
   213
          [quotient_thm])
wenzelm@41444
   214
  in
wenzelm@45279
   215
    (quotients, lthy4)
wenzelm@41444
   216
  end
kaliszyk@35222
   217
kaliszyk@35222
   218
kaliszyk@35222
   219
(* sanity checks for the quotient type specifications *)
kuncar@45676
   220
fun sanity_check ((vs, qty_name, _), (rty, rel, _), _) =
wenzelm@41444
   221
  let
wenzelm@41444
   222
    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
wenzelm@41444
   223
    val rel_tfrees = map fst (Term.add_tfrees rel [])
wenzelm@41444
   224
    val rel_frees = map fst (Term.add_frees rel [])
wenzelm@41444
   225
    val rel_vars = Term.add_vars rel []
wenzelm@41444
   226
    val rel_tvars = Term.add_tvars rel []
wenzelm@43547
   227
    val qty_str = Binding.print qty_name ^ ": "
kaliszyk@35222
   228
wenzelm@41444
   229
    val illegal_rel_vars =
wenzelm@41444
   230
      if null rel_vars andalso null rel_tvars then []
wenzelm@41444
   231
      else [qty_str ^ "illegal schematic variable(s) in the relation."]
kaliszyk@35222
   232
wenzelm@41444
   233
    val dup_vs =
wenzelm@41444
   234
      (case duplicates (op =) vs of
wenzelm@41444
   235
        [] => []
wenzelm@41444
   236
      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
kaliszyk@35222
   237
wenzelm@41444
   238
    val extra_rty_tfrees =
wenzelm@41444
   239
      (case subtract (op =) vs rty_tfreesT of
wenzelm@41444
   240
        [] => []
wenzelm@41444
   241
      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
kaliszyk@35222
   242
wenzelm@41444
   243
    val extra_rel_tfrees =
wenzelm@41444
   244
      (case subtract (op =) vs rel_tfrees of
wenzelm@41444
   245
        [] => []
wenzelm@41444
   246
      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
kaliszyk@35222
   247
wenzelm@41444
   248
    val illegal_rel_frees =
wenzelm@41444
   249
      (case rel_frees of
wenzelm@41444
   250
        [] => []
wenzelm@41444
   251
      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
kaliszyk@35222
   252
wenzelm@41444
   253
    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
wenzelm@41444
   254
  in
wenzelm@41444
   255
    if null errs then () else error (cat_lines errs)
wenzelm@41444
   256
  end
kaliszyk@35222
   257
kaliszyk@35222
   258
(* check for existence of map functions *)
kuncar@45795
   259
fun map_check ctxt (_, (rty, _, _), _) =
wenzelm@41444
   260
  let
wenzelm@41444
   261
    fun map_check_aux rty warns =
wenzelm@45280
   262
      (case rty of
wenzelm@41444
   263
        Type (_, []) => warns
wenzelm@45340
   264
      | Type (s, _) =>
kuncar@45795
   265
          if Symtab.defined (Enriched_Type.entries ctxt) s then warns else s :: warns
wenzelm@45280
   266
      | _ => warns)
kaliszyk@35222
   267
wenzelm@41444
   268
    val warns = map_check_aux rty []
wenzelm@41444
   269
  in
wenzelm@41444
   270
    if null warns then ()
wenzelm@41444
   271
    else warning ("No map function defined for " ^ commas warns ^
wenzelm@41444
   272
      ". This will cause problems later on.")
wenzelm@41444
   273
  end
kaliszyk@35222
   274
kaliszyk@35222
   275
kaliszyk@35222
   276
(*** interface and syntax setup ***)
kaliszyk@35222
   277
kuncar@45698
   278
(* the ML-interface takes a list of tuples consisting of:
kuncar@45698
   279
kuncar@45698
   280
 - the name of the quotient type
kuncar@45698
   281
 - its free type variables (first argument)
kuncar@45698
   282
 - its mixfix annotation
kuncar@45698
   283
 - the type to be quotient
kuncar@45698
   284
 - the partial flag (a boolean)
kuncar@45698
   285
 - the relation according to which the type is quotient
kuncar@45698
   286
 - optional names of morphisms (rep/abs)
kuncar@47937
   287
 - flag if code should be generated by Lifting package
kuncar@45698
   288
kuncar@45698
   289
 it opens a proof-state in which one has to show that the
kuncar@45698
   290
 relations are equivalence relations
kuncar@45698
   291
*)
kuncar@45698
   292
kuncar@47983
   293
fun quotient_type quot lthy =
wenzelm@41444
   294
  let
wenzelm@41444
   295
    (* sanity check *)
kuncar@47983
   296
    val _ = sanity_check quot
kuncar@47983
   297
    val _ = map_check lthy quot
kaliszyk@35222
   298
wenzelm@41444
   299
    fun mk_goal (rty, rel, partial) =
wenzelm@41444
   300
      let
wenzelm@41444
   301
        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
wenzelm@41444
   302
        val const =
wenzelm@41444
   303
          if partial then @{const_name part_equivp} else @{const_name equivp}
wenzelm@41444
   304
      in
wenzelm@41444
   305
        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
wenzelm@41444
   306
      end
wenzelm@41444
   307
kuncar@47983
   308
    val goal = (mk_goal o #2) quot
wenzelm@41444
   309
kuncar@47983
   310
    fun after_qed [[thm]] = (snd oo add_quotient_type) (quot, thm)
kaliszyk@35222
   311
  in
kuncar@47983
   312
    Proof.theorem NONE after_qed [[(goal, [])]] lthy
kaliszyk@35222
   313
  end
kaliszyk@35222
   314
kuncar@47983
   315
fun quotient_type_cmd spec lthy =
kaliszyk@35222
   316
  let
kuncar@47937
   317
    fun parse_spec ((((((gen_code, vs), qty_name), mx), rty_str), (partial, rel_str)), opt_morphs) lthy =
wenzelm@41444
   318
      let
wenzelm@41444
   319
        val rty = Syntax.read_typ lthy rty_str
cezarykaliszyk@46727
   320
        val tmp_lthy1 = Variable.declare_typ rty lthy
wenzelm@41444
   321
        val rel =
cezarykaliszyk@46727
   322
          Syntax.parse_term tmp_lthy1 rel_str
wenzelm@41444
   323
          |> Type.constraint (rty --> rty --> @{typ bool})
cezarykaliszyk@46727
   324
          |> Syntax.check_term tmp_lthy1
cezarykaliszyk@46727
   325
        val tmp_lthy2 = Variable.declare_term rel tmp_lthy1
wenzelm@41444
   326
      in
kuncar@47937
   327
        (((vs, qty_name, mx), (rty, rel, partial), (opt_morphs, gen_code)), tmp_lthy2)
wenzelm@41444
   328
      end
wenzelm@41444
   329
kuncar@47983
   330
    val (spec', _) = parse_spec spec lthy
kaliszyk@35222
   331
  in
cezarykaliszyk@46727
   332
    quotient_type spec' lthy
kaliszyk@35222
   333
  end
kaliszyk@35222
   334
kuncar@47937
   335
val opt_gen_code =
kuncar@47937
   336
  Scan.optional (@{keyword "("} |-- (Parse.reserved "no_code" >> K false) --| Parse.!!! @{keyword ")"}) true
kuncar@47937
   337
wenzelm@46949
   338
val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
kaliszyk@37493
   339
kuncar@47091
   340
val quotspec_parser =
kuncar@47983
   341
     (opt_gen_code -- Parse.type_args -- Parse.binding) --
kuncar@47091
   342
      (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
kuncar@47091
   343
      Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
kuncar@47091
   344
        (@{keyword "/"} |-- (partial -- Parse.term))  --
kuncar@47983
   345
        Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding))
kuncar@47091
   346
kaliszyk@35222
   347
val _ =
wenzelm@46961
   348
  Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
wenzelm@41444
   349
    "quotient type definitions (require equivalence proofs)"
kuncar@47096
   350
      (quotspec_parser >> quotient_type_cmd)
kuncar@47096
   351
kaliszyk@35222
   352
wenzelm@45280
   353
end;