# HG changeset patch # User desharna # Date 1404313309 -7200 # Node ID 8f0ba9f2d10ff92b98e77b9af3069d67710c5cde # Parent 58db442609ac705ca8cb1af0dd8359aa0d5c628d generate 'corec_code' theorem for codatatypes diff -r 58db442609ac -r 8f0ba9f2d10f src/HOL/BNF_FP_Base.thy --- a/src/HOL/BNF_FP_Base.thy Wed Jul 02 13:23:11 2014 +0200 +++ b/src/HOL/BNF_FP_Base.thy Wed Jul 02 17:01:49 2014 +0200 @@ -187,6 +187,9 @@ lemma prod_inj_map: "inj f \ inj g \ inj (map_prod f g)" by (simp add: inj_on_def) +lemma eq_ifI: "(P \ t = u1) \ (\ P \ t = u2) \ t = (if P then u1 else u2)" + by simp + ML_file "Tools/BNF/bnf_fp_util.ML" ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/BNF/bnf_lfp_size.ML" diff -r 58db442609ac -r 8f0ba9f2d10f src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 02 13:23:11 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Jul 02 17:01:49 2014 +0200 @@ -27,8 +27,8 @@ type gfp_sugar_thms = ((thm list * thm) list * (Args.src list * Args.src list)) - * (thm list list * Args.src list) - * (thm list list * Args.src list) + * thm list list + * thm list list * (thm list list * Args.src list) * (thm list list list * Args.src list) @@ -96,6 +96,8 @@ open BNF_LFP_Size val EqN = "Eq_"; + +val corec_codeN = "corec_code"; val disc_map_iffN = "disc_map_iff"; val sel_mapN = "sel_map"; val sel_setN = "sel_set"; @@ -278,18 +280,18 @@ type gfp_sugar_thms = ((thm list * thm) list * (Args.src list * Args.src list)) - * (thm list list * Args.src list) - * (thm list list * Args.src list) + * thm list list + * thm list list * (thm list list * Args.src list) * (thm list list list * Args.src list); fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair), - (corecss, corec_attrs), (disc_corecss, disc_corec_attrs), - (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) = + corecss, disc_corecss, (disc_corec_iffss, disc_corec_iff_attrs), + (sel_corecsss, sel_corec_attrs)) = ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs, coinduct_attrs_pair), - (map (map (Morphism.thm phi)) corecss, corec_attrs), - (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs), + map (map (Morphism.thm phi)) corecss, + map (map (Morphism.thm phi)) disc_corecss, (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs), (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms; @@ -962,8 +964,8 @@ val sel_corec_thmsss = mk_sel_corec_thms corec_thmss; in ((coinduct_thms_pairs, mk_coinduct_attrs fpTs ctr_sugars mss), - (corec_thmss, code_nitpicksimp_attrs), - (disc_corec_thmss, []), + corec_thmss, + disc_corec_thmss, (disc_corec_iff_thmss, simp_attrs), (sel_corec_thmsss, simp_attrs)) end; @@ -1629,13 +1631,25 @@ let val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)], (coinduct_attrs, common_coinduct_attrs)), - (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs), + corec_thmss, disc_corec_thmss, (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) = derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs (Proof_Context.export lthy' no_defs_lthy) lthy; + fun distinct_prems ctxt th = + Goal.prove ctxt [] [] + (th |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies) + (fn _ => HEADGOAL (cut_tac th THEN' atac) THEN ALLGOALS eq_assume_tac); + + fun eq_ifIN _ [thm] = thm + | eq_ifIN ctxt (thm :: thms) = + distinct_prems ctxt (@{thm eq_ifI} OF + (map (unfold_thms ctxt @{thms atomize_imp[of _ "t = u" for t u]}) + [thm, eq_ifIN ctxt thms])); + + val corec_code_thms = map (eq_ifIN lthy) corec_thmss val sel_corec_thmss = map flat sel_corec_thmsss; val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type; @@ -1675,8 +1689,9 @@ val notes = [(coinductN, map single coinduct_thms, fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]), - (corecN, corec_thmss, K corec_attrs), - (disc_corecN, disc_corec_thmss, K disc_corec_attrs), + (corecN, corec_thmss, K []), + (corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs), + (disc_corecN, disc_corec_thmss, K []), (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs), (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])), (sel_corecN, sel_corec_thmss, K sel_corec_attrs), diff -r 58db442609ac -r 8f0ba9f2d10f src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Jul 02 13:23:11 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Jul 02 17:01:49 2014 +0200 @@ -267,7 +267,7 @@ dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy - |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _, + |> `(fn ((coinduct_thms_pairs, _), corec_thmss, disc_corec_thmss, _, (sel_corec_thmsss, _)) => (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss, disc_corec_thmss, sel_corec_thmsss)) diff -r 58db442609ac -r 8f0ba9f2d10f src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 02 13:23:11 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Jul 02 17:01:49 2014 +0200 @@ -610,7 +610,7 @@ map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s; val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; - + fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong => mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs; val rewrite1s = mk_rewrites map_cong1s;