# HG changeset patch # User haftmann # Date 1245761481 -7200 # Node ID 2b041d16cc13c5f3ca8ff01c61f2fb137b31812b # Parent f897fe880f9dba8ac19b1b517a4c857202770427# Parent 861e675f01e614ceaf84d3437f15896661fcb4ac merged diff -r f897fe880f9d -r 2b041d16cc13 src/HOL/Nominal/nominal.ML --- a/src/HOL/Nominal/nominal.ML Tue Jun 23 14:33:35 2009 +0200 +++ b/src/HOL/Nominal/nominal.ML Tue Jun 23 14:51:21 2009 +0200 @@ -243,7 +243,7 @@ val new_type_names' = map (fn n => n ^ "_Rep") new_type_names; val full_new_type_names' = map (Sign.full_bname thy) new_type_names'; - val ({induction, ...},thy1) = + val ((dt_names, {induction, ...}),thy1) = Datatype.add_datatype config new_type_names' dts'' thy; val SOME {descr, ...} = Symtab.lookup diff -r f897fe880f9d -r 2b041d16cc13 src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Tue Jun 23 14:33:35 2009 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Tue Jun 23 14:51:21 2009 +0200 @@ -101,7 +101,7 @@ val (_,thy1) = fold_map (fn ak => fn thy => let val dt = ([], Binding.name ak, NoSyn, [(Binding.name ak, [@{typ nat}], NoSyn)]) - val ({inject,case_thms,...},thy1) = Datatype.add_datatype + val ((dt_names, {inject,case_thms,...}),thy1) = Datatype.add_datatype Datatype.default_config [ak] [dt] thy val inject_flat = flat inject val ak_type = Type (Sign.intern_type thy1 ak,[]) diff -r f897fe880f9d -r 2b041d16cc13 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Tue Jun 23 14:33:35 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Jun 23 14:51:21 2009 +0200 @@ -7,19 +7,15 @@ signature DATATYPE = sig include DATATYPE_COMMON - type rules = {distinct : thm list list, - inject : thm list list, - exhaustion : thm list, - rec_thms : thm list, - case_thms : thm list list, - split_thms : (thm * thm) list, - induction : thm, - simps : thm list} val add_datatype : config -> string list -> (string list * binding * mixfix * - (binding * typ list * mixfix) list) list -> theory -> rules * theory + (binding * typ list * mixfix) list) list -> theory -> + (string list * {inject : thm list list, + rec_thms : thm list, + case_thms : thm list list, + induction : thm}) * theory val datatype_cmd : string list -> (string list * binding * mixfix * (binding * string list * mixfix) list) list -> theory -> theory - val rep_datatype : config -> (rules -> Proof.context -> Proof.context) + val rep_datatype : config -> (string list -> Proof.context -> Proof.context) -> string list option -> term list -> theory -> Proof.state val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state val get_datatypes : theory -> info Symtab.table @@ -334,15 +330,6 @@ case_cong = case_cong, weak_case_cong = weak_case_cong}); -type rules = {distinct : thm list list, - inject : thm list list, - exhaustion : thm list, - rec_thms : thm list, - case_thms : thm list list, - split_thms : (thm * thm) list, - induction : thm, - simps : thm list} - structure DatatypeInterpretation = InterpretationFun (type T = config * string list val eq: T * T -> bool = eq_snd op =); fun interpretation f = DatatypeInterpretation.interpretation (uncurry f); @@ -377,10 +364,11 @@ val dt_infos = map (make_dt_info (SOME new_type_names) (flat descr) sorts induct reccomb_names rec_thms) - ((0 upto length (hd descr) - 1) ~~ (hd descr) ~~ case_names ~~ case_thms ~~ + ((0 upto length (hd descr) - 1) ~~ hd descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~ simproc_dists ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); val simps = flat (distinct @ inject @ case_thms) @ rec_thms; + val dt_names = map fst dt_infos; val thy12 = thy10 @@ -394,14 +382,10 @@ |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeInterpretation.data (config, map fst dt_infos); in - ({distinct = distinct, - inject = inject, - exhaustion = casedist_thms, + ((dt_names, {inject = inject, rec_thms = rec_thms, case_thms = case_thms, - split_thms = split_thms, - induction = induct, - simps = simps}, thy12) + induction = induct}), thy12) end; @@ -457,6 +441,7 @@ map FewConstrs distinct ~~ inject ~~ nchotomys ~~ case_congs ~~ weak_case_congs); val simps = flat (distinct @ inject @ case_thms) @ rec_thms; + val dt_names = map fst dt_infos; val thy11 = thy10 @@ -468,17 +453,8 @@ |> Sign.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd - |> DatatypeInterpretation.data (config, map fst dt_infos); - in - ({distinct = distinct, - inject = inject, - exhaustion = casedist_thms, - rec_thms = rec_thms, - case_thms = case_thms, - split_thms = split_thms, - induction = induct', - simps = simps}, thy11) - end; + |> DatatypeInterpretation.data (config, dt_names); + in (dt_names, thy11) end; fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy = let diff -r f897fe880f9d -r 2b041d16cc13 src/HOL/Tools/inductive_realizer.ML --- a/src/HOL/Tools/inductive_realizer.ML Tue Jun 23 14:33:35 2009 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Tue Jun 23 14:51:21 2009 +0200 @@ -305,16 +305,17 @@ (** datatype representing computational content of inductive set **) - val ((dummies, dt_info), thy2) = + val ((dummies, (dt_names_rules)), thy2) = thy1 |> add_dummies (Datatype.add_datatype { strict = false, flat_names = false, quiet = false } (map (Binding.name_of o #2) dts)) (map (pair false) dts) [] ||> Extraction.add_typeof_eqns_i ty_eqs ||> Extraction.add_realizes_eqns_i rlz_eqs; - fun get f = (these oo Option.map) f; + val rec_thms = these (Option.map (#rec_thms o snd) dt_names_rules); + val case_thms = these (Option.map (#case_thms o snd) dt_names_rules); val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o - HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info)); + HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms); val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) => if member (op =) rsets s then let @@ -324,7 +325,7 @@ HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies')) end else (replicate (length rs) Extraction.nullt, (recs, dummies))) - rss (get #rec_thms dt_info, dummies); + rss (rec_thms, dummies); val rintrs = map (fn (intr, c) => Envir.eta_contract (Extraction.realizes_of thy2 vs (if c = Extraction.nullt then c else list_comb (c, map Var (rev @@ -386,8 +387,7 @@ end) (rlzs ~~ rnames); val concl = HOLogic.mk_Trueprop (foldr1 HOLogic.mk_conj (map (fn (_, _ $ P, _ $ Q) => HOLogic.mk_imp (P, Q)) rlzs')); - val rews = map mk_meta_eq - (fst_conv :: snd_conv :: get #rec_thms dt_info); + val rews = map mk_meta_eq (fst_conv :: snd_conv :: rec_thms); val thm = Goal.prove_global thy [] prems concl (fn {prems, ...} => EVERY [rtac (#raw_induct ind_info) 1, rewrite_goals_tac rews, @@ -417,7 +417,7 @@ (** realizer for elimination rules **) val case_names = map (fst o dest_Const o head_of o fst o HOLogic.dest_eq o - HOLogic.dest_Trueprop o prop_of o hd) (get #case_thms dt_info); + HOLogic.dest_Trueprop o prop_of o hd) case_thms; fun add_elim_realizer Ps (((((elim, elimR), intrs), case_thms), case_name), dummy) thy = @@ -476,7 +476,7 @@ val thy6 = Library.foldl (fn (thy, p as (((((elim, _), _), _), _), _)) => thy |> add_elim_realizer [] p |> add_elim_realizer [fst (fst (dest_Var (HOLogic.dest_Trueprop (concl_of elim))))] p) (thy5, - elimps ~~ get #case_thms dt_info ~~ case_names ~~ dummies) + elimps ~~ case_thms ~~ case_names ~~ dummies) in Sign.restore_naming thy thy6 end;