--- 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 \<circ>) (op \<circ>)"
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: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)
--- 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
--- 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),
--- 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;