1.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 09 13:34:34 2009 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 09 13:34:40 2009 +0200
     1.3 @@ -161,23 +161,9 @@
     1.4  
     1.5  val distinctN = "constr_distinct";
     1.6  
     1.7 -fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
     1.8 -    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
     1.9 -      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.10 -        atac 2, resolve_tac thms 1, etac FalseE 1]))
    1.11 -  | ManyConstrs (thm, simpset) =>
    1.12 -      let
    1.13 -        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
    1.14 -          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
    1.15 -            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
    1.16 -      in
    1.17 -        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
    1.18 -        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
    1.19 -          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
    1.20 -          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
    1.21 -          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
    1.22 -          etac FalseE 1]))
    1.23 -      end;
    1.24 +fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t
    1.25 +  (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
    1.26 +    atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1]));
    1.27  
    1.28  fun get_constr thy dtco =
    1.29    get_info thy dtco
    1.30 @@ -408,7 +394,7 @@
    1.31    in
    1.32      thy2
    1.33      |> derive_datatype_props config dt_names alt_names [descr] sorts
    1.34 -         induct inject (distinct, distinct, map FewConstrs distinct)
    1.35 +         induct inject (distinct, distinct, distinct)
    1.36   end;
    1.37  
    1.38  fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
    1.39 @@ -545,7 +531,7 @@
    1.40        else raise exn;
    1.41  
    1.42      val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
    1.43 -    val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
    1.44 +    val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
    1.45        DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
    1.46          types_syntax constr_syntax (mk_case_names_induct (flat descr));
    1.47    in
    1.48 @@ -562,7 +548,6 @@
    1.49  (* setup theory *)
    1.50  
    1.51  val setup =
    1.52 -  DatatypeRepProofs.distinctness_limit_setup #>
    1.53    simproc_setup #>
    1.54    trfun_setup #>
    1.55    DatatypeInterpretation.init;

     2.1 --- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Oct 09 13:34:34 2009 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Oct 09 13:34:40 2009 +0200
     2.3 @@ -38,10 +38,6 @@
     2.4    val indtac : thm -> string list -> int -> tactic
     2.5    val exh_tac : (string -> thm) -> int -> tactic
     2.6  
     2.7 -  datatype simproc_dist = FewConstrs of thm list
     2.8 -                        | ManyConstrs of thm * simpset;
     2.9 -
    2.10 -
    2.11    exception Datatype
    2.12    exception Datatype_Empty of string
    2.13    val name_of_typ : typ -> string
    2.14 @@ -153,10 +149,6 @@
    2.15    in compose_tac (false, exhaustion', nprems_of exhaustion) i state
    2.16    end;
    2.17  
    2.18 -(* handling of distinctness theorems *)
    2.19 -
    2.20 -datatype simproc_dist = FewConstrs of thm list
    2.21 -                      | ManyConstrs of thm * simpset;
    2.22  
    2.23  (********************** Internal description of datatypes *********************)
    2.24  
    2.25 @@ -176,7 +168,7 @@
    2.26     descr : descr,
    2.27     sorts : (string * sort) list,
    2.28     inject : thm list,
    2.29 -   distinct : simproc_dist,
    2.30 +   distinct : thm list,
    2.31     induct : thm,
    2.32     inducts : thm list,
    2.33     exhaust : thm,

     3.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Oct 09 13:34:34 2009 +0200
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Oct 09 13:34:40 2009 +0200
     3.3 @@ -12,13 +12,11 @@
     3.4  signature DATATYPE_REP_PROOFS =
     3.5  sig
     3.6    include DATATYPE_COMMON
     3.7 -  val distinctness_limit : int Config.T
     3.8 -  val distinctness_limit_setup : theory -> theory
     3.9    val representation_proofs : config -> info Symtab.table ->
    3.10      string list -> descr list -> (string * sort) list ->
    3.11        (binding * mixfix) list -> (binding * mixfix) list list -> attribute
    3.12 -        -> theory -> (thm list list * thm list list * thm list list *
    3.13 -          DatatypeAux.simproc_dist list * thm) * theory
    3.14 +        -> theory -> (thm list list * (thm list list * thm list list *
    3.15 +          thm list list) * thm) * theory
    3.16  end;
    3.17  
    3.18  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    3.19 @@ -26,10 +24,6 @@
    3.20  
    3.21  open DatatypeAux;
    3.22  
    3.23 -(*the kind of distinctiveness axioms depends on number of constructors*)
    3.24 -val (distinctness_limit, distinctness_limit_setup) =
    3.25 -  Attrib.config_int "datatype_distinctness_limit" 9999 (*approx. infinity*);
    3.26 -
    3.27  val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
    3.28  
    3.29  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
    3.30 @@ -520,27 +514,18 @@
    3.31        dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
    3.32          (constr_rep_thms ~~ dist_lemmas);
    3.33  
    3.34 -    fun prove_distinct_thms _ _ (_, []) = []
    3.35 -      | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
    3.36 -          if k >= lim then [] else let
    3.37 -            (*number of constructors < distinctness_limit : C_i ... ~= C_j ...*)
    3.38 -            fun prove [] = []
    3.39 -              | prove (t :: ts) =
    3.40 -                  let
    3.41 -                    val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    3.42 -                      EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    3.43 -                  in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
    3.44 -          in prove ts end;
    3.45 +    fun prove_distinct_thms dist_rewrites' (k, ts) =
    3.46 +      let
    3.47 +        fun prove [] = []
    3.48 +          | prove (t :: ts) =
    3.49 +              let
    3.50 +                val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    3.51 +                  EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    3.52 +              in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
    3.53 +      in prove ts end;
    3.54  
    3.55 -    val distinct_thms = DatatypeProp.make_distincts descr sorts
    3.56 -      |> map2 (prove_distinct_thms
    3.57 -           (Config.get_thy thy5 distinctness_limit)) dist_rewrites;
    3.58 -
    3.59 -    val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
    3.60 -      if length constrs < Config.get_thy thy5 distinctness_limit
    3.61 -      then FewConstrs dists
    3.62 -      else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
    3.63 -        constr_rep_thms ~~ rep_congs ~~ distinct_thms);
    3.64 +    val distinct_thms = map2 (prove_distinct_thms)
    3.65 +      dist_rewrites (DatatypeProp.make_distincts descr sorts);
    3.66  
    3.67      (* prove injectivity of constructors *)
    3.68  
    3.69 @@ -633,7 +618,7 @@
    3.70        ||> Theory.checkpoint;
    3.71  
    3.72    in
    3.73 -    ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
    3.74 +    ((constr_inject', (distinct_thms', dist_rewrites, distinct_thms'), dt_induct'), thy7)
    3.75    end;
    3.76  
    3.77  end;