# HG changeset patch # User blanchet # Date 1367247001 -7200 # Node ID 9df935196be99602db8e267ebcd53435e5517cf8 # Parent 517f232e867d4f01870a20c57bcdc266e925327c use record instead of big tuple diff -r 517f232e867d -r 9df935196be9 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Apr 29 15:47:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Mon Apr 29 16:50:01 2013 +0200 @@ -8,8 +8,15 @@ signature BNF_CTR_SUGAR = sig type ctr_wrap_result = - term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list * - thm list list + {discs: term list, + selss: term list list, + exhaust: thm, + injects: thm list, + distincts: thm list, + case_thms: thm list, + disc_thmss: thm list list, + discIs: thm list, + sel_thmss: thm list list}; val rep_compat_prefix: string @@ -37,8 +44,15 @@ open BNF_Ctr_Sugar_Tactics type ctr_wrap_result = - term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list * - thm list list; + {discs: term list, + selss: term list list, + exhaust: thm, + injects: thm list, + distincts: thm list, + case_thms: thm list, + disc_thmss: thm list list, + discIs: thm list, + sel_thmss: thm list list}; val rep_compat_prefix = "new"; @@ -671,14 +685,15 @@ [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); in - ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms, - sel_thmss), - lthy - |> not rep_compat ? - (Local_Theory.declaration {syntax = false, pervasive = true} + ({discs = discs, selss = selss, exhaust = exhaust_thm, injects = inject_thms, + distincts = distinct_thms, case_thms = case_thms, disc_thmss = disc_thmss, + discIs = discI_thms, sel_thmss = sel_thmss}, + lthy + |> not rep_compat ? + (Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Case_Translation.register - (Morphism.term phi casex) (map (Morphism.term phi) ctrs))) - |> Local_Theory.notes (notes' @ notes) |> snd) + (Morphism.term phi casex) (map (Morphism.term phi) ctrs))) + |> Local_Theory.notes (notes' @ notes) |> snd) end; in (goalss, after_qed, lthy') diff -r 517f232e867d -r 9df935196be9 src/HOL/BNF/Tools/bnf_fp.ML --- a/src/HOL/BNF/Tools/bnf_fp.ML Mon Apr 29 15:47:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp.ML Mon Apr 29 16:50:01 2013 +0200 @@ -8,21 +8,21 @@ signature BNF_FP = sig type fp_result = - {bnfs : BNF_Def.BNF list, - dtors : term list, - ctors : term list, - folds : term list, - recs : term list, - induct : thm, - strong_induct : thm, - dtor_ctors : thm list, - ctor_dtors : thm list, - ctor_injects : thm list, - map_thms : thm list, - set_thmss : thm list list, - rel_thms : thm list, - fold_thms : thm list, - rec_thms : thm list} + {bnfs: BNF_Def.BNF list, + dtors: term list, + ctors: term list, + folds: term list, + recs: term list, + induct: thm, + strong_induct: thm, + dtor_ctors: thm list, + ctor_dtors: thm list, + ctor_injects: thm list, + map_thms: thm list, + set_thmss: thm list list, + rel_thms: thm list, + fold_thms: thm list, + rec_thms: thm list} val time: Timer.real_timer -> string -> Timer.real_timer @@ -168,21 +168,21 @@ open BNF_Util type fp_result = - {bnfs : BNF_Def.BNF list, - dtors : term list, - ctors : term list, - folds : term list, - recs : term list, - induct : thm, - strong_induct : thm, - dtor_ctors : thm list, - ctor_dtors : thm list, - ctor_injects : thm list, - map_thms : thm list, - set_thmss : thm list list, - rel_thms : thm list, - fold_thms : thm list, - rec_thms : thm list}; + {bnfs: BNF_Def.BNF list, + dtors: term list, + ctors: term list, + folds: term list, + recs: term list, + induct: thm, + strong_induct: thm, + dtor_ctors: thm list, + ctor_dtors: thm list, + ctor_injects: thm list, + map_thms: thm list, + set_thmss: thm list list, + rel_thms: thm list, + fold_thms: thm list, + rec_thms: thm list}; val timing = true; fun time timer msg = (if timing diff -r 517f232e867d -r 9df935196be9 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Apr 29 15:47:42 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Apr 29 16:50:01 2013 +0200 @@ -369,12 +369,12 @@ val fp_b_names = map base_name_of_typ fpTs; - val discss = map (map (mk_disc_or_sel As) o #1) ctr_wrap_ress; - val selsss = map (map (map (mk_disc_or_sel As)) o #2) ctr_wrap_ress; - val exhaust_thms = map #3 ctr_wrap_ress; - val disc_thmsss = map #7 ctr_wrap_ress; - val discIss = map #8 ctr_wrap_ress; - val sel_thmsss = map #9 ctr_wrap_ress; + val discss = map (map (mk_disc_or_sel As) o #discs) ctr_wrap_ress; + val selsss = map (map (map (mk_disc_or_sel As)) o #selss) ctr_wrap_ress; + val exhausts = map #exhaust ctr_wrap_ress; + val disc_thmsss = map #disc_thmss ctr_wrap_ress; + val discIss = map #discIs ctr_wrap_ress; + val sel_thmsss = map #sel_thmss ctr_wrap_ress; val (((rs, us'), vs'), names_lthy) = lthy @@ -440,7 +440,7 @@ fun prove dtor_coinduct' goal = Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors - exhaust_thms ctr_defss disc_thmsss sel_thmsss) + exhausts ctr_defss disc_thmsss sel_thmsss) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation; @@ -1202,8 +1202,8 @@ (* TODO: Add map, sets, rel simps *) val mk_simp_thmss = - map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes => - injects @ distincts @ cases @ rec_likes @ fold_likes); + map3 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes => + injects @ distincts @ case_thms @ rec_likes @ fold_likes); fun derive_and_note_induct_fold_rec_thms_for_types (((ctrss, xsss, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) =