# HG changeset patch # User blanchet # Date 1367321032 -7200 # Node ID 56523caf372fcf480ca17b4f62c58dc370ce7136 # Parent 8deb369ee70b4b0bfed728f0ef453703e9eb1b1b Added maps, sets, rels to "simps" thm collection diff -r 8deb369ee70b -r 56523caf372f src/HOL/BNF/Tools/bnf_fp_def_sugar.ML --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 12:26:41 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 13:23:52 2013 +0200 @@ -217,7 +217,7 @@ val mk_fold_fun_typess = map2 (map2 (curry (op --->))); val mk_rec_fun_typess = mk_fold_fun_typess oo massage_rec_fun_arg_typesss; -fun mk_fold_rec_terms_and_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy = +fun mk_fold_rec_terms_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy = let val y_Tsss = map3 mk_rec_like_fun_arg_typess ns mss ctor_fold_fun_Ts; val g_Tss = mk_fold_fun_typess y_Tsss Css; @@ -236,7 +236,7 @@ (((gss, g_Tss, ysss), (hss, h_Tss, zsss)), lthy) end; -fun mk_unfold_corec_terms_and_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy = +fun mk_unfold_corec_terms_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy = let (*avoid "'a itself" arguments in coiterators and corecursors*) fun repair_arity [0] = [1] @@ -378,8 +378,8 @@ val (_, ctor_fold_fun_Ts) = mk_fp_rec_like true As Cs ctor_folds0; val (_, ctor_rec_fun_Ts) = mk_fp_rec_like true As Cs ctor_recs0; - val (((gss, g_Tss, ysss), (hss, h_Tss, zsss)), names_lthy0) = - mk_fold_rec_terms_and_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy; + val (((gss, _, _), (hss, _, _)), names_lthy0) = + mk_fold_rec_terms_types fpTs Css ns mss ctor_fold_fun_Ts ctor_rec_fun_Ts lthy; val ((((ps, ps'), xsss), us'), names_lthy) = names_lthy0 @@ -549,7 +549,7 @@ val sel_thmsss = map #sel_thmss ctr_wrap_ress; val ((cs, cpss, ((pgss, crssss, cgssss), _), ((phss, csssss, chssss), _)), names_lthy0) = - mk_unfold_corec_terms_and_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy; + mk_unfold_corec_terms_types fpTs Cs ns mss dtor_unfold_fun_Ts dtor_corec_fun_Ts lthy; val (((rs, us'), vs'), names_lthy) = names_lthy0 @@ -961,10 +961,10 @@ (cs, cpss, unfold_only as ((_, crssss, cgssss), (_, g_Tsss, _)), corec_only as ((_, csssss, chssss), (_, h_Tsss, _)))), _) = if lfp then - mk_fold_rec_terms_and_types fpTs Css ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy + mk_fold_rec_terms_types fpTs Css ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy |>> rpair ([], [], (([], [], []), ([], [], [])), (([], [], []), ([], [], []))) else - mk_unfold_corec_terms_and_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy + mk_unfold_corec_terms_types fpTs Cs ns mss fp_fold_fun_Ts fp_rec_fun_Ts lthy |>> pair (([], [], []), ([], [], [])); fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor), @@ -1067,83 +1067,88 @@ end; fun derive_maps_sets_rels (ctr_wrap_res, lthy) = - let - val rel_flip = rel_flip_of_bnf fp_bnf; - val nones = replicate live NONE; + if live = 0 then + ((([], [], [], []), ctr_wrap_res), lthy) + else + let + val rel_flip = rel_flip_of_bnf fp_bnf; + val nones = replicate live NONE; - val ctor_cong = - if lfp then - Drule.dummy_thm - else - let val ctor' = mk_ctor Bs ctor in - cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong - end; + val ctor_cong = + if lfp then + Drule.dummy_thm + else + let val ctor' = mk_ctor Bs ctor in + cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor')] arg_cong + end; - fun mk_cIn ify = - certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo - mk_InN_balanced (ify ctr_sum_prod_T) n; - - val cxIns = map2 (mk_cIn I) tuple_xs ks; - val cyIns = map2 (mk_cIn B_ify) tuple_ys ks; + fun mk_cIn ify = + certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo + mk_InN_balanced (ify ctr_sum_prod_T) n; - fun mk_map_thm ctr_def' cxIn = - fold_thms lthy [ctr_def'] - (unfold_thms lthy (pre_map_def :: - (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map) - (cterm_instantiate_pos (nones @ [SOME cxIn]) - (if lfp then fp_map_thm else fp_map_thm RS ctor_cong))) - |> singleton (Proof_Context.export names_lthy no_defs_lthy); + val cxIns = map2 (mk_cIn I) tuple_xs ks; + val cyIns = map2 (mk_cIn B_ify) tuple_ys ks; - fun mk_set_thm fp_set_thm ctr_def' cxIn = - fold_thms lthy [ctr_def'] - (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @ - (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set) - (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) - |> singleton (Proof_Context.export names_lthy no_defs_lthy); + fun mk_map_thm ctr_def' cxIn = + fold_thms lthy [ctr_def'] + (unfold_thms lthy (pre_map_def :: + (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map) + (cterm_instantiate_pos (nones @ [SOME cxIn]) + (if lfp then fp_map_thm else fp_map_thm RS ctor_cong))) + |> singleton (Proof_Context.export names_lthy no_defs_lthy); - fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns; + fun mk_set_thm fp_set_thm ctr_def' cxIn = + fold_thms lthy [ctr_def'] + (unfold_thms lthy (pre_set_defs @ nested_set_map's @ nesting_set_map's @ + (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set) + (cterm_instantiate_pos [SOME cxIn] fp_set_thm)) + |> singleton (Proof_Context.export names_lthy no_defs_lthy); - val map_thms = map2 mk_map_thm ctr_defs' cxIns; - val set_thmss = map mk_set_thms fp_set_thms; + fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns; - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); + val map_thms = map2 mk_map_thm ctr_defs' cxIns; + val set_thmss = map mk_set_thms fp_set_thms; + + val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns); - fun mk_rel_thm postproc ctr_defs' cxIn cyIn = - fold_thms lthy ctr_defs' - (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def :: - (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel) - (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm)) - |> postproc - |> singleton (Proof_Context.export names_lthy no_defs_lthy); + fun mk_rel_thm postproc ctr_defs' cxIn cyIn = + fold_thms lthy ctr_defs' + (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def :: + (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel) + (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm)) + |> postproc + |> singleton (Proof_Context.export names_lthy no_defs_lthy); - fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = - mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; + fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) = + mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn; - val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); + val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos); - fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = - mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] - cxIn cyIn; + fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) = + mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def'] + cxIn cyIn; - fun mk_other_half_rel_distinct_thm thm = - flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); + fun mk_other_half_rel_distinct_thm thm = + flip_rels lthy live thm + RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2); - val half_rel_distinct_thmss = - map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); - val other_half_rel_distinct_thmss = - map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; - val (rel_distinct_thms, _) = - join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; + val half_rel_distinct_thmss = + map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos); + val other_half_rel_distinct_thmss = + map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss; + val (rel_distinct_thms, _) = + join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss; - val notes = - [(mapN, map_thms, code_simp_attrs), - (rel_distinctN, rel_distinct_thms, code_simp_attrs), - (rel_injectN, rel_inject_thms, code_simp_attrs), - (setsN, flat set_thmss, code_simp_attrs)] - |> massage_simple_notes fp_b_name; - in - (ctr_wrap_res, lthy |> Local_Theory.notes notes |> snd) - end; + val notes = + [(mapN, map_thms, code_simp_attrs), + (rel_distinctN, rel_distinct_thms, code_simp_attrs), + (rel_injectN, rel_inject_thms, code_simp_attrs), + (setsN, flat set_thmss, code_simp_attrs)] + |> massage_simple_notes fp_b_name; + in + (((map_thms, rel_inject_thms, rel_distinct_thms, set_thmss), ctr_wrap_res), + lthy |> Local_Theory.notes notes |> snd) + end; fun define_fold_rec no_defs_lthy = let @@ -1263,25 +1268,29 @@ ((unfold, corec, unfold_def, corec_def), lthy') end; - val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec; - - fun massage_res ((ctr_wrap_res, rec_like_res), lthy) = - (((ctrs, xss, ctr_defs, ctr_wrap_res), rec_like_res), lthy); + fun massage_res (((maps_sets_rels, ctr_wrap_res), rec_like_res), lthy) = + (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_wrap_res)), rec_like_res), lthy); in - (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy') + (wrap + #> derive_maps_sets_rels + ##>> (if lfp then define_fold_rec else define_unfold_corec) + #> massage_res, lthy') end; - fun wrap_types_and_more (wrap_types_and_mores, lthy) = - fold_map I wrap_types_and_mores lthy - |>> apsnd split_list4 o apfst split_list4 o split_list; + fun wrap_types_etc (wrap_types_etcs, lthy) = + fold_map I wrap_types_etcs lthy + |>> apsnd split_list4 o apfst (apsnd split_list4 o apfst split_list4 o split_list) + o split_list; - (* TODO: Add map, sets, rel simps *) val mk_simp_thmss = - map3 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes => - injects @ distincts @ case_thms @ rec_likes @ fold_likes); + map7 (fn {injects, distincts, case_thms, ...} => fn rec_likes => fn fold_likes => + fn mapsx => fn rel_injects => fn rel_distincts => fn setss => + injects @ distincts @ case_thms @ rec_likes @ fold_likes @ mapsx @ rel_injects + @ rel_distincts @ flat setss); fun derive_and_note_induct_fold_rec_thms_for_types - (((ctrss, _, ctr_defss, ctr_wrap_ress), (folds, recs, fold_defs, rec_defs)), lthy) = + ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)), + (folds, recs, fold_defs, rec_defs)), lthy) = let val ((induct_thm, induct_thms, induct_attrs), (fold_thmss, fold_attrs), (rec_thmss, rec_attrs)) = @@ -1291,7 +1300,8 @@ val induct_type_attr = Attrib.internal o K o Induct.induct_type; - val simp_thmss = mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss; + val simp_thmss = + mk_simp_thmss ctr_wrap_ress rec_thmss fold_thmss mapsx rel_injects rel_distincts setss; val common_notes = (if nn > 1 then [(inductN, [induct_thm], induct_attrs)] else []) @@ -1310,7 +1320,8 @@ end; fun derive_and_note_coinduct_unfold_corec_thms_for_types - (((ctrss, _, ctr_defss, ctr_wrap_ress), (unfolds, corecs, unfold_defs, corec_defs)), lthy) = + ((((mapsx, rel_injects, rel_distincts, setss), (ctrss, _, ctr_defss, ctr_wrap_ress)), + (unfolds, corecs, unfold_defs, corec_defs)), lthy) = let val ((coinduct_thm, coinduct_thms, strong_coinduct_thm, strong_coinduct_thms, coinduct_attrs), @@ -1331,7 +1342,8 @@ val simp_thmss = mk_simp_thmss ctr_wrap_ress (map3 flat_corec_like_thms safe_corec_thmss disc_corec_thmss sel_corec_thmss) - (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss); + (map3 flat_corec_like_thms safe_unfold_thmss disc_unfold_thmss sel_unfold_thmss) + mapsx rel_injects rel_distincts setss; val anonymous_notes = [(flat safe_unfold_thmss @ flat safe_corec_thmss, simp_attrs)] @@ -1371,7 +1383,7 @@ pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss) - |> wrap_types_and_more + |> wrap_types_etc |> (if lfp then derive_and_note_induct_fold_rec_thms_for_types else derive_and_note_coinduct_unfold_corec_thms_for_types);