src/HOL/Tools/Quotient/quotient_typ.ML
author wenzelm
Fri, 07 Jan 2011 15:35:00 +0100
changeset 41444 7f40120cd814
parent 39288 f1ae2493d93f
child 41451 892e67be8304
permissions -rw-r--r--
more precise parentheses and indentation; eliminated trailing whitespace;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
37744
3daaf23b9ab4 tuned titles
haftmann
parents: 37530
diff changeset
     1
(*  Title:      HOL/Tools/Quotient/quotient_typ.ML
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     2
    Author:     Cezary Kaliszyk and Christian Urban
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     3
35806
a814cccce0b8 rollback of local typedef until problem with type-variables can be sorted out; fixed header
Christian Urban <urbanc@in.tum.de>
parents: 35790
diff changeset
     4
Definition of a quotient type.
35790
a9507cd84326 removed Local_Theory.theory_result by using local Typedef.add_typedef
Christian Urban <urbanc@in.tum.de>
parents: 35788
diff changeset
     5
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     6
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     7
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     8
signature QUOTIENT_TYPE =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
     9
sig
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
    10
  val add_quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) * thm
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
    11
    -> Proof.context -> Quotient_Info.quotdata_info * local_theory
35415
1810b1ade437 export add_quotient_type.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 35351
diff changeset
    12
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
    13
  val quotient_type: ((string list * binding * mixfix) * (typ * term * bool)) list
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    14
    -> Proof.context -> Proof.state
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    15
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
    16
  val quotient_type_cmd: ((((string list * binding) * mixfix) * string) * (bool * string)) list
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    17
    -> Proof.context -> Proof.state
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    18
end;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    19
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    20
structure Quotient_Type: QUOTIENT_TYPE =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    21
struct
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    22
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    23
open Quotient_Info;
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    24
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    25
(* wrappers for define, note, Attrib.internal and theorem_i *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    26
fun define (name, mx, rhs) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    27
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    28
    val ((rhs, (_ , thm)), lthy') =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    29
      Local_Theory.define ((name, mx), (Attrib.empty_binding, rhs)) lthy
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    30
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    31
    ((rhs, thm), lthy')
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    32
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    33
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    34
fun note (name, thm, attrs) lthy =
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
    35
  Local_Theory.note ((name, attrs), [thm]) lthy |> snd
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
    36
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    37
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    38
fun intern_attr at = Attrib.internal (K at)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    39
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    40
fun theorem after_qed goals ctxt =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    41
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    42
    val goals' = map (rpair []) goals
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    43
    fun after_qed' thms = after_qed (the_single thms)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    44
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    45
    Proof.theorem NONE after_qed' [goals'] ctxt
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    46
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    47
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    48
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    49
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    50
(*** definition of quotient types ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    51
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    52
val mem_def1 = @{lemma "y : S ==> S y" by (simp add: mem_def)}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    53
val mem_def2 = @{lemma "S y ==> y : S" by (simp add: mem_def)}
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    54
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    55
(* constructs the term lambda (c::rty => bool). EX (x::rty). c = rel x *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    56
fun typedef_term rel rty lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    57
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    58
    val [x, c] =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    59
      [("x", rty), ("c", HOLogic.mk_setT rty)]
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    60
      |> Variable.variant_frees lthy [rel]
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    61
      |> map Free
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    62
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    63
    lambda c (HOLogic.exists_const rty $
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    64
        lambda x (HOLogic.mk_conj (rel $ x $ x, HOLogic.mk_eq (c, rel $ x))))
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    65
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    66
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    67
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    68
(* makes the new type definitions and proves non-emptyness *)
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
    69
fun typedef_make (vs, qty_name, mx, rel, rty) equiv_thm lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    70
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    71
    val typedef_tac =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    72
      EVERY1 (map rtac [@{thm part_equivp_typedef}, equiv_thm])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    73
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    74
  (* FIXME: purely local typedef causes at the moment
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    75
     problems with type variables
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    76
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    77
    Typedef.add_typedef false NONE (qty_name, vs, mx)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    78
      (typedef_term rel rty lthy) NONE typedef_tac lthy
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    79
  *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    80
  (* FIXME should really use local typedef here *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    81
    Local_Theory.background_theory_result
35806
a814cccce0b8 rollback of local typedef until problem with type-variables can be sorted out; fixed header
Christian Urban <urbanc@in.tum.de>
parents: 35790
diff changeset
    82
     (Typedef.add_typedef_global false NONE
35842
7c170d39a808 typedef etc.: no constraints;
wenzelm
parents: 35806
diff changeset
    83
       (qty_name, map (rpair dummyS) vs, mx)
35806
a814cccce0b8 rollback of local typedef until problem with type-variables can be sorted out; fixed header
Christian Urban <urbanc@in.tum.de>
parents: 35790
diff changeset
    84
         (typedef_term rel rty lthy)
a814cccce0b8 rollback of local typedef until problem with type-variables can be sorted out; fixed header
Christian Urban <urbanc@in.tum.de>
parents: 35790
diff changeset
    85
           NONE typedef_tac) lthy
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    86
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    87
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    88
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
    89
(* tactic to prove the quot_type theorem for the new type *)
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35842
diff changeset
    90
fun typedef_quot_type_tac equiv_thm ((_, typedef_info): Typedef.info) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    91
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    92
    val rep_thm = #Rep typedef_info RS mem_def1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    93
    val rep_inv = #Rep_inverse typedef_info
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    94
    val abs_inv = #Abs_inverse typedef_info
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    95
    val rep_inj = #Rep_inject typedef_info
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    96
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    97
    (rtac @{thm quot_type.intro} THEN' RANGE [
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    98
      rtac equiv_thm,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
    99
      rtac rep_thm,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   100
      rtac rep_inv,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   101
      rtac abs_inv THEN' rtac mem_def2 THEN' atac,
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   102
      rtac rep_inj]) 1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   103
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   104
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   105
(* proves the quot_type theorem for the new type *)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   106
fun typedef_quot_type_thm (rel, abs, rep, equiv_thm, typedef_info) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   107
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   108
    val quot_type_const = Const (@{const_name "quot_type"}, dummyT)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   109
    val goal =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   110
      HOLogic.mk_Trueprop (quot_type_const $ rel $ abs $ rep)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   111
      |> Syntax.check_term lthy
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   112
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   113
    Goal.prove lthy [] [] goal
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   114
      (K (typedef_quot_type_tac equiv_thm typedef_info))
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   115
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   116
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   117
(* main function for constructing a quotient type *)
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   118
fun add_quotient_type (((vs, qty_name, mx), (rty, rel, partial)), equiv_thm) lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   119
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   120
    val part_equiv =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   121
      if partial
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   122
      then equiv_thm
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   123
      else equiv_thm RS @{thm equivp_implies_part_equivp}
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   124
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   125
    (* generates the typedef *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   126
    val ((qty_full_name, typedef_info), lthy1) =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   127
      typedef_make (vs, qty_name, mx, rel, rty) part_equiv lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   128
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   129
    (* abs and rep functions from the typedef *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   130
    val Abs_ty = #abs_type (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   131
    val Rep_ty = #rep_type (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   132
    val Abs_name = #Abs_name (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   133
    val Rep_name = #Rep_name (#1 typedef_info)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   134
    val Abs_const = Const (Abs_name, Rep_ty --> Abs_ty)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   135
    val Rep_const = Const (Rep_name, Abs_ty --> Rep_ty)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   136
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   137
    (* more useful abs and rep definitions *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   138
    val abs_const = Const (@{const_name "quot_type.abs"}, dummyT )
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   139
    val rep_const = Const (@{const_name "quot_type.rep"}, dummyT )
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   140
    val abs_trm = Syntax.check_term lthy1 (abs_const $ rel $ Abs_const)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   141
    val rep_trm = Syntax.check_term lthy1 (rep_const $ Rep_const)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   142
    val abs_name = Binding.prefix_name "abs_" qty_name
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   143
    val rep_name = Binding.prefix_name "rep_" qty_name
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   144
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   145
    val ((_, abs_def), lthy2) = define (abs_name, NoSyn, abs_trm) lthy1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   146
    val ((_, rep_def), lthy3) = define (rep_name, NoSyn, rep_trm) lthy2
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   147
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   148
    (* quot_type theorem *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   149
    val quot_thm = typedef_quot_type_thm (rel, Abs_const, Rep_const, part_equiv, typedef_info) lthy3
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   150
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   151
    (* quotient theorem *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   152
    val quotient_thm_name = Binding.prefix_name "Quotient_" qty_name
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   153
    val quotient_thm =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   154
      (quot_thm RS @{thm quot_type.Quotient})
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   155
      |> fold_rule [abs_def, rep_def]
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   156
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   157
    (* name equivalence theorem *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   158
    val equiv_thm_name = Binding.suffix_name "_equivp" qty_name
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   159
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   160
    (* storing the quotdata *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   161
    val quotdata = {qtyp = Abs_ty, rtyp = rty, equiv_rel = rel, equiv_thm = equiv_thm}
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
   162
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   163
    fun qinfo phi = transform_quotdata phi quotdata
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
   164
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   165
    val lthy4 = lthy3
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   166
      |> Local_Theory.declaration true (fn phi => quotdata_update_gen qty_full_name (qinfo phi))
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   167
      |> note (equiv_thm_name, equiv_thm, if partial then [] else [intern_attr equiv_rules_add])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   168
      |> note (quotient_thm_name, quotient_thm, [intern_attr quotient_rules_add])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   169
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   170
    (quotdata, lthy4)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   171
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   172
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   173
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   174
(* sanity checks for the quotient type specifications *)
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   175
fun sanity_check ((vs, qty_name, _), (rty, rel, _)) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   176
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   177
    val rty_tfreesT = map fst (Term.add_tfreesT rty [])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   178
    val rel_tfrees = map fst (Term.add_tfrees rel [])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   179
    val rel_frees = map fst (Term.add_frees rel [])
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   180
    val rel_vars = Term.add_vars rel []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   181
    val rel_tvars = Term.add_tvars rel []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   182
    val qty_str = Binding.str_of qty_name ^ ": "
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   183
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   184
    val illegal_rel_vars =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   185
      if null rel_vars andalso null rel_tvars then []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   186
      else [qty_str ^ "illegal schematic variable(s) in the relation."]
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   187
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   188
    val dup_vs =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   189
      (case duplicates (op =) vs of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   190
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   191
      | dups => [qty_str ^ "duplicate type variable(s) on the lhs: " ^ commas_quote dups])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   192
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   193
    val extra_rty_tfrees =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   194
      (case subtract (op =) vs rty_tfreesT of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   195
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   196
      | extras => [qty_str ^ "extra type variable(s) on the lhs: " ^ commas_quote extras])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   197
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   198
    val extra_rel_tfrees =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   199
      (case subtract (op =) vs rel_tfrees of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   200
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   201
      | extras => [qty_str ^ "extra type variable(s) in the relation: " ^ commas_quote extras])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   202
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   203
    val illegal_rel_frees =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   204
      (case rel_frees of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   205
        [] => []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   206
      | xs => [qty_str ^ "illegal variable(s) in the relation: " ^ commas_quote xs])
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   207
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   208
    val errs = illegal_rel_vars @ dup_vs @ extra_rty_tfrees @ extra_rel_tfrees @ illegal_rel_frees
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   209
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   210
    if null errs then () else error (cat_lines errs)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   211
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   212
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   213
(* check for existence of map functions *)
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   214
fun map_check ctxt (_, (rty, _, _)) =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   215
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   216
    val thy = ProofContext.theory_of ctxt
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   217
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   218
    fun map_check_aux rty warns =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   219
      case rty of
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   220
        Type (_, []) => warns
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   221
      | Type (s, _) => if maps_defined thy s then warns else s::warns
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   222
      | _ => warns
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   223
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   224
    val warns = map_check_aux rty []
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   225
  in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   226
    if null warns then ()
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   227
    else warning ("No map function defined for " ^ commas warns ^
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   228
      ". This will cause problems later on.")
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   229
  end
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   230
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   231
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   232
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   233
(*** interface and syntax setup ***)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   234
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   235
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   236
(* the ML-interface takes a list of 5-tuples consisting of:
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   237
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   238
 - the name of the quotient type
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   239
 - its free type variables (first argument)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   240
 - its mixfix annotation
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   241
 - the type to be quotient
37530
70d03844b2f9 export of proper information in the ML-interface of the quotient package
Christian Urban <urbanc@in.tum.de>
parents: 37493
diff changeset
   242
 - the partial flag (a boolean)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   243
 - the relation according to which the type is quotient
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   244
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   245
 it opens a proof-state in which one has to show that the
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   246
 relations are equivalence relations
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   247
*)
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   248
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   249
fun quotient_type quot_list lthy =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   250
  let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   251
    (* sanity check *)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   252
    val _ = List.app sanity_check quot_list
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   253
    val _ = List.app (map_check lthy) quot_list
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   254
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   255
    fun mk_goal (rty, rel, partial) =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   256
      let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   257
        val equivp_ty = ([rty, rty] ---> @{typ bool}) --> @{typ bool}
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   258
        val const =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   259
          if partial then @{const_name part_equivp} else @{const_name equivp}
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   260
      in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   261
        HOLogic.mk_Trueprop (Const (const, equivp_ty) $ rel)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   262
      end
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   263
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   264
    val goals = map (mk_goal o snd) quot_list
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   265
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   266
    fun after_qed thms lthy =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   267
      fold_map add_quotient_type (quot_list ~~ thms) lthy |> snd
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   268
  in
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   269
    theorem after_qed goals lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   270
  end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   271
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   272
fun quotient_type_cmd specs lthy =
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   273
  let
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   274
    fun parse_spec ((((vs, qty_name), mx), rty_str), (partial, rel_str)) lthy =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   275
      let
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   276
        val rty = Syntax.read_typ lthy rty_str
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   277
        val lthy1 = Variable.declare_typ rty lthy
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   278
        val rel =
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   279
          Syntax.parse_term lthy1 rel_str
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   280
          |> Type.constraint (rty --> rty --> @{typ bool})
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   281
          |> Syntax.check_term lthy1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   282
        val lthy2 = Variable.declare_term rel lthy1
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   283
      in
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   284
        (((vs, qty_name, mx), (rty, rel, partial)), lthy2)
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   285
      end
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   286
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   287
    val (spec', lthy') = fold_map parse_spec specs lthy
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   288
  in
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   289
    quotient_type spec' lthy'
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   290
  end
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   291
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   292
val partial = Scan.optional (Parse.reserved "partial" -- Parse.$$$ ":" >> K true) false
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   293
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   294
val quotspec_parser =
37493
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   295
  Parse.and_list1
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   296
    ((Parse.type_args -- Parse.binding) --
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   297
      Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.typ) --
2377d246a631 Quotient package now uses Partial Equivalence instead place of equivalence
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents: 36960
diff changeset
   298
        (Parse.$$$ "/" |-- (partial -- Parse.term)))
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   299
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36323
diff changeset
   300
val _ = Keyword.keyword "/"
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   301
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   302
val _ =
41444
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   303
  Outer_Syntax.local_theory_to_proof "quotient_type"
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   304
    "quotient type definitions (require equivalence proofs)"
7f40120cd814 more precise parentheses and indentation;
wenzelm
parents: 39288
diff changeset
   305
       Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
35222
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   306
4f1fba00f66d Initial version of HOL quotient package.
Cezary Kaliszyk <kaliszyk@in.tum.de>
parents:
diff changeset
   307
end; (* structure *)