more appropriate abstraction over distinctness rules
authorhaftmann
Tue Oct 13 08:36:39 2009 +0200 (2009-10-13)
changeset 32915a7a97960054b
parent 32912 9fd51a25bd3a
child 32916 1e87e033423d
more appropriate abstraction over distinctness rules
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Mon Oct 12 15:26:50 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Tue Oct 13 08:36:39 2009 +0200
     1.3 @@ -334,15 +334,13 @@
     1.4      val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
     1.5      val _ = message config ("Deriving properties for datatype(s) " ^ commas_quote new_type_names);
     1.6  
     1.7 -    val other_distincts = all_distincts thy2 (get_rec_types flat_descr sorts);
     1.8 -
     1.9      val (exhaust, thy3) = DatatypeAbsProofs.prove_casedist_thms config new_type_names
    1.10        descr sorts induct (mk_case_names_exhausts flat_descr dt_names) thy2;
    1.11      val (nchotomys, thy4) = DatatypeAbsProofs.prove_nchotomys config new_type_names
    1.12        descr sorts exhaust thy3;
    1.13      val ((rec_names, rec_rewrites), thy5) = DatatypeAbsProofs.prove_primrec_thms
    1.14        config new_type_names descr sorts (#inject o the o Symtab.lookup (get_all thy4))
    1.15 -      inject distinct (Simplifier.theory_context thy4 (HOL_basic_ss addsimps (flat other_distincts)))
    1.16 +      inject (distinct, all_distincts thy2 (get_rec_types flat_descr sorts))
    1.17        induct thy4;
    1.18      val ((case_rewrites, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
    1.19        config new_type_names descr sorts rec_names rec_rewrites thy5;
     2.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Mon Oct 12 15:26:50 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Oct 13 08:36:39 2009 +0200
     2.3 @@ -20,8 +20,8 @@
     2.4      attribute list -> theory -> thm list * theory
     2.5    val prove_primrec_thms : config -> string list ->
     2.6      descr list -> (string * sort) list ->
     2.7 -      (string -> thm list) -> thm list list -> thm list list ->
     2.8 -        simpset -> thm -> theory -> (string list * thm list) * theory
     2.9 +      (string -> thm list) -> thm list list -> thm list list * thm list list ->
    2.10 +        thm -> theory -> (string list * thm list) * theory
    2.11    val prove_case_thms : config -> string list ->
    2.12      descr list -> (string * sort) list ->
    2.13        string list -> thm list -> theory -> (thm list list * string list) * theory
    2.14 @@ -88,7 +88,7 @@
    2.15  (*************************** primrec combinators ******************************)
    2.16  
    2.17  fun prove_primrec_thms (config : config) new_type_names descr sorts
    2.18 -    injects_of constr_inject dist_rewrites dist_ss induct thy =
    2.19 +    injects_of constr_inject (dist_rewrites, other_dist_rewrites) induct thy =
    2.20    let
    2.21      val _ = message config "Constructing primrec combinators ...";
    2.22  
    2.23 @@ -170,7 +170,7 @@
    2.24          val distinct_tac =
    2.25            (if i < length newTs then
    2.26               full_simp_tac (HOL_ss addsimps (nth dist_rewrites i)) 1
    2.27 -           else full_simp_tac dist_ss 1);
    2.28 +           else full_simp_tac (HOL_ss addsimps (flat other_dist_rewrites)) 1);
    2.29  
    2.30          val inject = map (fn r => r RS iffD1)
    2.31            (if i < length newTs then nth constr_inject i