--- a/src/HOL/Nominal/nominal_package.ML Fri Jun 20 21:00:21 2008 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Fri Jun 20 21:00:22 2008 +0200
@@ -844,17 +844,17 @@
(* prove distinctness theorems *)
val distinct_props = DatatypeProp.make_distincts descr' sorts';
- val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
- dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
- (constr_rep_thmss ~~ dist_lemmas);
+ val dist_rewrites = map2 (fn rep_thms => fn dist_lemma =>
+ dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])
+ constr_rep_thmss dist_lemmas;
fun prove_distinct_thms _ (_, []) = []
| prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
let
val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
- in dist_thm :: (standard (dist_thm RS not_sym)) ::
- (prove_distinct_thms p (k, ts))
+ in dist_thm :: standard (dist_thm RS not_sym) ::
+ prove_distinct_thms p (k, ts)
end;
val distinct_thms = map2 prove_distinct_thms
--- a/src/HOL/Tools/datatype_package.ML Fri Jun 20 21:00:21 2008 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Jun 20 21:00:22 2008 +0200
@@ -409,7 +409,7 @@
(*********************** declare existing type as datatype *********************)
-fun prove_rep_datatype alt_names new_type_names descr sorts induct inject distinct thy =
+fun prove_rep_datatype alt_names new_type_names descr sorts induct inject half_distinct thy =
let
val ((_, [induct']), _) =
Variable.importT_thms [induct] (Variable.thm_context induct);
@@ -424,6 +424,7 @@
val dt_info = get_datatypes thy;
+ val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
val (case_names_induct, case_names_exhausts) =
(mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
@@ -526,18 +527,18 @@
(map o apsnd) dtyps_of_typ constr))
val descr = map_index mk_spec cs;
val injs = DatatypeProp.make_injs [descr] vs;
- val distincts = map snd (DatatypeProp.make_distincts [descr] vs);
+ val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
val ind = DatatypeProp.make_ind [descr] vs;
- val rules = (map o map o map) Logic.close_form [[[ind]], injs, distincts];
+ val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
fun after_qed' raw_thms =
let
- val [[[induct]], injs, distincts] =
+ val [[[induct]], injs, half_distincts] =
unflat rules (map Drule.zero_var_indexes_list raw_thms);
(*FIXME somehow dubious*)
in
ProofContext.theory_result
- (prove_rep_datatype alt_names new_type_names descr vs induct injs distincts)
+ (prove_rep_datatype alt_names new_type_names descr vs induct injs half_distincts)
#-> after_qed
end;
in
--- a/src/HOL/Tools/datatype_prop.ML Fri Jun 20 21:00:21 2008 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Fri Jun 20 21:00:22 2008 +0200
@@ -11,7 +11,7 @@
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
+ (string * sort) list -> (int * term list) list (*no symmetric inequalities*)
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 ->
@@ -53,41 +53,6 @@
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;
-
- 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 =
@@ -111,6 +76,40 @@
(hd descr) (Library.take (length (hd descr), get_rec_types descr' sorts))
end;
+
+(************************* distinctness of constructors ***********************)
+
+fun make_distincts descr sorts =
+ let
+ val descr' = flat 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'' (cname', cargs') =
+ 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'))
+ end
+
+ in map make_distincts'' constrs @ make_distincts' T constrs end;
+
+ in
+ map2 (fn ((_, (_, _, constrs))) => fn T =>
+ (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs
+ end;
+
+
(********************************* induction **********************************)
fun make_ind descr sorts =
--- a/src/HOL/Tools/datatype_rep_proofs.ML Fri Jun 20 21:00:21 2008 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri Jun 20 21:00:22 2008 +0200
@@ -530,16 +530,16 @@
if k >= lim then [] else let
(*number of constructors < distinctness_limit : C_i ... ~= C_j ...*)
fun prove [] = []
- | prove (t :: _ :: ts) =
+ | 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 distincts = DatatypeProp.make_distincts descr sorts;
- val distinct_thms = map2 (prove_distinct_thms
- (Config.get_thy thy5 distinctness_limit)) dist_rewrites distincts;
+ 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