datatype packages: record datatype_config for configuration flags; less verbose signatures
authorhaftmann
Tue Jun 16 16:37:07 2009 +0200 (2009-06-16)
changeset 31668a616e56a5ec8
parent 31667 cc969090c204
child 31669 6802c34af5a9
datatype packages: record datatype_config for configuration flags; less verbose signatures
src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package/datatype_aux.ML
src/HOL/Tools/datatype_package/datatype_codegen.ML
src/HOL/Tools/datatype_package/datatype_package.ML
src/HOL/Tools/datatype_package/datatype_realizer.ML
src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/size.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/quickcheck_generators.ML
     1.1 --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Tue Jun 16 16:36:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Tue Jun 16 16:37:07 2009 +0200
     1.3 @@ -14,26 +14,29 @@
     1.4  
     1.5  signature DATATYPE_ABS_PROOFS =
     1.6  sig
     1.7 -  val prove_casedist_thms : string list ->
     1.8 -    DatatypeAux.descr list -> (string * sort) list -> thm ->
     1.9 +  type datatype_config = DatatypeAux.datatype_config
    1.10 +  type descr = DatatypeAux.descr
    1.11 +  type datatype_info = DatatypeAux.datatype_info
    1.12 +  val prove_casedist_thms : datatype_config -> string list ->
    1.13 +    descr list -> (string * sort) list -> thm ->
    1.14      attribute list -> theory -> thm list * theory
    1.15 -  val prove_primrec_thms : bool -> string list ->
    1.16 -    DatatypeAux.descr list -> (string * sort) list ->
    1.17 -      DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
    1.18 +  val prove_primrec_thms : datatype_config -> string list ->
    1.19 +    descr list -> (string * sort) list ->
    1.20 +      datatype_info Symtab.table -> thm list list -> thm list list ->
    1.21          simpset -> thm -> theory -> (string list * thm list) * theory
    1.22 -  val prove_case_thms : bool -> string list ->
    1.23 -    DatatypeAux.descr list -> (string * sort) list ->
    1.24 +  val prove_case_thms : datatype_config -> string list ->
    1.25 +    descr list -> (string * sort) list ->
    1.26        string list -> thm list -> theory -> (thm list list * string list) * theory
    1.27 -  val prove_split_thms : string list ->
    1.28 -    DatatypeAux.descr list -> (string * sort) list ->
    1.29 +  val prove_split_thms : datatype_config -> string list ->
    1.30 +    descr list -> (string * sort) list ->
    1.31        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.32          (thm * thm) list * theory
    1.33 -  val prove_nchotomys : string list -> DatatypeAux.descr list ->
    1.34 +  val prove_nchotomys : datatype_config -> string list -> descr list ->
    1.35      (string * sort) list -> thm list -> theory -> thm list * theory
    1.36 -  val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
    1.37 +  val prove_weak_case_congs : string list -> descr list ->
    1.38      (string * sort) list -> theory -> thm list * theory
    1.39    val prove_case_congs : string list ->
    1.40 -    DatatypeAux.descr list -> (string * sort) list ->
    1.41 +    descr list -> (string * sort) list ->
    1.42        thm list -> thm list list -> theory -> thm list * theory
    1.43  end;
    1.44  
    1.45 @@ -44,9 +47,9 @@
    1.46  
    1.47  (************************ case distinction theorems ***************************)
    1.48  
    1.49 -fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
    1.50 +fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
    1.51    let
    1.52 -    val _ = message "Proving case distinction theorems ...";
    1.53 +    val _ = message config "Proving case distinction theorems ...";
    1.54  
    1.55      val descr' = List.concat descr;
    1.56      val recTs = get_rec_types descr' sorts;
    1.57 @@ -86,13 +89,13 @@
    1.58  
    1.59  (*************************** primrec combinators ******************************)
    1.60  
    1.61 -fun prove_primrec_thms flat_names new_type_names descr sorts
    1.62 +fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
    1.63      (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    1.64    let
    1.65 -    val _ = message "Constructing primrec combinators ...";
    1.66 +    val _ = message config "Constructing primrec combinators ...";
    1.67  
    1.68      val big_name = space_implode "_" new_type_names;
    1.69 -    val thy0 = add_path flat_names big_name thy;
    1.70 +    val thy0 = add_path (#flat_names config) big_name thy;
    1.71  
    1.72      val descr' = List.concat descr;
    1.73      val recTs = get_rec_types descr' sorts;
    1.74 @@ -153,7 +156,7 @@
    1.75  
    1.76      val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
    1.77          InductivePackage.add_inductive_global (serial_string ())
    1.78 -          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    1.79 +          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.80              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    1.81              skip_mono = true, fork_mono = false}
    1.82            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.83 @@ -162,7 +165,7 @@
    1.84  
    1.85      (* prove uniqueness and termination of primrec combinators *)
    1.86  
    1.87 -    val _ = message "Proving termination and uniqueness of primrec functions ...";
    1.88 +    val _ = message config "Proving termination and uniqueness of primrec functions ...";
    1.89  
    1.90      fun mk_unique_tac ((tac, intrs), ((((i, (tname, _, constrs)), elim), T), T')) =
    1.91        let
    1.92 @@ -242,13 +245,13 @@
    1.93             Const ("The", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.94               set $ Free ("x", T) $ Free ("y", T'))))))
    1.95                 (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
    1.96 -      ||> parent_path flat_names
    1.97 +      ||> parent_path (#flat_names config) 
    1.98        ||> Theory.checkpoint;
    1.99  
   1.100  
   1.101      (* prove characteristic equations for primrec combinators *)
   1.102  
   1.103 -    val _ = message "Proving characteristic theorems for primrec combinators ..."
   1.104 +    val _ = message config "Proving characteristic theorems for primrec combinators ..."
   1.105  
   1.106      val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
   1.107        (fn _ => EVERY
   1.108 @@ -272,11 +275,11 @@
   1.109  
   1.110  (***************************** case combinators *******************************)
   1.111  
   1.112 -fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
   1.113 +fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
   1.114    let
   1.115 -    val _ = message "Proving characteristic theorems for case combinators ...";
   1.116 +    val _ = message config "Proving characteristic theorems for case combinators ...";
   1.117  
   1.118 -    val thy1 = add_path flat_names (space_implode "_" new_type_names) thy;
   1.119 +    val thy1 = add_path (#flat_names config) (space_implode "_" new_type_names) thy;
   1.120  
   1.121      val descr' = List.concat descr;
   1.122      val recTs = get_rec_types descr' sorts;
   1.123 @@ -338,7 +341,7 @@
   1.124      thy2
   1.125      |> Context.the_theory o fold (fold Nitpick_Const_Simp_Thms.add_thm) case_thms
   1.126         o Context.Theory
   1.127 -    |> parent_path flat_names
   1.128 +    |> parent_path (#flat_names config)
   1.129      |> store_thmss "cases" new_type_names case_thms
   1.130      |-> (fn thmss => pair (thmss, case_names))
   1.131    end;
   1.132 @@ -346,12 +349,12 @@
   1.133  
   1.134  (******************************* case splitting *******************************)
   1.135  
   1.136 -fun prove_split_thms new_type_names descr sorts constr_inject dist_rewrites
   1.137 +fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
   1.138      casedist_thms case_thms thy =
   1.139    let
   1.140 -    val _ = message "Proving equations for case splitting ...";
   1.141 +    val _ = message config "Proving equations for case splitting ...";
   1.142  
   1.143 -    val descr' = List.concat descr;
   1.144 +    val descr' = flat descr;
   1.145      val recTs = get_rec_types descr' sorts;
   1.146      val newTs = Library.take (length (hd descr), recTs);
   1.147  
   1.148 @@ -395,9 +398,9 @@
   1.149  
   1.150  (************************* additional theorems for TFL ************************)
   1.151  
   1.152 -fun prove_nchotomys new_type_names descr sorts casedist_thms thy =
   1.153 +fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
   1.154    let
   1.155 -    val _ = message "Proving additional theorems for TFL ...";
   1.156 +    val _ = message config "Proving additional theorems for TFL ...";
   1.157  
   1.158      fun prove_nchotomy (t, exhaustion) =
   1.159        let
     2.1 --- a/src/HOL/Tools/datatype_package/datatype_aux.ML	Tue Jun 16 16:36:56 2009 +0200
     2.2 +++ b/src/HOL/Tools/datatype_package/datatype_aux.ML	Tue Jun 16 16:37:07 2009 +0200
     2.3 @@ -6,8 +6,9 @@
     2.4  
     2.5  signature DATATYPE_AUX =
     2.6  sig
     2.7 -  val quiet_mode : bool ref
     2.8 -  val message : string -> unit
     2.9 +  type datatype_config
    2.10 +  val default_datatype_config : datatype_config
    2.11 +  val message : datatype_config -> string -> unit
    2.12    
    2.13    val add_path : bool -> string -> theory -> theory
    2.14    val parent_path : bool -> theory -> theory
    2.15 @@ -67,8 +68,13 @@
    2.16  structure DatatypeAux : DATATYPE_AUX =
    2.17  struct
    2.18  
    2.19 -val quiet_mode = ref false;
    2.20 -fun message s = if !quiet_mode then () else writeln s;
    2.21 +(* datatype option flags *)
    2.22 +
    2.23 +type datatype_config = { strict: bool, flat_names: bool, quiet: bool };
    2.24 +val default_datatype_config : datatype_config =
    2.25 +  { strict = true, flat_names = false, quiet = false };
    2.26 +fun message ({ quiet, ...} : datatype_config) s =
    2.27 +  if quiet then () else writeln s;
    2.28  
    2.29  fun add_path flat_names s = if flat_names then I else Sign.add_path s;
    2.30  fun parent_path flat_names = if flat_names then I else Sign.parent_path;
     3.1 --- a/src/HOL/Tools/datatype_package/datatype_codegen.ML	Tue Jun 16 16:36:56 2009 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package/datatype_codegen.ML	Tue Jun 16 16:37:07 2009 +0200
     3.3 @@ -426,7 +426,7 @@
     3.4  
     3.5  (* register a datatype etc. *)
     3.6  
     3.7 -fun add_all_code dtcos thy =
     3.8 +fun add_all_code config dtcos thy =
     3.9    let
    3.10      val (vs :: _, coss) = (split_list o map (DatatypePackage.the_datatype_spec thy)) dtcos;
    3.11      val any_css = map2 (mk_constr_consts thy vs) dtcos coss;
    3.12 @@ -437,7 +437,7 @@
    3.13    in
    3.14      if null css then thy
    3.15      else thy
    3.16 -      |> tap (fn _ => DatatypeAux.message "Registering datatype for code generator ...")
    3.17 +      |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
    3.18        |> fold Code.add_datatype css
    3.19        |> fold_rev Code.add_default_eqn case_rewrites
    3.20        |> fold Code.add_case certs
     4.1 --- a/src/HOL/Tools/datatype_package/datatype_package.ML	Tue Jun 16 16:36:56 2009 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package/datatype_package.ML	Tue Jun 16 16:37:07 2009 +0200
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  signature DATATYPE_PACKAGE =
     4.6  sig
     4.7 +  type datatype_config = DatatypeAux.datatype_config
     4.8    type datatype_info = DatatypeAux.datatype_info
     4.9    type descr = DatatypeAux.descr
    4.10    val get_datatypes : theory -> datatype_info Symtab.table
    4.11 @@ -24,39 +25,23 @@
    4.12    val strip_case : Proof.context -> bool -> term -> (term * (term * term) list) option
    4.13    val read_typ: theory ->
    4.14      (typ list * (string * sort) list) * string -> typ list * (string * sort) list
    4.15 -  val interpretation : (string list -> theory -> theory) -> theory -> theory
    4.16 -  val rep_datatype : ({distinct : thm list list,
    4.17 -       inject : thm list list,
    4.18 -       exhaustion : thm list,
    4.19 -       rec_thms : thm list,
    4.20 -       case_thms : thm list list,
    4.21 -       split_thms : (thm * thm) list,
    4.22 -       induction : thm,
    4.23 -       simps : thm list} -> Proof.context -> Proof.context) -> string list option -> term list
    4.24 -    -> theory -> Proof.state;
    4.25 -  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state;
    4.26 -  val add_datatype : bool -> bool -> string list -> (string list * binding * mixfix *
    4.27 -    (binding * typ list * mixfix) list) list -> theory ->
    4.28 -      {distinct : thm list list,
    4.29 -       inject : thm list list,
    4.30 -       exhaustion : thm list,
    4.31 -       rec_thms : thm list,
    4.32 -       case_thms : thm list list,
    4.33 -       split_thms : (thm * thm) list,
    4.34 -       induction : thm,
    4.35 -       simps : thm list} * theory
    4.36 -  val add_datatype_cmd : bool -> string list -> (string list * binding * mixfix *
    4.37 -    (binding * string list * mixfix) list) list -> theory ->
    4.38 -      {distinct : thm list list,
    4.39 -       inject : thm list list,
    4.40 -       exhaustion : thm list,
    4.41 -       rec_thms : thm list,
    4.42 -       case_thms : thm list list,
    4.43 -       split_thms : (thm * thm) list,
    4.44 -       induction : thm,
    4.45 -       simps : thm list} * theory
    4.46 +  val interpretation : (datatype_config -> string list -> theory -> theory) -> theory -> theory
    4.47 +  type rules = {distinct : thm list list,
    4.48 +    inject : thm list list,
    4.49 +    exhaustion : thm list,
    4.50 +    rec_thms : thm list,
    4.51 +    case_thms : thm list list,
    4.52 +    split_thms : (thm * thm) list,
    4.53 +    induction : thm,
    4.54 +    simps : thm list}
    4.55 +  val rep_datatype : datatype_config -> (rules -> Proof.context -> Proof.context)
    4.56 +    -> string list option -> term list -> theory -> Proof.state;
    4.57 +  val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
    4.58 +  val add_datatype : datatype_config -> string list -> (string list * binding * mixfix *
    4.59 +    (binding * typ list * mixfix) list) list -> theory -> rules * theory
    4.60 +  val add_datatype_cmd : string list -> (string list * binding * mixfix *
    4.61 +    (binding * string list * mixfix) list) list -> theory -> rules * theory
    4.62    val setup: theory -> theory
    4.63 -  val quiet_mode : bool ref
    4.64    val print_datatypes : theory -> unit
    4.65  end;
    4.66  
    4.67 @@ -65,8 +50,6 @@
    4.68  
    4.69  open DatatypeAux;
    4.70  
    4.71 -val quiet_mode = quiet_mode;
    4.72 -
    4.73  
    4.74  (* theory data *)
    4.75  
    4.76 @@ -358,31 +341,41 @@
    4.77      case_cong = case_cong,
    4.78      weak_case_cong = weak_case_cong});
    4.79  
    4.80 -structure DatatypeInterpretation = InterpretationFun(type T = string list val eq = op =);
    4.81 -val interpretation = DatatypeInterpretation.interpretation;
    4.82 +type rules = {distinct : thm list list,
    4.83 +  inject : thm list list,
    4.84 +  exhaustion : thm list,
    4.85 +  rec_thms : thm list,
    4.86 +  case_thms : thm list list,
    4.87 +  split_thms : (thm * thm) list,
    4.88 +  induction : thm,
    4.89 +  simps : thm list}
    4.90 +
    4.91 +structure DatatypeInterpretation = InterpretationFun
    4.92 +  (type T = datatype_config * string list val eq = eq_snd op =);
    4.93 +fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
    4.94  
    4.95  
    4.96  (******************* definitional introduction of datatypes *******************)
    4.97  
    4.98 -fun add_datatype_def flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
    4.99 +fun add_datatype_def (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
   4.100      case_names_induct case_names_exhausts thy =
   4.101    let
   4.102 -    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   4.103 +    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   4.104  
   4.105      val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
   4.106 -      DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
   4.107 +      DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
   4.108          types_syntax constr_syntax case_names_induct;
   4.109  
   4.110 -    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
   4.111 +    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names descr
   4.112        sorts induct case_names_exhausts thy2;
   4.113      val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
   4.114 -      flat_names new_type_names descr sorts dt_info inject dist_rewrites
   4.115 +      config new_type_names descr sorts dt_info inject dist_rewrites
   4.116        (Simplifier.theory_context thy3 dist_ss) induct thy3;
   4.117      val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
   4.118 -      flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
   4.119 -    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
   4.120 +      config new_type_names descr sorts reccomb_names rec_thms thy4;
   4.121 +    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms config new_type_names
   4.122        descr sorts inject dist_rewrites casedist_thms case_thms thy6;
   4.123 -    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
   4.124 +    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   4.125        descr sorts casedist_thms thy7;
   4.126      val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
   4.127        descr sorts nchotomys case_thms thy8;
   4.128 @@ -406,7 +399,7 @@
   4.129        |> add_cases_induct dt_infos induct
   4.130        |> Sign.parent_path
   4.131        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
   4.132 -      |> DatatypeInterpretation.data (map fst dt_infos);
   4.133 +      |> DatatypeInterpretation.data (config, map fst dt_infos);
   4.134    in
   4.135      ({distinct = distinct,
   4.136        inject = inject,
   4.137 @@ -421,7 +414,7 @@
   4.138  
   4.139  (*********************** declare existing type as datatype *********************)
   4.140  
   4.141 -fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
   4.142 +fun prove_rep_datatype (config : datatype_config) alt_names new_type_names descr sorts induct inject half_distinct thy =
   4.143    let
   4.144      val ((_, [induct']), _) =
   4.145        Variable.importT_thms [induct] (Variable.thm_context induct);
   4.146 @@ -440,19 +433,19 @@
   4.147      val (case_names_induct, case_names_exhausts) =
   4.148        (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
   4.149  
   4.150 -    val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   4.151 +    val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
   4.152  
   4.153      val (casedist_thms, thy2) = thy |>
   4.154 -      DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induct
   4.155 +      DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
   4.156          case_names_exhausts;
   4.157      val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
   4.158 -      false new_type_names [descr] sorts dt_info inject distinct
   4.159 +      config new_type_names [descr] sorts dt_info inject distinct
   4.160        (Simplifier.theory_context thy2 dist_ss) induct thy2;
   4.161 -    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
   4.162 -      new_type_names [descr] sorts reccomb_names rec_thms thy3;
   4.163 +    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
   4.164 +      config new_type_names [descr] sorts reccomb_names rec_thms thy3;
   4.165      val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
   4.166 -      new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   4.167 -    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
   4.168 +      config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
   4.169 +    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
   4.170        [descr] sorts casedist_thms thy5;
   4.171      val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
   4.172        [descr] sorts nchotomys case_thms thy6;
   4.173 @@ -482,7 +475,7 @@
   4.174        |> Sign.parent_path
   4.175        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
   4.176        |> snd
   4.177 -      |> DatatypeInterpretation.data (map fst dt_infos);
   4.178 +      |> DatatypeInterpretation.data (config, map fst dt_infos);
   4.179    in
   4.180      ({distinct = distinct,
   4.181        inject = inject,
   4.182 @@ -494,7 +487,7 @@
   4.183        simps = simps}, thy11)
   4.184    end;
   4.185  
   4.186 -fun gen_rep_datatype prep_term after_qed alt_names raw_ts thy =
   4.187 +fun gen_rep_datatype prep_term (config : datatype_config) after_qed alt_names raw_ts thy =
   4.188    let
   4.189      fun constr_of_term (Const (c, T)) = (c, T)
   4.190        | constr_of_term t =
   4.191 @@ -550,7 +543,7 @@
   4.192              (*FIXME somehow dubious*)
   4.193        in
   4.194          ProofContext.theory_result
   4.195 -          (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
   4.196 +          (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
   4.197          #-> after_qed
   4.198        end;
   4.199    in
   4.200 @@ -560,13 +553,13 @@
   4.201    end;
   4.202  
   4.203  val rep_datatype = gen_rep_datatype Sign.cert_term;
   4.204 -val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global (K I);
   4.205 +val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_datatype_config (K I);
   4.206  
   4.207  
   4.208  
   4.209  (******************************** add datatype ********************************)
   4.210  
   4.211 -fun gen_add_datatype prep_typ err flat_names new_type_names dts thy =
   4.212 +fun gen_add_datatype prep_typ (config : datatype_config) new_type_names dts thy =
   4.213    let
   4.214      val _ = Theory.requires thy "Datatype" "datatype definitions";
   4.215  
   4.216 @@ -598,7 +591,7 @@
   4.217              val _ = (case fold (curry OldTerm.add_typ_tfree_names) cargs' [] \\ tvs of
   4.218                  [] => ()
   4.219                | vs => error ("Extra type variables on rhs: " ^ commas vs))
   4.220 -          in (constrs @ [((if flat_names then Sign.full_name tmp_thy else
   4.221 +          in (constrs @ [((if #flat_names config then Sign.full_name tmp_thy else
   4.222                  Sign.full_name_path tmp_thy tname')
   4.223                    (Binding.map_name (Syntax.const_name mx') cname),
   4.224                     map (dtyp_of_typ new_dts) cargs')],
   4.225 @@ -626,7 +619,7 @@
   4.226      val dt_info = get_datatypes thy;
   4.227      val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
   4.228      val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
   4.229 -      if err then error ("Nonemptiness check failed for datatype " ^ s)
   4.230 +      if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
   4.231        else raise exn;
   4.232  
   4.233      val descr' = flat descr;
   4.234 @@ -634,12 +627,12 @@
   4.235      val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
   4.236    in
   4.237      add_datatype_def
   4.238 -      flat_names new_type_names descr sorts types_syntax constr_syntax dt_info
   4.239 +      (config : datatype_config) new_type_names descr sorts types_syntax constr_syntax dt_info
   4.240        case_names_induct case_names_exhausts thy
   4.241    end;
   4.242  
   4.243  val add_datatype = gen_add_datatype cert_typ;
   4.244 -val add_datatype_cmd = gen_add_datatype read_typ true;
   4.245 +val add_datatype_cmd = gen_add_datatype read_typ default_datatype_config;
   4.246  
   4.247  
   4.248  
   4.249 @@ -668,7 +661,7 @@
   4.250        (fn ((((NONE, _), t), _), _) => Binding.name_of t | ((((SOME t, _), _), _), _) => t) args;
   4.251      val specs = map (fn ((((_, vs), t), mx), cons) =>
   4.252        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   4.253 -  in snd o add_datatype_cmd false names specs end;
   4.254 +  in snd o add_datatype_cmd names specs end;
   4.255  
   4.256  val _ =
   4.257    OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
     5.1 --- a/src/HOL/Tools/datatype_package/datatype_realizer.ML	Tue Jun 16 16:36:56 2009 +0200
     5.2 +++ b/src/HOL/Tools/datatype_package/datatype_realizer.ML	Tue Jun 16 16:37:07 2009 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  
     5.5  signature DATATYPE_REALIZER =
     5.6  sig
     5.7 -  val add_dt_realizers: string list -> theory -> theory
     5.8 +  val add_dt_realizers: DatatypeAux.datatype_config -> string list -> theory -> theory
     5.9    val setup: theory -> theory
    5.10  end;
    5.11  
    5.12 @@ -213,10 +213,10 @@
    5.13       (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
    5.14    end;
    5.15  
    5.16 -fun add_dt_realizers names thy =
    5.17 +fun add_dt_realizers config names thy =
    5.18    if ! Proofterm.proofs < 2 then thy
    5.19    else let
    5.20 -    val _ = message "Adding realizers for induction and case analysis ..."
    5.21 +    val _ = message config "Adding realizers for induction and case analysis ..."
    5.22      val infos = map (DatatypePackage.the_datatype thy) names;
    5.23      val info :: _ = infos;
    5.24    in
     6.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Tue Jun 16 16:36:56 2009 +0200
     6.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Tue Jun 16 16:37:07 2009 +0200
     6.3 @@ -11,10 +11,13 @@
     6.4  
     6.5  signature DATATYPE_REP_PROOFS =
     6.6  sig
     6.7 +  type datatype_config = DatatypeAux.datatype_config
     6.8 +  type descr = DatatypeAux.descr
     6.9 +  type datatype_info = DatatypeAux.datatype_info
    6.10    val distinctness_limit : int Config.T
    6.11    val distinctness_limit_setup : theory -> theory
    6.12 -  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
    6.13 -    string list -> DatatypeAux.descr list -> (string * sort) list ->
    6.14 +  val representation_proofs : datatype_config -> datatype_info Symtab.table ->
    6.15 +    string list -> descr list -> (string * sort) list ->
    6.16        (binding * mixfix) list -> (binding * mixfix) list list -> attribute
    6.17          -> theory -> (thm list list * thm list list * thm list list *
    6.18            DatatypeAux.simproc_dist list * thm) * theory
    6.19 @@ -45,7 +48,7 @@
    6.20  
    6.21  (******************************************************************************)
    6.22  
    6.23 -fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    6.24 +fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
    6.25        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    6.26    let
    6.27      val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
    6.28 @@ -69,7 +72,7 @@
    6.29      val descr' = flat descr;
    6.30  
    6.31      val big_name = space_implode "_" new_type_names;
    6.32 -    val thy1 = add_path flat_names big_name thy;
    6.33 +    val thy1 = add_path (#flat_names config) big_name thy;
    6.34      val big_rec_name = big_name ^ "_rep_set";
    6.35      val rep_set_names' =
    6.36        (if length descr' = 1 then [big_rec_name] else
    6.37 @@ -147,7 +150,7 @@
    6.38  
    6.39      (************** generate introduction rules for representing set **********)
    6.40  
    6.41 -    val _ = message "Constructing representing sets ...";
    6.42 +    val _ = message config "Constructing representing sets ...";
    6.43  
    6.44      (* make introduction rule for a single constructor *)
    6.45  
    6.46 @@ -181,7 +184,7 @@
    6.47  
    6.48      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
    6.49          InductivePackage.add_inductive_global (serial_string ())
    6.50 -          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    6.51 +          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    6.52             alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
    6.53             skip_mono = true, fork_mono = false}
    6.54            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    6.55 @@ -190,7 +193,7 @@
    6.56      (********************************* typedef ********************************)
    6.57  
    6.58      val (typedefs, thy3) = thy2 |>
    6.59 -      parent_path flat_names |>
    6.60 +      parent_path (#flat_names config) |>
    6.61        fold_map (fn ((((name, mx), tvs), c), name') =>
    6.62            TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
    6.63              (Collect $ Const (c, UnivT')) NONE
    6.64 @@ -199,7 +202,7 @@
    6.65                (resolve_tac rep_intrs 1)))
    6.66                  (types_syntax ~~ tyvars ~~
    6.67                    (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
    6.68 -      add_path flat_names big_name;
    6.69 +      add_path (#flat_names config) big_name;
    6.70  
    6.71      (*********************** definition of constructors ***********************)
    6.72  
    6.73 @@ -257,19 +260,19 @@
    6.74          val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    6.75          val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    6.76          val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
    6.77 -          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
    6.78 +          ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
    6.79        in
    6.80 -        (parent_path flat_names thy', defs', eqns @ [eqns'],
    6.81 +        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
    6.82            rep_congs @ [cong'], dist_lemmas @ [dist])
    6.83        end;
    6.84  
    6.85      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
    6.86 -      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
    6.87 +      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
    6.88          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
    6.89  
    6.90      (*********** isomorphisms for new types (introduced by typedef) ***********)
    6.91  
    6.92 -    val _ = message "Proving isomorphism properties ...";
    6.93 +    val _ = message config "Proving isomorphism properties ...";
    6.94  
    6.95      val newT_iso_axms = map (fn (_, td) =>
    6.96        (collect_simp (#Abs_inverse td), #Rep_inverse td,
    6.97 @@ -358,7 +361,7 @@
    6.98        in (thy', char_thms' @ char_thms) end;
    6.99  
   6.100      val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
   6.101 -      (add_path flat_names big_name thy4, []) (tl descr));
   6.102 +      (add_path (#flat_names config) big_name thy4, []) (tl descr));
   6.103  
   6.104      (* prove isomorphism properties *)
   6.105  
   6.106 @@ -496,7 +499,7 @@
   6.107  
   6.108      (******************* freeness theorems for constructors *******************)
   6.109  
   6.110 -    val _ = message "Proving freeness of constructors ...";
   6.111 +    val _ = message config "Proving freeness of constructors ...";
   6.112  
   6.113      (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   6.114      
   6.115 @@ -568,13 +571,13 @@
   6.116  
   6.117      val ((constr_inject', distinct_thms'), thy6) =
   6.118        thy5
   6.119 -      |> parent_path flat_names
   6.120 +      |> parent_path (#flat_names config)
   6.121        |> store_thmss "inject" new_type_names constr_inject
   6.122        ||>> store_thmss "distinct" new_type_names distinct_thms;
   6.123  
   6.124      (*************************** induction theorem ****************************)
   6.125  
   6.126 -    val _ = message "Proving induction rule for datatypes ...";
   6.127 +    val _ = message config "Proving induction rule for datatypes ...";
   6.128  
   6.129      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
   6.130        (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);
     7.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 16 16:36:56 2009 +0200
     7.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Tue Jun 16 16:37:07 2009 +0200
     7.3 @@ -191,9 +191,7 @@
     7.4                             |> safe_mk_meta_eq)))
     7.5                         thy
     7.6  
     7.7 -val case_cong = fold add_case_cong
     7.8 -
     7.9 -val setup_case_cong = DatatypePackage.interpretation case_cong
    7.10 +val setup_case_cong = DatatypePackage.interpretation (K (fold add_case_cong))
    7.11  
    7.12  
    7.13  (* setup *)
     8.1 --- a/src/HOL/Tools/function_package/size.ML	Tue Jun 16 16:36:56 2009 +0200
     8.2 +++ b/src/HOL/Tools/function_package/size.ML	Tue Jun 16 16:37:07 2009 +0200
     8.3 @@ -218,7 +218,7 @@
     8.4        (new_type_names ~~ size_names)) thy''
     8.5    end;
     8.6  
     8.7 -fun add_size_thms (new_type_names as name :: _) thy =
     8.8 +fun add_size_thms config (new_type_names as name :: _) thy =
     8.9    let
    8.10      val info as {descr, alt_names, ...} = DatatypePackage.the_datatype thy name;
    8.11      val prefix = Long_Name.map_base_name (K (space_implode "_"
     9.1 --- a/src/HOL/Tools/inductive_realizer.ML	Tue Jun 16 16:36:56 2009 +0200
     9.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Tue Jun 16 16:37:07 2009 +0200
     9.3 @@ -307,8 +307,8 @@
     9.4  
     9.5      val ((dummies, dt_info), thy2) =
     9.6        thy1
     9.7 -      |> add_dummies
     9.8 -           (DatatypePackage.add_datatype false false (map (Binding.name_of o #2) dts))
     9.9 +      |> add_dummies (DatatypePackage.add_datatype
    9.10 +           { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts))
    9.11             (map (pair false) dts) []
    9.12        ||> Extraction.add_typeof_eqns_i ty_eqs
    9.13        ||> Extraction.add_realizes_eqns_i rlz_eqs;
    10.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 16 16:36:56 2009 +0200
    10.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Tue Jun 16 16:37:07 2009 +0200
    10.3 @@ -15,7 +15,7 @@
    10.4    val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list
    10.5      -> string list -> string list * string list -> typ list * typ list
    10.6      -> string * (term list * (term * term) list)
    10.7 -  val ensure_random_datatype: string list -> theory -> theory
    10.8 +  val ensure_random_datatype: DatatypeAux.datatype_config -> string list -> theory -> theory
    10.9    val eval_ref: (unit -> int -> seed -> term list option * seed) option ref
   10.10    val setup: theory -> theory
   10.11  end;
   10.12 @@ -320,9 +320,9 @@
   10.13      val prefix = space_implode "_" (random_auxN :: names);
   10.14    in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end;
   10.15  
   10.16 -fun mk_random_datatype descr vs tycos (names, auxnames) (Ts, Us) thy =
   10.17 +fun mk_random_datatype config descr vs tycos (names, auxnames) (Ts, Us) thy =
   10.18    let
   10.19 -    val _ = DatatypeAux.message "Creating quickcheck generators ...";
   10.20 +    val _ = DatatypeAux.message config "Creating quickcheck generators ...";
   10.21      val i = @{term "i\<Colon>code_numeral"};
   10.22      val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
   10.23      fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k
   10.24 @@ -356,7 +356,7 @@
   10.25    in SOME (fn (v, _) => (v, (the o Vartab.lookup vtab) (v, 0)))
   10.26    end handle CLASS_ERROR => NONE;
   10.27  
   10.28 -fun ensure_random_datatype raw_tycos thy =
   10.29 +fun ensure_random_datatype config raw_tycos thy =
   10.30    let
   10.31      val pp = Syntax.pp_global thy;
   10.32      val algebra = Sign.classes_of thy;
   10.33 @@ -370,7 +370,7 @@
   10.34        can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   10.35    in if has_inst then thy
   10.36      else case perhaps_constrain thy (random_insts @ term_of_insts) raw_vs
   10.37 -     of SOME constrain => mk_random_datatype descr
   10.38 +     of SOME constrain => mk_random_datatype config descr
   10.39            (map constrain raw_vs) tycos (names, auxnames)
   10.40              ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
   10.41        | NONE => thy