# HG changeset patch # User desharna # Date 1412595279 -7200 # Node ID a3434015faf026352ce6e0eabb47c7182383288a # Parent 3f61adcc1fc92b9a213788422c5140c8b412c55b add 'case_transfers' to 'fp_sugar' diff -r 3f61adcc1fc9 -r a3434015faf0 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:34:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:34:39 2014 +0200 @@ -12,7 +12,8 @@ {ctrXs_Tss: typ list list, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, - ctr_transfers: thm list} + ctr_transfers: thm list, + case_transfers: thm list} type fp_bnf_sugar = {map_thms: thm list, @@ -174,7 +175,8 @@ {ctrXs_Tss: typ list list, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, - ctr_transfers: thm list}; + ctr_transfers: thm list, + case_transfers: thm list}; type fp_bnf_sugar = {map_thms: thm list, @@ -239,11 +241,13 @@ co_rec_discs = map (Morphism.thm phi) co_rec_discs, co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss}; -fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers} : fp_ctr_sugar) = +fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, + case_transfers} : 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_transfers = map (Morphism.thm phi) ctr_transfers}; + ctr_transfers = map (Morphism.thm phi) ctr_transfers, + case_transfers = map (Morphism.thm phi) case_transfers}; fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, fp_nesting_bnfs, live_nesting_bnfs, fp_ctr_sugar, fp_bnf_sugar, @@ -313,7 +317,7 @@ 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 map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selss - set_intross set_casess ctr_transferss noted = + set_intross set_casess ctr_transferss case_transferss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -324,7 +328,8 @@ {ctrXs_Tss = nth ctrXs_Tsss kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, - ctr_transfers = nth ctr_transferss kk}, + ctr_transfers = nth ctr_transferss kk, + case_transfers = nth case_transferss kk}, fp_bnf_sugar = {map_thms = nth map_thmss kk, map_disc_iffs = nth map_disc_iffss kk, @@ -497,7 +502,7 @@ distincts, distinct_discsss, ...} : ctr_sugar) lthy = if live = 0 then - (([], [], [], [], [], [], [], [], [], [], [], [], []), lthy) + (([], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy) else let val n = length ctr_Tss; @@ -802,7 +807,7 @@ (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) end; - val case_transfer_thms = + val case_transfer_thm = let val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy; val caseA = mk_case As C casex; @@ -950,7 +955,7 @@ |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); val notes = - [(case_transferN, [case_transfer_thms], K []), + [(case_transferN, [case_transfer_thm], K []), (ctr_transferN, ctr_transfer_thms, K []), (disc_transferN, disc_transfer_thms, K []), (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)), @@ -989,7 +994,8 @@ map subst set_sel_thms, map subst set_intros_thms, map subst set_cases_thms, - map subst ctr_transfer_thms), lthy') + map subst ctr_transfer_thms, + [subst case_transfer_thm]), lthy') end; type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); @@ -2093,7 +2099,7 @@ fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) = fold_map I wrap_one_etc lthy - |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list13 o split_list) + |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list14 o split_list) o split_list; fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects @@ -2128,7 +2134,8 @@ fun derive_note_induct_recs_thms_for_types ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, - rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss), + rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss, + case_transferss), (ctrss, _, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = let @@ -2189,6 +2196,7 @@ map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss + case_transferss end; fun derive_corec_transfer_thms lthy corecs corec_defs = @@ -2208,7 +2216,8 @@ fun derive_note_coinduct_corecs_thms_for_types ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, - rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss), + rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss, + case_transferss), (_, _, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = let @@ -2305,6 +2314,7 @@ (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss + case_transferss end; val lthy'' = lthy' diff -r 3f61adcc1fc9 -r a3434015faf0 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:39 2014 +0200 @@ -293,7 +293,7 @@ fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss - ({fp_ctr_sugar = {ctr_transfers, ...}, + ({fp_ctr_sugar = {ctr_transfers, case_transfers, ...}, fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels, rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...}, ...} : fp_sugar) = @@ -304,7 +304,8 @@ {ctrXs_Tss = ctrXs_Tss, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, - ctr_transfers = ctr_transfers}, + ctr_transfers = ctr_transfers, + case_transfers = case_transfers}, fp_bnf_sugar = {map_thms = map_thms, map_disc_iffs = map_disc_iffs, diff -r 3f61adcc1fc9 -r a3434015faf0 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:39 2014 +0200 @@ -80,7 +80,8 @@ {ctrXs_Tss = ctr_Tss, ctr_defs = @{thms Inl_def_alt Inr_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, - ctr_transfers = []}, + ctr_transfers = [], + case_transfers = []}, fp_bnf_sugar = {map_thms = @{thms map_sum.simps}, map_disc_iffs = [], @@ -134,7 +135,8 @@ {ctrXs_Tss = [ctr_Ts], ctr_defs = @{thms Pair_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, - ctr_transfers = []}, + ctr_transfers = [], + case_transfers = []}, fp_bnf_sugar = {map_thms = @{thms map_prod_simp}, map_disc_iffs = [], diff -r 3f61adcc1fc9 -r a3434015faf0 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:34:24 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:34:39 2014 +0200 @@ -78,6 +78,9 @@ val split_list13: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm) list -> 'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list * 'k list * 'l list * 'm list + val split_list14: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n) list -> + 'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * + 'j list * 'k list * 'l list * 'm list * 'n list val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context val mk_Freesss: string -> typ list list list -> Proof.context -> @@ -358,6 +361,13 @@ in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13) end; +fun split_list14 [] = ([], [], [], [], [], [], [], [], [], [], [], [], [], []) + | split_list14 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) :: xs) = + let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12, xs13, xs14) = + split_list14 xs; + in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, + x9 :: xs9, x10 :: xs10, x11 :: xs11, x12 :: xs12, x13 :: xs13, x14 :: xs14) end; + val parse_type_arg_constrained = Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);