# HG changeset patch # User blanchet # Date 1370512031 -7200 # Node ID 9606cf6770214147ae8acc57b79fc7b2934b5b10 # Parent 62f794b9e9ccd1085871643c28086ecc81149943 continuation of f461dca57c66 diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 11:41:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Thu Jun 06 11:47:11 2013 +0200 @@ -1080,9 +1080,8 @@ val (pre_bnfs, (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0, dtors = dtors0, xtor_un_folds = xtor_un_folds0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, - xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, map_thms = fp_map_thms, - set_thmss = fp_set_thmss, rel_thms = fp_rel_thms, xtor_un_fold_thms, xtor_co_rec_thms = - xtor_co_rec_thms, ...}, lthy)) = + xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, + xtor_set_thmss, xtor_rel_thms, xtor_un_fold_thms, xtor_co_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; @@ -1436,9 +1435,9 @@ val lthy' = lthy |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ xtor_un_folds ~~ xtor_co_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~ - pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~ - mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ - raw_sel_defaultsss) + pre_set_defss ~~ pre_rel_defs ~~ xtor_map_thms ~~ xtor_set_thmss ~~ xtor_rel_thms ~~ ns ~~ + kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ + sel_bindingsss ~~ raw_sel_defaultsss) |> wrap_types_etc |> (if fp = Least_FP then derive_and_note_induct_fold_rec_thms_for_types else derive_and_note_coinduct_unfold_corec_thms_for_types); diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 11:41:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jun 06 11:47:11 2013 +0200 @@ -22,9 +22,9 @@ 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, + xtor_map_thms: thm list, + xtor_set_thmss: thm list list, + xtor_rel_thms: thm list, xtor_un_fold_thms: thm list, xtor_co_rec_thms: thm list} @@ -192,15 +192,15 @@ 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, + xtor_map_thms: thm list, + xtor_set_thmss: thm list list, + xtor_rel_thms: thm list, xtor_un_fold_thms: thm list, xtor_co_rec_thms: thm list}; 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} = + xtor_strong_co_induct, dtor_ctors, ctor_dtors, ctor_injects, xtor_map_thms, xtor_set_thmss, + xtor_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, @@ -212,9 +212,9 @@ 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, + xtor_map_thms = map (Morphism.thm phi) xtor_map_thms, + xtor_set_thmss = map (map (Morphism.thm phi)) xtor_set_thmss, + xtor_rel_thms = map (Morphism.thm phi) xtor_rel_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}; diff -r 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 11:41:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jun 06 11:47:11 2013 +0200 @@ -3111,8 +3111,8 @@ 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, xtor_un_fold_thms = ctor_dtor_unfold_thms, + xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss', + xtor_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 62f794b9e9cc -r 9606cf677021 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 11:41:19 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jun 06 11:47:11 2013 +0200 @@ -1859,9 +1859,10 @@ ({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, - xtor_un_fold_thms = ctor_fold_thms, xtor_co_rec_thms = ctor_rec_thms}, + ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, + xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss', + xtor_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;