# HG changeset patch
# User haftmann
# Date 1255088080 -7200
# Node ID dc883c6126d4474d3e924cef3294d2ab0d291c4c
# Parent  c913cc8316306504bc610f3b15b00cd9b827aebc
dropped simproc_dist formally

diff -r c913cc831630 -r dc883c6126d4 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 09 13:34:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Fri Oct 09 13:34:40 2009 +0200
@@ -161,23 +161,9 @@
 
 val distinctN = "constr_distinct";
 
-fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
-    FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
-      (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
-        atac 2, resolve_tac thms 1, etac FalseE 1]))
-  | ManyConstrs (thm, simpset) =>
-      let
-        val [In0_inject, In1_inject, In0_not_In1, In1_not_In0] =
-          map (PureThy.get_thm (ThyInfo.the_theory "Datatype" thy))
-            ["In0_inject", "In1_inject", "In0_not_In1", "In1_not_In0"];
-      in
-        Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
-        (EVERY [rtac eq_reflection 1, rtac iffI 1, dtac thm 1,
-          full_simp_tac (Simplifier.inherit_context ss simpset) 1,
-          REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
-          eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1,
-          etac FalseE 1]))
-      end;
+fun distinct_rule thy ss tname eq_t = Goal.prove (Simplifier.the_context ss) [] [] eq_t
+  (K (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
+    atac 2, resolve_tac (#distinct (the_info thy tname)) 1, etac FalseE 1]));
 
 fun get_constr thy dtco =
   get_info thy dtco
@@ -408,7 +394,7 @@
   in
     thy2
     |> derive_datatype_props config dt_names alt_names [descr] sorts
-         induct inject (distinct, distinct, map FewConstrs distinct)
+         induct inject (distinct, distinct, distinct)
  end;
 
 fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
@@ -545,7 +531,7 @@
       else raise exn;
 
     val _ = message config ("Constructing datatype(s) " ^ commas_quote new_type_names);
-    val ((inject, distinct_rules, distinct_rewrites, distinct_entry, induct), thy') = thy |>
+    val ((inject, (distinct_rules, distinct_rewrites, distinct_entry), induct), thy') = thy |>
       DatatypeRepProofs.representation_proofs config dt_info new_type_names descr sorts
         types_syntax constr_syntax (mk_case_names_induct (flat descr));
   in
@@ -562,7 +548,6 @@
 (* setup theory *)
 
 val setup =
-  DatatypeRepProofs.distinctness_limit_setup #>
   simproc_setup #>
   trfun_setup #>
   DatatypeInterpretation.init;
diff -r c913cc831630 -r dc883c6126d4 src/HOL/Tools/Datatype/datatype_aux.ML
--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Oct 09 13:34:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Fri Oct 09 13:34:40 2009 +0200
@@ -38,10 +38,6 @@
   val indtac : thm -> string list -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
 
-  datatype simproc_dist = FewConstrs of thm list
-                        | ManyConstrs of thm * simpset;
-
-
   exception Datatype
   exception Datatype_Empty of string
   val name_of_typ : typ -> string
@@ -153,10 +149,6 @@
   in compose_tac (false, exhaustion', nprems_of exhaustion) i state
   end;
 
-(* handling of distinctness theorems *)
-
-datatype simproc_dist = FewConstrs of thm list
-                      | ManyConstrs of thm * simpset;
 
 (********************** Internal description of datatypes *********************)
 
@@ -176,7 +168,7 @@
    descr : descr,
    sorts : (string * sort) list,
    inject : thm list,
-   distinct : simproc_dist,
+   distinct : thm list,
    induct : thm,
    inducts : thm list,
    exhaust : thm,
diff -r c913cc831630 -r dc883c6126d4 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Oct 09 13:34:34 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Oct 09 13:34:40 2009 +0200
@@ -12,13 +12,11 @@
 signature DATATYPE_REP_PROOFS =
 sig
   include DATATYPE_COMMON
-  val distinctness_limit : int Config.T
-  val distinctness_limit_setup : theory -> theory
   val representation_proofs : config -> info Symtab.table ->
     string list -> descr list -> (string * sort) list ->
       (binding * mixfix) list -> (binding * mixfix) list list -> attribute
-        -> theory -> (thm list list * thm list list * thm list list *
-          DatatypeAux.simproc_dist list * thm) * theory
+        -> theory -> (thm list list * (thm list list * thm list list *
+          thm list list) * thm) * theory
 end;
 
 structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -26,10 +24,6 @@
 
 open DatatypeAux;
 
-(*the kind of distinctiveness axioms depends on number of constructors*)
-val (distinctness_limit, distinctness_limit_setup) =
-  Attrib.config_int "datatype_distinctness_limit" 9999 (*approx. infinity*);
-
 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
 
 val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
@@ -520,27 +514,18 @@
       dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
         (constr_rep_thms ~~ dist_lemmas);
 
-    fun prove_distinct_thms _ _ (_, []) = []
-      | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) =
-          if k >= lim then [] else let
-            (*number of constructors < distinctness_limit : C_i ... ~= C_j ...*)
-            fun prove [] = []
-              | prove (t :: ts) =
-                  let
-                    val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
-                      EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
-                  in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
-          in prove ts end;
+    fun prove_distinct_thms dist_rewrites' (k, ts) =
+      let
+        fun prove [] = []
+          | prove (t :: ts) =
+              let
+                val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
+                  EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
+              in dist_thm :: standard (dist_thm RS not_sym) :: prove ts end;
+      in prove ts end;
 
-    val distinct_thms = DatatypeProp.make_distincts descr sorts
-      |> map2 (prove_distinct_thms
-           (Config.get_thy thy5 distinctness_limit)) dist_rewrites;
-
-    val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
-      if length constrs < Config.get_thy thy5 distinctness_limit
-      then FewConstrs dists
-      else ManyConstrs (congr, HOL_basic_ss addsimps rep_thms)) (hd descr ~~
-        constr_rep_thms ~~ rep_congs ~~ distinct_thms);
+    val distinct_thms = map2 (prove_distinct_thms)
+      dist_rewrites (DatatypeProp.make_distincts descr sorts);
 
     (* prove injectivity of constructors *)
 
@@ -633,7 +618,7 @@
       ||> Theory.checkpoint;
 
   in
-    ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
+    ((constr_inject', (distinct_thms', dist_rewrites, distinct_thms'), dt_induct'), thy7)
   end;
 
 end;