# HG changeset patch # User haftmann # Date 1211978930 -7200 # Node ID 215d64dc971e61b4fecc6a7b8f7ac266d9acaf45 # Parent d21bb9f733640c12b38aa5bfc3d63e09a6cd166e moved distinctness_limit to datatype_rep_proofs.ML diff -r d21bb9f73364 -r 215d64dc971e src/HOL/Tools/datatype_package.ML --- 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 #> diff -r d21bb9f73364 -r 215d64dc971e src/HOL/Tools/datatype_prop.ML --- 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 diff -r d21bb9f73364 -r 215d64dc971e src/HOL/Tools/datatype_rep_proofs.ML --- 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);