transfer rule for {c,d}tor_{,un}fold
authortraytel
Thu, 25 Jul 2013 16:46:53 +0200
changeset 52731 dacd47a0633f
parent 52730 6bf02eb4ddf7
child 52732 b4da1f2ec73f
transfer rule for {c,d}tor_{,un}fold
src/HOL/BNF/BNF.thy
src/HOL/BNF/BNF_Def.thy
src/HOL/BNF/BNF_FP_Basic.thy
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/BNF_LFP.thy
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_def_tactics.ML
src/HOL/BNF/Tools/bnf_fp_util.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_gfp_tactics.ML
src/HOL/BNF/Tools/bnf_lfp.ML
src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/BNF.thy	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF.thy	Thu Jul 25 16:46:53 2013 +0200
@@ -13,7 +13,7 @@
 imports More_BNFs
 begin
 
-hide_const (open) vimagep Gr Grp collect fsts snds setl setr 
+hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
   convol thePull pick_middlep fstOp sndOp csquare inver
   image2 relImage relInvImage prefCl PrefCl Succ Shift shift
 
--- a/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 16:46:53 2013 +0200
@@ -193,20 +193,20 @@
   ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
 unfolding Func_def by (auto elim: the_inv_into_f_f)
 
-definition vimagep where
-  "vimagep f g R = (\<lambda>x y. R (f x) (g y))"
+definition vimage2p where
+  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
 
-lemma vimagepI: "R (f x) (g y) \<Longrightarrow> vimagep f g R x y"
-  unfolding vimagep_def by -
+lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
+  unfolding vimage2p_def by -
 
-lemma vimagepD: "vimagep f g R x y \<Longrightarrow> R (f x) (g y)"
-  unfolding vimagep_def by -
+lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)"
+  unfolding vimage2p_def by -
 
-lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \<le> vimagep f g S)"
-  unfolding fun_rel_def vimagep_def by auto
+lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
+  unfolding fun_rel_def vimage2p_def by auto
 
-lemma convol_image_vimagep: "<f o fst, g o snd> ` Collect (split (vimagep f g R)) \<subseteq> Collect (split R)"
-  unfolding vimagep_def convol_def by auto
+lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
+  unfolding vimage2p_def convol_def by auto
 
 ML_file "Tools/bnf_def_tactics.ML"
 ML_file "Tools/bnf_def.ML"
--- a/src/HOL/BNF/BNF_FP_Basic.thy	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy	Thu Jul 25 16:46:53 2013 +0200
@@ -113,6 +113,10 @@
 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
 by blast
 
+lemma fun_rel_def_butlast:
+  "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
+  unfolding fun_rel_def ..
+
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF/BNF_GFP.thy	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Thu Jul 25 16:46:53 2013 +0200
@@ -307,6 +307,27 @@
 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
 by auto
 
+definition image2p where
+  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
+
+lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
+  unfolding image2p_def by blast
+
+lemma image2p_eqI: "\<lbrakk>fx = f x; gy = g y; R x y\<rbrakk> \<Longrightarrow> (image2p f g R) fx gy"
+  unfolding image2p_def by blast
+
+lemma image2pE: "\<lbrakk>(image2p f g R) fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+  unfolding image2p_def by blast
+
+lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
+  unfolding fun_rel_def image2p_def by auto
+
+lemma convol_image_image2p: "<f o fst, g o snd> ` Collect (split R) \<subseteq> Collect (split (image2p f g R))"
+  unfolding convol_def image2p_def by fastforce
+
+lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
+  unfolding fun_rel_def image2p_def by auto
+
 ML_file "Tools/bnf_gfp_util.ML"
 ML_file "Tools/bnf_gfp_tactics.ML"
 ML_file "Tools/bnf_gfp.ML"
--- a/src/HOL/BNF/BNF_LFP.thy	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Thu Jul 25 16:46:53 2013 +0200
@@ -226,6 +226,12 @@
   shows "PROP P x y"
 by (rule `(\<And>x y. PROP P x y)`)
 
+lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
+  unfolding fun_rel_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
+
 ML_file "Tools/bnf_lfp_util.ML"
 ML_file "Tools/bnf_lfp_tactics.ML"
 ML_file "Tools/bnf_lfp.ML"
--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -374,7 +374,7 @@
 val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
 val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
 val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
-val map_transfer_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
+val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
 val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
 val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
 val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -217,13 +217,13 @@
     val n = length set_map's;
   in
     REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
-    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN
+    unfold_thms_tac ctxt @{thms fun_rel_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),
       REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
-      rtac @{thm vimagepI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
+      rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
       CONJ_WRAP' (fn thm =>
-        etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimagep]]}))
+        etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
       set_map's,
       rtac conjI,
       EVERY' (map (fn convol =>
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -54,6 +54,7 @@
   val ctor_injectN: string
   val ctor_foldN: string
   val ctor_fold_uniqueN: string
+  val ctor_fold_transferN: string
   val ctor_mapN: string
   val ctor_map_uniqueN: string
   val ctor_recN: string
@@ -82,6 +83,7 @@
   val dtor_strong_coinductN: string
   val dtor_unfoldN: string
   val dtor_unfold_uniqueN: string
+  val dtor_unfold_transferN: string
   val exhaustN: string
   val foldN: string
   val hsetN: string
@@ -169,6 +171,9 @@
   val mk_rel_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
+  val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list ->
+    term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
+    Proof.context -> thm list
 
   val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
       BNF_Def.bnf list -> local_theory -> 'a) ->
@@ -240,6 +245,7 @@
 val foldN = "fold"
 val unfoldN = unN ^ foldN
 val uniqueN = "_unique"
+val transferN = "_transfer"
 val simpsN = "simps"
 val ctorN = "ctor"
 val dtorN = "dtor"
@@ -247,6 +253,8 @@
 val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
 val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
 val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
+val ctor_fold_transferN = ctor_foldN ^ transferN
+val dtor_unfold_transferN = dtor_unfoldN ^ transferN
 val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
 val ctor_mapN = ctorN ^ "_" ^ mapN
 val dtor_mapN = dtorN ^ "_" ^ mapN
@@ -485,6 +493,25 @@
     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   end;
 
+fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy =
+  let
+    val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
+    val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
+    fun flip f x y = if fp = Greatest_FP then f y x else f x y;
+
+    val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis;
+    fun mk_transfer relphi pre_phi un_fold un_fold' =
+      fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold';
+    val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
+
+    val goal = fold_rev Logic.all (phis @ pre_phis)
+      (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
+  in
+    Goal.prove_sorry lthy [] [] goal tac
+    |> Thm.close_derivation
+    |> split_conj_thm
+  end;
+
 fun fp_bnf construct_fp bs resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -72,12 +72,12 @@
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
-    val ((((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
+    val ((((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
       (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy
       |> mk_TFrees live
       |> apfst (`(chop m))
       ||> mk_TFrees live
-      ||>> apfst (chop m)
+      ||>> apfst (`(chop m))
       ||> mk_TFrees live
       ||>> apfst (chop m)
       ||>> mk_TFrees m
@@ -1762,6 +1762,11 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val unfolds = map (Morphism.term phi) unfold_frees;
     val unfold_names = map (fst o dest_Const) unfolds;
+    fun mk_unfolds passives actives =
+      map3 (fn name => fn T => fn active =>
+        Const (name, Library.foldr (op -->)
+          (map2 (curry (op -->)) actives (mk_FTs (passives @ actives)), active --> T)))
+      unfold_names (mk_Ts passives) actives;
     fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
     val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
@@ -2116,9 +2121,11 @@
     val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts';
     val fstsTsTs' = map fst_const prodTsTs';
     val sndsTsTs' = map snd_const prodTsTs';
+    val activephiTs = map2 mk_pred2T activeAs activeBs;
     val activeJphiTs = map2 mk_pred2T Ts Ts';
-    val ((Jphis, activeJphis), names_lthy) = names_lthy
+    val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy
       |> mk_Frees "R" JphiTs
+      ||>> mk_Frees "S" activephiTs
       ||>> mk_Frees "JR" activeJphiTs;
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
     val in_rels = map in_rel_of_bnf bnfs;
@@ -2867,6 +2874,14 @@
         mk_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
           Jrel_coinduct_tac lthy;
 
+      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+      val dtor_unfold_transfer_thms =
+        mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis
+          (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
+          (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
+            dtor_unfold_thms)
+          lthy;
+
       val timer = time (timer "relator coinduction");
 
       val common_notes =
@@ -2874,7 +2889,8 @@
         (dtor_map_coinductN, [dtor_map_coinduct_thm]),
         (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
         (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
-        (rel_coinductN, [Jrel_coinduct_thm])]
+        (rel_coinductN, [Jrel_coinduct_thm]),
+        (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -115,6 +115,8 @@
   val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
     thm list -> thm list -> thm list list -> thm list list -> tactic
   val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
+  val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
+    {prems: thm list, context: Proof.context} -> tactic
   val mk_unique_mor_tac: thm list -> thm -> tactic
   val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
@@ -1458,4 +1460,23 @@
     (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
   end;
 
+fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
+  let
+    val n = length map_transfers;
+  in
+    unfold_thms_tac ctxt
+      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+    unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
+    HEADGOAL (EVERY'
+      [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct,
+      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 fun_relD}) map_transfer),
+        REPEAT_DETERM_N m o rtac @{thm id_transfer},
+        REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
+        etac @{thm predicate2D}, etac @{thm image2pI}])
+      map_transfers)])
+  end;
+
 end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -42,12 +42,12 @@
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
-    val (((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
+    val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
       activeCs), passiveXs), passiveYs) = names_lthy
       |> mk_TFrees live
       |> apfst (`(chop m))
       ||> mk_TFrees live
-      ||>> apfst (chop m)
+      ||>> apfst (`(chop m))
       ||>> mk_TFrees n
       ||>> mk_TFrees m
       ||> fst o mk_TFrees m;
@@ -1091,6 +1091,11 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val folds = map (Morphism.term phi) fold_frees;
     val fold_names = map (fst o dest_Const) folds;
+    fun mk_folds passives actives =
+      map3 (fn name => fn T => fn active =>
+        Const (name, Library.foldr (op -->)
+          (map2 (curry (op -->)) (mk_FTs (passives @ actives)) actives, T --> active)))
+      fold_names (mk_Ts passives) actives;
     fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
     val fold_defs = map (Morphism.thm phi) fold_def_frees;
@@ -1382,9 +1387,11 @@
       trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
 
     val IphiTs = map2 mk_pred2T passiveAs passiveBs;
+    val activephiTs = map2 mk_pred2T activeAs activeBs;
     val activeIphiTs = map2 mk_pred2T Ts Ts';
-    val ((Iphis, activeIphis), names_lthy) = names_lthy
+    val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy
       |> mk_Frees "R" IphiTs
+      ||>> mk_Frees "S" activephiTs
       ||>> mk_Frees "IR" activeIphiTs;
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
 
@@ -1801,12 +1808,20 @@
           (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs))
           lthy;
 
+      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+      val ctor_fold_transfer_thms =
+        mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
+          (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
+          (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms)
+          lthy;
+
       val timer = time (timer "relator induction");
 
       val common_notes =
         [(ctor_inductN, [ctor_induct_thm]),
         (ctor_induct2N, [ctor_induct2_thm]),
-        (rel_inductN, [Irel_induct_thm])]
+        (rel_inductN, [Irel_induct_thm]),
+        (ctor_fold_transferN, ctor_fold_transfer_thms)]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Jul 25 12:25:07 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Jul 25 16:46:53 2013 +0200
@@ -34,6 +34,8 @@
     thm list -> tactic
   val mk_iso_alt_tac: thm list -> thm -> tactic
   val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
+  val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
+    {prems: thm list, context: Proof.context} -> tactic
   val mk_least_min_alg_tac: thm -> thm -> tactic
   val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
     thm list list -> thm list list list -> thm list -> tactic
@@ -838,4 +840,24 @@
       IHs ctor_rels rel_mono_strongs)] 1
   end;
 
+fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} =
+  let
+    val n = length map_transfers;
+  in
+    unfold_thms_tac ctxt
+      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
+    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
+    HEADGOAL (EVERY'
+      [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct,
+      EVERY' (map (fn map_transfer => EVERY'
+        [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 fun_relD}) map_transfer),
+        REPEAT_DETERM_N m o rtac @{thm id_transfer},
+        REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel},
+        atac])
+      map_transfers)])
+  end;
+
 end;