src/HOL/Tools/datatype_package.ML
changeset 5661 6ecb6ea25f19
parent 5578 7de426cf179c
child 5663 aad79a127628
equal deleted inserted replaced
5660:f2c5354cd32f 5661:6ecb6ea25f19
     6 Datatype package for Isabelle/HOL
     6 Datatype package for Isabelle/HOL
     7 *)
     7 *)
     8 
     8 
     9 signature DATATYPE_PACKAGE =
     9 signature DATATYPE_PACKAGE =
    10 sig
    10 sig
    11   val add_datatype : string list -> (string list * bstring * mixfix *
    11   val quiet_mode : bool ref
    12     (bstring * mixfix * string list) list) list -> theory -> theory *
    12   val add_datatype : bool -> string list -> (string list * bstring * mixfix *
       
    13     (bstring * string list * mixfix) list) list -> theory -> theory *
    13       {distinct : thm list list,
    14       {distinct : thm list list,
    14        inject : thm list list,
    15        inject : thm list list,
    15        exhaustion : thm list,
    16        exhaustion : thm list,
    16        rec_thms : thm list,
    17        rec_thms : thm list,
    17        case_thms : thm list list,
    18        case_thms : thm list list,
    18        split_thms : (thm * thm) list,
    19        split_thms : (thm * thm) list,
    19        induction : thm,
    20        induction : thm,
    20        size : thm list,
    21        size : thm list,
    21        simps : thm list}
    22        simps : thm list}
    22   val add_datatype_i : string list -> (string list * bstring * mixfix *
    23   val add_datatype_i : bool -> string list -> (string list * bstring * mixfix *
    23     (bstring * mixfix * typ list) list) list -> theory -> theory *
    24     (bstring * typ list * mixfix) list) list -> theory -> theory *
    24       {distinct : thm list list,
    25       {distinct : thm list list,
    25        inject : thm list list,
    26        inject : thm list list,
    26        exhaustion : thm list,
    27        exhaustion : thm list,
    27        rec_thms : thm list,
    28        rec_thms : thm list,
    28        case_thms : thm list list,
    29        case_thms : thm list list,
    55 structure DatatypePackage : DATATYPE_PACKAGE =
    56 structure DatatypePackage : DATATYPE_PACKAGE =
    56 struct
    57 struct
    57 
    58 
    58 open DatatypeAux;
    59 open DatatypeAux;
    59 
    60 
       
    61 val quiet_mode = quiet_mode;
       
    62 
    60 (* data kind 'HOL/datatypes' *)
    63 (* data kind 'HOL/datatypes' *)
    61 
    64 
    62 structure DatatypesArgs =
    65 structure DatatypesArgs =
    63 struct
    66 struct
    64   val name = "HOL/datatypes";
    67   val name = "HOL/datatypes";
   230 
   233 
   231 fun add_and_get_axioms label tnames ts thy =
   234 fun add_and_get_axioms label tnames ts thy =
   232   foldr (fn ((tname, t), (thy', axs)) =>
   235   foldr (fn ((tname, t), (thy', axs)) =>
   233     let
   236     let
   234       val thy'' = thy' |>
   237       val thy'' = thy' |>
   235         (if length tnames = 1 then I else Theory.add_path tname) |>
   238         Theory.add_path tname |>
   236         PureThy.add_axioms_i [((label, t), [])];
   239         PureThy.add_axioms_i [((label, t), [])];
   237       val ax = get_axiom thy'' label
   240       val ax = get_axiom thy'' label
   238     in (if length tnames = 1 then thy'' else Theory.parent_path thy'', ax::axs)
   241     in (Theory.parent_path thy'', ax::axs)
   239     end) (tnames ~~ ts, (thy, []));
   242     end) (tnames ~~ ts, (thy, []));
   240 
   243 
   241 fun add_and_get_axiomss label tnames tss thy =
   244 fun add_and_get_axiomss label tnames tss thy =
   242   foldr (fn ((tname, ts), (thy', axss)) =>
   245   foldr (fn ((tname, ts), (thy', axss)) =>
   243     let
   246     let
   244       val thy'' = thy' |>
   247       val thy'' = thy' |>
   245         (if length tnames = 1 then I else Theory.add_path tname) |>
   248         Theory.add_path tname |>
   246         PureThy.add_axiomss_i [((label, ts), [])];
   249         PureThy.add_axiomss_i [((label, ts), [])];
   247       val axs = PureThy.get_thms thy'' label
   250       val axs = PureThy.get_thms thy'' label
   248     in (if length tnames = 1 then thy'' else Theory.parent_path thy'', axs::axss)
   251     in (Theory.parent_path thy'', axs::axss)
   249     end) (tnames ~~ tss, (thy, []));
   252     end) (tnames ~~ tss, (thy, []));
   250 
   253 
   251 fun add_datatype_axm new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   254 fun add_datatype_axm flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   252   let
   255   let
   253     val descr' = flat descr;
   256     val descr' = flat descr;
   254     val recTs = get_rec_types descr' sorts;
   257     val recTs = get_rec_types descr' sorts;
   255     val used = foldr add_typ_tfree_names (recTs, []);
   258     val used = foldr add_typ_tfree_names (recTs, []);
   256     val newTs = take (length (hd descr), recTs);
   259     val newTs = take (length (hd descr), recTs);
   257 
   260 
   258     val _ = writeln ("Adding axioms for datatype(s) " ^ commas new_type_names);
   261     val _ = message ("Adding axioms for datatype(s) " ^ commas new_type_names);
   259 
   262 
   260     (**** declare new types and constants ****)
   263     (**** declare new types and constants ****)
   261 
   264 
   262     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   265     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);
   263 
   266 
   296 
   299 
   297     val case_names = map (fn s => (s ^ "_case")) new_type_names;
   300     val case_names = map (fn s => (s ^ "_case")) new_type_names;
   298 
   301 
   299     val thy2 = thy |>
   302     val thy2 = thy |>
   300 
   303 
   301       Theory.add_path (space_implode "_" new_type_names) |>
       
   302 
       
   303       (** new types **)
   304       (** new types **)
   304 
   305 
   305       curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
   306       curry (foldr (fn (((name, mx), tvs), thy') => thy' |>
   306         PureThy.add_typedecls [(name, tvs, mx)] |>
   307         PureThy.add_typedecls [(name, tvs, mx)] |>
   307         Theory.add_arities_i
   308         Theory.add_arities_i
   308           [(Sign.full_name (sign_of thy') (Syntax.type_name name mx),
   309           [(Sign.full_name (sign_of thy') (Syntax.type_name name mx),
   309             replicate (length tvs) HOLogic.termS, HOLogic.termS)]))
   310             replicate (length tvs) HOLogic.termS, HOLogic.termS)]))
   310               (types_syntax ~~ tyvars) |>
   311               (types_syntax ~~ tyvars) |>
   311 
   312 
   312       (** constructors **)
   313       add_path flat_names (space_implode "_" new_type_names) |>
   313 
       
   314       curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
       
   315         constr_syntax'), thy') => thy' |>
       
   316           (if length newTs = 1 then I else Theory.add_path tname) |>
       
   317             Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
       
   318               (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
       
   319                 (constrs ~~ constr_syntax')) |>
       
   320           (if length newTs = 1 then I else Theory.parent_path)))
       
   321             (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax) |>
       
   322 
   314 
   323       (** primrec combinators **)
   315       (** primrec combinators **)
   324 
   316 
   325       Theory.add_consts_i (map (fn ((name, T), T') =>
   317       Theory.add_consts_i (map (fn ((name, T), T') =>
   326         (name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
   318         (name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
   343 
   335 
   344       (** size functions **)
   336       (** size functions **)
   345 
   337 
   346       Theory.add_consts_i (map (fn (s, T) =>
   338       Theory.add_consts_i (map (fn (s, T) =>
   347         (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   339         (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   348           (size_names ~~ drop (length (hd descr), recTs)));
   340           (size_names ~~ drop (length (hd descr), recTs))) |>
       
   341 
       
   342       (** constructors **)
       
   343 
       
   344       parent_path flat_names |>
       
   345       curry (foldr (fn (((((_, (_, _, constrs)), T), tname),
       
   346         constr_syntax'), thy') => thy' |>
       
   347           add_path flat_names tname |>
       
   348             Theory.add_consts_i (map (fn ((_, cargs), (cname, mx)) =>
       
   349               (cname, map (typ_of_dtyp descr' sorts) cargs ---> T, mx))
       
   350                 (constrs ~~ constr_syntax')) |>
       
   351           parent_path flat_names))
       
   352             (hd descr ~~ newTs ~~ new_type_names ~~ constr_syntax);
   349 
   353 
   350     (**** introduction of axioms ****)
   354     (**** introduction of axioms ****)
   351 
   355 
       
   356     val rec_axs = DatatypeProp.make_primrecs new_type_names descr sorts thy2;
       
   357     val size_axs = DatatypeProp.make_size new_type_names descr sorts thy2;
       
   358 
   352     val (thy3, inject) = thy2 |>
   359     val (thy3, inject) = thy2 |>
       
   360       Theory.add_path (space_implode "_" new_type_names) |>
   353       PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
   361       PureThy.add_axioms_i [(("induct", DatatypeProp.make_ind descr sorts), [])] |>
       
   362       PureThy.add_axiomss_i [(("recs", rec_axs), [])] |>
       
   363       PureThy.add_axiomss_i [(("size", size_axs), [])] |>
       
   364       Theory.parent_path |>
   354       add_and_get_axiomss "inject" new_type_names
   365       add_and_get_axiomss "inject" new_type_names
   355         (DatatypeProp.make_injs descr sorts);
   366         (DatatypeProp.make_injs descr sorts);
       
   367     val induct = get_axiom thy3 "induct";
       
   368     val rec_thms = get_thms thy3 "recs";
       
   369     val size_thms = get_thms thy3 "size";
   356     val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
   370     val (thy4, distinct) = add_and_get_axiomss "distinct" new_type_names
   357       (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   371       (DatatypeProp.make_distincts new_type_names descr sorts thy3) thy3;
   358     val induct = get_axiom thy4 "induct";
       
   359 
       
   360     val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
   372     val (thy5, exhaustion) = add_and_get_axioms "exhaust" new_type_names
   361       (DatatypeProp.make_casedists descr sorts) (PureThy.add_axiomss_i [(("recs",
   373       (DatatypeProp.make_casedists descr sorts) thy4;
   362         DatatypeProp.make_primrecs new_type_names descr sorts thy4), [])] thy4);
       
   363     val rec_thms = get_thms thy5 "recs";
       
   364     val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
   374     val (thy6, case_thms) = add_and_get_axiomss "cases" new_type_names
   365       (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   375       (DatatypeProp.make_cases new_type_names descr sorts thy5) thy5;
   366     val (split_ts, split_asm_ts) = ListPair.unzip
   376     val (split_ts, split_asm_ts) = ListPair.unzip
   367       (DatatypeProp.make_splits new_type_names descr sorts thy6);
   377       (DatatypeProp.make_splits new_type_names descr sorts thy6);
   368     val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
   378     val (thy7, split) = add_and_get_axioms "split" new_type_names split_ts thy6;
   370       split_asm_ts thy7;
   380       split_asm_ts thy7;
   371     val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
   381     val (thy9, nchotomys) = add_and_get_axioms "nchotomy" new_type_names
   372       (DatatypeProp.make_nchotomys descr sorts) thy8;
   382       (DatatypeProp.make_nchotomys descr sorts) thy8;
   373     val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
   383     val (thy10, case_congs) = add_and_get_axioms "case_cong" new_type_names
   374       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   384       (DatatypeProp.make_case_congs new_type_names descr sorts thy9) thy9;
   375     val thy11 = PureThy.add_axiomss_i [(("size",
       
   376       DatatypeProp.make_size new_type_names descr sorts thy10), [])] thy10;
       
   377     val size_thms = get_thms thy11 "size";
       
   378     
   385     
   379     val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
   386     val dt_infos = map (make_dt_info descr' induct reccomb_names rec_thms)
   380       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   387       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   381         exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   388         exhaustion ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   382 
   389 
   383     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   390     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   384 
   391 
   385     val thy12 = thy11 |>
   392     val thy11 = thy10 |>
       
   393       Theory.add_path (space_implode "_" new_type_names) |>
   386       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   394       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   387       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   395       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   388       Theory.parent_path;
   396       Theory.parent_path;
   389 
   397 
   390     val _ = store_clasimp thy12 ((claset_of thy12, simpset_of thy12)
   398     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   391       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   399       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   392       addIffs flat inject addDistinct (distinct, hd descr));
   400       addIffs flat inject addDistinct (distinct, hd descr));
   393 
   401 
   394   in
   402   in
   395     (thy12,
   403     (thy11,
   396      {distinct = distinct,
   404      {distinct = distinct,
   397       inject = inject,
   405       inject = inject,
   398       exhaustion = exhaustion,
   406       exhaustion = exhaustion,
   399       rec_thms = rec_thms,
   407       rec_thms = rec_thms,
   400       case_thms = case_thms,
   408       case_thms = case_thms,
   405   end;
   413   end;
   406 
   414 
   407 
   415 
   408 (******************* definitional introduction of datatypes *******************)
   416 (******************* definitional introduction of datatypes *******************)
   409 
   417 
   410 fun add_datatype_def new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   418 fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy =
   411   let
   419   let
   412     val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
   420     val _ = message ("Proofs for datatype(s) " ^ commas new_type_names);
   413 
   421 
   414     val (thy2, inject, dist_rewrites, induct) = thy |>
   422     val (thy2, inject, dist_rewrites, induct) = thy |>
   415       Theory.add_path (space_implode "_" new_type_names) |>
   423       DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   416       DatatypeRepProofs.representation_proofs dt_info new_type_names descr sorts
       
   417         types_syntax constr_syntax;
   424         types_syntax constr_syntax;
   418 
   425 
   419     val (thy3, casedist_thms) =
   426     val (thy3, casedist_thms) =
   420       DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
   427       DatatypeAbsProofs.prove_casedist_thms new_type_names descr sorts induct thy2;
   421     val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   428     val (thy4, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   422       new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
   429       flat_names new_type_names descr sorts dt_info inject dist_rewrites induct thy3;
   423     val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   430     val (thy5, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   424       new_type_names descr sorts reccomb_names rec_thms thy4;
   431       flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   425     val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
   432     val (thy6, distinct) = DatatypeAbsProofs.prove_distinctness_thms
   426       new_type_names descr sorts dist_rewrites case_thms thy5;
   433       flat_names new_type_names descr sorts dist_rewrites case_thms thy5;
   427     val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
   434     val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
   428       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   435       descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   429     val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   436     val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   430       descr sorts casedist_thms thy7;
   437       descr sorts casedist_thms thy7;
   431     val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   438     val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   432       descr sorts nchotomys case_thms thy8;
   439       descr sorts nchotomys case_thms thy8;
   433     val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms new_type_names
   440     val (thy10, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
   434       descr sorts reccomb_names rec_thms thy9;
   441       descr sorts reccomb_names rec_thms thy9;
   435 
   442 
   436     val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
   443     val dt_infos = map (make_dt_info (flat descr) induct reccomb_names rec_thms)
   437       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   444       ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~
   438         casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   445         casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   439 
   446 
   440     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   447     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   441 
   448 
   442     val thy11 = thy10 |>
   449     val thy11 = thy10 |>
       
   450       Theory.add_path (space_implode "_" new_type_names) |>
   443       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   451       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   444       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   452       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   445       Theory.parent_path;
   453       parent_path flat_names;
   446 
   454 
   447     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   455     val _ = store_clasimp thy11 ((claset_of thy11, simpset_of thy11)
   448       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   456       addsimps2 flat case_thms addsimps2 size_thms addsimps2 rec_thms
   449       addIffs flat inject addDistinct (distinct, hd descr));
   457       addIffs flat inject addDistinct (distinct, hd descr));
   450 
   458 
   500     val dt_info = get_datatypes thy;
   508     val dt_info = get_datatypes thy;
   501 
   509 
   502     val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
   510     val _ = writeln ("Proofs for datatype(s) " ^ commas new_type_names);
   503 
   511 
   504     val (thy2, casedist_thms) = thy |>
   512     val (thy2, casedist_thms) = thy |>
   505       Theory.add_path (space_implode "_" new_type_names) |>
       
   506       DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
   513       DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction;
   507     val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   514     val (thy3, reccomb_names, rec_thms) = DatatypeAbsProofs.prove_primrec_thms
   508       new_type_names [descr] sorts dt_info inject distinct induction thy2;
   515       false new_type_names [descr] sorts dt_info inject distinct induction thy2;
   509     val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms
   516     val (thy4, case_names, case_thms) = DatatypeAbsProofs.prove_case_thms false
   510       new_type_names [descr] sorts reccomb_names rec_thms thy3;
   517       new_type_names [descr] sorts reccomb_names rec_thms thy3;
   511     val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
   518     val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
   512       new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   519       new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   513     val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   520     val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
   514       [descr] sorts casedist_thms thy5;
   521       [descr] sorts casedist_thms thy5;
   515     val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   522     val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
   516       [descr] sorts nchotomys case_thms thy6;
   523       [descr] sorts nchotomys case_thms thy6;
   517     val (thy8, size_thms) =
   524     val (thy8, size_thms) =
   518       if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
   525       if exists (equal "Arith") (Sign.stamp_names_of (sign_of thy7)) then
   519         DatatypeAbsProofs.prove_size_thms new_type_names
   526         DatatypeAbsProofs.prove_size_thms false new_type_names
   520           [descr] sorts reccomb_names rec_thms thy7
   527           [descr] sorts reccomb_names rec_thms thy7
   521       else (thy7, []);
   528       else (thy7, []);
   522 
   529 
   523     val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
   530     val dt_infos = map (make_dt_info descr induction reccomb_names rec_thms)
   524       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
   531       ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~
   525         casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   532         casedist_thms ~~ distinct ~~ inject ~~ nchotomys ~~ case_congs);
   526 
   533 
   527     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   534     val simps = flat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
   528 
   535 
   529     val thy9 = thy8 |>
   536     val thy9 = thy8 |>
       
   537       Theory.add_path (space_implode "_" new_type_names) |>
   530       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   538       PureThy.add_tthmss [(("simps", map Attribute.tthm_of simps), [])] |>
   531       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   539       put_datatypes (foldr Symtab.update (dt_infos, dt_info)) |>
   532       Theory.parent_path;
   540       Theory.parent_path;
   533 
   541 
   534     val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
   542     val _ = store_clasimp thy9 ((claset_of thy9, simpset_of thy9)
   549   end;
   557   end;
   550 
   558 
   551 
   559 
   552 (******************************** add datatype ********************************)
   560 (******************************** add datatype ********************************)
   553 
   561 
   554 fun gen_add_datatype prep_typ new_type_names dts thy =
   562 fun gen_add_datatype prep_typ flat_names new_type_names dts thy =
   555   let
   563   let
   556     val _ = Theory.requires thy "Datatype" "datatype definitions";
   564     val _ = Theory.requires thy "Datatype" "datatype definitions";
   557 
   565 
   558     (* this theory is used just for parsing *)
   566     (* this theory is used just for parsing *)
   559 
   567 
   560     val tmp_thy = thy |>
   568     val tmp_thy = thy |>
   561       Theory.prep_ext |>
   569       Theory.prep_ext |>
   562       Theory.add_path (space_implode "_" new_type_names) |>
       
   563       Theory.add_types (map (fn (tvs, tname, mx, _) =>
   570       Theory.add_types (map (fn (tvs, tname, mx, _) =>
   564         (tname, length tvs, mx)) dts);
   571         (tname, length tvs, mx)) dts);
   565 
   572 
   566     val sign = sign_of tmp_thy;
   573     val sign = sign_of tmp_thy;
   567 
   574 
       
   575     val (tyvars, _, _, _)::_ = dts;
   568     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   576     val (new_dts, types_syntax) = ListPair.unzip (map (fn (tvs, tname, mx, _) =>
   569       let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
   577       let val full_tname = Sign.full_name sign (Syntax.type_name tname mx)
   570       in (case duplicates tvs of
   578       in (case duplicates tvs of
   571             [] => ((full_tname, tvs), (tname, mx))
   579             [] => if eq_set (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
       
   580                   else error ("Mutually recursive datatypes must have same type parameters")
   572           | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
   581           | dups => error ("Duplicate parameter(s) for datatype " ^ full_tname ^
   573               " : " ^ commas dups))
   582               " : " ^ commas dups))
   574       end) dts);
   583       end) dts);
   575 
   584 
   576     val _ = (case duplicates (map fst new_dts) @ duplicates new_type_names of
   585     val _ = (case duplicates (map fst new_dts) @ duplicates new_type_names of
   577       [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   586       [] => () | dups => error ("Duplicate datatypes: " ^ commas dups));
   578 
   587 
   579     fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
   588     fun prep_dt_spec ((dts', constr_syntax, sorts, i), (tvs, tname, mx, constrs)) =
   580       let
   589       let
   581         fun prep_constr ((constrs, constr_syntax', sorts'), (cname, mx', cargs)) =
   590         fun prep_constr ((constrs, constr_syntax', sorts'), (cname, cargs, mx')) =
   582           let
   591           let
   583             val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
   592             val (cargs', sorts'') = foldl (prep_typ sign) (([], sorts'), cargs);
   584             val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
   593             val _ = (case foldr add_typ_tfree_names (cargs', []) \\ tvs of
   585                 [] => ()
   594                 [] => ()
   586               | vs => error ("Extra type variables on rhs: " ^ commas vs))
   595               | vs => error ("Extra type variables on rhs: " ^ commas vs))
   587           in (constrs @ [((if length dts = 1 then Sign.full_name sign
   596           in (constrs @ [((if flat_names then Sign.full_name sign else
   588                else Sign.full_name_path sign (Sign.base_name tname))
   597                 Sign.full_name_path sign tname) (Syntax.const_name cname mx'),
   589                  (Syntax.const_name cname mx'),
       
   590                    map (dtyp_of_typ new_dts) cargs')],
   598                    map (dtyp_of_typ new_dts) cargs')],
   591               constr_syntax' @ [(cname, mx')], sorts'')
   599               constr_syntax' @ [(cname, mx')], sorts'')
   592           end handle ERROR =>
   600           end handle ERROR =>
   593             error ("The error above occured in constructor " ^ cname ^
   601             error ("The error above occured in constructor " ^ cname ^
   594               " of datatype " ^ tname);
   602               " of datatype " ^ tname);
   604               constr_syntax @ [constr_syntax'], sorts', i + 1)
   612               constr_syntax @ [constr_syntax'], sorts', i + 1)
   605          | dups => error ("Duplicate constructors " ^ commas dups ^
   613          | dups => error ("Duplicate constructors " ^ commas dups ^
   606              " in datatype " ^ tname)
   614              " in datatype " ^ tname)
   607       end;
   615       end;
   608 
   616 
   609     val (dts', constr_syntax, sorts, i) = foldl prep_dt_spec (([], [], [], 0), dts);
   617     val (dts', constr_syntax, sorts', i) = foldl prep_dt_spec (([], [], [], 0), dts);
   610     val dt_info = get_datatypes thy;
   618     val dt_info = get_datatypes thy;
   611     val (descr, _) = unfold_datatypes dt_info dts' i;
   619     val (descr, _) = unfold_datatypes dt_info dts' i;
   612     val _ = check_nonempty descr;
   620     val _ = check_nonempty descr;
       
   621     val sorts = sorts' @ (map (rpair (Sign.defaultS sign)) (tyvars \\ map fst sorts'));
   613 
   622 
   614   in
   623   in
   615     (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   624     (if (!quick_and_dirty) then add_datatype_axm else add_datatype_def)
   616       new_type_names descr sorts types_syntax constr_syntax dt_info thy
   625       flat_names new_type_names descr sorts types_syntax constr_syntax dt_info thy
   617   end;
   626   end;
   618 
   627 
   619 val add_datatype_i = gen_add_datatype cert_typ;
   628 val add_datatype_i = gen_add_datatype cert_typ;
   620 val add_datatype = gen_add_datatype read_typ;
   629 val add_datatype = gen_add_datatype read_typ;
   621 
   630