--- a/src/HOL/Tools/datatype_package.ML Wed May 28 12:24:48 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML Wed May 28 14:48:50 2008 +0200
@@ -781,7 +781,7 @@
(* setup theory *)
val setup =
- DatatypeProp.distinctness_limit_setup #>
+ DatatypeRepProofs.distinctness_limit_setup #>
Method.add_methods tactic_emulations #>
simproc_setup #>
trfun_setup #>
--- a/src/HOL/Tools/datatype_prop.ML Wed May 28 12:24:48 2008 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Wed May 28 14:48:50 2008 +0200
@@ -7,8 +7,6 @@
signature DATATYPE_PROP =
sig
- val distinctness_limit : int Config.T
- val distinctness_limit_setup : theory -> theory
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
@@ -37,10 +35,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" 7;
-
fun indexify_names names =
let
fun index (x :: xs) tab =
@@ -89,8 +83,6 @@
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
--- a/src/HOL/Tools/datatype_rep_proofs.ML Wed May 28 12:24:48 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Wed May 28 14:48:50 2008 +0200
@@ -13,6 +13,8 @@
signature DATATYPE_REP_PROOFS =
sig
+ val distinctness_limit : int Config.T
+ val distinctness_limit_setup : theory -> theory
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> DatatypeAux.descr list -> (string * sort) list ->
(string * mixfix) list -> (string * mixfix) list list -> attribute
@@ -25,6 +27,10 @@
open DatatypeAux;
+(*the kind of distinctiveness axioms depends on number of constructors*)
+val (distinctness_limit, distinctness_limit_setup) =
+ Attrib.config_int "datatype_distinctness_limit" 7;
+
val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
@@ -522,6 +528,7 @@
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
@@ -532,11 +539,10 @@
val distincts = DatatypeProp.make_distincts descr sorts;
val distinct_thms = map2 (prove_distinct_thms
- (Config.get_thy thy5 DatatypeProp.distinctness_limit))
- dist_rewrites distincts;
+ (Config.get_thy thy5 distinctness_limit)) dist_rewrites distincts;
val simproc_dists = map (fn ((((_, (_, _, constrs)), rep_thms), congr), dists) =>
- if length constrs < Config.get_thy thy5 DatatypeProp.distinctness_limit
+ 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);