# HG changeset patch # User desharna # Date 1411655751 -7200 # Node ID 86b5b02ef33a9a64374e32d2077598cd35b80454 # Parent ed95293f14b65435a6e96c755fdcc4c0a0d39d43 generate 'dtor_corec_transfer' for codatatypes diff -r ed95293f14b6 -r 86b5b02ef33a src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:50 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:51 2014 +0200 @@ -200,6 +200,13 @@ "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \) (op \)" unfolding rel_fun_def by simp +lemma Inl_transfer: + "rel_fun S (rel_sum S T) Inl Inl" + by auto + +lemma Inr_transfer: + "rel_fun T (rel_sum S T) Inr Inr" + by auto lemma ssubst_Pair_rhs: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) diff -r ed95293f14b6 -r 86b5b02ef33a src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:50 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:51 2014 +0200 @@ -72,6 +72,7 @@ val dtor_coinductN: string val dtor_corecN: string val dtor_corec_o_mapN: string + val dtor_corec_transferN: string val dtor_corec_uniqueN: string val dtor_ctorN: string val dtor_exhaustN: string @@ -299,6 +300,7 @@ val ctor_rec_uniqueN = ctor_recN ^ uniqueN val dtor_corecN = dtorN ^ "_" ^ corecN val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN +val dtor_corec_transferN = dtor_corecN ^ transferN val dtor_corec_uniqueN = dtor_corecN ^ uniqueN val ctor_dtorN = ctorN ^ "_" ^ dtorN diff -r ed95293f14b6 -r 86b5b02ef33a src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 16:35:50 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 25 16:35:51 2014 +0200 @@ -2500,7 +2500,8 @@ val dtor_corec_transfer_thms = mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs) - (fn {context = ctxt, prems = _} => print_tac ctxt "xxx" THEN Skip_Proof.cheat_tac 1) + (fn {context = ctxt, prems = _} => mk_dtor_corec_transfer_tac ctxt n m corec_defs + dtor_unfold_transfer_thms (map map_transfer_of_bnf bnfs) dtor_Jrel_thms) lthy; val timer = time (timer "relator coinduction"); @@ -2517,6 +2518,7 @@ (ctor_exhaustN, ctor_exhaust_thms), (ctor_injectN, ctor_inject_thms), (dtor_corecN, dtor_corec_thms), + (dtor_corec_transferN, dtor_corec_transfer_thms), (dtor_ctorN, dtor_ctor_thms), (dtor_exhaustN, dtor_exhaust_thms), (dtor_injectN, dtor_inject_thms), diff -r ed95293f14b6 -r 86b5b02ef33a src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Sep 25 16:35:50 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Sep 25 16:35:51 2014 +0200 @@ -28,6 +28,8 @@ val mk_corec_tac: Proof.context -> int -> thm list -> thm -> thm -> thm list -> tactic val mk_corec_unique_mor_tac: Proof.context -> thm list -> thm list -> thm -> tactic val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic + val mk_dtor_corec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list -> + thm list -> tactic val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm list -> thm list list -> tactic val mk_dtor_o_ctor_tac: Proof.context -> thm -> thm -> thm -> thm -> thm list -> tactic @@ -609,7 +611,7 @@ EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd => DETERM o EVERY' [rtac trans, rtac o_apply, rtac prod_injectI, rtac conjI, rtac trans, rtac @{thm Shift_def}, - rtac equalityI, rtac subsetI, etac thin_rl, + rtac equalityI, rtac subsetI, etac thin_rl, REPEAT_DETERM o eresolve_tac [CollectE, @{thm UN_E}], dtac length_Lev', dtac asm_rl, etac thin_rl, dtac @{thm set_rev_mp[OF _ equalityD1]}, rtac (@{thm length_Cons} RS arg_cong RS trans), rtac Lev_Suc, @@ -926,7 +928,30 @@ unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN ALLGOALS (TRY o - FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]) + FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE]); + +fun mk_dtor_corec_transfer_tac ctxt n m dtor_corec_defs dtor_unfold_transfer pre_T_map_transfers + dtor_rels = + let + val rel_funD = @{thm rel_funD}; + fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD); + val rel_funD_n_rotated = rotate_prems 1 oo rel_funD_n; + in + CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) => + REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN + unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN + HEADGOAL (rtac (rel_funD_n (n + 1) dtor_unfold_transfer) THEN' + EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel => + etac (rel_funD_n_rotated 2 @{thm case_sum_transfer}) THEN' + rtac (rel_funD_n 2 @{thm comp_transfer}) THEN' + rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN' + REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN' + REPEAT_DETERM_N n o rtac @{thm Inl_transfer} THEN' + rtac @{thm rel_funI} THEN' + etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN' + etac (rel_funD_n 1 @{thm Inr_transfer}))) + (dtor_corec_defs ~~ dtor_unfold_transfer) + end; fun mk_dtor_rel_tac ctxt in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss = @@ -991,7 +1016,7 @@ EVERY' [rtac iffI, if_tac, only_if_tac] 1 end; -fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss +fun mk_rel_coinduct_coind_tac ctxt fst m coinduct ks map_comp0s map_congs map_arg_congs set_map0ss dtor_unfolds dtor_maps in_rels = let val n = length ks;