# HG changeset patch # User blanchet # Date 1378729331 -7200 # Node ID eb3865c3ee584e3ad5fa7a9132bb86a8bbe1bbbe # Parent 185ad6cf65765ae50907b189bbc5831d17763a80 include map theorems in datastructure for "primcorec" diff -r 185ad6cf6576 -r eb3865c3ee58 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 13:47:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Mon Sep 09 14:22:11 2013 +0200 @@ -18,6 +18,7 @@ ctr_defss: thm list list, ctr_sugars: BNF_Ctr_Sugar.ctr_sugar list, co_iterss: term list list, + mapss: thm list list, co_inducts: thm list, co_iter_thmsss: thm list list list, disc_co_itersss: thm list list list, @@ -120,6 +121,7 @@ ctr_defss: thm list list, ctr_sugars: ctr_sugar list, co_iterss: term list list, + mapss: thm list list, co_inducts: thm list, co_iter_thmsss: thm list list list, disc_co_itersss: thm list list list, @@ -132,13 +134,14 @@ T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2); fun morph_fp_sugar phi {T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss, - ctr_sugars, co_iterss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} = + ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss} = {T = Morphism.typ phi T, fp = fp, index = index, pre_bnfs = map (morph_bnf phi) pre_bnfs, nested_bnfs = map (morph_bnf phi) nested_bnfs, nesting_bnfs = map (morph_bnf phi) nesting_bnfs, fp_res = morph_fp_result phi fp_res, ctr_defss = map (map (Morphism.thm phi)) ctr_defss, ctr_sugars = map (morph_ctr_sugar phi) ctr_sugars, co_iterss = map (map (Morphism.term phi)) co_iterss, + mapss = map (map (Morphism.thm phi)) mapss, co_inducts = map (Morphism.thm phi) co_inducts, co_iter_thmsss = map (map (map (Morphism.thm phi))) co_iter_thmsss, disc_co_itersss = map (map (map (Morphism.thm phi))) disc_co_itersss, @@ -167,12 +170,12 @@ (fn phi => Data.map (Symtab.default (key, morph_fp_sugar phi fp_sugar))); fun register_fp_sugars fp pre_bnfs nested_bnfs nesting_bnfs (fp_res as {Ts, ...}) ctr_defss - ctr_sugars co_iterss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy = + ctr_sugars co_iterss mapss co_inducts co_iter_thmsss disc_co_itersss sel_co_iterssss lthy = (0, lthy) |> fold (fn T as Type (s, _) => fn (kk, lthy) => (kk + 1, register_fp_sugar s {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res, - ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, + ctr_defss = ctr_defss, ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts, co_iter_thmsss = co_iter_thmsss, disc_co_itersss = disc_co_itersss, sel_co_iterssss = sel_co_iterssss} lthy)) Ts @@ -1414,7 +1417,7 @@ @ rel_distincts @ flat setss); fun derive_and_note_induct_iters_thms_for_types - ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), + ((((mapss, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_sugars)), (iterss, iter_defss)), lthy) = let val ((induct_thms, induct_thm, induct_attrs), (fold_thmss, fold_attrs), @@ -1426,7 +1429,7 @@ val induct_type_attr = Attrib.internal o K o Induct.induct_type; val simp_thmss = - mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapsx rel_injects rel_distincts setss; + mk_simp_thmss ctr_sugars fold_thmss rec_thmss mapss rel_injects rel_distincts setss; val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) @@ -1442,11 +1445,11 @@ lthy |> Local_Theory.notes (common_notes @ notes) |> snd |> register_fp_sugars Least_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss ctr_sugars - iterss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] [] + iterss mapss [induct_thm] (transpose [fold_thmss, rec_thmss]) [] [] end; fun derive_and_note_coinduct_coiters_thms_for_types - ((((mapsx, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), + ((((mapss, rel_injects, rel_distincts, setss), (_, _, ctr_defss, ctr_sugars)), (coiterss, coiter_defss)), lthy) = let val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], @@ -1472,7 +1475,7 @@ mk_simp_thmss ctr_sugars (map3 flat_coiter_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss) (map3 flat_coiter_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss) - mapsx rel_injects rel_distincts setss; + mapss rel_injects rel_distincts setss; val anonymous_notes = [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)] @@ -1504,7 +1507,7 @@ lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd |> register_fp_sugars Greatest_FP pre_bnfs nested_bnfs nesting_bnfs fp_res ctr_defss - ctr_sugars coiterss [coinduct_thm, strong_coinduct_thm] + ctr_sugars coiterss mapss [coinduct_thm, strong_coinduct_thm] (transpose [unfold_thmss, corec_thmss]) (transpose [disc_unfold_thmss, disc_corec_thmss]) (transpose [sel_unfold_thmsss, sel_corec_thmsss]) end; diff -r 185ad6cf6576 -r eb3865c3ee58 src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Sep 09 13:47:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m_sugar.ML Mon Sep 09 14:22:11 2013 +0200 @@ -59,6 +59,7 @@ end; val ctr_defss = map (of_fp_sugar #ctr_defss) fp_sugars0; + val mapss = map (of_fp_sugar #mapss) fp_sugars0; val ctr_sugars0 = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; val ctrss = map #ctrs ctr_sugars0; @@ -168,7 +169,7 @@ fun mk_target_fp_sugar (kk, T) = {T = T, fp = fp, index = kk, pre_bnfs = pre_bnfs, nested_bnfs = nested_bnfs, nesting_bnfs = nesting_bnfs, fp_res = fp_res, ctr_defss = ctr_defss, - ctr_sugars = ctr_sugars, co_inducts = co_inducts, co_iterss = co_iterss, + ctr_sugars = ctr_sugars, co_iterss = co_iterss, mapss = mapss, co_inducts = co_inducts, co_iter_thmsss = transpose [un_fold_thmss, co_rec_thmss], disc_co_itersss = transpose [disc_unfold_thmss, disc_corec_thmss], sel_co_iterssss = transpose [sel_unfold_thmsss, sel_corec_thmsss]} diff -r 185ad6cf6576 -r eb3865c3ee58 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Sep 09 13:47:58 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Mon Sep 09 14:22:11 2013 +0200 @@ -272,6 +272,18 @@ fun find_index_eq hs h = find_index (curry (op =) h) hs; +(*FIXME: remove special cases for products and sum once they are registered as datatypes*) +fun map_thms_of_typ ctxt (Type (s, _)) = + if s = @{type_name prod} then + @{thms map_pair_simp} + else if s = @{type_name sum} then + @{thms sum_map.simps} + else + (case fp_sugar_of ctxt s of + SOME {index, mapss, ...} => nth mapss index + | NONE => []) + | map_thms_of_typ _ _ = []; + val lose_co_rec = false (*FIXME: try true?*); fun rec_specs_of bs arg_Ts res_Ts get_indices callssss0 lthy = @@ -361,7 +373,7 @@ val ((nontriv, missing_res_Ts, perm0_kks, fp_sugars as {nested_bnfs, fp_res = {xtor_co_iterss = dtor_coiters1 :: _, ...}, - co_inducts = coinduct_thms, ...} :: _), lthy') = + co_inducts = coinduct_thms, ...} :: _), lthy') = nested_to_mutual_fps lose_co_rec Greatest_FP bs res_Ts get_indices callssss0 lthy; val perm_fp_sugars = sort (int_ord o pairself #index) fp_sugars; @@ -446,7 +458,7 @@ disc_co_itersss = disc_coitersss, sel_co_iterssss = sel_coiterssss, ...} p_is q_isss f_isss f_Tsss = {corec = mk_co_iter thy Greatest_FP (substAT T) perm_Cs' (co_rec_of (nth coiterss index)), - nested_maps = [] (*FIXME*), + nested_maps = maps (map_thms_of_typ lthy o T_of_bnf) nested_bnfs, nested_map_idents = map (unfold_thms lthy [id_def] o map_id0_of_bnf) nested_bnfs, nested_map_comps = map map_comp_of_bnf nested_bnfs, ctr_specs = mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss