# HG changeset patch # User desharna # Date 1412595184 -7200 # Node ID e94cd4f71d0c2e515b6f6e7b01b143dc5d7cfc99 # Parent 7d7473b54fe0e43db7bd1e1018f461d688c3aac2 add 'rel_sels' to 'fp_sugar' diff -r 7d7473b54fe0 -r e94cd4f71d0c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:32:53 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:33:04 2014 +0200 @@ -18,7 +18,8 @@ map_disc_iffs: thm list, map_sels: thm list, rel_injects: thm list, - rel_distincts: thm list} + rel_distincts: thm list, + rel_sels: thm list} type fp_co_induct_sugar = {co_rec: term, @@ -172,7 +173,8 @@ map_disc_iffs: thm list, map_sels: thm list, rel_injects: thm list, - rel_distincts: thm list}; + rel_distincts: thm list, + rel_sels: thm list}; type fp_co_induct_sugar = {co_rec: term, @@ -198,12 +200,14 @@ fp_bnf_sugar: fp_bnf_sugar, fp_co_induct_sugar: fp_co_induct_sugar}; -fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts} : fp_bnf_sugar) = +fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts, + rel_sels} : fp_bnf_sugar) = {map_thms = map (Morphism.thm phi) map_thms, map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, map_sels = map (Morphism.thm phi) map_sels, rel_injects = map (Morphism.thm phi) rel_injects, - rel_distincts = map (Morphism.thm phi) rel_distincts}; + rel_distincts = map (Morphism.thm phi) rel_distincts, + rel_sels = map (Morphism.thm phi) rel_sels}; 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) = @@ -287,7 +291,7 @@ 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 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 noted = + rel_distinctss map_disc_iffss map_selss rel_selss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -303,7 +307,8 @@ map_disc_iffs = nth map_disc_iffss kk, map_sels = nth map_selss kk, rel_injects = nth rel_injectss kk, - rel_distincts = nth rel_distinctss kk}, + rel_distincts = nth rel_distinctss kk, + rel_sels = nth rel_selss kk}, fp_co_induct_sugar = {co_rec = nth co_recs kk, common_co_inducts = common_co_inducts, @@ -463,7 +468,7 @@ distincts, distinct_discsss, ...} : ctr_sugar) lthy = if live = 0 then - (([], [], [], [], [], []), lthy) + (([],[], [], [], [], [], []), lthy) else let val n = length ctr_Tss; @@ -948,6 +953,7 @@ map subst map_sel_thms, map subst rel_inject_thms, map subst rel_distinct_thms, + map subst rel_sel_thms, map (map subst) set0_thmss), lthy') end; @@ -2052,7 +2058,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_list6 o split_list) + |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list7 o split_list) o split_list; fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects @@ -2085,7 +2091,7 @@ end; fun derive_note_induct_recs_thms_for_types - ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, setss), + ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, setss), (ctrss, _, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = let @@ -2144,7 +2150,7 @@ |-> 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 map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) - rel_injectss rel_distinctss map_disc_iffss map_selss + rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss end; fun derive_corec_transfer_thms lthy corecs corec_defs = @@ -2163,7 +2169,7 @@ end; fun derive_note_coinduct_corecs_thms_for_types - ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, setss), + ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, setss), (_, _, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = let @@ -2258,7 +2264,7 @@ fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs 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 map_disc_iffss map_selss + corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss end; val lthy'' = lthy' diff -r 7d7473b54fe0 -r e94cd4f71d0c src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:32:53 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:04 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_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, ...}, ...} : fp_sugar) = + ({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels, ...}, ...} : 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, @@ -306,7 +306,8 @@ map_disc_iffs = map_disc_iffs, map_sels = map_sels, rel_injects = rel_injects, - rel_distincts = rel_distincts}, + rel_distincts = rel_distincts, + rel_sels = rel_sels}, fp_co_induct_sugar = {co_rec = co_rec, common_co_inducts = common_co_inducts, diff -r 7d7473b54fe0 -r e94cd4f71d0c src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:32:53 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:04 2014 +0200 @@ -85,7 +85,8 @@ map_disc_iffs = [], map_sels = [], rel_injects = @{thms rel_sum_simps(1,4)}, - rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}}, + rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]}, + rel_sels = []}, fp_co_induct_sugar = {co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C), common_co_inducts = @{thms sum.induct}, @@ -131,7 +132,8 @@ map_disc_iffs = [], map_sels = [], rel_injects = @{thms rel_prod_apply}, - rel_distincts = []}, + rel_distincts = [], + rel_sels = []}, fp_co_induct_sugar = {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), common_co_inducts = @{thms prod.induct}, diff -r 7d7473b54fe0 -r e94cd4f71d0c src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:32:53 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:33:04 2014 +0200 @@ -61,6 +61,8 @@ val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list val split_list6: ('a * 'b * 'c * 'd * 'e * 'f) list -> 'a list * 'b list * 'c list * 'd list * 'e list * 'f list + val split_list7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list -> 'a list * 'b list * 'c list * 'd list * + 'e list * 'f list * 'g list val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context val mk_Freesss: string -> typ list list list -> Proof.context -> @@ -301,6 +303,11 @@ let val (xs1, xs2, xs3, xs4, xs5, xs6) = split_list6 xs; in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6) end; +fun split_list7 [] = ([], [], [], [], [], [], []) + | split_list7 ((x1, x2, x3, x4, x5, x6, x7) :: xs) = + let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7) = split_list7 xs; + in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7) end; + val parse_type_arg_constrained = Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);