--- 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;
--- 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,
--- 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;