# HG changeset patch # User haftmann # Date 1213988422 -7200 # Node ID 4cb3101d2bf779ba871acdffcc0944ae2c8ac75b # Parent 3447cd2e18e88de0c3a9b0e35bfdc2a6e6842082 DatatypeProp.make_distincts: only one half of each symmetric pair is constructed diff -r 3447cd2e18e8 -r 4cb3101d2bf7 src/HOL/Nominal/nominal_package.ML --- 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 diff -r 3447cd2e18e8 -r 4cb3101d2bf7 src/HOL/Tools/datatype_package.ML --- 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 diff -r 3447cd2e18e8 -r 4cb3101d2bf7 src/HOL/Tools/datatype_prop.ML --- 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 = diff -r 3447cd2e18e8 -r 4cb3101d2bf7 src/HOL/Tools/datatype_rep_proofs.ML --- 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