src/HOL/Tools/typedef.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 36960 01594f816e3a
child 38350 480b2de9927c
permissions -rw-r--r--
tuned titles
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 30345
diff changeset
     1
(*  Title:      HOL/Tools/typedef.ML
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16126
diff changeset
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     3
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
     4
Gordon/HOL-style type definitions: create a new syntactic type
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
     5
represented by a non-empty set.
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     6
*)
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     7
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 30345
diff changeset
     8
signature TYPEDEF =
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
     9
sig
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    10
  type info =
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
    11
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    12
   {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
29061
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    13
    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
c67cc9402ba9 inhabitance goal is now stated in original form and result contracted --
wenzelm
parents: 29059
diff changeset
    14
    Rep_induct: thm, Abs_induct: thm}
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    15
  val transform_info: morphism -> info -> info
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    16
  val get_info: Proof.context -> string -> info list
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    17
  val get_info_global: theory -> string -> info list
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    18
  val interpretation: (string -> theory -> theory) -> theory -> theory
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    19
  val setup: theory -> theory
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
    20
  val add_typedef: bool -> binding option -> binding * (string * sort) list * mixfix ->
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    21
    term -> (binding * binding) option -> tactic -> local_theory -> (string * info) * local_theory
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
    22
  val add_typedef_global: bool -> binding option -> binding * (string * sort) list * mixfix ->
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
    23
    term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
    24
  val typedef: (bool * binding) * (binding * (string * sort) list * mixfix) * term *
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    25
    (binding * binding) option -> local_theory -> Proof.state
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
    26
  val typedef_cmd: (bool * binding) * (binding * (string * string option) list * mixfix) * string *
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    27
    (binding * binding) option -> local_theory -> Proof.state
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    28
end;
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    29
31723
f5cafe803b55 discontinued ancient tradition to suffix certain ML module names with "_package"
haftmann
parents: 30345
diff changeset
    30
structure Typedef: TYPEDEF =
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    31
struct
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
    32
17922
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
    33
(** type definitions **)
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
    34
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
    35
(* theory data *)
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    36
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
    37
type info =
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    38
  (*global part*)
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
    39
  {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, axiom_name: string} *
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    40
  (*local part*)
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    41
  {inhabited: thm, type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    42
    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    43
    Rep_induct: thm, Abs_induct: thm};
19459
2041d472fc17 seperated typedef codegen from main code
haftmann
parents: 19391
diff changeset
    44
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    45
fun transform_info phi (info: info) =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    46
  let
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    47
    val thm = Morphism.thm phi;
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    48
    val (global_info, {inhabited, type_definition,
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    49
      set_def, Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    50
      Rep_cases, Abs_cases, Rep_induct, Abs_induct}) = info;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    51
  in
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    52
    (global_info,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    53
     {inhabited = thm inhabited, type_definition = thm type_definition,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    54
      set_def = Option.map thm set_def, Rep = thm Rep, Rep_inverse = thm Rep_inverse,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    55
      Abs_inverse = thm Abs_inverse, Rep_inject = thm Rep_inject, Abs_inject = thm Abs_inject,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    56
      Rep_cases = thm Rep_cases, Abs_cases = thm Abs_cases, Rep_induct = thm Rep_induct,
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
    57
      Abs_induct = thm Abs_induct})
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    58
  end;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    59
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    60
structure Data = Generic_Data
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 21565
diff changeset
    61
(
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    62
  type T = info list Symtab.table;
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    63
  val empty = Symtab.empty;
16458
4c6fd0c01d28 accomodate change of TheoryDataFun;
wenzelm
parents: 16126
diff changeset
    64
  val extend = I;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    65
  fun merge data = Symtab.merge_list (K true) data;
22846
fb79144af9a3 simplified DataFun interfaces;
wenzelm
parents: 21565
diff changeset
    66
);
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
    67
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    68
val get_info = Symtab.lookup_list o Data.get o Context.Proof;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    69
val get_info_global = Symtab.lookup_list o Data.get o Context.Theory;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    70
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    71
fun put_info name info = Data.map (Symtab.cons_list (name, info));
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    72
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    73
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    74
(* global interpretation *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    75
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    76
structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    77
val interpretation = Typedef_Interpretation.interpretation;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    78
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    79
val setup = Typedef_Interpretation.init;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    80
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    81
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    82
(* primitive typedef axiomatization -- for fresh typedecl *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    83
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    84
fun mk_inhabited A =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    85
  let val T = HOLogic.dest_setT (Term.fastype_of A)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    86
  in HOLogic.mk_Trueprop (HOLogic.exists_const T $ Abs ("x", T, HOLogic.mk_mem (Bound 0, A))) end;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    87
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    88
fun mk_typedef newT oldT RepC AbsC A =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    89
  let
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    90
    val typedefC =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    91
      Const (@{const_name type_definition},
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    92
        (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    93
  in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
35134
d8d6c2f55c0c Typedef.the_info;
wenzelm
parents: 35129
diff changeset
    94
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    95
fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A thy =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    96
  let
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    97
    (* errors *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    98
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
    99
    fun show_names pairs = commas_quote (map fst pairs);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   100
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   101
    val lhs_tfrees = Term.add_tfreesT newT [];
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   102
    val rhs_tfrees = Term.add_tfreesT oldT [];
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   103
    val _ =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   104
      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => ()
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   105
      | extras => error ("Extra type variables in representing set: " ^ show_names extras));
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   106
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   107
    val _ =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   108
      (case Term.add_frees A [] of [] => []
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   109
      | xs => error ("Illegal variables in representing set: " ^ show_names xs));
35134
d8d6c2f55c0c Typedef.the_info;
wenzelm
parents: 35129
diff changeset
   110
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   111
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   112
    (* axiomatization *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   113
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   114
    val ((RepC, AbsC), consts_thy) = thy
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   115
      |> Sign.declare_const ((Rep_name, newT --> oldT), NoSyn)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   116
      ||>> Sign.declare_const ((Abs_name, oldT --> newT), NoSyn);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   117
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   118
    val typedef_deps = Term.add_consts A [];
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   119
36106
19deea200358 Thm.add_axiom/add_def: return internal name of foundational axiom;
wenzelm
parents: 35994
diff changeset
   120
    val ((axiom_name, axiom), axiom_thy) = consts_thy
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   121
      |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   122
      ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   123
      ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   124
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
   125
  in ((RepC, AbsC, axiom_name, axiom), axiom_thy) end;
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   126
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   127
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   128
(* prepare_typedef *)
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   129
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   130
fun prepare_typedef prep_term def_set name (tname, raw_args, mx) raw_set opt_morphs lthy =
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   131
  let
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   132
    val full_name = Local_Theory.full_name lthy name;
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   133
    val bname = Binding.name_of name;
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   134
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   135
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   136
    (* rhs *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   137
36153
1ac501e16a6a replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents: 36107
diff changeset
   138
    val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args;
1ac501e16a6a replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents: 36107
diff changeset
   139
    val set = prep_term tmp_ctxt raw_set;
1ac501e16a6a replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents: 36107
diff changeset
   140
    val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set;
35836
9380fab5f4f7 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
wenzelm
parents: 35766
diff changeset
   141
21352
073c79be780c removed legacy read/cert/string_of;
wenzelm
parents: 20483
diff changeset
   142
    val setT = Term.fastype_of set;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   143
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   144
      error ("Not a set type: " ^ quote (Syntax.string_of_typ lthy setT));
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   145
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   146
    val goal = mk_inhabited set;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   147
    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   148
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   149
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   150
    (* lhs *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   151
36153
1ac501e16a6a replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
wenzelm
parents: 36107
diff changeset
   152
    val args = map (ProofContext.check_tfree tmp_ctxt') raw_args;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   153
    val (newT, typedecl_lthy) = lthy
35836
9380fab5f4f7 eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;
wenzelm
parents: 35766
diff changeset
   154
      |> Typedecl.typedecl (tname, args, mx)
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   155
      ||> Variable.declare_term set;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   156
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   157
    val Type (full_tname, type_args) = newT;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   158
    val lhs_tfrees = map Term.dest_TFree type_args;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   159
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   160
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   161
    (* set definition *)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   162
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   163
    val ((set', set_def), set_lthy) =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   164
      if def_set then
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   165
        typedecl_lthy
35766
eafaa9990712 Local_Theory.define handles hidden polymorphism;
wenzelm
parents: 35741
diff changeset
   166
        |> Local_Theory.define ((name, NoSyn), ((Thm.def_binding name, []), set))
eafaa9990712 Local_Theory.define handles hidden polymorphism;
wenzelm
parents: 35741
diff changeset
   167
        |>> (fn (set', (_, set_def)) => (set', SOME set_def))
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   168
      else ((set, NONE), typedecl_lthy);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   169
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   170
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   171
    (* axiomatization *)
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   172
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   173
    val (Rep_name, Abs_name) =
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   174
      (case opt_morphs of
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   175
        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   176
      | SOME morphs => morphs);
10280
2626d4e37341 provide more theorems (see subset.thy);
wenzelm
parents: 9969
diff changeset
   177
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   178
    val typedef_name = Binding.prefix_name "type_definition_" name;
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   179
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
   180
    val ((RepC, AbsC, axiom_name, typedef), typedef_lthy) =
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   181
      let
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   182
        val thy = ProofContext.theory_of set_lthy;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   183
        val cert = Thm.cterm_of thy;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   184
        val (defs, A) =
36610
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 36323
diff changeset
   185
          Local_Defs.export_cterm set_lthy (ProofContext.init_global thy) (cert set')
bafd82950e24 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
wenzelm
parents: 36323
diff changeset
   186
          ||> Thm.term_of;
18358
0a733e11021a re-oriented some result tuples in PureThy
haftmann
parents: 17956
diff changeset
   187
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
   188
        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   189
          Local_Theory.theory_result (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   190
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   191
        val cert = Thm.cterm_of (ProofContext.theory_of axiom_lthy);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   192
        val typedef =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   193
          Local_Defs.contract axiom_lthy defs (cert (mk_typedef newT oldT RepC AbsC set')) axiom;
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
   194
      in ((RepC, AbsC, axiom_name, typedef), axiom_lthy) end;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   195
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   196
    val alias_lthy = typedef_lthy
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   197
      |> Local_Theory.const_alias Rep_name (#1 (Term.dest_Const RepC))
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   198
      |> Local_Theory.const_alias Abs_name (#1 (Term.dest_Const AbsC));
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   199
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   200
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   201
    (* result *)
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   202
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   203
    fun note_qualify ((b, atts), th) =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   204
      Local_Theory.note ((Binding.qualify false bname b, map (Attrib.internal o K) atts), [th])
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   205
      #>> (fn (_, [th']) => th');
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   206
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   207
    fun typedef_result inhabited lthy1 =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   208
      let
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   209
        val cert = Thm.cterm_of (ProofContext.theory_of lthy1);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   210
        val inhabited' =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   211
          Local_Defs.contract lthy1 (the_list set_def) (cert (mk_inhabited set')) inhabited;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   212
        val typedef' = inhabited' RS typedef;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   213
        fun make th = Goal.norm_result (typedef' RS th);
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   214
        val (((((((((((_, [type_definition]), Rep), Rep_inverse), Abs_inverse), Rep_inject),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   215
            Abs_inject), Rep_cases), Abs_cases), Rep_induct), Abs_induct), lthy2) = lthy1
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   216
          |> Local_Theory.note ((typedef_name, []), [typedef'])
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   217
          ||>> note_qualify ((Rep_name, []), make @{thm type_definition.Rep})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   218
          ||>> note_qualify ((Binding.suffix_name "_inverse" Rep_name, []),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   219
              make @{thm type_definition.Rep_inverse})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   220
          ||>> note_qualify ((Binding.suffix_name "_inverse" Abs_name, []),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   221
              make @{thm type_definition.Abs_inverse})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   222
          ||>> note_qualify ((Binding.suffix_name "_inject" Rep_name, []),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   223
              make @{thm type_definition.Rep_inject})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   224
          ||>> note_qualify ((Binding.suffix_name "_inject" Abs_name, []),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   225
              make @{thm type_definition.Abs_inject})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   226
          ||>> note_qualify ((Binding.suffix_name "_cases" Rep_name,
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   227
                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   228
              make @{thm type_definition.Rep_cases})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   229
          ||>> note_qualify ((Binding.suffix_name "_cases" Abs_name,
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   230
                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   231
              make @{thm type_definition.Abs_cases})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   232
          ||>> note_qualify ((Binding.suffix_name "_induct" Rep_name,
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   233
                [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   234
              make @{thm type_definition.Rep_induct})
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   235
          ||>> note_qualify ((Binding.suffix_name "_induct" Abs_name,
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   236
                [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname]),
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   237
              make @{thm type_definition.Abs_induct});
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   238
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
   239
        val info =
36107
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
   240
          ({rep_type = oldT, abs_type = newT, Rep_name = #1 (Term.dest_Const RepC),
2af69e16eced expose foundational typedef axiom name;
wenzelm
parents: 36106
diff changeset
   241
            Abs_name = #1 (Term.dest_Const AbsC), axiom_name = axiom_name},
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
   242
           {inhabited = inhabited, type_definition = type_definition, set_def = set_def,
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   243
            Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   244
            Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
35994
9cc3df9a606e Typedef.info: separate global and local part, only the latter is transformed by morphisms;
wenzelm
parents: 35840
diff changeset
   245
          Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   246
      in
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   247
        lthy2
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   248
        |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   249
        |> Local_Theory.theory (Typedef_Interpretation.data full_tname)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   250
        |> pair (full_tname, info)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   251
      end;
11426
f280d4b29a2c abtract non-emptiness statements (no longer use Eps);
wenzelm
parents: 10697
diff changeset
   252
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   253
  in ((goal, goal_pat, typedef_result), alias_lthy) end
30345
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   254
  handle ERROR msg =>
76fd85bbf139 more uniform handling of binding in packages;
wenzelm
parents: 29579
diff changeset
   255
    cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   256
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   257
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   258
(* add_typedef: tactic interface *)
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   259
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   260
fun add_typedef def opt_name typ set opt_morphs tac lthy =
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   261
  let
17922
0cba8edb269e removed obsolete add_typedef_x;
wenzelm
parents: 17412
diff changeset
   262
    val name = the_default (#1 typ) opt_name;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   263
    val ((goal, _, typedef_result), lthy') =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   264
      prepare_typedef Syntax.check_term def name typ set opt_morphs lthy;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   265
    val inhabited =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   266
      Goal.prove lthy' [] [] goal (K tac)
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   267
      |> Goal.norm_result |> Thm.close_derivation;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   268
  in typedef_result inhabited lthy' end;
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   269
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   270
fun add_typedef_global def opt_name typ set opt_morphs tac =
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   271
  Theory_Target.init NONE
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   272
  #> add_typedef def opt_name typ set opt_morphs tac
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   273
  #> Local_Theory.exit_result_global (apsnd o transform_info);
4866
72a46bd00c8d renamed from typedef.ML;
wenzelm
parents:
diff changeset
   274
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   275
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   276
(* typedef: proof interface *)
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   277
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   278
local
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   279
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   280
fun gen_typedef prep_term prep_constraint ((def, name), (b, raw_args, mx), set, opt_morphs) lthy =
11822
122834177ec1 improved internal interface of typedef;
wenzelm
parents: 11807
diff changeset
   281
  let
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   282
    val args = map (apsnd (prep_constraint lthy)) raw_args;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   283
    val ((goal, goal_pat, typedef_result), lthy') =
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   284
      prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
35741
4f3660a3e5af localized typedef;
wenzelm
parents: 35682
diff changeset
   285
    fun after_qed [[th]] = snd o typedef_result th;
36323
655e2d74de3a modernized naming conventions of main Isar proof elements;
wenzelm
parents: 36153
diff changeset
   286
  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   287
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   288
in
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   289
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   290
val typedef = gen_typedef Syntax.check_term (K I);
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   291
val typedef_cmd = gen_typedef Syntax.read_term Typedecl.read_constraint;
17339
ab97ccef124a tuned Isar interfaces;
wenzelm
parents: 17280
diff changeset
   292
19705
08de66826677 simplified info/get_info;
wenzelm
parents: 19617
diff changeset
   293
end;
15259
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   294
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   295
6aa593317905 Added simple code generator.
berghofe
parents: 14981
diff changeset
   296
6383
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   297
(** outer syntax **)
45bb139e6ceb actually check non-emptiness theorem;
wenzelm
parents: 6357
diff changeset
   298
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   299
val _ = Keyword.keyword "morphisms";
24867
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24861
diff changeset
   300
e5b55d7be9bb simplified interfaces for outer syntax;
wenzelm
parents: 24861
diff changeset
   301
val _ =
36960
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   302
  Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   303
    Keyword.thy_goal
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   304
    (Scan.optional (Parse.$$$ "(" |--
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   305
        ((Parse.$$$ "open" >> K false) -- Scan.option Parse.binding ||
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   306
          Parse.binding >> (fn s => (true, SOME s))) --| Parse.$$$ ")") (true, NONE) --
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   307
      (Parse.type_args_constrained -- Parse.binding) --
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   308
        Parse.opt_mixfix -- (Parse.$$$ "=" |-- Parse.term) --
01594f816e3a prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
wenzelm
parents: 36610
diff changeset
   309
        Scan.option (Parse.$$$ "morphisms" |-- Parse.!!! (Parse.binding -- Parse.binding))
35840
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   310
    >> (fn ((((((def, opt_name), (args, t)), mx), A), morphs)) =>
01d7c4ba9050 allow sort constraints in HOL/typedef and related HOLCF variants;
wenzelm
parents: 35836
diff changeset
   311
        typedef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)));
6357
12448b8f92fb named witnesses: PureThy.get_thmss;
wenzelm
parents: 6092
diff changeset
   312
29056
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   313
end;
dc08e3990c77 misc tuning and modernisation;
wenzelm
parents: 29054
diff changeset
   314