# HG changeset patch # User desharna # Date 1412595252 -7200 # Node ID 727e014c6dbd9f6f5ffe6c24dc723ef5841e0af8 # Parent f0d09e17edba4e7c3d04c360e47b98753c519e98 add 'set_cases' to 'fp_sugar' diff -r f0d09e17edba -r 727e014c6dbd src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:34:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:34:12 2014 +0200 @@ -24,7 +24,8 @@ rel_cases: thm list, set_thms: thm list, set_sels: thm list, - set_intros: thm list} + set_intros: thm list, + set_cases: thm list} type fp_co_induct_sugar = {co_rec: term, @@ -184,7 +185,8 @@ rel_cases: thm list, set_thms: thm list, set_sels: thm list, - set_intros: thm list}; + set_intros: thm list, + set_cases: thm list}; type fp_co_induct_sugar = {co_rec: term, @@ -211,7 +213,7 @@ 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, - rel_sels, rel_intros, rel_cases, set_thms, set_sels, set_intros} : fp_bnf_sugar) = + rel_sels, rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases} : 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, @@ -222,7 +224,8 @@ rel_cases = map (Morphism.thm phi) rel_cases, set_thms = map (Morphism.thm phi) set_thms, set_sels = map (Morphism.thm phi) set_sels, - set_intros = map (Morphism.thm phi) set_intros}; + set_intros = map (Morphism.thm phi) set_intros, + set_cases = map (Morphism.thm phi) set_cases}; 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) = @@ -307,7 +310,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 noted = + set_intross set_casess noted = let val fp_sugars = map_index (fn (kk, T) => @@ -329,7 +332,8 @@ rel_cases = nth rel_casess kk, set_thms = nth set_thmss kk, set_sels = nth set_selss kk, - set_intros = nth set_intross kk}, + set_intros = nth set_intross kk, + set_cases = nth set_casess kk}, fp_co_induct_sugar = {co_rec = nth co_recs kk, common_co_inducts = common_co_inducts, @@ -489,7 +493,7 @@ distincts, distinct_discsss, ...} : ctr_sugar) lthy = if live = 0 then - (([], [], [], [], [], [], [], [], [], [], []), lthy) + (([], [], [], [], [], [], [], [], [], [], [], []), lthy) else let val n = length ctr_Tss; @@ -979,7 +983,8 @@ [subst rel_cases_thm], map subst set_thms, map subst set_sel_thms, - map subst set_intros_thms), lthy') + map subst set_intros_thms, + map subst set_cases_thms), lthy') end; type lfp_sugar_thms = (thm list * thm * Token.src list) * (thm list list * Token.src list); @@ -2083,7 +2088,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_list11 o split_list) + |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list12 o split_list) o split_list; fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects @@ -2118,7 +2123,7 @@ 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), + rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess), (ctrss, _, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = let @@ -2178,7 +2183,7 @@ 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_selss - rel_intross rel_casess set_thmss set_selss set_intross + rel_intross rel_casess set_thmss set_selss set_intross set_casess end; fun derive_corec_transfer_thms lthy corecs corec_defs = @@ -2198,7 +2203,7 @@ 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), + rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess), (_, _, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = let @@ -2294,7 +2299,7 @@ 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 rel_selss - rel_intross rel_casess set_thmss set_selss set_intross + rel_intross rel_casess set_thmss set_selss set_intross set_casess end; val lthy'' = lthy' diff -r f0d09e17edba -r 727e014c6dbd src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:34:12 2014 +0200 @@ -294,7 +294,8 @@ 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, rel_sels, - rel_intros, rel_cases, set_thms, set_sels, set_intros, ...}, ...} : fp_sugar) = + rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...}, + ...} : 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, @@ -313,7 +314,8 @@ rel_cases = rel_cases, set_thms = set_thms, set_sels = set_sels, - set_intros = set_intros}, + set_intros = set_intros, + set_cases = set_cases}, fp_co_induct_sugar = {co_rec = co_rec, common_co_inducts = common_co_inducts, diff -r f0d09e17edba -r 727e014c6dbd src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:34:12 2014 +0200 @@ -91,7 +91,8 @@ rel_cases = [], set_thms = [], set_sels = [], - set_intros = []}, + set_intros = [], + set_cases = []}, 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}, @@ -143,7 +144,8 @@ rel_cases = [], set_thms = [], set_sels = [], - set_intros = []}, + set_intros = [], + set_cases = []}, fp_co_induct_sugar = {co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C), common_co_inducts = @{thms prod.induct}, diff -r f0d09e17edba -r 727e014c6dbd src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:34:04 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:34:12 2014 +0200 @@ -72,6 +72,9 @@ val split_list11: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k) list -> 'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list * 'j list * 'k list + val split_list12: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l) 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 val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context val mk_Freesss: string -> typ list list list -> Proof.context -> @@ -340,6 +343,12 @@ in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8, x9 :: xs9, x10 :: xs10, x11 :: xs11) end; +fun split_list12 [] = ([], [], [], [], [], [], [], [], [], [], [], []) + | split_list12 ((x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) :: xs) = + let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9, xs10, xs11, xs12) = split_list12 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) end; + val parse_type_arg_constrained = Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);