# HG changeset patch # User haftmann # Date 1211551504 -7200 # Node ID cf3f998d063187759407d46426081f3cb7488eb8 # Parent bb0a56a66180a91b34f0374c2dd9e05f495f46ad moved case distinction over number of constructors for distinctness rules from DatatypeProp to DatatypeRepProofs diff -r bb0a56a66180 -r cf3f998d0631 src/HOL/Nominal/nominal_package.ML --- a/src/HOL/Nominal/nominal_package.ML Fri May 23 16:05:02 2008 +0200 +++ b/src/HOL/Nominal/nominal_package.ML Fri May 23 16:05:04 2008 +0200 @@ -850,26 +850,22 @@ (* prove distinctness theorems *) - val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit; - val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8; - val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8'; - val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8'; - + 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); - fun prove_distinct_thms (_, []) = [] - | prove_distinct_thms (p as (rep_thms, dist_lemma), t::ts) = + 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, ts)) + in dist_thm :: (standard (dist_thm RS not_sym)) :: + (prove_distinct_thms p (k, ts)) end; - val distinct_thms = map prove_distinct_thms - (constr_rep_thmss ~~ dist_lemmas ~~ distinct_props); + val distinct_thms = map2 prove_distinct_thms + (constr_rep_thmss ~~ dist_lemmas) distinct_props; (** prove equations for permutation functions **) diff -r bb0a56a66180 -r cf3f998d0631 src/HOL/Tools/datatype_prop.ML --- a/src/HOL/Tools/datatype_prop.ML Fri May 23 16:05:02 2008 +0200 +++ b/src/HOL/Tools/datatype_prop.ML Fri May 23 16:05:04 2008 +0200 @@ -12,6 +12,8 @@ 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 + val make_distincts : DatatypeAux.descr list -> + (string * sort) list -> (int * term list) list 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 -> @@ -20,8 +22,6 @@ (string * sort) list -> theory -> term list val make_cases : string list -> DatatypeAux.descr list -> (string * sort) list -> theory -> term list list - val make_distincts : string list -> DatatypeAux.descr list -> - (string * sort) list -> theory -> term list list val make_splits : string list -> DatatypeAux.descr list -> (string * sort) list -> theory -> (term * term) list val make_weak_case_congs : string list -> DatatypeAux.descr list -> @@ -59,6 +59,43 @@ 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; + + (**** 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 + end; + (************************* injectivity of constructors ************************) fun make_injs descr sorts = @@ -268,45 +305,6 @@ ((hd descr) ~~ newTs ~~ (make_case_combs new_type_names descr sorts thy "f")) end; -(************************* distinctness of constructors ***********************) - -fun make_distincts new_type_names descr sorts thy = - let - val descr' = List.concat descr; - val recTs = get_rec_types descr' sorts; - val newTs = Library.take (length (hd descr), recTs); - - (**** number of constructors < distinctness_limit : C_i ... ~= C_j ... ****) - - fun make_distincts_1 _ [] = [] - | make_distincts_1 T ((cname, cargs)::constrs) = - let - val Ts = map (typ_of_dtyp descr' sorts) cargs; - val frees = map Free ((make_tnames Ts) ~~ Ts); - val t = list_comb (Const (cname, Ts ---> T), frees); - - fun make_distincts' [] = [] - | make_distincts' ((cname', cargs')::constrs') = - let - val Ts' = map (typ_of_dtyp descr' sorts) cargs'; - val frees' = map Free ((map ((op ^) o (rpair "'")) - (make_tnames Ts')) ~~ Ts'); - val t' = list_comb (Const (cname', Ts' ---> 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_1 T constrs) - end; - - in map (fn (((_, (_, _, constrs)), T), tname) => - if length constrs < Config.get_thy thy distinctness_limit - then make_distincts_1 T constrs else []) - ((hd descr) ~~ newTs ~~ new_type_names) - end; - (*************************** the "split" - equations **************************) diff -r bb0a56a66180 -r cf3f998d0631 src/HOL/Tools/datatype_rep_proofs.ML --- a/src/HOL/Tools/datatype_rep_proofs.ML Fri May 23 16:05:02 2008 +0200 +++ b/src/HOL/Tools/datatype_rep_proofs.ML Fri May 23 16:05:04 2008 +0200 @@ -519,17 +519,21 @@ 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 (dist_rewrites', 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_distinct_thms (dist_rewrites', ts)) - end; + fun prove_distinct_thms _ _ (_, []) = [] + | prove_distinct_thms lim dist_rewrites' (k, ts as _ :: _) = + if k >= lim then [] else 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 = map prove_distinct_thms (dist_rewrites ~~ - DatatypeProp.make_distincts new_type_names descr sorts thy5); + val distincts = DatatypeProp.make_distincts descr sorts; + val distinct_thms = map2 (prove_distinct_thms + (Config.get_thy thy5 DatatypeProp.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