# HG changeset patch # User desharna # Date 1411735268 -7200 # Node ID 0c9d59cb3af9ab41ed7defaf8c3336c782228fe6 # Parent 01d9908477b36ce99f63876834abe297c8108a98 refactor fp_sugar move theorems diff -r 01d9908477b3 -r 0c9d59cb3af9 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:36:54 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:41:08 2014 +0200 @@ -9,7 +9,11 @@ signature BNF_FP_DEF_SUGAR = sig type fp_ctr_sugar = {} - type fp_bnf_sugar = {} + + type fp_bnf_sugar = + {rel_injects: thm list, + rel_distincts: thm list} + type fp_co_induct_sugar = {} type fp_sugar = @@ -34,8 +38,6 @@ co_rec_thms: thm list, co_rec_discs: thm list, co_rec_selss: thm list list, - rel_injects: thm list, - rel_distincts: thm list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; @@ -159,7 +161,11 @@ val set_selN = "set_sel"; type fp_ctr_sugar = {} -type fp_bnf_sugar = {} + +type fp_bnf_sugar = + {rel_injects: thm list, + rel_distincts: thm list} + type fp_co_induct_sugar = {} type fp_sugar = @@ -184,16 +190,18 @@ co_rec_thms: thm list, co_rec_discs: thm list, co_rec_selss: thm list list, - rel_injects: thm list, - rel_distincts: thm list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; +fun morph_fp_bnf_sugar phi ({rel_injects, rel_distincts} : fp_bnf_sugar) = + {rel_injects = map (Morphism.thm phi) rel_injects, + rel_distincts = map (Morphism.thm phi) rel_distincts} + fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs, live_nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts, - co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, rel_injects, rel_distincts, - fp_ctr_sugar, fp_bnf_sugar, fp_co_induct_sugar} : fp_sugar) = + co_inducts, co_rec_thms, co_rec_discs, co_rec_selss, fp_ctr_sugar, fp_bnf_sugar, + fp_co_induct_sugar} : fp_sugar) = {T = Morphism.typ phi T, BT = Morphism.typ phi BT, X = Morphism.typ phi X, @@ -215,10 +223,8 @@ co_rec_thms = map (Morphism.thm phi) co_rec_thms, co_rec_discs = map (Morphism.thm phi) co_rec_discs, co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss, - rel_injects = map (Morphism.thm phi) rel_injects, - rel_distincts = map (Morphism.thm phi) rel_distincts, fp_ctr_sugar = fp_ctr_sugar, - fp_bnf_sugar = fp_bnf_sugar, + fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar, fp_co_induct_sugar = fp_co_induct_sugar}; val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism; @@ -282,8 +288,8 @@ co_rec = nth co_recs kk, co_rec_def = nth co_rec_defs kk, maps = nth mapss kk, common_co_inducts = common_co_inducts, co_inducts = nth co_inductss kk, co_rec_thms = nth co_rec_thmss kk, co_rec_discs = nth co_rec_discss kk, - co_rec_selss = nth co_rec_selsss kk, rel_injects = nth rel_injectss kk, - rel_distincts = nth rel_distinctss kk, fp_ctr_sugar = {}, fp_bnf_sugar = {}, + co_rec_selss = nth co_rec_selsss kk, fp_ctr_sugar = {}, + fp_bnf_sugar = {rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}, fp_co_induct_sugar = {}} |> morph_fp_sugar (substitute_noted_thm noted)) Ts; in diff -r 01d9908477b3 -r 0c9d59cb3af9 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:36:54 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:08 2014 +0200 @@ -293,15 +293,15 @@ fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec co_rec_def maps co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss - ({rel_injects, rel_distincts, ...} : fp_sugar) = + ({fp_bnf_sugar = {rel_injects, rel_distincts, ...}, ...} : fp_sugar) = {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, co_rec = co_rec, co_rec_def = co_rec_def, maps = maps, common_co_inducts = common_co_inducts, co_inducts = co_inducts, co_rec_thms = co_rec_thms, co_rec_discs = co_rec_disc_thms, - co_rec_selss = co_rec_sel_thmss, rel_injects = rel_injects, - rel_distincts = rel_distincts, fp_ctr_sugar = {}, fp_bnf_sugar = {}, + co_rec_selss = co_rec_sel_thmss, fp_ctr_sugar = {}, + fp_bnf_sugar = {rel_injects = rel_injects, rel_distincts = rel_distincts}, fp_co_induct_sugar = {}} |> morph_fp_sugar phi; diff -r 01d9908477b3 -r 0c9d59cb3af9 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:36:54 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:08 2014 +0200 @@ -87,10 +87,10 @@ co_rec_thms = @{thms sum.case}, co_rec_discs = [], co_rec_selss = [], - rel_injects = @{thms rel_sum_simps(1,4)}, - rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}, fp_ctr_sugar = {}, - fp_bnf_sugar = {}, + fp_bnf_sugar = { + rel_injects = @{thms rel_sum_simps(1,4)}, + rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, fp_co_induct_sugar = {}} end; @@ -131,10 +131,10 @@ co_rec_thms = @{thms prod.case}, co_rec_discs = [], co_rec_selss = [], - rel_injects = @{thms rel_prod_apply}, - rel_distincts = [], fp_ctr_sugar = {}, - fp_bnf_sugar = {}, + fp_bnf_sugar = { + rel_injects = @{thms rel_prod_apply}, + rel_distincts = []}, fp_co_induct_sugar = {}} end; diff -r 01d9908477b3 -r 0c9d59cb3af9 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 26 14:36:54 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Sep 26 14:41:08 2014 +0200 @@ -348,7 +348,7 @@ else thm RS (@{thm eq_onp_same_args} RS iffD1)) |> kill_top end - val rel_injects = #rel_injects fp_sugar + val rel_injects = #rel_injects (#fp_bnf_sugar fp_sugar) in rel_injects |> map (Local_Defs.unfold lthy [@{thm conj_assoc}])