# HG changeset patch # User desharna # Date 1411735408 -7200 # Node ID b46874f2090fce9ce4e48a08221cf4807d7535ed # Parent 75ee8d49c724ae26e0a0d51a2d2b30898ea520c5 refactor fp_sugar move theorems diff -r 75ee8d49c724 -r b46874f2090f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:43:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:43:28 2014 +0200 @@ -14,7 +14,8 @@ ctr_sugar: Ctr_Sugar.ctr_sugar} type fp_bnf_sugar = - {rel_injects: thm list, + {map_thms: thm list, + rel_injects: thm list, rel_distincts: thm list} type fp_co_induct_sugar = @@ -37,7 +38,6 @@ absT_info: BNF_Comp.absT_info, fp_nesting_bnfs: BNF_Def.bnf list, live_nesting_bnfs: BNF_Def.bnf list, - maps: thm list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; @@ -163,11 +163,12 @@ type fp_ctr_sugar = {ctrXs_Tss: typ list list, ctr_defs: thm list, - ctr_sugar: Ctr_Sugar.ctr_sugar} + ctr_sugar: Ctr_Sugar.ctr_sugar}; type fp_bnf_sugar = - {rel_injects: thm list, - rel_distincts: thm list} + {map_thms: thm list, + rel_injects: thm list, + rel_distincts: thm list}; type fp_co_induct_sugar = {co_rec: term, @@ -176,7 +177,7 @@ co_rec_def: thm, co_rec_thms: thm list, co_rec_discs: thm list, - co_rec_selss: thm list list} + co_rec_selss: thm list list}; type fp_sugar = {T: typ, @@ -189,14 +190,14 @@ absT_info: absT_info, fp_nesting_bnfs: bnf list, live_nesting_bnfs: bnf list, - maps: 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_bnf_sugar phi ({map_thms, rel_injects, rel_distincts} : fp_bnf_sugar) = + {map_thms = map (Morphism.thm phi) map_thms, + rel_injects = map (Morphism.thm phi) rel_injects, + rel_distincts = map (Morphism.thm phi) rel_distincts}; fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, co_rec_discs, co_rec_selss} : fp_co_induct_sugar) = @@ -206,15 +207,15 @@ co_rec_def = Morphism.thm phi co_rec_def, 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} + co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss}; fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar} : fp_ctr_sugar) = {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, ctr_defs = map (Morphism.thm phi) ctr_defs, - ctr_sugar = morph_ctr_sugar phi ctr_sugar} + ctr_sugar = morph_ctr_sugar phi ctr_sugar}; fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs, - live_nesting_bnfs, maps, fp_ctr_sugar, fp_bnf_sugar, + live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar, fp_co_induct_sugar} : fp_sugar) = {T = Morphism.typ phi T, BT = Morphism.typ phi BT, @@ -226,7 +227,6 @@ absT_info = morph_absT_info phi absT_info, fp_nesting_bnfs = map (morph_bnf phi) fp_nesting_bnfs, live_nesting_bnfs = map (morph_bnf phi) live_nesting_bnfs, - maps = map (Morphism.thm phi) maps, fp_ctr_sugar = morph_fp_ctr_sugar phi fp_ctr_sugar, fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar, fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar}; @@ -279,7 +279,7 @@ register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs - live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss + live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss rel_distinctss noted = let @@ -288,13 +288,13 @@ {T = T, BT = nth BTs kk, X = nth Xs kk, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = nth pre_bnfs kk, absT_info = nth absT_infos kk, fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, - maps = nth mapss kk, fp_ctr_sugar = {ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk}, fp_bnf_sugar = - {rel_injects = nth rel_injectss kk, + {map_thms = nth map_thmss kk, + rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}, fp_co_induct_sugar = {co_rec = nth co_recs kk, @@ -2048,9 +2048,9 @@ |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list4 o split_list) o split_list; - fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs mapsx rel_injects + fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects rel_distincts setss = - injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss; + injects @ distincts @ case_thms @ co_recs @ map_thms @ rel_injects @ rel_distincts @ flat setss; fun mk_co_rec_transfer_goals lthy co_recs = let @@ -2078,7 +2078,7 @@ end; fun derive_note_induct_recs_thms_for_types - ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)), + ((((map_thmss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = let val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = @@ -2109,7 +2109,7 @@ end; val simp_thmss = - map6 mk_simp_thms ctr_sugars rec_thmss mapss rel_injectss rel_distinctss setss; + map6 mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss setss; val common_notes = (if nn > 1 then @@ -2135,7 +2135,7 @@ (fst (dest_Type (hd fpTs)) ^ (implode (map (prefix "_") (tl fp_b_names)))) inductN |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs - mapss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) + map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss rel_distinctss end; @@ -2155,7 +2155,7 @@ end; fun derive_note_coinduct_corecs_thms_for_types - ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)), + ((((map_thmss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = let val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], @@ -2216,7 +2216,7 @@ val simp_thmss = map6 mk_simp_thms ctr_sugars (map3 flat_corec_thms corec_disc_thmss corec_disc_iff_thmss corec_sel_thmss) - mapss rel_injectss rel_distinctss setss; + map_thmss rel_injectss rel_distinctss setss; val common_notes = (set_inductN, set_induct_thms, nth set_induct_attrss) :: @@ -2247,7 +2247,7 @@ |> Local_Theory.notes (common_notes @ notes) |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs - mapss [coinduct_thm, coinduct_strong_thm] + map_thmss [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss end; diff -r 75ee8d49c724 -r b46874f2090f src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:43:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:43:28 2014 +0200 @@ -145,7 +145,7 @@ end; val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0; - val mapss = map #maps fp_sugars0; + val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0; val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; val ctrss = map #ctrs ctr_sugars; @@ -292,17 +292,18 @@ val phi = Proof_Context.export_morphism names_lthy no_defs_lthy; 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 + co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss ({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, maps = maps, + live_nesting_bnfs = live_nesting_bnfs, fp_ctr_sugar = {ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar}, fp_bnf_sugar = - {rel_injects = rel_injects, + {map_thms = map_thms, + rel_injects = rel_injects, rel_distincts = rel_distincts}, fp_co_induct_sugar = {co_rec = co_rec, diff -r 75ee8d49c724 -r b46874f2090f src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:43:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:43:28 2014 +0200 @@ -400,7 +400,7 @@ | _ => not_codatatype ctxt res_T); fun map_thms_of_typ ctxt (Type (s, _)) = - (case fp_sugar_of ctxt s of SOME {maps, ...} => maps | NONE => []) + (case fp_sugar_of ctxt s of SOME {fp_bnf_sugar = {map_thms, ...}, ...} => map_thms | NONE => []) | map_thms_of_typ _ _ = []; fun corec_specs_of bs arg_Ts res_Ts callers callssss0 lthy0 = diff -r 75ee8d49c724 -r b46874f2090f src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:43:26 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:43:28 2014 +0200 @@ -76,13 +76,13 @@ absT_info = trivial_absT_info_of fpT, fp_nesting_bnfs = [], live_nesting_bnfs = [], - maps = @{thms map_sum.simps}, fp_ctr_sugar = {ctrXs_Tss = ctr_Tss, ctr_defs = @{thms Inl_def_alt Inr_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, fp_bnf_sugar = - {rel_injects = @{thms rel_sum_simps(1,4)}, + {map_thms = @{thms map_sum.simps}, + 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 = {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), @@ -120,13 +120,13 @@ absT_info = trivial_absT_info_of fpT, fp_nesting_bnfs = [], live_nesting_bnfs = [], - maps = @{thms map_prod_simp}, fp_ctr_sugar = {ctrXs_Tss = [ctr_Ts], ctr_defs = @{thms Pair_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name}, fp_bnf_sugar = - {rel_injects = @{thms rel_prod_apply}, + {map_thms = @{thms map_prod_simp}, + rel_injects = @{thms rel_prod_apply}, rel_distincts = []}, fp_co_induct_sugar = {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),