# HG changeset patch
# User desharna
# Date 1411655753 -7200
# Node ID e89f57d1e46c6270efe8687f5f943ce902d29d63
# Parent  86b5b02ef33a9a64374e32d2077598cd35b80454
generate 'rec_transfer' for datatypes

diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Def.thy	Thu Sep 25 16:35:53 2014 +0200
@@ -19,6 +19,14 @@
   by auto
 
 definition
+   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
+where
+   "rel_sum R1 R2 x y =
+     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
+     | (Inr x, Inr y) \<Rightarrow> R2 x y
+     | _ \<Rightarrow> False)"
+
+definition
   rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
 where
   "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/BNF_Fixpoint_Base.thy
--- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 16:35:53 2014 +0200
@@ -177,6 +177,9 @@
 lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
   unfolding fun_eq_iff vimage2p_def o_apply by simp
 
+lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
+  unfolding rel_fun_def vimage2p_def by auto
+
 lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
   by (erule arg_cong)
 
@@ -189,15 +192,27 @@
 lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
   by (case_tac x) simp+
 
+lemma case_sum_transfer:
+  "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
+  unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
+
 lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
   by (case_tac x) simp+
 
+lemma case_prod_transfer:
+  "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
+  unfolding rel_fun_def rel_prod_def by simp
+
 lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
   by (simp add: inj_on_def)
 
 lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
   by simp
 
+lemma comp_transfer:
+  "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
+
 ML_file "Tools/BNF/bnf_fp_util.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/BNF_Least_Fixpoint.thy
--- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 16:35:53 2014 +0200
@@ -169,9 +169,6 @@
   ultimately show P by (blast intro: assms(3))
 qed
 
-lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
-  unfolding rel_fun_def vimage2p_def by auto
-
 lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   unfolding vimage2p_def by auto
 
@@ -184,10 +181,6 @@
 lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
   unfolding rel_fun_def rel_prod_def by simp
 
-lemma case_sum_transfer:
-  "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
-  unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
-
 lemma map_sum_transfer:
   "rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum"
   unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
@@ -196,10 +189,6 @@
   "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
   unfolding rel_prod_def rel_fun_def convol_def by auto
 
-lemma comp_transfer:
-  "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
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Basic_BNFs.thy
--- a/src/HOL/Basic_BNFs.thy	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Basic_BNFs.thy	Thu Sep 25 16:35:53 2014 +0200
@@ -21,14 +21,6 @@
 
 lemmas sum_set_defs = setl_def[abs_def] setr_def[abs_def]
 
-definition
-   rel_sum :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> 'a + 'b \<Rightarrow> 'c + 'd \<Rightarrow> bool"
-where
-   "rel_sum R1 R2 x y =
-     (case (x, y) of (Inl x, Inl y) \<Rightarrow> R1 x y
-     | (Inr x, Inr y) \<Rightarrow> R2 x y
-     | _ \<Rightarrow> False)"
-
 lemma rel_sum_simps[simp]:
   "rel_sum R1 R2 (Inl a1) (Inl b1) = R1 a1 b1"
   "rel_sum R1 R2 (Inl a1) (Inr b2) = False"
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Lifting_Product.thy
--- a/src/HOL/Lifting_Product.thy	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Lifting_Product.thy	Thu Sep 25 16:35:53 2014 +0200
@@ -24,10 +24,7 @@
 
 declare fst_transfer [transfer_rule]
 declare snd_transfer [transfer_rule]
-
-lemma case_prod_transfer [transfer_rule]:
-  "((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
-  unfolding rel_fun_def rel_prod_def by simp
+declare case_prod_transfer [transfer_rule]
 
 lemma curry_transfer [transfer_rule]:
   "((rel_prod A B ===> C) ===> A ===> B ===> C) curry curry"
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -243,7 +243,7 @@
       REPEAT_DETERM (HEADGOAL (etac (@{thm predicate2_transferD} RS iffD) THEN'
         REPEAT_DETERM o atac));
   in
-    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+    REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
     (HEADGOAL (hyp_subst_tac ctxt THEN' rtac refl) ORELSE
      REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
        @{thms exE conjE CollectE}))) THEN
@@ -260,7 +260,7 @@
           @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
       set_maps;
   in
-    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm rel_funI})) THEN
+    REPEAT_DETERM_N n (HEADGOAL (rtac rel_funI)) THEN
     unfold_thms_tac ctxt @{thms rel_fun_iff_leq_vimage2p} THEN
     HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
       rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
@@ -340,7 +340,7 @@
 
 fun mk_set_transfer_tac ctxt in_rel set_maps =
   Goal.conjunction_tac 1 THEN
-  EVERY (map (fn set_map => HEADGOAL (rtac @{thm rel_funI}) THEN
+  EVERY (map (fn set_map => HEADGOAL (rtac rel_funI) THEN
   REPEAT_DETERM (HEADGOAL (eresolve_tac (Tactic.make_elim (in_rel RS iffD1) ::
     @{thms exE conjE CollectE}))) THEN
   HEADGOAL (hyp_subst_tac ctxt THEN' rtac (@{thm iffD2[OF arg_cong2]} OF [set_map, set_map]) THEN'
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -140,6 +140,7 @@
 val corec_codeN = "corec_code";
 val map_disc_iffN = "map_disc_iff";
 val map_selN = "map_sel";
+val rec_transferN = "rec_transfer";
 val set_casesN = "set_cases";
 val set_introsN = "set_intros";
 val set_inductN = "set_induct";
@@ -418,9 +419,9 @@
       val ks = 1 upto n;
       val ms = map length ctr_Tss;
 
-      val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+      val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
 
-      val fpBT = B_ify fpT;
+      val fpBT = B_ify_T fpT;
       val live_AsBs = filter (op <>) (As ~~ Bs);
       val fTs = map (op -->) live_AsBs;
 
@@ -428,7 +429,7 @@
         |> fold (fold Variable.declare_typ) [As, Bs]
         |> mk_TFrees 2
         ||>> mk_Freess "x" ctr_Tss
-        ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
+        ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
         ||>> mk_Frees "f" fTs
         ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
         ||>> yield_singleton (mk_Frees "a") fpT
@@ -461,7 +462,7 @@
         end;
 
       val cxIns = map2 (mk_cIn ctor) ks xss;
-      val cyIns = map2 (mk_cIn (Term.map_types B_ify ctor)) ks yss;
+      val cyIns = map2 (mk_cIn (Term.map_types B_ify_T ctor)) ks yss;
 
       fun mk_map_thm ctr_def' cxIn =
         fold_thms lthy [ctr_def']
@@ -1092,10 +1093,12 @@
 fun derive_rel_induct_thms_for_types lthy fpA_Ts As Bs ctrAss ctrAs_Tsss exhausts ctor_rel_induct
     ctor_defss ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs =
   let
-    val B_ify = typ_subst_nonatomic (As ~~ Bs);
-    val fpB_Ts = map B_ify fpA_Ts;
-    val ctrBs_Tsss = map (map (map B_ify)) ctrAs_Tsss;
-    val ctrBss = map (map (subst_nonatomic_types (As ~~ Bs))) ctrAss;
+    val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+    val B_ify = Term.subst_atomic_types (As ~~ Bs);
+
+    val fpB_Ts = map B_ify_T fpA_Ts;
+    val ctrBs_Tsss = map (map (map B_ify_T)) ctrAs_Tsss;
+    val ctrBss = map (map B_ify) ctrAss;
 
     val ((((Rs, IRs), ctrAsss), ctrBsss), names_lthy) = lthy
       |> mk_Frees "R" (map2 mk_pred2T As Bs)
@@ -1319,7 +1322,8 @@
     abs_inverses abs_injects ctor_injects dtor_ctors rel_pre_defs ctor_defss dtor_rel_coinduct
     live_nesting_rel_eqs =
   let
-    val fpB_Ts = map (typ_subst_nonatomic (As ~~ Bs)) fpA_Ts;
+    val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+    val fpB_Ts = map B_ify_T fpA_Ts;
 
     val (Rs, IRs, fpAs, fpBs, names_lthy) =
       let
@@ -1711,11 +1715,12 @@
     val set_boss = map (map fst o type_args_named_constrained_of_spec) specs;
     val set_bss = map (map (the_default Binding.empty)) set_boss;
 
-    val (((Bs0, Cs), Xs), names_no_defs_lthy) =
+    val ((((Bs0, Cs), Es), Xs), names_no_defs_lthy) =
       no_defs_lthy
       |> fold (Variable.declare_typ o resort_tfree_or_tvar dummyS) unsorted_As
       |> mk_TFrees num_As
       ||>> mk_TFrees nn
+      ||>> mk_TFrees nn
       ||>> variant_tfrees fp_b_names;
 
     fun add_fake_type spec =
@@ -1793,7 +1798,8 @@
     val ((pre_bnfs, absT_infos), (fp_res as {bnfs = fp_bnfs as any_fp_bnf :: _, ctors = ctors0,
              dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
              ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
-             xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms, ...},
+             xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
+             ctor_rec_transfer_thms, ...},
            lthy)) =
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
         (map dest_TFree killed_As) fp_eqs no_defs_lthy
@@ -1857,13 +1863,13 @@
           if alive then resort_tfree_or_tvar S B else A)
         (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
 
-    val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+    val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
 
     val ctors = map (mk_ctor As) ctors0;
     val dtors = map (mk_dtor As) dtors0;
 
     val fpTs = map (domain_type o fastype_of) dtors;
-    val fpBTs = map B_ify fpTs;
+    val fpBTs = map B_ify_T fpTs;
 
     val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
 
@@ -1999,6 +2005,28 @@
         rel_distincts setss =
       injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
 
+    fun derive_rec_transfer_thms lthy recs rec_defs ns =
+      let
+        val liveAsBs = filter (op <>) (As ~~ Bs);
+        val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
+
+        val ((Rs, Ss), names_lthy) = lthy
+          |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+          ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
+
+        val recBs = map B_ify recs;
+        val goals = map2 (mk_parametricity_goal lthy (Rs @ Ss)) recs recBs;
+      in
+        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+          (fn {context = ctxt, prems = _} =>
+             mk_rec_transfer_tac names_lthy nn ns (map (certify ctxt) Ss)
+               (map (certify ctxt) Rs) rec_defs ctor_rec_transfer_thms pre_rel_defs
+               live_nesting_rel_eqs)
+        |> Conjunction.elim_balanced nn
+        |> Proof_Context.export names_lthy lthy
+        |> map Thm.close_derivation
+      end;
+
     fun derive_note_induct_recs_thms_for_types
         ((((mapss, rel_injectss, rel_distinctss, setss), (ctrss, _, ctr_defss, ctr_sugars)),
           (recs, rec_defs)), lthy) =
@@ -2008,6 +2036,11 @@
             xtor_co_rec_thms live_nesting_bnfs fp_nesting_bnfs fpTs Cs Xs ctrXs_Tsss abs_inverses
             type_definitions abs_inverses ctrss ctr_defss recs rec_defs lthy;
 
+        val rec_transfer_thmss =
+          if live = 0 then replicate nn []
+          else
+            map single (derive_rec_transfer_thms lthy recs rec_defs ns);
+
         val induct_type_attr = Attrib.internal o K o Induct.induct_type;
         val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
 
@@ -2040,6 +2073,7 @@
         val notes =
           [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
            (recN, rec_thmss, K rec_attrs),
+           (rec_transferN, rec_transfer_thmss, K []),
            (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
            (simpsN, simp_thmss, K [])]
           |> massage_multi_notes fp_b_names fpTs;
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -33,6 +33,8 @@
     thm list -> tactic
   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 ->
+    thm list -> thm list -> thm list -> thm list -> tactic
   val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list -> tactic
   val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
@@ -57,6 +59,11 @@
 open BNF_Util
 open BNF_FP_Util
 
+val case_sum_transfer = @{thm case_sum_transfer};
+val case_sum_transfer_eq = @{thm case_sum_transfer[of "op =" _ "op =", unfolded sum.rel_eq]};
+val case_prod_transfer = @{thm case_prod_transfer};
+val case_prod_transfer_eq = @{thm case_prod_transfer[of "op =" "op =", unfolded prod.rel_eq]};
+
 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
 val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
 val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
@@ -96,19 +103,19 @@
   let
     val n = length (tl (prems_of rel_cases));
   in
-    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+    REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
     HEADGOAL (etac rel_cases) THEN
     ALLGOALS (hyp_subst_tac ctxt) THEN
     unfold_thms_tac ctxt cases THEN
     ALLGOALS (fn k => (select_prem_tac n (dtac asm_rl) k THEN' rotate_tac ~1) k) THEN
-    ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD}))
+    ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac rel_funD))
   end;
 
 fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
   HEADGOAL Goal.conjunction_tac THEN
-  ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
-    TRY o (REPEAT_DETERM1 o atac ORELSE'
-      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl)));
+  ALLGOALS (REPEAT o (resolve_tac (rel_funI :: rel_intros) THEN'
+    TRY o (REPEAT_DETERM1 o (atac ORELSE'
+      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl))));
 
 fun mk_disc_transfer_tac rel_sel exhaust_disc distinct_disc=
   let
@@ -118,7 +125,7 @@
         rotate_tac ~1 THEN' etac (rotate_prems 1 notE) THEN' eresolve_tac distinct_disc));
   in
     HEADGOAL Goal.conjunction_tac THEN
-    REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI} THEN' dtac (rel_sel RS iffD1) THEN'
+    REPEAT_DETERM (HEADGOAL (rtac rel_funI THEN' dtac (rel_sel RS iffD1) THEN'
       REPEAT_DETERM o (etac conjE) THEN' (atac ORELSE' rtac iffI))) THEN
     TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
   end;
@@ -155,6 +162,39 @@
   unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @
     pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl);
 
+fun mk_rec_transfer_tac ctxt nn ns actives passives rec_defs ctor_rec_transfers rel_pre_T_defs
+    rel_eqs =
+  let
+    val ctor_rec_transfers' =
+      map (cterm_instantiate_pos (map SOME passives @ map SOME actives)) ctor_rec_transfers;
+    val ns' = Integer.sum ns;
+  in
+    HEADGOAL Goal.conjunction_tac THEN
+    EVERY (map (fn ctor_rec_transfer =>
+        REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+        unfold_thms_tac ctxt rec_defs THEN
+        HEADGOAL (etac (mk_rel_funDN_rotated (nn + 1) ctor_rec_transfer)) THEN
+        unfold_thms_tac ctxt rel_pre_T_defs THEN
+        EVERY (fst (fold_map (fn k => fn acc => rpair (k + acc)
+            (HEADGOAL (rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer})) THEN
+             HEADGOAL (rtac @{thm vimage2p_rel_fun}) THEN
+             unfold_thms_tac ctxt rel_eqs THEN
+             EVERY (map (fn n =>
+                 REPEAT_DETERM (HEADGOAL
+                   (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE'
+                    rtac (mk_rel_funDN 2 case_sum_transfer))) THEN
+                 HEADGOAL (select_prem_tac ns' (dtac asm_rl) (acc + n)) THEN
+                 HEADGOAL (SELECT_GOAL (HEADGOAL
+                   ((REPEAT_DETERM o (atac ORELSE'
+                       rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE'
+                       rtac (mk_rel_funDN 1 case_prod_transfer) ORELSE'
+                       rtac rel_funI)) THEN_ALL_NEW
+                    (REPEAT_ALL_NEW (dtac rel_funD) THEN_ALL_NEW atac)))))
+               (1 upto k))))
+          ns 0)))
+      ctor_rec_transfers')
+  end;
+
 val corec_unfold_thms = @{thms id_def} @ sumprod_thms_map;
 
 fun mk_corec_tac corec_defs map_ident0s ctor_dtor_corec pre_map_def abs_inverse ctr_def ctxt =
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_fp_n2m.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -477,7 +477,8 @@
         xtor_co_rec_thms = xtor_co_rec_thms,
         xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
         rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
-        dtor_set_induct_thms = []}
+        dtor_set_induct_thms = [],
+        ctor_rec_transfer_thms = []}
        |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
   in
     (fp_res, lthy)
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -27,7 +27,8 @@
      xtor_co_rec_thms: thm list,
      xtor_co_rec_o_map_thms: thm list,
      rel_xtor_co_induct_thm: thm,
-     dtor_set_induct_thms: thm list}
+     dtor_set_induct_thms: thm list,
+     ctor_rec_transfer_thms: thm list}
 
   val morph_fp_result: morphism -> fp_result -> fp_result
 
@@ -218,11 +219,13 @@
    xtor_co_rec_thms: thm list,
    xtor_co_rec_o_map_thms: thm list,
    rel_xtor_co_induct_thm: thm,
-   dtor_set_induct_thms: thm list};
+   dtor_set_induct_thms: thm list,
+   ctor_rec_transfer_thms: thm list};
 
 fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
     dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
-    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms} =
+    xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
+    dtor_set_induct_thms, ctor_rec_transfer_thms} =
   {Ts = map (Morphism.typ phi) Ts,
    bnfs = map (morph_bnf phi) bnfs,
    ctors = map (Morphism.term phi) ctors,
@@ -239,7 +242,8 @@
    xtor_co_rec_thms = map (Morphism.thm phi) xtor_co_rec_thms,
    xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
-   dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms}; (* No idea of what this is doing... *)
+   dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
+   ctor_rec_transfer_thms = map (Morphism.thm phi) ctor_rec_transfer_thms};
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_gfp.ML
--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -2542,7 +2542,7 @@
        xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
        xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
        xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
-       dtor_set_induct_thms = dtor_Jset_induct_thms};
+       dtor_set_induct_thms = dtor_Jset_induct_thms, ctor_rec_transfer_thms = []};
   in
     timer; (fp_res, lthy')
   end;
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -932,26 +932,20 @@
 
 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;
+  CONJ_WRAP (fn (dtor_corec_def, dtor_unfold_transfer) =>
+      REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+      unfold_thms_tac ctxt [dtor_corec_def, o_apply] THEN
+      HEADGOAL (rtac (mk_rel_funDN (n + 1) dtor_unfold_transfer) THEN'
+        EVERY' (map2 (fn pre_T_map_transfer => fn dtor_rel =>
+          etac (mk_rel_funDN_rotated 2 @{thm case_sum_transfer}) THEN'
+          rtac (mk_rel_funDN 2 @{thm comp_transfer}) THEN'
+          rtac (mk_rel_funDN (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 rel_funI THEN'
+          etac (dtor_rel RS iffD1)) pre_T_map_transfers dtor_rels) THEN'
+        etac (mk_rel_funDN 1 @{thm Inr_transfer})))
+    (dtor_corec_defs ~~ dtor_unfold_transfer);
 
 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 =
@@ -1113,7 +1107,7 @@
       EVERY' (map (fn map_transfer => EVERY'
         [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
         SELECT_GOAL (unfold_thms_tac ctxt unfolds),
-        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
+        rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
         REPEAT_DETERM_N m o rtac @{thm id_transfer},
         REPEAT_DETERM_N n o rtac @{thm rel_fun_image2p},
         etac @{thm predicate2D}, etac @{thm image2pI}])
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -1829,7 +1829,7 @@
        xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
        xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
        xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
-       dtor_set_induct_thms = []};
+       dtor_set_induct_thms = [], ctor_rec_transfer_thms = ctor_rec_transfer_thms};
   in
     timer; (fp_res, lthy')
   end;
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -47,7 +47,8 @@
    xtor_co_rec_thms = [map_id0_of_bnf fp_bnf RS @{thm ctor_rec}],
    xtor_co_rec_o_map_thms = [ctor_rec_o_map],
    rel_xtor_co_induct_thm = xtor_rel_induct,
-   dtor_set_induct_thms = []};
+   dtor_set_induct_thms = [],
+   ctor_rec_transfer_thms = []};
 
 fun fp_sugar_of_sum ctxt =
   let
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -705,26 +705,20 @@
 
 fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
     ctor_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 (ctor_rec_def, ctor_fold_transfer) =>
-        REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
-        unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
-        HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
-          etac (rel_funD_n_rotated (n + 1) ctor_fold_transfer) THEN'
-          EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
-            etac (rel_funD_n_rotated 2 @{thm convol_transfer}) THEN'
-            rtac (rel_funD_n_rotated 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 o rtac @{thm fst_transfer} THEN'
-            rtac @{thm rel_funI} THEN'
-            etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
-      (ctor_rec_defs ~~ ctor_fold_transfers)
-  end;
+  CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
+      REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
+      unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
+      HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
+        etac (mk_rel_funDN_rotated (n + 1) ctor_fold_transfer) THEN'
+        EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
+          etac (mk_rel_funDN_rotated 2 @{thm convol_transfer}) THEN'
+          rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer}) THEN'
+          rtac (mk_rel_funDN (m + n) pre_T_map_transfer) THEN'
+          REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+          REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
+          rtac rel_funI THEN'
+          etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
+    (ctor_rec_defs ~~ ctor_fold_transfers);
 
 fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
   let val n = length ks;
@@ -754,7 +748,7 @@
         [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
         SELECT_GOAL (unfold_thms_tac ctxt folds),
         etac @{thm predicate2D_vimage2p},
-        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm rel_funD}) map_transfer),
+        rtac (funpow (m + n + 1) (fn thm => thm RS rel_funD) map_transfer),
         REPEAT_DETERM_N m o rtac @{thm id_transfer},
         REPEAT_DETERM_N n o rtac @{thm vimage2p_rel_fun},
         atac])
diff -r 86b5b02ef33a -r e89f57d1e46c src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 25 16:35:51 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Thu Sep 25 16:35:53 2014 +0200
@@ -35,11 +35,11 @@
       'o) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
- val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+  val map15: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
       'o -> 'p) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list
- val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
+  val map16: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n ->
       'o -> 'p -> 'q) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list -> 'p list -> 'q list
@@ -116,13 +116,6 @@
   val mk_nthN: int -> term -> int -> term
 
   (*parameterized thms*)
-  val mk_Un_upper: int -> int -> thm
-  val mk_conjIN: int -> thm
-  val mk_nthI: int -> int -> thm
-  val mk_nth_conv: int -> int -> thm
-  val mk_ordLeq_csum: int -> int -> thm -> thm
-  val mk_UnIN: int -> int -> thm
-
   val eqTrueI: thm
   val eqFalseI: thm
   val prod_injectD: thm
@@ -132,11 +125,22 @@
   val meta_mp: thm
   val meta_spec: thm
   val o_apply: thm
+  val rel_funD: thm
+  val rel_funI: thm
   val set_mp: thm
   val set_rev_mp: thm
   val subset_UNIV: thm
+
+  val mk_conjIN: int -> thm
+  val mk_nthI: int -> int -> thm
+  val mk_nth_conv: int -> int -> thm
+  val mk_ordLeq_csum: int -> int -> thm -> thm
+  val mk_rel_funDN: int -> thm -> thm
+  val mk_rel_funDN_rotated: int -> thm -> thm
   val mk_sym: thm -> thm
   val mk_trans: thm -> thm -> thm
+  val mk_UnIN: int -> int -> thm
+  val mk_Un_upper: int -> int -> thm
 
   val is_refl_bool: term -> bool
   val is_refl: thm -> bool
@@ -528,6 +532,8 @@
 val meta_mp = @{thm meta_mp};
 val meta_spec = @{thm meta_spec};
 val o_apply = @{thm o_apply};
+val rel_funD = @{thm rel_funD};
+val rel_funI = @{thm rel_funI};
 val set_mp = @{thm set_mp};
 val set_rev_mp = @{thm set_rev_mp};
 val subset_UNIV = @{thm subset_UNIV};
@@ -560,6 +566,10 @@
   | mk_ordLeq_csum n m thm = @{thm ordLeq_transitive} OF
     [mk_ordLeq_csum (n - 1) (m - 1) thm, @{thm ordLeq_csum2[OF Card_order_csum]}];
 
+fun mk_rel_funDN n = funpow n (fn thm => thm RS @{thm rel_funD});
+
+val mk_rel_funDN_rotated = rotate_prems ~1 oo mk_rel_funDN;
+
 local
   fun mk_Un_upper' 0 = subset_refl
     | mk_Un_upper' 1 = @{thm Un_upper1}