src/ZF/Tools/datatype_package.ML
author wenzelm
Mon Nov 19 20:47:57 2001 +0100 (2001-11-19 ago)
changeset 12243 a2c0aaf94460
parent 12226 0474ed2b23aa
child 12876 a70df1e5bf10
permissions -rw-r--r--
tuned;
paulson@6065
     1
(*  Title:      ZF/Tools/datatype_package.ML
paulson@6052
     2
    ID:         $Id$
paulson@6052
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6052
     4
    Copyright   1994  University of Cambridge
paulson@6052
     5
paulson@6065
     6
Datatype/Codatatype Definitions
paulson@6052
     7
paulson@6052
     8
The functor will be instantiated for normal sums/products (datatype defs)
paulson@6052
     9
                         and non-standard sums/products (codatatype defs)
paulson@6052
    10
paulson@6052
    11
Sums are used only for mutual recursion;
paulson@6052
    12
Products are used only to derive "streamlined" induction rules for relations
paulson@6052
    13
*)
paulson@6052
    14
paulson@6052
    15
type datatype_result =
paulson@6052
    16
   {con_defs   : thm list,             (*definitions made in thy*)
paulson@6052
    17
    case_eqns  : thm list,             (*equations for case operator*)
paulson@6052
    18
    recursor_eqns : thm list,          (*equations for the recursor*)
paulson@6052
    19
    free_iffs  : thm list,             (*freeness rewrite rules*)
paulson@6052
    20
    free_SEs   : thm list,             (*freeness destruct rules*)
paulson@6112
    21
    mk_free    : string -> thm};       (*function to make freeness theorems*)
paulson@6052
    22
paulson@6052
    23
signature DATATYPE_ARG =
wenzelm@12183
    24
sig
paulson@6052
    25
  val intrs : thm list
paulson@6052
    26
  val elims : thm list
wenzelm@12183
    27
end;
paulson@6052
    28
paulson@6052
    29
(*Functor's result signature*)
paulson@6052
    30
signature DATATYPE_PACKAGE =
wenzelm@12131
    31
sig
paulson@6052
    32
  (*Insert definitions for the recursive sets, which
paulson@6052
    33
     must *already* be declared as constants in parent theory!*)
wenzelm@12183
    34
  val add_datatype_i: term * term list -> Ind_Syntax.constructor_spec list list ->
wenzelm@12183
    35
    thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
wenzelm@12183
    36
  val add_datatype_x: string * string list -> (string * string list * mixfix) list list ->
wenzelm@12183
    37
    thm list * thm list * thm list -> theory -> theory * inductive_result * datatype_result
wenzelm@12183
    38
  val add_datatype: string * string list -> (string * string list * mixfix) list list ->
wenzelm@12183
    39
    (xstring * Args.src list) list * (xstring * Args.src list) list *
wenzelm@12183
    40
    (xstring * Args.src list) list -> theory -> theory * inductive_result * datatype_result
wenzelm@12131
    41
end;
paulson@6052
    42
wenzelm@12131
    43
functor Add_datatype_def_Fun
wenzelm@12183
    44
 (structure Fp: FP and Pr : PR and CP: CARTPROD and Su : SU
wenzelm@12183
    45
  and Ind_Package : INDUCTIVE_PACKAGE
wenzelm@12183
    46
  and Datatype_Arg : DATATYPE_ARG
wenzelm@12183
    47
  val coind : bool): DATATYPE_PACKAGE =
paulson@6052
    48
struct
paulson@6052
    49
wenzelm@12183
    50
(*con_ty_lists specifies the constructors in the form (name, prems, mixfix) *)
paulson@6052
    51
wenzelm@12183
    52
fun add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy =
paulson@6052
    53
 let
paulson@6052
    54
  val dummy = (*has essential ancestors?*)
paulson@6052
    55
    Theory.requires thy "Datatype" "(co)datatype definitions";
paulson@6052
    56
paulson@6052
    57
  val rec_names = map (#1 o dest_Const o head_of) rec_tms
paulson@6052
    58
  val rec_base_names = map Sign.base_name rec_names
paulson@6052
    59
  val big_rec_base_name = space_implode "_" rec_base_names
paulson@6052
    60
paulson@6052
    61
  val thy_path = thy |> Theory.add_path big_rec_base_name
paulson@6052
    62
  val sign = sign_of thy_path
paulson@6052
    63
paulson@6052
    64
  val big_rec_name = Sign.intern_const sign big_rec_base_name;
paulson@6052
    65
wenzelm@12131
    66
  val intr_tms = Ind_Syntax.mk_all_intr_tms sign (rec_tms, con_ty_lists);
paulson@6052
    67
wenzelm@12131
    68
  val dummy =
wenzelm@12243
    69
    writeln ((if coind then "Codatatype" else "Datatype") ^ " definition " ^ quote big_rec_name);
paulson@6052
    70
paulson@6052
    71
  val case_varname = "f";                (*name for case variables*)
paulson@6052
    72
paulson@6052
    73
  (** Define the constructors **)
paulson@6052
    74
paulson@6052
    75
  (*The empty tuple is 0*)
paulson@6052
    76
  fun mk_tuple [] = Const("0",iT)
wenzelm@7696
    77
    | mk_tuple args = foldr1 (fn (t1, t2) => Pr.pair $ t1 $ t2) args;
paulson@6052
    78
wenzelm@7696
    79
  fun mk_inject n k u = access_bal (fn t => Su.inl $ t, fn t => Su.inr $ t, u) n k;
paulson@6052
    80
paulson@6052
    81
  val npart = length rec_names;  (*number of mutually recursive parts*)
paulson@6052
    82
paulson@6052
    83
paulson@6052
    84
  val full_name = Sign.full_name sign;
paulson@6052
    85
wenzelm@12131
    86
  (*Make constructor definition;
paulson@6052
    87
    kpart is the number of this mutually recursive part*)
wenzelm@12131
    88
  fun mk_con_defs (kpart, con_ty_list) =
paulson@6052
    89
    let val ncon = length con_ty_list    (*number of constructors*)
wenzelm@12131
    90
        fun mk_def (((id,T,syn), name, args, prems), kcon) =
wenzelm@12131
    91
              (*kcon is index of constructor*)
wenzelm@12131
    92
            Logic.mk_defpair (list_comb (Const (full_name name, T), args),
wenzelm@12131
    93
                        mk_inject npart kpart
wenzelm@12131
    94
                        (mk_inject ncon kcon (mk_tuple args)))
paulson@6052
    95
    in  ListPair.map mk_def (con_ty_list, 1 upto ncon)  end;
paulson@6052
    96
paulson@6052
    97
paulson@6052
    98
  (*** Define the case operator ***)
paulson@6052
    99
paulson@6052
   100
  (*Combine split terms using case; yields the case operator for one part*)
wenzelm@12131
   101
  fun call_case case_list =
paulson@6052
   102
    let fun call_f (free,[]) = Abs("null", iT, free)
wenzelm@12131
   103
          | call_f (free,args) =
wenzelm@12131
   104
                CP.ap_split (foldr1 CP.mk_prod (map (#2 o dest_Free) args))
wenzelm@12131
   105
                            Ind_Syntax.iT
wenzelm@12131
   106
                            free
wenzelm@7696
   107
    in  fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_f case_list)  end;
paulson@6052
   108
paulson@6052
   109
  (** Generating function variables for the case definition
paulson@6052
   110
      Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
paulson@6052
   111
paulson@6052
   112
  (*The function variable for a single constructor*)
paulson@6052
   113
  fun add_case (((_, T, _), name, args, _), (opno, cases)) =
paulson@6052
   114
    if Syntax.is_identifier name then
paulson@6052
   115
      (opno, (Free (case_varname ^ "_" ^ name, T), args) :: cases)
paulson@6052
   116
    else
wenzelm@12131
   117
      (opno + 1, (Free (case_varname ^ "_op_" ^ string_of_int opno, T), args)
paulson@6052
   118
       :: cases);
paulson@6052
   119
paulson@6052
   120
  (*Treatment of a list of constructors, for one part
paulson@6052
   121
    Result adds a list of terms, each a function variable with arguments*)
paulson@6052
   122
  fun add_case_list (con_ty_list, (opno, case_lists)) =
paulson@6052
   123
    let val (opno', case_list) = foldr add_case (con_ty_list, (opno, []))
paulson@6052
   124
    in (opno', case_list :: case_lists) end;
paulson@6052
   125
paulson@6052
   126
  (*Treatment of all parts*)
paulson@6052
   127
  val (_, case_lists) = foldr add_case_list (con_ty_lists, (1,[]));
paulson@6052
   128
paulson@6052
   129
  (*extract the types of all the variables*)
paulson@6052
   130
  val case_typ = flat (map (map (#2 o #1)) con_ty_lists) ---> (iT-->iT);
paulson@6052
   131
paulson@6052
   132
  val case_base_name = big_rec_base_name ^ "_case";
paulson@6052
   133
  val case_name = full_name case_base_name;
paulson@6052
   134
paulson@6052
   135
  (*The list of all the function variables*)
paulson@6052
   136
  val case_args = flat (map (map #1) case_lists);
paulson@6052
   137
wenzelm@12131
   138
  val case_const = Const (case_name, case_typ);
paulson@6052
   139
  val case_tm = list_comb (case_const, case_args);
paulson@6052
   140
paulson@6052
   141
  val case_def = Logic.mk_defpair
wenzelm@7696
   142
           (case_tm, fold_bal (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
paulson@6052
   143
paulson@6052
   144
paulson@6052
   145
  (** Generating function variables for the recursor definition
paulson@6052
   146
      Non-identifiers (e.g. infixes) get a name of the form f_op_nnn. **)
paulson@6052
   147
paulson@6052
   148
  (*a recursive call for x is the application rec`x  *)
paulson@6052
   149
  val rec_call = Ind_Syntax.apply_const $ Free ("rec", iT);
paulson@6052
   150
wenzelm@12131
   151
  (*look back down the "case args" (which have been reversed) to
paulson@6052
   152
    determine the de Bruijn index*)
paulson@6052
   153
  fun make_rec_call ([], _) arg = error
wenzelm@12131
   154
          "Internal error in datatype (variable name mismatch)"
wenzelm@12131
   155
    | make_rec_call (a::args, i) arg =
wenzelm@12131
   156
           if a = arg then rec_call $ Bound i
wenzelm@12131
   157
           else make_rec_call (args, i+1) arg;
paulson@6052
   158
paulson@6052
   159
  (*creates one case of the "X_case" definition of the recursor*)
wenzelm@12131
   160
  fun call_recursor ((case_var, case_args), (recursor_var, recursor_args)) =
paulson@6052
   161
      let fun add_abs (Free(a,T), u) = Abs(a,T,u)
wenzelm@12131
   162
          val ncase_args = length case_args
wenzelm@12131
   163
          val bound_args = map Bound ((ncase_args - 1) downto 0)
wenzelm@12131
   164
          val rec_args = map (make_rec_call (rev case_args,0))
wenzelm@12131
   165
                         (List.drop(recursor_args, ncase_args))
paulson@6052
   166
      in
wenzelm@12131
   167
          foldr add_abs
wenzelm@12131
   168
            (case_args, list_comb (recursor_var,
wenzelm@12131
   169
                                   bound_args @ rec_args))
paulson@6052
   170
      end
paulson@6052
   171
paulson@6052
   172
  (*Find each recursive argument and add a recursive call for it*)
paulson@6052
   173
  fun rec_args [] = []
paulson@6052
   174
    | rec_args ((Const("op :",_)$arg$X)::prems) =
paulson@6052
   175
       (case head_of X of
wenzelm@12131
   176
            Const(a,_) => (*recursive occurrence?*)
wenzelm@12131
   177
                          if a mem_string rec_names
wenzelm@12131
   178
                              then arg :: rec_args prems
wenzelm@12131
   179
                          else rec_args prems
wenzelm@12131
   180
          | _ => rec_args prems)
wenzelm@12131
   181
    | rec_args (_::prems) = rec_args prems;
paulson@6052
   182
paulson@6052
   183
  (*Add an argument position for each occurrence of a recursive set.
paulson@6052
   184
    Strictly speaking, the recursive arguments are the LAST of the function
paulson@6052
   185
    variable, but they all have type "i" anyway*)
paulson@6052
   186
  fun add_rec_args args' T = (map (fn _ => iT) args') ---> T
paulson@6052
   187
paulson@6052
   188
  (*Plug in the function variable type needed for the recursor
paulson@6052
   189
    as well as the new arguments (recursive calls)*)
paulson@6052
   190
  fun rec_ty_elem ((id, T, syn), name, args, prems) =
wenzelm@12131
   191
      let val args' = rec_args prems
wenzelm@12131
   192
      in ((id, add_rec_args args' T, syn),
wenzelm@12131
   193
          name, args @ args', prems)
paulson@6052
   194
      end;
paulson@6052
   195
wenzelm@12131
   196
  val rec_ty_lists = (map (map rec_ty_elem) con_ty_lists);
paulson@6052
   197
paulson@6052
   198
  (*Treatment of all parts*)
paulson@6052
   199
  val (_, recursor_lists) = foldr add_case_list (rec_ty_lists, (1,[]));
paulson@6052
   200
paulson@6052
   201
  (*extract the types of all the variables*)
paulson@6052
   202
  val recursor_typ = flat (map (map (#2 o #1)) rec_ty_lists)
wenzelm@12131
   203
                         ---> (iT-->iT);
paulson@6052
   204
paulson@6052
   205
  val recursor_base_name = big_rec_base_name ^ "_rec";
paulson@6052
   206
  val recursor_name = full_name recursor_base_name;
paulson@6052
   207
paulson@6052
   208
  (*The list of all the function variables*)
paulson@6052
   209
  val recursor_args = flat (map (map #1) recursor_lists);
paulson@6052
   210
paulson@6052
   211
  val recursor_tm =
wenzelm@12131
   212
    list_comb (Const (recursor_name, recursor_typ), recursor_args);
paulson@6052
   213
wenzelm@12131
   214
  val recursor_cases = map call_recursor
wenzelm@12131
   215
                         (flat case_lists ~~ flat recursor_lists)
paulson@6052
   216
wenzelm@12131
   217
  val recursor_def =
paulson@6052
   218
      Logic.mk_defpair
wenzelm@12131
   219
        (recursor_tm,
wenzelm@12131
   220
         Ind_Syntax.Vrecursor_const $
wenzelm@12131
   221
           absfree ("rec", iT, list_comb (case_const, recursor_cases)));
paulson@6052
   222
paulson@6052
   223
  (* Build the new theory *)
paulson@6052
   224
wenzelm@12183
   225
  val need_recursor = (not coind andalso recursor_typ <> case_typ);
paulson@6052
   226
wenzelm@12131
   227
  fun add_recursor thy =
paulson@6052
   228
      if need_recursor then
wenzelm@12131
   229
           thy |> Theory.add_consts_i
wenzelm@12131
   230
                    [(recursor_base_name, recursor_typ, NoSyn)]
wenzelm@12131
   231
               |> (#1 o PureThy.add_defs_i false [Thm.no_attributes recursor_def])
paulson@6052
   232
      else thy;
paulson@6052
   233
wenzelm@8438
   234
  val (thy0, con_defs) = thy_path
wenzelm@12131
   235
             |> Theory.add_consts_i
wenzelm@12131
   236
                 ((case_base_name, case_typ, NoSyn) ::
wenzelm@12131
   237
                  map #1 (flat con_ty_lists))
wenzelm@12131
   238
             |> PureThy.add_defs_i false
wenzelm@12131
   239
                 (map Thm.no_attributes
wenzelm@12131
   240
                  (case_def ::
wenzelm@12131
   241
                   flat (ListPair.map mk_con_defs
wenzelm@12131
   242
                         (1 upto npart, con_ty_lists))))
wenzelm@12131
   243
             |>> add_recursor
wenzelm@12131
   244
             |>> Theory.parent_path
paulson@6052
   245
wenzelm@12187
   246
  val intr_names = map #2 (flat con_ty_lists);
wenzelm@12131
   247
  val (thy1, ind_result) =
wenzelm@12187
   248
    thy0 |> Ind_Package.add_inductive_i
wenzelm@12187
   249
      false (rec_tms, dom_sum) (map Thm.no_attributes (intr_names ~~ intr_tms))
wenzelm@12187
   250
      (monos, con_defs, type_intrs @ Datatype_Arg.intrs, type_elims @ Datatype_Arg.elims);
paulson@6052
   251
paulson@6052
   252
  (**** Now prove the datatype theorems in this theory ****)
paulson@6052
   253
paulson@6052
   254
paulson@6052
   255
  (*** Prove the case theorems ***)
paulson@6052
   256
wenzelm@12131
   257
  (*Each equation has the form
paulson@6052
   258
    case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
wenzelm@12131
   259
  fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
paulson@6052
   260
    FOLogic.mk_Trueprop
paulson@6052
   261
      (FOLogic.mk_eq
paulson@6052
   262
       (case_tm $
wenzelm@12131
   263
         (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
wenzelm@12131
   264
                     args)),
wenzelm@12131
   265
        list_comb (case_free, args)));
paulson@6052
   266
paulson@6052
   267
  val case_trans = hd con_defs RS Ind_Syntax.def_trans
paulson@6052
   268
  and split_trans = Pr.split_eq RS meta_eq_to_obj_eq RS trans;
paulson@6052
   269
paulson@6052
   270
  (*Proves a single case equation.  Could use simp_tac, but it's slower!*)
wenzelm@12131
   271
  fun case_tacsf con_def _ =
paulson@6052
   272
    [rewtac con_def,
paulson@6052
   273
     rtac case_trans 1,
wenzelm@12131
   274
     REPEAT (resolve_tac [refl, split_trans,
wenzelm@12131
   275
                          Su.case_inl RS trans,
wenzelm@12131
   276
                          Su.case_inr RS trans] 1)];
paulson@6052
   277
paulson@6052
   278
  fun prove_case_eqn (arg,con_def) =
wenzelm@12131
   279
      prove_goalw_cterm []
wenzelm@12131
   280
        (Ind_Syntax.traceIt "next case equation = "
wenzelm@12131
   281
           (cterm_of (sign_of thy1) (mk_case_eqn arg)))
wenzelm@12131
   282
        (case_tacsf con_def);
paulson@6052
   283
wenzelm@12187
   284
  val free_iffs = map standard (con_defs RL [Ind_Syntax.def_swap_iff]);
paulson@6052
   285
wenzelm@12131
   286
  val case_eqns =
wenzelm@12131
   287
      map prove_case_eqn
wenzelm@12131
   288
         (flat con_ty_lists ~~ case_args ~~ tl con_defs);
paulson@6052
   289
paulson@6052
   290
  (*** Prove the recursor theorems ***)
paulson@6052
   291
paulson@6052
   292
  val recursor_eqns = case try (get_def thy1) recursor_base_name of
paulson@6052
   293
     None => (writeln "  [ No recursion operator ]";
wenzelm@12131
   294
              [])
wenzelm@12131
   295
   | Some recursor_def =>
paulson@6052
   296
      let
wenzelm@12131
   297
        (*Replace subterms rec`x (where rec is a Free var) by recursor_tm(x) *)
wenzelm@12131
   298
        fun subst_rec (Const("op `",_) $ Free _ $ arg) = recursor_tm $ arg
wenzelm@12131
   299
          | subst_rec tm =
wenzelm@12131
   300
              let val (head, args) = strip_comb tm
wenzelm@12131
   301
              in  list_comb (head, map subst_rec args)  end;
paulson@6052
   302
wenzelm@12131
   303
        (*Each equation has the form
wenzelm@12131
   304
          REC(coni(args)) = f_coni(args, REC(rec_arg), ...)
wenzelm@12131
   305
          where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
wenzelm@12131
   306
          constructor argument.*)
wenzelm@12131
   307
        fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
wenzelm@12131
   308
          FOLogic.mk_Trueprop
wenzelm@12131
   309
           (FOLogic.mk_eq
wenzelm@12131
   310
            (recursor_tm $
wenzelm@12131
   311
             (list_comb (Const (Sign.intern_const (sign_of thy1) name,T),
wenzelm@12131
   312
                         args)),
wenzelm@12131
   313
             subst_rec (foldl betapply (recursor_case, args))));
paulson@6052
   314
wenzelm@12131
   315
        val recursor_trans = recursor_def RS def_Vrecursor RS trans;
paulson@6052
   316
wenzelm@12131
   317
        (*Proves a single recursor equation.*)
wenzelm@12131
   318
        fun recursor_tacsf _ =
wenzelm@12131
   319
          [rtac recursor_trans 1,
wenzelm@12131
   320
           simp_tac (rank_ss addsimps case_eqns) 1,
wenzelm@12131
   321
           IF_UNSOLVED (simp_tac (rank_ss addsimps tl con_defs) 1)];
paulson@6052
   322
wenzelm@12131
   323
        fun prove_recursor_eqn arg =
wenzelm@12131
   324
            prove_goalw_cterm []
wenzelm@12131
   325
              (Ind_Syntax.traceIt "next recursor equation = "
wenzelm@12131
   326
                (cterm_of (sign_of thy1) (mk_recursor_eqn arg)))
wenzelm@12131
   327
              recursor_tacsf
paulson@6052
   328
      in
wenzelm@12131
   329
         map prove_recursor_eqn (flat con_ty_lists ~~ recursor_cases)
paulson@6052
   330
      end
paulson@6052
   331
paulson@6052
   332
  val constructors =
paulson@6052
   333
      map (head_of o #1 o Logic.dest_equals o #prop o rep_thm) (tl con_defs);
paulson@6052
   334
wenzelm@12187
   335
  val free_SEs = map standard (Ind_Syntax.mk_free_SEs free_iffs);
paulson@6052
   336
paulson@6154
   337
  val {intrs, elim, induct, mutual_induct, ...} = ind_result
paulson@6052
   338
paulson@6052
   339
  (*Typical theorems have the form ~con1=con2, con1=con2==>False,
paulson@6052
   340
    con1(x)=con1(y) ==> x=y, con1(x)=con1(y) <-> x=y, etc.  *)
paulson@6052
   341
  fun mk_free s =
paulson@6052
   342
      prove_goalw (theory_of_thm elim)   (*Don't use thy1: it will be stale*)
paulson@6052
   343
                  con_defs s
wenzelm@12131
   344
        (fn prems => [cut_facts_tac prems 1,
wenzelm@12131
   345
                      fast_tac (ZF_cs addSEs free_SEs @ Su.free_SEs) 1]);
paulson@6052
   346
paulson@6052
   347
  val simps = case_eqns @ recursor_eqns;
paulson@6052
   348
paulson@6052
   349
  val dt_info =
wenzelm@12131
   350
        {inductive = true,
wenzelm@12131
   351
         constructors = constructors,
wenzelm@12131
   352
         rec_rewrites = recursor_eqns,
wenzelm@12131
   353
         case_rewrites = case_eqns,
wenzelm@12131
   354
         induct = induct,
wenzelm@12131
   355
         mutual_induct = mutual_induct,
wenzelm@12131
   356
         exhaustion = elim};
paulson@6052
   357
paulson@6052
   358
  val con_info =
paulson@6052
   359
        {big_rec_name = big_rec_name,
wenzelm@12131
   360
         constructors = constructors,
paulson@6052
   361
            (*let primrec handle definition by cases*)
wenzelm@12131
   362
         free_iffs = free_iffs,
wenzelm@12131
   363
         rec_rewrites = (case recursor_eqns of
wenzelm@12131
   364
                             [] => case_eqns | _ => recursor_eqns)};
paulson@6052
   365
paulson@6052
   366
  (*associate with each constructor the datatype name and rewrites*)
paulson@6052
   367
  val con_pairs = map (fn c => (#1 (dest_Const c), con_info)) constructors
paulson@6052
   368
paulson@6052
   369
 in
paulson@6052
   370
  (*Updating theory components: simprules and datatype info*)
paulson@6052
   371
  (thy1 |> Theory.add_path big_rec_base_name
wenzelm@12183
   372
        |> (#1 o PureThy.add_thmss
wenzelm@12183
   373
         [(("simps", simps), [Simplifier.simp_add_global]),
wenzelm@12187
   374
          (("", intrs), [Classical.safe_intro_global]),
wenzelm@12187
   375
          (("con_defs", con_defs), []),
wenzelm@12187
   376
          (("case_eqns", case_eqns), []),
wenzelm@12187
   377
          (("recursor_eqns", recursor_eqns), []),
wenzelm@12187
   378
          (("free_iffs", free_iffs), []),
wenzelm@12187
   379
          (("free_elims", free_SEs), [])])
wenzelm@12183
   380
        |> DatatypesData.map (fn tab => Symtab.update ((big_rec_name, dt_info), tab))
wenzelm@12183
   381
        |> ConstructorsData.map (fn tab => foldr Symtab.update (con_pairs, tab))
wenzelm@12131
   382
        |> Theory.parent_path,
paulson@6052
   383
   ind_result,
paulson@6052
   384
   {con_defs = con_defs,
paulson@6052
   385
    case_eqns = case_eqns,
paulson@6052
   386
    recursor_eqns = recursor_eqns,
paulson@6052
   387
    free_iffs = free_iffs,
paulson@6052
   388
    free_SEs = free_SEs,
paulson@6052
   389
    mk_free = mk_free})
paulson@6052
   390
  end;
paulson@6052
   391
paulson@6052
   392
wenzelm@12183
   393
fun add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy =
wenzelm@12183
   394
  let
wenzelm@12183
   395
    val sign = sign_of thy;
wenzelm@12183
   396
    val read_i = Sign.simple_read_term sign Ind_Syntax.iT;
wenzelm@12183
   397
    val rec_tms = map read_i srec_tms;
wenzelm@12183
   398
    val con_ty_lists = Ind_Syntax.read_constructs sign scon_ty_lists
wenzelm@12183
   399
    val dom_sum =
wenzelm@12183
   400
      if sdom = "" then Ind_Syntax.data_domain coind (rec_tms, con_ty_lists)
wenzelm@12183
   401
      else read_i sdom;
wenzelm@12183
   402
  in add_datatype_i (dom_sum, rec_tms) con_ty_lists (monos, type_intrs, type_elims) thy end;
wenzelm@12183
   403
wenzelm@12183
   404
fun add_datatype (sdom, srec_tms) scon_ty_lists (raw_monos, raw_type_intrs, raw_type_elims) thy =
wenzelm@12183
   405
  let
wenzelm@12183
   406
    val (thy', ((monos, type_intrs), type_elims)) = thy
wenzelm@12183
   407
      |> IsarThy.apply_theorems raw_monos
wenzelm@12183
   408
      |>>> IsarThy.apply_theorems raw_type_intrs
wenzelm@12183
   409
      |>>> IsarThy.apply_theorems raw_type_elims;
wenzelm@12183
   410
  in add_datatype_x (sdom, srec_tms) scon_ty_lists (monos, type_intrs, type_elims) thy' end;
wenzelm@12183
   411
wenzelm@12183
   412
wenzelm@12183
   413
(* outer syntax *)
wenzelm@12183
   414
wenzelm@12183
   415
local structure P = OuterParse and K = OuterSyntax.Keyword in
wenzelm@12183
   416
wenzelm@12183
   417
fun mk_datatype ((((dom, dts), monos), type_intrs), type_elims) =
wenzelm@12183
   418
  #1 o add_datatype (dom, map fst dts) (map snd dts) (monos, type_intrs, type_elims);
wenzelm@12183
   419
wenzelm@12183
   420
val con_decl =
wenzelm@12183
   421
  P.name -- Scan.optional (P.$$$ "(" |-- P.list1 P.term --| P.$$$ ")") [] -- P.opt_mixfix
wenzelm@12226
   422
  --| P.marg_comment >> P.triple1;
wenzelm@12183
   423
wenzelm@12183
   424
val datatype_decl =
wenzelm@12226
   425
  (Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<=") |-- P.!!! P.term --| P.marg_comment) "") --
wenzelm@12183
   426
  P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) --
wenzelm@12183
   427
  Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
wenzelm@12183
   428
  Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1 --| P.marg_comment) [] --
wenzelm@12183
   429
  Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1 --| P.marg_comment) []
wenzelm@12183
   430
  >> (Toplevel.theory o mk_datatype);
wenzelm@12183
   431
wenzelm@12183
   432
val coind_prefix = if coind then "co" else "";
wenzelm@12183
   433
wenzelm@12183
   434
val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
wenzelm@12183
   435
  ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
wenzelm@12183
   436
wenzelm@12183
   437
val _ = OuterSyntax.add_parsers [inductiveP];
paulson@6052
   438
paulson@6052
   439
end;
wenzelm@12183
   440
wenzelm@12183
   441
end;