# HG changeset patch # User desharna # Date 1411735275 -7200 # Node ID f70bffabd7cfcb39f995d506cf2223cb32774bff # Parent 0c9d59cb3af9ab41ed7defaf8c3336c782228fe6 refactor fp_sugar move theorems diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Library/bnf_lfp_countable.ML --- a/src/HOL/Library/bnf_lfp_countable.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Library/bnf_lfp_countable.ML Fri Sep 26 14:41:15 2014 +0200 @@ -159,7 +159,7 @@ val recs0 = map #co_rec fp_sugars; val nchotomys = map #nchotomy ctr_sugars; val injectss = map #injects ctr_sugars; - val rec_thmss = map #co_rec_thms fp_sugars; + val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars; val map_comps' = map (unfold_thms ctxt @{thms comp_def} o map_comp_of_bnf) fp_nesting_bnfs; val inj_map_strongs' = map (Thm.permute_prems 0 ~1 o inj_map_strong_of_bnf) fp_nesting_bnfs; diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 26 14:41:15 2014 +0200 @@ -14,7 +14,11 @@ {rel_injects: thm list, rel_distincts: thm list} - type fp_co_induct_sugar = {} + type fp_co_induct_sugar = + {co_inducts: thm list, + co_rec_thms: thm list, + co_rec_discs: thm list, + co_rec_selss: thm list list} type fp_sugar = {T: typ, @@ -34,10 +38,6 @@ co_rec_def: thm, maps: thm list, common_co_inducts: thm list, - co_inducts: thm list, - co_rec_thms: thm list, - co_rec_discs: thm list, - co_rec_selss: thm list list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; @@ -166,7 +166,11 @@ {rel_injects: thm list, rel_distincts: thm list} -type fp_co_induct_sugar = {} +type fp_co_induct_sugar = + {co_inducts: thm list, + co_rec_thms: thm list, + co_rec_discs: thm list, + co_rec_selss: thm list list} type fp_sugar = {T: typ, @@ -186,10 +190,6 @@ co_rec_def: thm, maps: thm list, common_co_inducts: thm list, - co_inducts: thm list, - co_rec_thms: thm list, - co_rec_discs: thm list, - co_rec_selss: thm list list, fp_ctr_sugar: fp_ctr_sugar, fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; @@ -198,10 +198,16 @@ {rel_injects = map (Morphism.thm phi) rel_injects, rel_distincts = map (Morphism.thm phi) rel_distincts} +fun morph_fp_co_induct_sugar phi ({co_inducts, co_rec_thms, co_rec_discs, + co_rec_selss} : fp_co_induct_sugar) = + {co_inducts = map (Morphism.thm phi) co_inducts, + 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} + 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, fp_ctr_sugar, fp_bnf_sugar, - fp_co_induct_sugar} : fp_sugar) = + 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, @@ -219,13 +225,9 @@ co_rec_def = Morphism.thm phi co_rec_def, maps = map (Morphism.thm phi) maps, common_co_inducts = map (Morphism.thm phi) common_co_inducts, - co_inducts = map (Morphism.thm phi) co_inducts, - 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, fp_ctr_sugar = fp_ctr_sugar, fp_bnf_sugar = morph_fp_bnf_sugar phi fp_bnf_sugar, - fp_co_induct_sugar = fp_co_induct_sugar}; + fp_co_induct_sugar = morph_fp_co_induct_sugar phi fp_co_induct_sugar}; val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism; @@ -286,11 +288,16 @@ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, 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, fp_ctr_sugar = {}, - fp_bnf_sugar = {rel_injects = nth rel_injectss kk, rel_distincts = nth rel_distinctss kk}, - fp_co_induct_sugar = {}} + common_co_inducts = common_co_inducts, + fp_ctr_sugar = {}, + fp_bnf_sugar = + {rel_injects = nth rel_injectss kk, + rel_distincts = nth rel_distinctss kk}, + fp_co_induct_sugar = + {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}} |> morph_fp_sugar (substitute_noted_thm noted)) Ts; in register_fp_sugars_raw fp_sugars diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Fri Sep 26 14:41:15 2014 +0200 @@ -298,11 +298,16 @@ 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, fp_ctr_sugar = {}, - fp_bnf_sugar = {rel_injects = rel_injects, rel_distincts = rel_distincts}, - fp_co_induct_sugar = {}} + common_co_inducts = common_co_inducts, + fp_ctr_sugar = {}, + fp_bnf_sugar = + {rel_injects = rel_injects, + rel_distincts = rel_distincts}, + fp_co_induct_sugar = + {co_inducts = co_inducts, + co_rec_thms = co_rec_thms, + co_rec_discs = co_rec_disc_thms, + co_rec_selss = co_rec_sel_thmss}} |> morph_fp_sugar phi; val target_fp_sugars = diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 26 14:41:15 2014 +0200 @@ -496,8 +496,8 @@ end; fun mk_spec ({T, ctr_sugar as {exhaust_discs, sel_defs, ...}, co_rec = corec, - co_rec_thms = corec_thms, co_rec_discs = corec_discs, - co_rec_selss = corec_selss, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = + fp_co_induct_sugar = {co_rec_thms = corec_thms, co_rec_discs = corec_discs, + co_rec_selss = corec_selss, ...}, ...} : fp_sugar) p_is q_isss f_isss f_Tsss = {corec = mk_co_rec thy Greatest_FP perm_Cs' (substAT T) corec, exhaust_discs = exhaust_discs, sel_defs = sel_defs, fp_nesting_maps = maps (map_thms_of_typ lthy o T_of_bnf) fp_nesting_bnfs, diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Fri Sep 26 14:41:15 2014 +0200 @@ -83,15 +83,15 @@ co_rec_def = @{thm ctor_rec_def_alt[of "case_sum f1 f2" for f1 f2]}, maps = @{thms map_sum.simps}, common_co_inducts = @{thms sum.induct}, - co_inducts = @{thms sum.induct}, - co_rec_thms = @{thms sum.case}, - co_rec_discs = [], - co_rec_selss = [], fp_ctr_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 = {}} + 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 = + {co_inducts = @{thms sum.induct}, + co_rec_thms = @{thms sum.case}, + co_rec_discs = [], + co_rec_selss = []}} end; fun fp_sugar_of_prod ctxt = @@ -127,15 +127,15 @@ co_rec_def = @{thm ctor_rec_def_alt[of "case_prod f" for f]}, maps = @{thms map_prod_simp}, common_co_inducts = @{thms prod.induct}, - co_inducts = @{thms prod.induct}, - co_rec_thms = @{thms prod.case}, - co_rec_discs = [], - co_rec_selss = [], fp_ctr_sugar = {}, - fp_bnf_sugar = { - rel_injects = @{thms rel_prod_apply}, - rel_distincts = []}, - fp_co_induct_sugar = {}} + fp_bnf_sugar = + {rel_injects = @{thms rel_prod_apply}, + rel_distincts = []}, + fp_co_induct_sugar = + {co_inducts = @{thms prod.induct}, + co_rec_thms = @{thms prod.case}, + co_rec_discs = [], + co_rec_selss = []}} end; val _ = Theory.setup (map_local_theory (fn lthy => diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Fri Sep 26 14:41:15 2014 +0200 @@ -297,9 +297,9 @@ val ctrXs_Tsss' = map (map (map substAT) o #ctrXs_Tss) fp_sugars'; val ctrss' = map2 mk_ctr_of fp_sugars' fpTs'; val {common_co_inducts = induct :: _, ...} :: _ = fp_sugars'; - val inducts = map (hd o #co_inducts) fp_sugars'; + val inducts = map (hd o #co_inducts o #fp_co_induct_sugar) fp_sugars'; val recs = map #co_rec fp_sugars'; - val rec_thmss = map #co_rec_thms fp_sugars'; + val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars'; fun is_nested_rec_type (Type (@{type_name fun}, [_, T])) = member (op =) Xs' (body_type T) | is_nested_rec_type _ = false; diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Fri Sep 26 14:41:15 2014 +0200 @@ -25,7 +25,7 @@ (case fp_sugar_of ctxt s of SOME {fp = Least_FP, ...} => true | _ => false); fun basic_lfp_sugar_of C fun_arg_Tsss ({T, fp_res_index, ctr_sugar, co_rec = recx, - co_rec_thms = rec_thms, ...} : fp_sugar) = + fp_co_induct_sugar = {co_rec_thms = rec_thms, ...}, ...} : fp_sugar) = {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar, recx = recx, rec_thms = rec_thms}; diff -r 0c9d59cb3af9 -r f70bffabd7cf src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 26 14:41:08 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Fri Sep 26 14:41:15 2014 +0200 @@ -94,7 +94,7 @@ val B_ify = Term.typ_subst_atomic (As ~~ Bs); val recs = map #co_rec fp_sugars; - val rec_thmss = map #co_rec_thms fp_sugars; + val rec_thmss = map (#co_rec_thms o #fp_co_induct_sugar) fp_sugars; val rec_Ts as rec_T1 :: _ = map fastype_of recs; val rec_arg_Ts = binder_fun_types rec_T1; val Cs = map body_type rec_Ts;