src/HOL/Tools/typedef.ML
author wenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 35625 9c818cab0dd0
parent 35430 df2862dc23a8
child 35626 06197484c6ad
permissions -rw-r--r--
modernized structure Object_Logic;
haftmann@31723
     1
(*  Title:      HOL/Tools/typedef.ML
wenzelm@16458
     2
    Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
wenzelm@4866
     3
wenzelm@21352
     4
Gordon/HOL-style type definitions: create a new syntactic type
wenzelm@21352
     5
represented by a non-empty subset.
wenzelm@4866
     6
*)
wenzelm@4866
     7
haftmann@31723
     8
signature TYPEDEF =
wenzelm@4866
     9
sig
wenzelm@19705
    10
  type info =
wenzelm@29061
    11
   {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
wenzelm@29061
    12
    type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
wenzelm@29061
    13
    Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
wenzelm@29061
    14
    Rep_induct: thm, Abs_induct: thm}
wenzelm@30345
    15
  val add_typedef: bool -> binding option -> binding * string list * mixfix ->
wenzelm@30345
    16
    term -> (binding * binding) option -> tactic -> theory -> (string * info) * theory
wenzelm@35202
    17
  val typedef: (bool * binding) * (binding * string list * mixfix) * term *
wenzelm@35202
    18
    (binding * binding) option -> theory -> Proof.state
wenzelm@35202
    19
  val typedef_cmd: (bool * binding) * (binding * string list * mixfix) * string *
wenzelm@35202
    20
    (binding * binding) option -> theory -> Proof.state
haftmann@31735
    21
  val get_info: theory -> string -> info option
wenzelm@35134
    22
  val the_info: theory -> string -> info
haftmann@25513
    23
  val interpretation: (string -> theory -> theory) -> theory -> theory
haftmann@25535
    24
  val setup: theory -> theory
wenzelm@4866
    25
end;
wenzelm@4866
    26
haftmann@31723
    27
structure Typedef: TYPEDEF =
wenzelm@4866
    28
struct
wenzelm@4866
    29
wenzelm@17922
    30
(** type definitions **)
wenzelm@17922
    31
wenzelm@17922
    32
(* theory data *)
berghofe@15259
    33
wenzelm@19705
    34
type info =
wenzelm@29061
    35
 {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, inhabited: thm,
wenzelm@29061
    36
  type_definition: thm, set_def: thm option, Rep: thm, Rep_inverse: thm,
wenzelm@29061
    37
  Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
wenzelm@29061
    38
  Rep_induct: thm, Abs_induct: thm};
haftmann@19459
    39
wenzelm@33522
    40
structure TypedefData = Theory_Data
wenzelm@22846
    41
(
wenzelm@19705
    42
  type T = info Symtab.table;
berghofe@15259
    43
  val empty = Symtab.empty;
wenzelm@16458
    44
  val extend = I;
wenzelm@33522
    45
  fun merge data = Symtab.merge (K true) data;
wenzelm@22846
    46
);
berghofe@15259
    47
wenzelm@19705
    48
val get_info = Symtab.lookup o TypedefData.get;
wenzelm@35134
    49
wenzelm@35134
    50
fun the_info thy name =
wenzelm@35134
    51
  (case get_info thy name of
wenzelm@35134
    52
    SOME info => info
wenzelm@35134
    53
  | NONE => error ("Unknown typedef " ^ quote name));
wenzelm@35134
    54
wenzelm@19705
    55
fun put_info name info = TypedefData.map (Symtab.update (name, info));
berghofe@15259
    56
berghofe@15259
    57
wenzelm@6383
    58
(* prepare_typedef *)
wenzelm@6383
    59
wenzelm@21352
    60
fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
wenzelm@21352
    61
wenzelm@33314
    62
structure Typedef_Interpretation = Interpretation(type T = string val eq = op =);
wenzelm@33314
    63
val interpretation = Typedef_Interpretation.interpretation;
haftmann@25535
    64
wenzelm@35129
    65
fun prepare_typedef prep_term def name (tname, vs, mx) raw_set opt_morphs thy =
wenzelm@4866
    66
  let
wenzelm@11608
    67
    val _ = Theory.requires thy "Typedef" "typedefs";
wenzelm@21352
    68
    val ctxt = ProofContext.init thy;
wenzelm@30345
    69
wenzelm@30345
    70
    val full = Sign.full_name thy;
wenzelm@30345
    71
    val full_name = full name;
wenzelm@30345
    72
    val bname = Binding.name_of name;
wenzelm@4866
    73
wenzelm@4866
    74
    (*rhs*)
wenzelm@21352
    75
    val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
wenzelm@21352
    76
    val setT = Term.fastype_of set;
wenzelm@17280
    77
    val rhs_tfrees = Term.add_tfrees set [];
wenzelm@17280
    78
    val rhs_tfreesT = Term.add_tfreesT setT [];
wenzelm@4866
    79
    val oldT = HOLogic.dest_setT setT handle TYPE _ =>
wenzelm@24920
    80
      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
wenzelm@4866
    81
wenzelm@4866
    82
    (*lhs*)
wenzelm@17280
    83
    val defS = Sign.defaultS thy;
wenzelm@19473
    84
    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
wenzelm@17280
    85
    val args_setT = lhs_tfrees
wenzelm@17280
    86
      |> filter (member (op =) rhs_tfrees andf (not o member (op =) rhs_tfreesT))
wenzelm@17280
    87
      |> map TFree;
wenzelm@17280
    88
wenzelm@10280
    89
    val full_tname = full tname;
wenzelm@10280
    90
    val newT = Type (full_tname, map TFree lhs_tfrees);
wenzelm@4866
    91
wenzelm@30345
    92
    val (Rep_name, Abs_name) =
wenzelm@30345
    93
      (case opt_morphs of
wenzelm@30345
    94
        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
wenzelm@30345
    95
      | SOME morphs => morphs);
wenzelm@19391
    96
    val setT' = map Term.itselfT args_setT ---> setT;
wenzelm@17280
    97
    val setC = Term.list_comb (Const (full_name, setT'), map Logic.mk_type args_setT);
wenzelm@10280
    98
    val RepC = Const (full Rep_name, newT --> oldT);
wenzelm@10280
    99
    val AbsC = Const (full Abs_name, oldT --> newT);
wenzelm@10280
   100
wenzelm@29061
   101
    (*inhabitance*)
wenzelm@29061
   102
    fun mk_inhabited A =
krauss@29054
   103
      HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
wenzelm@29061
   104
    val set' = if def then setC else set;
wenzelm@29062
   105
    val goal' = mk_inhabited set';
wenzelm@29061
   106
    val goal = mk_inhabited set;
wenzelm@30345
   107
    val goal_pat = mk_inhabited (Var (the_default (bname, 0) (Syntax.read_variable bname), setT));
wenzelm@4866
   108
wenzelm@29061
   109
    (*axiomatization*)
wenzelm@30345
   110
    val typedef_name = Binding.prefix_name "type_definition_" name;
wenzelm@10280
   111
    val typedefC =
wenzelm@29056
   112
      Const (@{const_name type_definition},
wenzelm@29056
   113
        (newT --> oldT) --> (oldT --> newT) --> setT --> HOLogic.boolT);
wenzelm@29061
   114
    val typedef_prop = Logic.mk_implies (goal', HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set'));
wenzelm@30345
   115
    val typedef_deps = Term.add_consts set' [];
wenzelm@4866
   116
wenzelm@29061
   117
    (*set definition*)
wenzelm@29061
   118
    fun add_def theory =
wenzelm@29056
   119
      if def then
wenzelm@29061
   120
        theory
wenzelm@35430
   121
        |> Sign.add_consts_i [(name, setT', NoSyn)]
wenzelm@35238
   122
        |> PureThy.add_defs false [((Thm.def_binding name, Logic.mk_equals (setC, set)), [])]
wenzelm@19705
   123
        |-> (fn [th] => pair (SOME th))
wenzelm@29061
   124
      else (NONE, theory);
wenzelm@29061
   125
    fun contract_def NONE th = th
wenzelm@29061
   126
      | contract_def (SOME def_eq) th =
wenzelm@29061
   127
          let
wenzelm@29061
   128
            val cert = Thm.cterm_of (Thm.theory_of_thm def_eq);
wenzelm@29061
   129
            val goal_eq = MetaSimplifier.rewrite true [def_eq] (cert goal');
wenzelm@35021
   130
          in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
haftmann@18358
   131
wenzelm@29056
   132
    fun typedef_result inhabited =
wenzelm@35625
   133
      Object_Logic.typedecl (tname, vs, mx)
haftmann@25458
   134
      #> snd
wenzelm@24712
   135
      #> Sign.add_consts_i
wenzelm@6383
   136
        [(Rep_name, newT --> oldT, NoSyn),
krauss@29053
   137
         (Abs_name, oldT --> newT, NoSyn)]
wenzelm@29061
   138
      #> add_def
wenzelm@29061
   139
      #-> (fn set_def =>
wenzelm@30345
   140
        PureThy.add_axioms [((typedef_name, typedef_prop),
wenzelm@29061
   141
          [Thm.rule_attribute (K (fn cond_axm => contract_def set_def inhabited RS cond_axm))])]
wenzelm@29061
   142
        ##>> pair set_def)
wenzelm@21352
   143
      ##> Theory.add_deps "" (dest_Const RepC) typedef_deps
wenzelm@21352
   144
      ##> Theory.add_deps "" (dest_Const AbsC) typedef_deps
wenzelm@29061
   145
      #-> (fn ([type_definition], set_def) => fn thy1 =>
wenzelm@11822
   146
        let
wenzelm@35021
   147
          fun make th = Drule.export_without_context (th OF [type_definition]);
haftmann@18377
   148
          val ([Rep, Rep_inverse, Abs_inverse, Rep_inject, Abs_inject,
wenzelm@19705
   149
              Rep_cases, Abs_cases, Rep_induct, Abs_induct], thy2) =
wenzelm@19705
   150
            thy1
wenzelm@30345
   151
            |> Sign.add_path (Binding.name_of name)
wenzelm@12338
   152
            |> PureThy.add_thms
wenzelm@30345
   153
              [((Rep_name, make @{thm type_definition.Rep}), []),
wenzelm@30345
   154
                ((Binding.suffix_name "_inverse" Rep_name, make @{thm type_definition.Rep_inverse}), []),
wenzelm@30345
   155
                ((Binding.suffix_name "_inverse" Abs_name, make @{thm type_definition.Abs_inverse}), []),
wenzelm@30345
   156
                ((Binding.suffix_name "_inject" Rep_name, make @{thm type_definition.Rep_inject}), []),
wenzelm@30345
   157
                ((Binding.suffix_name "_inject" Abs_name, make @{thm type_definition.Abs_inject}), []),
wenzelm@30345
   158
                ((Binding.suffix_name "_cases" Rep_name, make @{thm type_definition.Rep_cases}),
wenzelm@33368
   159
                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.cases_pred full_name]),
wenzelm@30345
   160
                ((Binding.suffix_name "_cases" Abs_name, make @{thm type_definition.Abs_cases}),
wenzelm@33368
   161
                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.cases_type full_tname]),
wenzelm@30345
   162
                ((Binding.suffix_name "_induct" Rep_name, make @{thm type_definition.Rep_induct}),
wenzelm@33368
   163
                  [Rule_Cases.case_names [Binding.name_of Rep_name], Induct.induct_pred full_name]),
wenzelm@30345
   164
                ((Binding.suffix_name "_induct" Abs_name, make @{thm type_definition.Abs_induct}),
wenzelm@33368
   165
                  [Rule_Cases.case_names [Binding.name_of Abs_name], Induct.induct_type full_tname])]
wenzelm@35202
   166
            ||> Sign.restore_naming thy1;
wenzelm@19705
   167
          val info = {rep_type = oldT, abs_type = newT,
wenzelm@19705
   168
            Rep_name = full Rep_name, Abs_name = full Abs_name,
haftmann@28848
   169
              inhabited = inhabited, type_definition = type_definition, set_def = set_def,
wenzelm@19705
   170
              Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse,
wenzelm@19705
   171
              Rep_inject = Rep_inject, Abs_inject = Abs_inject, Rep_cases = Rep_cases,
wenzelm@11822
   172
            Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct};
haftmann@25535
   173
        in
haftmann@25535
   174
          thy2
haftmann@25535
   175
          |> put_info full_tname info
wenzelm@33314
   176
          |> Typedef_Interpretation.data full_tname
haftmann@25535
   177
          |> pair (full_tname, info)
haftmann@25535
   178
        end);
wenzelm@6383
   179
wenzelm@29056
   180
wenzelm@4866
   181
    (* errors *)
wenzelm@4866
   182
wenzelm@4866
   183
    fun show_names pairs = commas_quote (map fst pairs);
wenzelm@4866
   184
wenzelm@4866
   185
    val illegal_vars =
wenzelm@29264
   186
      if null (Term.add_vars set []) andalso null (Term.add_tvars set []) then []
wenzelm@4866
   187
      else ["Illegal schematic variable(s) on rhs"];
wenzelm@4866
   188
wenzelm@4866
   189
    val dup_lhs_tfrees =
wenzelm@18964
   190
      (case duplicates (op =) lhs_tfrees of [] => []
wenzelm@4866
   191
      | dups => ["Duplicate type variables on lhs: " ^ show_names dups]);
wenzelm@4866
   192
wenzelm@4866
   193
    val extra_rhs_tfrees =
wenzelm@17280
   194
      (case fold (remove (op =)) lhs_tfrees rhs_tfrees of [] => []
wenzelm@4866
   195
      | extras => ["Extra type variables on rhs: " ^ show_names extras]);
wenzelm@4866
   196
wenzelm@4866
   197
    val illegal_frees =
wenzelm@29264
   198
      (case Term.add_frees set [] of [] => []
wenzelm@29264
   199
      | xs => ["Illegal variables on rhs: " ^ show_names xs]);
wenzelm@4866
   200
wenzelm@4866
   201
    val errs = illegal_vars @ dup_lhs_tfrees @ extra_rhs_tfrees @ illegal_frees;
wenzelm@11426
   202
    val _ = if null errs then () else error (cat_lines errs);
wenzelm@11426
   203
wenzelm@11426
   204
    (*test theory errors now!*)
wenzelm@29061
   205
    val test_thy = Theory.copy thy;
wenzelm@32970
   206
    val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy;
wenzelm@11426
   207
wenzelm@29062
   208
  in (set, goal, goal_pat, typedef_result) end
wenzelm@30345
   209
  handle ERROR msg =>
wenzelm@30345
   210
    cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
wenzelm@4866
   211
wenzelm@4866
   212
wenzelm@29056
   213
(* add_typedef: tactic interface *)
wenzelm@4866
   214
haftmann@28662
   215
fun add_typedef def opt_name typ set opt_morphs tac thy =
wenzelm@6383
   216
  let
wenzelm@17922
   217
    val name = the_default (#1 typ) opt_name;
wenzelm@29061
   218
    val (set, goal, _, typedef_result) =
haftmann@28662
   219
      prepare_typedef Syntax.check_term def name typ set opt_morphs thy;
wenzelm@29061
   220
    val inhabited = Goal.prove_global thy [] [] goal (K tac)
wenzelm@29061
   221
      handle ERROR msg => cat_error msg
wenzelm@29061
   222
        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
wenzelm@29061
   223
  in typedef_result inhabited thy end;
wenzelm@4866
   224
wenzelm@17339
   225
wenzelm@29056
   226
(* typedef: proof interface *)
wenzelm@6383
   227
wenzelm@17339
   228
local
wenzelm@17339
   229
wenzelm@17339
   230
fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
wenzelm@11822
   231
  let
wenzelm@29062
   232
    val (_, goal, goal_pat, typedef_result) =
wenzelm@13443
   233
      prepare_typedef prep_term def name typ set opt_morphs thy;
wenzelm@21352
   234
    fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
wenzelm@29062
   235
  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end;
wenzelm@17339
   236
wenzelm@17339
   237
in
wenzelm@6383
   238
haftmann@28662
   239
val typedef = gen_typedef Syntax.check_term;
haftmann@28662
   240
val typedef_cmd = gen_typedef Syntax.read_term;
wenzelm@17339
   241
wenzelm@19705
   242
end;
berghofe@15259
   243
berghofe@15259
   244
berghofe@15259
   245
wenzelm@6383
   246
(** outer syntax **)
wenzelm@6383
   247
wenzelm@29056
   248
local structure P = OuterParse in
wenzelm@6383
   249
wenzelm@27353
   250
val _ = OuterKeyword.keyword "morphisms";
wenzelm@24867
   251
wenzelm@24867
   252
val _ =
wenzelm@29056
   253
  OuterSyntax.command "typedef" "HOL type definition (requires non-emptiness proof)"
wenzelm@29056
   254
    OuterKeyword.thy_goal
wenzelm@35202
   255
    (Scan.optional (P.$$$ "(" |--
wenzelm@35202
   256
        ((P.$$$ "open" >> K false) -- Scan.option P.binding ||
wenzelm@35202
   257
          P.binding >> (fn s => (true, SOME s))) --| P.$$$ ")") (true, NONE) --
wenzelm@35351
   258
      (P.type_args -- P.binding) -- P.opt_mixfix -- (P.$$$ "=" |-- P.term) --
wenzelm@35202
   259
      Scan.option (P.$$$ "morphisms" |-- P.!!! (P.binding -- P.binding))
wenzelm@35202
   260
    >> (fn ((((((def, opt_name), (vs, t)), mx), A), morphs)) =>
wenzelm@35202
   261
        Toplevel.print o Toplevel.theory_to_proof
wenzelm@35202
   262
          (typedef_cmd ((def, the_default t opt_name), (t, vs, mx), A, morphs))));
wenzelm@6357
   263
wenzelm@29056
   264
end;
wenzelm@29056
   265
wenzelm@33314
   266
val setup = Typedef_Interpretation.init;
haftmann@25535
   267
wenzelm@4866
   268
end;