src/HOL/Tools/datatype_prop.ML
changeset 26969 cf3f998d0631
parent 25154 6155f2faf23e
child 27002 215d64dc971e
--- a/src/HOL/Tools/datatype_prop.ML	Fri May 23 16:05:02 2008 +0200
+++ b/src/HOL/Tools/datatype_prop.ML	Fri May 23 16:05:04 2008 +0200
@@ -12,6 +12,8 @@
   val indexify_names: string list -> string list
   val make_tnames: typ list -> string list
   val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
+  val make_distincts : DatatypeAux.descr list ->
+    (string * sort) list -> (int * term list) list
   val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
   val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
   val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
@@ -20,8 +22,6 @@
     (string * sort) list -> theory -> term list
   val make_cases : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> term list list
-  val make_distincts : string list -> DatatypeAux.descr list ->
-    (string * sort) list -> theory -> term list list
   val make_splits : string list -> DatatypeAux.descr list ->
     (string * sort) list -> theory -> (term * term) list
   val make_weak_case_congs : string list -> DatatypeAux.descr list ->
@@ -59,6 +59,43 @@
   in indexify_names (map type_name Ts) end;
 
 
+(************************* distinctness of constructors ***********************)
+
+fun make_distincts descr sorts =
+  let
+    val descr' = List.concat descr;
+    val recTs = get_rec_types descr' sorts;
+    val newTs = Library.take (length (hd descr), recTs);
+
+    fun prep_constr (cname, cargs) = (cname, map (typ_of_dtyp descr' sorts) cargs);
+
+    fun make_distincts' _ [] = []
+      | make_distincts' T ((cname, cargs)::constrs) =
+          let
+            val frees = map Free ((make_tnames cargs) ~~ cargs);
+            val t = list_comb (Const (cname, cargs ---> T), frees);
+
+            fun make_distincts'' [] = []
+              | make_distincts'' ((cname', cargs')::constrs') =
+                  let
+                    val frees' = map Free ((map ((op ^) o (rpair "'"))
+                      (make_tnames cargs')) ~~ cargs');
+                    val t' = list_comb (Const (cname', cargs' ---> T), frees')
+                  in
+                    HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')) ::
+                    HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)) ::
+                      make_distincts'' constrs'
+                  end
+
+          in make_distincts'' constrs @ make_distincts' T constrs end;
+
+    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
+
+  in
+    map2 (fn ((_, (_, _, constrs))) => fn T =>
+      (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
+  end;
+
 (************************* injectivity of constructors ************************)
 
 fun make_injs descr sorts =
@@ -268,45 +305,6 @@
       ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f"))
   end;
 
-(************************* distinctness of constructors ***********************)
-
-fun make_distincts new_type_names descr sorts thy =
-  let
-    val descr' = List.concat descr;
-    val recTs = get_rec_types descr' sorts;
-    val newTs = Library.take (length (hd descr), recTs);
-
-    (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****)
-
-    fun make_distincts_1 _ [] = []
-      | make_distincts_1 T ((cname, cargs)::constrs) =
-          let
-            val Ts = map (typ_of_dtyp descr' sorts) cargs;
-            val frees = map Free ((make_tnames Ts) ~~ Ts);
-            val t = list_comb (Const (cname, Ts ---> T), frees);
-
-            fun make_distincts' [] = []
-              | make_distincts' ((cname', cargs')::constrs') =
-                  let
-                    val Ts' = map (typ_of_dtyp descr' sorts) cargs';
-                    val frees' = map Free ((map ((op ^) o (rpair "'"))
-                      (make_tnames Ts')) ~~ Ts');
-                    val t' = list_comb (Const (cname', Ts' ---> T), frees')
-                  in
-                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t')))::
-                    (HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t', t)))::
-                      (make_distincts' constrs')
-                  end
-
-          in (make_distincts' constrs) @ (make_distincts_1 T constrs)
-          end;
-
-  in map (fn (((_, (_, _, constrs)), T), tname) =>
-      if length constrs < Config.get_thy thy distinctness_limit
-      then make_distincts_1 T constrs else [])
-        ((hd descr) ~~ newTs ~~ new_type_names)
-  end;
-
 
 (*************************** the "split" - equations **************************)