# HG changeset patch # User blanchet # Date 1370511221 -7200 # Node ID f461dca57c664c3ad27ac6ffbc2b103305c5c08e # Parent e2f6ac15d79a882dab315b7a00a7269f33d77476 tuned record field names to avoid confusion between low-level and high-level constants/theorems diff -r e2f6ac15d79a -r f461dca57c66 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 11:19:04 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 11:33:41 2013 +0200 @@ -1079,10 +1079,10 @@ map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctrXs_sum_prod_Ts; val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, - un_folds = fp_folds0, co_recs = fp_recs0, co_induct = fp_induct, - strong_co_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, + xtor_un_folds = fp_folds0, xtor_co_recs = fp_recs0, xtor_co_induct = fp_induct, + xtor_strong_co_induct = fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, set_thmss = fp_set_thmss, rel_thms = fp_rel_thms, - un_fold_thms = fp_fold_thms, co_rec_thms = fp_rec_thms, ...}, lthy)) = + xtor_un_fold_thms = fp_fold_thms, xtor_co_rec_thms = fp_rec_thms, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0; diff -r e2f6ac15d79a -r f461dca57c66 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 11:19:04 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 11:33:41 2013 +0200 @@ -15,18 +15,18 @@ bnfs: BNF_Def.bnf list, ctors: term list, dtors: term list, - un_folds: term list, - co_recs: term list, - co_induct: thm, - strong_co_induct: thm, + xtor_un_folds: term list, + xtor_co_recs: term list, + xtor_co_induct: thm, + xtor_strong_co_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, - un_fold_thms: thm list, - co_rec_thms: thm list} + xtor_un_fold_thms: thm list, + xtor_co_rec_thms: thm list} val morph_fp_result: morphism -> fp_result -> fp_result val eq_fp_result: fp_result * fp_result -> bool @@ -185,38 +185,38 @@ bnfs: BNF_Def.bnf list, ctors: term list, dtors: term list, - un_folds: term list, - co_recs: term list, - co_induct: thm, - strong_co_induct: thm, + xtor_un_folds: term list, + xtor_co_recs: term list, + xtor_co_induct: thm, + xtor_strong_co_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, - un_fold_thms: thm list, - co_rec_thms: thm list}; + xtor_un_fold_thms: thm list, + xtor_co_rec_thms: thm list}; -fun morph_fp_result phi {Ts, bnfs, ctors, dtors, un_folds, co_recs, co_induct, strong_co_induct, - dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, un_fold_thms, - co_rec_thms} = +fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_un_folds, xtor_co_recs, xtor_co_induct, + xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms, set_thmss, rel_thms, + xtor_un_fold_thms, xtor_co_rec_thms} = {Ts = map (Morphism.typ phi) Ts, bnfs = map (morph_bnf phi) bnfs, ctors = map (Morphism.term phi) ctors, dtors = map (Morphism.term phi) dtors, - un_folds = map (Morphism.term phi) un_folds, - co_recs = map (Morphism.term phi) co_recs, - co_induct = Morphism.thm phi co_induct, - strong_co_induct = Morphism.thm phi strong_co_induct, + xtor_un_folds = map (Morphism.term phi) xtor_un_folds, + xtor_co_recs = map (Morphism.term phi) xtor_co_recs, + xtor_co_induct = Morphism.thm phi xtor_co_induct, + xtor_strong_co_induct = Morphism.thm phi xtor_strong_co_induct, dtor_ctors = map (Morphism.thm phi) dtor_ctors, ctor_dtors = map (Morphism.thm phi) ctor_dtors, ctor_injects = map (Morphism.thm phi) ctor_injects, map_thms = map (Morphism.thm phi) map_thms, set_thmss = map (map (Morphism.thm phi)) set_thmss, rel_thms = map (Morphism.thm phi) rel_thms, - un_fold_thms = map (Morphism.thm phi) un_fold_thms, - co_rec_thms = map (Morphism.thm phi) co_rec_thms}; + xtor_un_fold_thms = map (Morphism.thm phi) xtor_un_fold_thms, + xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms}; fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) = eq_list eq_bnf (bnfs1, bnfs2); diff -r e2f6ac15d79a -r f461dca57c66 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 11:19:04 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 11:33:41 2013 +0200 @@ -3107,12 +3107,13 @@ bs thmss) in timer; - ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, un_folds = unfolds, co_recs = corecs, - co_induct = dtor_coinduct_thm, strong_co_induct = dtor_strong_coinduct_thm, - dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, + ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, xtor_un_folds = unfolds, + xtor_co_recs = corecs, xtor_co_induct = dtor_coinduct_thm, + xtor_strong_co_induct = dtor_strong_coinduct_thm, dtor_ctors = dtor_ctor_thms, + ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_dtor_map_thms, set_thmss = folded_dtor_set_thmss', - rel_thms = dtor_Jrel_thms, un_fold_thms = ctor_dtor_unfold_thms, - co_rec_thms = ctor_dtor_corec_thms}, + rel_thms = dtor_Jrel_thms, xtor_un_fold_thms = ctor_dtor_unfold_thms, + xtor_co_rec_thms = ctor_dtor_corec_thms}, lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end; diff -r e2f6ac15d79a -r f461dca57c66 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 11:19:04 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 11:33:41 2013 +0200 @@ -1856,11 +1856,12 @@ bs thmss) in timer; - ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs, - co_induct = ctor_induct_thm, strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, + ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_un_folds = folds, + xtor_co_recs = recs, xtor_co_induct = ctor_induct_thm, + xtor_strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms, - set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, un_fold_thms = ctor_fold_thms, - co_rec_thms = ctor_rec_thms}, + set_thmss = folded_ctor_set_thmss', rel_thms = ctor_Irel_thms, + xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms}, lthy |> Local_Theory.notes (common_notes @ notes) |> snd) end;