src/HOL/Tools/datatype_package.ML
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 6305 4cbdb974220c
child 6360 83573ae0f22c
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (*  Title:      HOL/Tools/datatype_package.ML
     2     ID:         $Id$
     3     Author:     Stefan Berghofer
     4     Copyright   1998  TU Muenchen
     5 
     6 Datatype package for Isabelle/HOL
     7 *)
     8 
     9 signature DATATYPE_PACKAGE =
    10 sig
    11   val quiet_mode : bool ref
    12   val add_datatype : bool -> string list -> (string list * bstring * mixfix *
    13     (bstring * string list * mixfix) list) list -> theory -> theory *
    14       {distinct : thm list list,
    15        inject : thm list list,
    16        exhaustion : thm list,
    17        rec_thms : thm list,
    18        case_thms : thm list list,
    19        split_thms : (thm * thm) list,
    20        induction : thm,
    21        size : thm list,
    22        simps : thm list}
    23   val add_datatype_i : bool -> string list -> (string list * bstring * mixfix *
    24     (bstring * typ list * mixfix) list) list -> theory -> theory *
    25       {distinct : thm list list,
    26        inject : thm list list,
    27        exhaustion : thm list,
    28        rec_thms : thm list,
    29        case_thms : thm list list,
    30        split_thms : (thm * thm) list,
    31        induction : thm,
    32        size : thm list,
    33        simps : thm list}
    34   val rep_datatype : string list option -> thm list list ->
    35     thm list list -> thm -> theory -> theory *
    36       {distinct : thm list list,
    37        inject : thm list list,
    38        exhaustion : thm list,
    39        rec_thms : thm list,
    40        case_thms : thm list list,
    41        split_thms : (thm * thm) list,
    42        induction : thm,
    43        size : thm list,
    44        simps : thm list}
    45   val setup: (theory -> theory) list
    46   val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
    47   val datatype_info_sg : Sign.sg -> string -> DatatypeAux.datatype_info
    48   val datatype_info : theory -> string -> DatatypeAux.datatype_info
    49   val constrs_of : theory -> string -> term list option
    50   val case_const_of : theory -> string -> term option
    51   val mutual_induct_tac : string list -> int -> tactic
    52   val induct_tac : string -> int -> tactic
    53   val exhaust_tac : string -> int -> tactic
    54 end;
    55 
    56 structure DatatypePackage : DATATYPE_PACKAGE =
    57 struct
    58 
    59 open DatatypeAux;
    60 
    61 val quiet_mode = quiet_mode;
    62 
    63 (* data kind 'HOL/datatypes' *)
    64 
    65 structure DatatypesArgs =
    66 struct
    67   val name = "HOL/datatypes";
    68   type T = datatype_info Symtab.table;
    69 
    70   val empty = Symtab.empty;
    71   val prep_ext = I;
    72   val merge: T * T -> T = Symtab.merge (K true);
    73 
    74   fun print sg tab =
    75     Pretty.writeln (Pretty.strs ("datatypes:" ::
    76       map (Sign.cond_extern sg Sign.typeK o fst) (Symtab.dest tab)));
    77 end;
    78 
    79 structure DatatypesData = TheoryDataFun(DatatypesArgs);
    80 val get_datatypes_sg = DatatypesData.get_sg;
    81 val get_datatypes = DatatypesData.get;
    82 val put_datatypes = DatatypesData.put;
    83 
    84 (* setup *)
    85 
    86 val setup = [DatatypesData.init];
    87 
    88 (** theory information about datatypes **)
    89 
    90 fun datatype_info_sg sg name =
    91   (case Symtab.lookup (get_datatypes_sg sg, name) of
    92     Some info => info
    93   | None => error ("Unknown datatype " ^ quote name));
    94 
    95 val datatype_info = datatype_info_sg o sign_of;
    96 
    97 fun constrs_of thy tname =
    98   let
    99     val {index, descr, ...} = datatype_info thy tname;
   100     val (_, _, constrs) = the (assoc (descr, index))
   101   in
   102     Some (map (fn (cname, _) =>
   103       Const (cname, the (Sign.const_type (sign_of thy) cname))) constrs)
   104   end handle _ => None;
   105 
   106 fun case_const_of thy tname =
   107   let
   108     val {case_name, ...} = datatype_info thy tname;
   109   in
   110     Some (Const (case_name, the (Sign.const_type (sign_of thy) case_name)))
   111   end handle _ => None;
   112 
   113 fun find_tname var Bi =
   114   let val frees = map dest_Free (term_frees Bi)
   115       val params = Logic.strip_params Bi;
   116   in case assoc (frees @ params, var) of
   117        None => error ("No such variable in subgoal: " ^ quote var)
   118      | Some(Type (tn, _)) => tn
   119      | _ => error ("Cannot determine type of " ^ quote var)
   120   end;
   121 
   122 fun infer_tname state sign i aterm =
   123   let
   124     val (_, _, Bi, _) = dest_state (state, i)
   125     val params = Logic.strip_params Bi;   (*params of subgoal i*)
   126     val params = rev (rename_wrt_term Bi params);   (*as they are printed*)
   127     val (types, sorts) = types_sorts state;
   128     fun types' (a, ~1) = (case assoc (params, a) of None => types(a, ~1) | sm => sm)
   129       | types' ixn = types ixn;
   130     val (ct, _) = read_def_cterm (sign, types', sorts) [] false
   131                                   (aterm, TVar (("", 0), []));
   132   in case #T (rep_cterm ct) of
   133        Type (tn, _) => tn
   134      | _ => error ("Cannot determine type of " ^ quote aterm)
   135   end;
   136 
   137 (*Warn if the (induction) variable occurs Free among the premises, which
   138   usually signals a mistake.  But calls the tactic either way!*)
   139 fun occs_in_prems tacf vars = 
   140   SUBGOAL (fn (Bi, i) =>
   141 	   (if  exists (fn Free (a, _) => a mem vars)
   142 	              (foldr add_term_frees (#2 (strip_context Bi), []))
   143 	     then warning "Induction variable occurs also among premises!"
   144 	     else ();
   145 	    tacf i));
   146 
   147 (* generic induction tactic for datatypes *)
   148 
   149 fun mutual_induct_tac vars i state =
   150   let
   151     val (_, _, Bi, _) = dest_state (state, i);
   152     val {sign, ...} = rep_thm state;
   153     val tn = find_tname (hd vars) Bi;
   154     val {induction, ...} = datatype_info_sg sign tn;
   155     val ind_vnames = map (fn (_ $ Var (ixn, _)) =>
   156       implode (tl (explode (Syntax.string_of_vname ixn))))
   157         (dest_conj (HOLogic.dest_Trueprop (concl_of induction)));
   158     val insts = (ind_vnames ~~ vars) handle _ =>
   159       error ("Induction rule for type " ^ tn ^ " has different number of variables")
   160   in
   161     occs_in_prems (res_inst_tac insts induction) vars i state
   162   end;
   163 
   164 fun induct_tac var = mutual_induct_tac [var];
   165 
   166 (* generic exhaustion tactic for datatypes *)
   167 
   168 fun exhaust_tac aterm i state =
   169   let
   170     val {sign, ...} = rep_thm state;
   171     val tn = infer_tname state sign i aterm;
   172     val {exhaustion, ...} = datatype_info_sg sign tn;
   173     val _ $ Var (ixn, _) $ _ = HOLogic.dest_Trueprop
   174       (hd (Logic.strip_assums_hyp (hd (prems_of exhaustion))));
   175     val exh_vname = implode (tl (explode (Syntax.string_of_vname ixn)))
   176   in
   177     res_inst_tac [(exh_vname, aterm)] exhaustion i state
   178   end;
   179 
   180 
   181 (* prepare types *)
   182 
   183 fun read_typ sign ((Ts, sorts), str) =
   184   let
   185     val T = Type.no_tvars (Sign.read_typ (sign, (curry assoc)
   186       (map (apfst (rpair ~1)) sorts)) str) handle TYPE (msg, _, _) => error msg
   187   in (Ts @ [T], add_typ_tfrees (T, sorts)) end;
   188 
   189 fun cert_typ sign ((Ts, sorts), raw_T) =
   190   let
   191     val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
   192       TYPE (msg, _, _) => error msg;
   193     val sorts' = add_typ_tfrees (T, sorts)
   194   in (Ts @ [T],
   195       case duplicates (map fst sorts') of
   196          [] => sorts'
   197        | dups => error ("Inconsistent sort constraints for " ^ commas dups))
   198   end;
   199 
   200 
   201 (**** make datatype info ****)
   202 
   203 fun make_dt_info descr induct reccomb_names rec_thms
   204   ((((((((i, (_, (tname, _, _))), case_name), case_thms),
   205     exhaustion_thm), distinct_thm), inject), nchotomy), case_cong) = (tname,
   206       {index = i,
   207        descr = descr,
   208        rec_names = reccomb_names,
   209        rec_rewrites = rec_thms,
   210        case_name = case_name,
   211        case_rewrites = case_thms,
   212        induction = induct,
   213        exhaustion = exhaustion_thm,
   214        distinct = distinct_thm,
   215        inject = inject,
   216        nchotomy = nchotomy,
   217        case_cong = case_cong});
   218 
   219 fun store_clasimp thy (cla, simp) =
   220   (claset_ref_of thy := cla; simpset_ref_of thy := simp);
   221 
   222 infix 4 addDistinct;
   223 
   224 fun clasimp addDistinct ([], _) = clasimp
   225   | clasimp addDistinct (thms::thmss, (_, (_, _, constrs))::descr) =
   226       if length constrs < DatatypeProp.dtK then
   227         clasimp addIffs thms addDistinct (thmss, descr)
   228       else
   229         clasimp addsimps2 thms addDistinct (thmss, descr);
   230 
   231 
   232 (********************* axiomatic introduction of datatypes ********************)
   233 
   234 fun add_and_get_axioms label tnames ts thy =
   235   foldr (fn ((tname, t), (thy', axs)) =>
   236     let
   237       val thy'' = thy' |>
   238         Theory.add_path tname |>
   239         PureThy.add_axioms_i [((label, t), [])];
   240       val ax = get_axiom thy'' label
   241     in (Theory.parent_path thy'', ax::axs)
   242     end) (tnames ~~ ts, (thy, []));
   243 
   244 fun add_and_get_axiomss label tnames tss thy =
   245   foldr (fn ((tname, ts), (thy', axss)) =>
   246     let
   247       val thy'' = thy' |>
   248         Theory.add_path tname |>
   249         PureThy.add_axiomss_i [((label, ts), [])];
   250       val axs = PureThy.get_thms thy'' label
   251     in (Theory.parent_path thy'', axs::axss)
   252     end) (tnames ~~ tss, (thy, []));
   253 
   254 fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   255   let
   256     val descr' = flat descr;
   257     val recTs = get_rec_types descr' sorts;
   258     val used = foldr add_typ_tfree_names (recTs, []);
   259     val newTs = take (length (hd descr), recTs);
   260 
   261     val _ = message ("Adding axioms for datatype(s) " ^ commas new_type_names);
   262 
   263     (**** declare new types and constants ****)
   264 
   265     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   266 
   267     val constr_decls = map (fn (((_, (_, _, constrs)), T), constr_syntax') =>
   268       map (fn ((_, cargs), (cname, mx)) =>
   269         (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
   270           (constrs ~~ constr_syntax')) ((hd descr) ~~ newTs ~~ constr_syntax);
   271 
   272     val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
   273       replicate (length descr') HOLogic.termS);
   274 
   275     val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
   276       map (fn (_, cargs) =>
   277         let
   278           val recs = filter is_rec_type cargs;
   279           val argTs = (map (typ_of_dtyp descr' sorts) cargs) @
   280             (map (fn r => nth_elem (dest_DtRec r, rec_result_Ts)) recs)
   281         in argTs ---> nth_elem (i, rec_result_Ts)
   282         end) constrs) descr');
   283 
   284     val big_reccomb_name = (space_implode "_" new_type_names) ^ "_rec";
   285     val reccomb_names = if length descr' = 1 then [big_reccomb_name] else
   286       (map ((curry (op ^) (big_reccomb_name ^ "_")) o string_of_int)
   287         (1 upto (length descr')));
   288 
   289     val big_size_name = space_implode "_" new_type_names ^ "_size";
   290     val size_names = if length (flat (tl descr)) = 1 then [big_size_name] else
   291       map (fn i => big_size_name ^ "_" ^ string_of_int i)
   292         (1 upto length (flat (tl descr)));
   293 
   294     val freeT = TFree (variant used "'t", HOLogic.termS);
   295     val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
   296       map (fn (_, cargs) =>
   297         let val Ts = map (typ_of_dtyp descr' sorts) cargs
   298         in Ts ---> freeT end) constrs) (hd descr);
   299 
   300     val case_names = map (fn s => (s ^ "_case")) new_type_names;
   301 
   302     val thy2' = thy |>
   303 
   304       (** new types **)
   305 
   306       curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
   307         PureThy.add_typedecls [(name, tvs, mx)] |>
   308         Theory.add_arities_i
   309           [(Sign.full_name (sign_of thy') (Syntax.type_name name mx),
   310             replicate (length tvs) HOLogic.termS, HOLogic.termS)]))
   311               (types_syntax ~~ tyvars) |>
   312 
   313       add_path flat_names (space_implode "_" new_type_names) |>
   314 
   315       (** primrec combinators **)
   316 
   317       Theory.add_consts_i (map (fn ((name, T), T') =>
   318         (name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
   319           (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
   320 
   321       (** case combinators **)
   322 
   323       Theory.add_consts_i (map (fn ((name, T), Ts) =>
   324         (name, Ts @ [T] ---> freeT, NoSyn))
   325           (case_names ~~ newTs ~~ case_fn_Ts)) |>
   326       Theory.add_trrules_i (DatatypeProp.make_case_trrules new_type_names descr);
   327 
   328     val reccomb_names' = map (Sign.intern_const (sign_of thy2')) reccomb_names;
   329     val case_names' = map (Sign.intern_const (sign_of thy2')) case_names;
   330 
   331     val thy2 = thy2' |>
   332 
   333       (** t_ord functions **)
   334 
   335       Theory.add_consts_i
   336         (foldr (fn ((((_, (_, _, constrs)), tname), T), decls) =>
   337           if length constrs < DatatypeProp.dtK then decls
   338           else (tname ^ "_ord", T --> HOLogic.natT, NoSyn)::decls)
   339             ((hd descr) ~~ new_type_names ~~ newTs, [])) |>
   340 
   341       (** size functions **)
   342 
   343       Theory.add_consts_i (map (fn (s, T) =>
   344         (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   345           (size_names ~~ drop (length (hd descr), recTs))) |>
   346 
   347       (** constructors **)
   348 
   349       parent_path flat_names |>
   350       curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
   351         constr_syntax'), thy') => thy' |>
   352           add_path flat_names tname |>
   353             Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
   354               (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
   355                 (constrs ~~ constr_syntax')) |>
   356           parent_path flat_names))
   357             (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax);
   358 
   359     (**** introduction of axioms ****)
   360 
   361     val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
   362     val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
   363 
   364     val (thy3, inject) = thy2 |>
   365       Theory.add_path (space_implode "_" new_type_names) |>
   366       PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
   367       PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
   368       PureThy.add_axiomss_i [(("size", size_axs), [])] |>
   369       Theory.parent_path |>
   370       add_and_get_axiomss "inject" new_type_names
   371         (DatatypeProp.make_injs descr sorts);
   372     val induct = get_axiom thy3 "induct";
   373     val rec_thms = get_thms thy3 "recs";
   374     val size_thms = get_thms thy3 "size";
   375     val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
   376       (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   377     val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
   378       (DatatypeProp.make_casedists descr sorts) thy4;
   379     val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
   380       (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   381     val (split_ts, split_asm_ts) = ListPair.unzip
   382       (DatatypeProp.make_splits new_type_names descr sorts thy6);
   383     val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
   384     val (thy8, split_asm) = add_and_get_axioms "split_asm" new_type_names
   385       split_asm_ts thy7;
   386     val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
   387       (DatatypeProp.make_nchotomys descr sorts) thy8;
   388     val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
   389       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   390     
   391     val dt_infos = map (make_dt_info descr' induct reccomb_names' rec_thms)
   392       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names' ~~ case_thms ~~
   393         exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   394 
   395     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   396 
   397     val thy11 = thy10 |>
   398       Theory.add_path (space_implode "_" new_type_names) |>
   399       PureThy.add_thmss [(("simps", simps), [])] |>
   400       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   401       Theory.parent_path;
   402 
   403     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   404       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   405       addIffs flat inject addDistinct (distinct, hd descr));
   406 
   407   in
   408     (thy11,
   409      {distinct = distinct,
   410       inject = inject,
   411       exhaustion = exhaustion,
   412       rec_thms = rec_thms,
   413       case_thms = case_thms,
   414       split_thms = split ~~ split_asm,
   415       induction = induct,
   416       size = size_thms,
   417       simps = simps})
   418   end;
   419 
   420 
   421 (******************* definitional introduction of datatypes *******************)
   422 
   423 fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   424   let
   425     val _ = message ("Proofs for datatype(s) " ^ commas new_type_names);
   426 
   427     val (thy2, inject, dist_rewrites, induct) = thy |>
   428       DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   429         types_syntax constr_syntax;
   430 
   431     val (thy3, casedist_thms) =
   432       DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
   433     val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   434       flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
   435     val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   436       flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   437     val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
   438       flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
   439     val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
   440       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   441     val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   442       descr sorts casedist_thms thy7;
   443     val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   444       descr sorts nchotomys case_thms thy8;
   445     val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
   446       descr sorts reccomb_names rec_thms thy9;
   447 
   448     val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
   449       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   450         casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   451 
   452     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   453 
   454     val thy11 = thy10 |>
   455       Theory.add_path (space_implode "_" new_type_names) |>
   456       PureThy.add_thmss [(("simps", simps), [])] |>
   457       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   458       Theory.parent_path;
   459 
   460     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   461       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   462       addIffs flat inject addDistinct (distinct, hd descr));
   463 
   464   in
   465     (thy11,
   466      {distinct = distinct,
   467       inject = inject,
   468       exhaustion = casedist_thms,
   469       rec_thms = rec_thms,
   470       case_thms = case_thms,
   471       split_thms = split_thms,
   472       induction = induct,
   473       size = size_thms,
   474       simps = simps})
   475   end;
   476 
   477 
   478 (*********************** declare non-datatype as datatype *********************)
   479 
   480 fun rep_datatype alt_names distinct inject induction thy =
   481   let
   482     val sign = sign_of thy;
   483 
   484     val induction' = freezeT induction;
   485 
   486     fun err t = error ("Ill-formed predicate in induction rule: " ^
   487       Sign.string_of_term sign t);
   488 
   489     fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
   490           ((tname, map dest_TFree Ts) handle _ => err t)
   491       | get_typ t = err t;
   492 
   493     val dtnames = map get_typ (dest_conj (HOLogic.dest_Trueprop (concl_of induction')));
   494     val new_type_names = if_none alt_names (map fst dtnames);
   495 
   496     fun get_constr t = (case Logic.strip_assums_concl t of
   497         _ $ (_ $ t') => (case head_of t' of
   498             Const (cname, cT) => (case strip_type cT of
   499                 (Ts, Type (tname, _)) => (tname, (cname, map (dtyp_of_typ dtnames) Ts))
   500               | _ => err t)
   501           | _ => err t)
   502       | _ => err t);
   503 
   504     fun make_dt_spec [] _ _ = []
   505       | make_dt_spec ((tname, tvs)::dtnames') i constrs =
   506           let val (constrs', constrs'') = take_prefix (equal tname o fst) constrs
   507           in (i, (tname, map DtTFree tvs, map snd constrs'))::
   508             (make_dt_spec dtnames' (i + 1) constrs'')
   509           end;
   510 
   511     val descr = make_dt_spec dtnames 0 (map get_constr (prems_of induction'));
   512     val sorts = add_term_tfrees (concl_of induction', []);
   513     val dt_info = get_datatypes thy;
   514 
   515     val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
   516 
   517     val (thy2, casedist_thms) = thy |>
   518       DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
   519     val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   520       false new_type_names [descr] sorts dt_info inject distinct induction thy2;
   521     val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
   522       new_type_names [descr] sorts reccomb_names rec_thms thy3;
   523     val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
   524       new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   525     val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   526       [descr] sorts casedist_thms thy5;
   527     val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   528       [descr] sorts nchotomys case_thms thy6;
   529     val (thy8, size_thms) =
   530       if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
   531         DatatypeAbsProofs.prove_size_thms false new_type_names
   532           [descr] sorts reccomb_names rec_thms thy7
   533       else (thy7, []);
   534 
   535     val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
   536       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
   537         casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   538 
   539     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   540 
   541     val thy9 = thy8 |>
   542       Theory.add_path (space_implode "_" new_type_names) |>
   543       PureThy.add_thmss [(("simps", simps), [])] |>
   544       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   545       Theory.parent_path;
   546 
   547     val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
   548       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   549       addIffs flat inject addDistinct (distinct, descr));
   550 
   551   in
   552     (thy9,
   553      {distinct = distinct,
   554       inject = inject,
   555       exhaustion = casedist_thms,
   556       rec_thms = rec_thms,
   557       case_thms = case_thms,
   558       split_thms = split_thms,
   559       induction = induction,
   560       size = size_thms,
   561       simps = simps})
   562   end;
   563 
   564 
   565 (******************************** add datatype ********************************)
   566 
   567 fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
   568   let
   569     val _ = Theory.requires thy "Datatype" "datatype definitions";
   570 
   571     (* this theory is used just for parsing *)
   572 
   573     val tmp_thy = thy |>
   574       Theory.copy |>
   575       Theory.add_types (map (fn (tvs, tname, mx, _) =>
   576         (tname, length tvs, mx)) dts);
   577 
   578     val sign = sign_of tmp_thy;
   579 
   580     val (tyvars, _, _, _)::_ = dts;
   581     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   582       let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
   583       in (case duplicates tvs of
   584             [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
   585                   else error ("Mutually recursive datatypes must have same type parameters")
   586           | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
   587               " : " ^ commas dups))
   588       end) dts);
   589 
   590     val _ = (case duplicates (map fst new_dts) @ duplicates new_type_names of
   591       [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   592 
   593     fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
   594       let
   595         fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   596           let
   597             val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
   598             val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
   599                 [] => ()
   600               | vs => error ("Extra type variables on rhs: " ^ commas vs))
   601           in (constrs @ [((if flat_names then Sign.full_name sign else
   602                 Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
   603                    map (dtyp_of_typ new_dts) cargs')],
   604               constr_syntax' @ [(cname, mx')], sorts'')
   605           end handle ERROR =>
   606             error ("The error above occured in constructor " ^ cname ^
   607               " of datatype " ^ tname);
   608 
   609         val (constrs', constr_syntax', sorts') =
   610           foldl prep_constr (([], [], sorts), constrs)
   611 
   612       in 
   613         case duplicates (map fst constrs') of
   614            [] =>
   615              (dts' @ [(i, (Sign.full_name sign (Syntax.type_name tname mx),
   616                 map DtTFree tvs, constrs'))],
   617               constr_syntax @ [constr_syntax'], sorts', i + 1)
   618          | dups => error ("Duplicate constructors " ^ commas dups ^
   619              " in datatype " ^ tname)
   620       end;
   621 
   622     val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
   623     val dt_info = get_datatypes thy;
   624     val (descr, _) = unfold_datatypes dt_info dts' i;
   625     val _ = check_nonempty descr;
   626     val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   627 
   628   in
   629     (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   630       flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
   631   end;
   632 
   633 val add_datatype_i = gen_add_datatype cert_typ;
   634 val add_datatype = gen_add_datatype read_typ;
   635 
   636 end;
   637 
   638 val induct_tac = DatatypePackage.induct_tac;
   639 val mutual_induct_tac = DatatypePackage.mutual_induct_tac;
   640 val exhaust_tac = DatatypePackage.exhaust_tac;