# HG changeset patch # User desharna # Date 1413904992 -7200 # Node ID 20235f0512e2af5d9a08f238981121519c04e574 # Parent 797d0e7aefc77f78424520b96007c11981e2cab1 generate 'map_o_corec' for (co)datatypes * * * document 'map_o_corec' diff -r 797d0e7aefc7 -r 20235f0512e2 src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:12 2014 +0200 +++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:12 2014 +0200 @@ -186,6 +186,16 @@ lemma inj_on_convol_ident: "inj_on (\x. (x, f x)) X" unfolding inj_on_def by simp +lemma map_sum_if_distrib_then: + "\f g e x y. map_sum f g (if e then Inl x else y) = (if e then Inl (f x) else map_sum f g y)" + "\f g e x y. map_sum f g (if e then Inr x else y) = (if e then Inr (g x) else map_sum f g y)" + by simp_all + +lemma map_sum_if_distrib_else: + "\f g e x y. map_sum f g (if e then x else Inl y) = (if e then map_sum f g x else Inl (f y))" + "\f g e x y. map_sum f g (if e then x else Inr y) = (if e then map_sum f g x else Inr (g y))" + by simp_all + lemma case_prod_app: "case_prod f x y = case_prod (\l r. f l r y) x" by (case_tac x) simp diff -r 797d0e7aefc7 -r 20235f0512e2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:12 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:12 2014 +0200 @@ -42,7 +42,7 @@ co_rec_selss: thm list list, co_rec_codes: thm list, co_rec_transfers: thm list, - rec_o_maps: thm list, + co_rec_o_maps: thm list, common_rel_co_inducts: thm list, rel_co_inducts: thm list, common_set_inducts: thm list, @@ -176,6 +176,7 @@ val corec_codeN = "corec_code"; val corec_transferN = "corec_transfer"; val map_disc_iffN = "map_disc_iff"; +val map_o_corecN = "map_o_corec"; val map_selN = "map_sel"; val rec_o_mapN = "rec_o_map"; val rec_transferN = "rec_transfer"; @@ -218,7 +219,7 @@ co_rec_selss: thm list list, co_rec_codes: thm list, co_rec_transfers: thm list, - rec_o_maps: thm list, + co_rec_o_maps: thm list, common_rel_co_inducts: thm list, rel_co_inducts: thm list, common_set_inducts: thm list, @@ -257,7 +258,7 @@ 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_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, rec_o_maps, + co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) = {co_rec = Morphism.term phi co_rec, common_co_inducts = map (Morphism.thm phi) common_co_inducts, @@ -269,7 +270,7 @@ co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss, co_rec_codes = map (Morphism.thm phi) co_rec_codes, co_rec_transfers = map (Morphism.thm phi) co_rec_transfers, - rec_o_maps = map (Morphism.thm phi) rec_o_maps, + co_rec_o_maps = map (Morphism.thm phi) co_rec_o_maps, common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts, rel_co_inducts = map (Morphism.thm phi) rel_co_inducts, common_set_inducts = map (Morphism.thm phi) common_set_inducts, @@ -352,7 +353,7 @@ rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts - set_inductss sel_transferss rec_o_mapss noted = + set_inductss sel_transferss co_rec_o_mapss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -392,7 +393,7 @@ co_rec_selss = nth co_rec_selsss kk, co_rec_codes = nth co_rec_codess kk, co_rec_transfers = nth co_rec_transferss kk, - rec_o_maps = nth rec_o_mapss kk, + co_rec_o_maps = nth co_rec_o_mapss kk, common_rel_co_inducts = common_rel_co_inducts, rel_co_inducts = nth rel_co_inductss kk, common_set_inducts = common_set_inducts, @@ -2296,8 +2297,8 @@ val rec_o_map_thms = @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} => - mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses - ctor_rec_o_map) + mk_co_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s + abs_inverses ctor_rec_o_map) |> Thm.close_derivation) rec_o_map_goals rec_defs xtor_co_rec_o_maps; in @@ -2391,6 +2392,66 @@ |> map Thm.close_derivation end; + fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs = + if live = 0 then replicate nn [] + else + let + fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); + val maps0 = map map_of_bnf fp_bnfs; + val ABs = As ~~ Bs + val liveness = map (op <>) ABs; + val f_names = variant_names num_As "f"; + val fs = map2 (curry Free) f_names (map (op -->) ABs); + val live_fs = AList.find (op =) (fs ~~ liveness) true; + + val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0; + + val corec_Ts as corec_T1 :: _ = map fastype_of corecs; + val corec_arg_Ts = binder_fun_types corec_T1; + + val B_ify = Term.subst_atomic_types (As ~~ Bs); + val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); + + val num_rec_args = length corec_arg_Ts; + val g_names = variant_names num_rec_args "g"; + val gs = map2 (curry Free) g_names corec_arg_Ts; + val gcorecs = map (fn corecx => Term.list_comb (corecx, gs)) corecs; + + val map_o_corec_lhss = map2 (curry HOLogic.mk_comp) fmaps gcorecs; + + val ABgs = ABs ~~ fs; + + fun mk_map_o_corec_arg corec_argB_T g = + let + val T = range_type (fastype_of g); + val U = range_type corec_argB_T; + in + if T = U then g + else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U), g) + end; + + fun mk_map_o_corec_rhs corecx = + let val args = map2 (mk_map_o_corec_arg o B_ify_T) corec_arg_Ts gs in + Term.list_comb (B_ify corecx, args) + end; + + val map_o_corec_rhss = map mk_map_o_corec_rhs corecs; + + val map_o_corec_goals = + map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo + curry HOLogic.mk_eq) map_o_corec_lhss map_o_corec_rhss; + + val map_o_corec_thms = + @{map 3} (fn goal => fn corec_def => fn dtor_map_o_corec => + Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => + mk_co_rec_o_map_tac ctxt corec_def pre_map_defs live_nesting_map_ident0s + abs_inverses dtor_map_o_corec) + |> Thm.close_derivation) + map_o_corec_goals corec_defs xtor_co_rec_o_maps; + in + map single map_o_corec_thms + end; + fun derive_note_coinduct_corecs_thms_for_types ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss, rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess, @@ -2446,6 +2507,8 @@ (rel_coinduct_attrs, common_rel_coinduct_attrs)) end; + val map_o_corec_thmss = derive_map_o_corec_thmss lthy lthy corecs corec_defs; + val (set_induct_thms, set_induct_attrss) = derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars) (map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts @@ -2477,6 +2540,7 @@ (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs), (corec_selN, corec_sel_thmss, K corec_sel_attrs), (corec_transferN, corec_transfer_thmss, K []), + (map_o_corecN, map_o_corec_thmss, K []), (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])), (simpsN, simp_thmss, K [])] |> massage_multi_notes fp_b_names fpTs; @@ -2493,7 +2557,7 @@ rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms) corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms - (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss (replicate nn []) + (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss map_o_corec_thmss end; val lthy'' = lthy' diff -r 797d0e7aefc7 -r 20235f0512e2 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:12 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:12 2014 +0200 @@ -19,6 +19,8 @@ thm list list list -> tactic val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic + val mk_co_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm -> + thm Seq.seq val mk_corec_transfer_tac: Proof.context -> cterm list -> cterm list -> thm list -> thm list -> thm list -> thm list -> thm list -> ''a list -> ''a list list -> ''a list list list list -> ''a list list list list -> tactic @@ -34,8 +36,6 @@ val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> tactic - val mk_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm -> - thm Seq.seq val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> @@ -163,13 +163,14 @@ @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv case_unit_Unity} @ sumprod_thms_map; -fun mk_rec_o_map_tac ctxt rec_def pre_map_defs map_ident0s abs_inverses ctor_rec_o_map = +fun mk_co_rec_o_map_tac ctxt co_rec_def pre_map_defs map_ident0s abs_inverses xtor_co_rec_o_map = let - val rec_o_map_simps = - @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def}; + val rec_o_map_simps = @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum map_sum.simps + case_prod_map_prod id_bnf_def map_prod_simp map_sum_if_distrib_then map_sum_if_distrib_else + if_distrib[THEN sym]}; in - HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' - rtac (ctor_rec_o_map RS trans) THEN' + HEADGOAL (subst_tac @{context} (SOME [1, 2]) [co_rec_def] THEN' + rtac (xtor_co_rec_o_map RS trans) THEN' CONVERSION Thm.eta_long_conversion THEN' asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop (map_ident0s @ abs_inverses) @ rec_o_map_simps) ctxt)) diff -r 797d0e7aefc7 -r 20235f0512e2 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:12 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:12 2014 +0200 @@ -297,7 +297,7 @@ fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, - rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, + co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, ...} : fp_sugar) = {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, @@ -335,7 +335,7 @@ co_rec_selss = co_rec_sel_thmss, co_rec_codes = co_rec_codes, co_rec_transfers = co_rec_transfers, - rec_o_maps = rec_o_maps, + co_rec_o_maps = co_rec_o_maps, common_rel_co_inducts = common_rel_co_inducts, rel_co_inducts = rel_co_inducts, common_set_inducts = common_set_inducts, diff -r 797d0e7aefc7 -r 20235f0512e2 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:12 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:12 2014 +0200 @@ -109,7 +109,7 @@ co_rec_selss = [], co_rec_codes = [], co_rec_transfers = [], - rec_o_maps = @{thms case_sum_o_map_sum}, + co_rec_o_maps = @{thms case_sum_o_map_sum}, common_rel_co_inducts = [], rel_co_inducts = [], common_set_inducts = [], @@ -175,7 +175,7 @@ co_rec_selss = [], co_rec_codes = [], co_rec_transfers = [], - rec_o_maps = @{thms case_prod_o_map_prod}, + co_rec_o_maps = @{thms case_prod_o_map_prod}, common_rel_co_inducts = [], rel_co_inducts = [], common_set_inducts = [], diff -r 797d0e7aefc7 -r 20235f0512e2 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:12 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:12 2014 +0200 @@ -285,7 +285,8 @@ curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss; - val rec_o_maps = fold_rev (curry (op @) o (#rec_o_maps o #fp_co_induct_sugar)) fp_sugars []; + val rec_o_maps = + fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars []; val size_o_map_thmss = if nested_size_o_maps_complete then