src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
changeset 31668 a616e56a5ec8
parent 31643 b040f1679f77
child 31723 f5cafe803b55
     1.1 --- a/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Tue Jun 16 16:36:56 2009 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package/datatype_rep_proofs.ML	Tue Jun 16 16:37:07 2009 +0200
     1.3 @@ -11,10 +11,13 @@
     1.4  
     1.5  signature DATATYPE_REP_PROOFS =
     1.6  sig
     1.7 +  type datatype_config = DatatypeAux.datatype_config
     1.8 +  type descr = DatatypeAux.descr
     1.9 +  type datatype_info = DatatypeAux.datatype_info
    1.10    val distinctness_limit : int Config.T
    1.11    val distinctness_limit_setup : theory -> theory
    1.12 -  val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
    1.13 -    string list -> DatatypeAux.descr list -> (string * sort) list ->
    1.14 +  val representation_proofs : datatype_config -> datatype_info Symtab.table ->
    1.15 +    string list -> descr list -> (string * sort) list ->
    1.16        (binding * mixfix) list -> (binding * mixfix) list list -> attribute
    1.17          -> theory -> (thm list list * thm list list * thm list list *
    1.18            DatatypeAux.simproc_dist list * thm) * theory
    1.19 @@ -45,7 +48,7 @@
    1.20  
    1.21  (******************************************************************************)
    1.22  
    1.23 -fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    1.24 +fun representation_proofs (config : datatype_config) (dt_info : datatype_info Symtab.table)
    1.25        new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    1.26    let
    1.27      val Datatype_thy = ThyInfo.the_theory "Datatype" thy;
    1.28 @@ -69,7 +72,7 @@
    1.29      val descr' = flat descr;
    1.30  
    1.31      val big_name = space_implode "_" new_type_names;
    1.32 -    val thy1 = add_path flat_names big_name thy;
    1.33 +    val thy1 = add_path (#flat_names config) big_name thy;
    1.34      val big_rec_name = big_name ^ "_rep_set";
    1.35      val rep_set_names' =
    1.36        (if length descr' = 1 then [big_rec_name] else
    1.37 @@ -147,7 +150,7 @@
    1.38  
    1.39      (************** generate introduction rules for representing set **********)
    1.40  
    1.41 -    val _ = message "Constructing representing sets ...";
    1.42 +    val _ = message config "Constructing representing sets ...";
    1.43  
    1.44      (* make introduction rule for a single constructor *)
    1.45  
    1.46 @@ -181,7 +184,7 @@
    1.47  
    1.48      val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
    1.49          InductivePackage.add_inductive_global (serial_string ())
    1.50 -          {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK,
    1.51 +          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
    1.52             alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
    1.53             skip_mono = true, fork_mono = false}
    1.54            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    1.55 @@ -190,7 +193,7 @@
    1.56      (********************************* typedef ********************************)
    1.57  
    1.58      val (typedefs, thy3) = thy2 |>
    1.59 -      parent_path flat_names |>
    1.60 +      parent_path (#flat_names config) |>
    1.61        fold_map (fn ((((name, mx), tvs), c), name') =>
    1.62            TypedefPackage.add_typedef false (SOME (Binding.name name')) (name, tvs, mx)
    1.63              (Collect $ Const (c, UnivT')) NONE
    1.64 @@ -199,7 +202,7 @@
    1.65                (resolve_tac rep_intrs 1)))
    1.66                  (types_syntax ~~ tyvars ~~
    1.67                    (Library.take (length newTs, rep_set_names)) ~~ new_type_names) ||>
    1.68 -      add_path flat_names big_name;
    1.69 +      add_path (#flat_names config) big_name;
    1.70  
    1.71      (*********************** definition of constructors ***********************)
    1.72  
    1.73 @@ -257,19 +260,19 @@
    1.74          val cong' = standard (cterm_instantiate [(cterm_of thy cong_f, rep_const)] arg_cong);
    1.75          val dist = standard (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma);
    1.76          val (thy', defs', eqns', _) = Library.foldl ((make_constr_def tname T) (length constrs))
    1.77 -          ((add_path flat_names tname thy, defs, [], 1), constrs ~~ constr_syntax)
    1.78 +          ((add_path (#flat_names config) tname thy, defs, [], 1), constrs ~~ constr_syntax)
    1.79        in
    1.80 -        (parent_path flat_names thy', defs', eqns @ [eqns'],
    1.81 +        (parent_path (#flat_names config) thy', defs', eqns @ [eqns'],
    1.82            rep_congs @ [cong'], dist_lemmas @ [dist])
    1.83        end;
    1.84  
    1.85      val (thy4, constr_defs, constr_rep_eqns, rep_congs, dist_lemmas) = Library.foldl dt_constr_defs
    1.86 -      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path flat_names, [], [], [], []),
    1.87 +      ((thy3 |> Sign.add_consts_i iso_decls |> parent_path (#flat_names config), [], [], [], []),
    1.88          hd descr ~~ new_type_names ~~ newTs ~~ constr_syntax);
    1.89  
    1.90      (*********** isomorphisms for new types (introduced by typedef) ***********)
    1.91  
    1.92 -    val _ = message "Proving isomorphism properties ...";
    1.93 +    val _ = message config "Proving isomorphism properties ...";
    1.94  
    1.95      val newT_iso_axms = map (fn (_, td) =>
    1.96        (collect_simp (#Abs_inverse td), #Rep_inverse td,
    1.97 @@ -358,7 +361,7 @@
    1.98        in (thy', char_thms' @ char_thms) end;
    1.99  
   1.100      val (thy5, iso_char_thms) = apfst Theory.checkpoint (List.foldr make_iso_defs
   1.101 -      (add_path flat_names big_name thy4, []) (tl descr));
   1.102 +      (add_path (#flat_names config) big_name thy4, []) (tl descr));
   1.103  
   1.104      (* prove isomorphism properties *)
   1.105  
   1.106 @@ -496,7 +499,7 @@
   1.107  
   1.108      (******************* freeness theorems for constructors *******************)
   1.109  
   1.110 -    val _ = message "Proving freeness of constructors ...";
   1.111 +    val _ = message config "Proving freeness of constructors ...";
   1.112  
   1.113      (* prove theorem  Rep_i (Constr_j ...) = Inj_j ...  *)
   1.114      
   1.115 @@ -568,13 +571,13 @@
   1.116  
   1.117      val ((constr_inject', distinct_thms'), thy6) =
   1.118        thy5
   1.119 -      |> parent_path flat_names
   1.120 +      |> parent_path (#flat_names config)
   1.121        |> store_thmss "inject" new_type_names constr_inject
   1.122        ||>> store_thmss "distinct" new_type_names distinct_thms;
   1.123  
   1.124      (*************************** induction theorem ****************************)
   1.125  
   1.126 -    val _ = message "Proving induction rule for datatypes ...";
   1.127 +    val _ = message config "Proving induction rule for datatypes ...";
   1.128  
   1.129      val Rep_inverse_thms = (map (fn (_, iso, _) => iso RS subst) newT_iso_axms) @
   1.130        (map (fn r => r RS myinv_f_f RS subst) iso_inj_thms_unfolded);