src/HOL/Tools/datatype_package/datatype_abs_proofs.ML
changeset 31737 b3f63611784e
parent 31723 f5cafe803b55
     1.1 --- a/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Sun Jun 21 08:38:57 2009 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package/datatype_abs_proofs.ML	Sun Jun 21 08:38:58 2009 +0200
     1.3 @@ -14,24 +14,22 @@
     1.4  
     1.5  signature DATATYPE_ABS_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 prove_casedist_thms : datatype_config -> string list ->
    1.11 +  include DATATYPE_COMMON
    1.12 +  val prove_casedist_thms : 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 : datatype_config -> string list ->
    1.16 +  val prove_primrec_thms : config -> string list ->
    1.17      descr list -> (string * sort) list ->
    1.18 -      datatype_info Symtab.table -> thm list list -> thm list list ->
    1.19 +      info Symtab.table -> thm list list -> thm list list ->
    1.20          simpset -> thm -> theory -> (string list * thm list) * theory
    1.21 -  val prove_case_thms : datatype_config -> string list ->
    1.22 +  val prove_case_thms : config -> string list ->
    1.23      descr list -> (string * sort) list ->
    1.24        string list -> thm list -> theory -> (thm list list * string list) * theory
    1.25 -  val prove_split_thms : datatype_config -> string list ->
    1.26 +  val prove_split_thms : config -> string list ->
    1.27      descr list -> (string * sort) list ->
    1.28        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.29          (thm * thm) list * theory
    1.30 -  val prove_nchotomys : datatype_config -> string list -> descr list ->
    1.31 +  val prove_nchotomys : config -> string list -> descr list ->
    1.32      (string * sort) list -> thm list -> theory -> thm list * theory
    1.33    val prove_weak_case_congs : string list -> descr list ->
    1.34      (string * sort) list -> theory -> thm list * theory
    1.35 @@ -47,7 +45,7 @@
    1.36  
    1.37  (************************ case distinction theorems ***************************)
    1.38  
    1.39 -fun prove_casedist_thms (config : datatype_config) new_type_names descr sorts induct case_names_exhausts thy =
    1.40 +fun prove_casedist_thms (config : config) new_type_names descr sorts induct case_names_exhausts thy =
    1.41    let
    1.42      val _ = message config "Proving case distinction theorems ...";
    1.43  
    1.44 @@ -89,8 +87,8 @@
    1.45  
    1.46  (*************************** primrec combinators ******************************)
    1.47  
    1.48 -fun prove_primrec_thms (config : datatype_config) new_type_names descr sorts
    1.49 -    (dt_info : datatype_info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    1.50 +fun prove_primrec_thms (config : config) new_type_names descr sorts
    1.51 +    (dt_info : info Symtab.table) constr_inject dist_rewrites dist_ss induct thy =
    1.52    let
    1.53      val _ = message config "Constructing primrec combinators ...";
    1.54  
    1.55 @@ -275,7 +273,7 @@
    1.56  
    1.57  (***************************** case combinators *******************************)
    1.58  
    1.59 -fun prove_case_thms (config : datatype_config) new_type_names descr sorts reccomb_names primrec_thms thy =
    1.60 +fun prove_case_thms (config : config) new_type_names descr sorts reccomb_names primrec_thms thy =
    1.61    let
    1.62      val _ = message config "Proving characteristic theorems for case combinators ...";
    1.63  
    1.64 @@ -349,7 +347,7 @@
    1.65  
    1.66  (******************************* case splitting *******************************)
    1.67  
    1.68 -fun prove_split_thms (config : datatype_config) new_type_names descr sorts constr_inject dist_rewrites
    1.69 +fun prove_split_thms (config : config) new_type_names descr sorts constr_inject dist_rewrites
    1.70      casedist_thms case_thms thy =
    1.71    let
    1.72      val _ = message config "Proving equations for case splitting ...";
    1.73 @@ -398,7 +396,7 @@
    1.74  
    1.75  (************************* additional theorems for TFL ************************)
    1.76  
    1.77 -fun prove_nchotomys (config : datatype_config) new_type_names descr sorts casedist_thms thy =
    1.78 +fun prove_nchotomys (config : config) new_type_names descr sorts casedist_thms thy =
    1.79    let
    1.80      val _ = message config "Proving additional theorems for TFL ...";
    1.81