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