src/HOL/Tools/BNF/bnf_def.ML

   val pred_map_of_bnf: bnf -> thm
   val pred_mono_strong0_of_bnf: bnf -> thm
   val pred_mono_strong_of_bnf: bnf -> thm
   val pred_set_of_bnf: bnf -> thm
   val pred_rel_of_bnf: bnf -> thm
+  val pred_transfer_of_bnf: bnf -> thm
+  val pred_True_of_bnf: bnf -> thm
   val rel_Grp_of_bnf: bnf -> thm
   val rel_OO_Grp_of_bnf: bnf -> thm
   val rel_OO_of_bnf: bnf -> thm
   val rel_cong0_of_bnf: bnf -> thm
   val rel_cong_of_bnf: bnf -> thm

   rel_reflp: thm lazy,
   rel_symp: thm lazy,
   rel_transp: thm lazy,
   rel_transfer: thm lazy,
   rel_eq_onp: thm lazy,
+  pred_transfer: thm lazy,
   pred_True: thm lazy,
   pred_map: thm lazy,
   pred_rel: thm lazy,
   pred_mono_strong0: thm lazy,
   pred_mono_strong: thm lazy,

 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
     inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id map_ident0 map_ident
     map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono
     rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl
-    rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp pred_True pred_map pred_rel
-    pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong pred_cong_simp = {
+    rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp pred_transfer pred_True
+    pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong pred_cong_simp = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
   collect_set_map = collect_set_map,
   in_bd = in_bd,

   rel_reflp = rel_reflp,
   rel_symp = rel_symp,
   rel_transp = rel_transp,
   set_transfer = set_transfer,
   rel_eq_onp = rel_eq_onp,
+  pred_transfer = pred_transfer,
   pred_True = pred_True,
   pred_map = pred_map,
   pred_rel = pred_rel,
   pred_mono_strong0 = pred_mono_strong0,
   pred_mono_strong = pred_mono_strong,

   rel_reflp,
   rel_symp,
   rel_transp,
   set_transfer,
   rel_eq_onp,
+  pred_transfer,
   pred_True,
   pred_map,
   pred_rel,
   pred_mono_strong0,
   pred_mono_strong,

     rel_reflp = Lazy.map f rel_reflp,
     rel_symp = Lazy.map f rel_symp,
     rel_transp = Lazy.map f rel_transp,
     set_transfer = Lazy.map (map f) set_transfer,
     rel_eq_onp = Lazy.map f rel_eq_onp,
+    pred_transfer = Lazy.map f pred_transfer,
     pred_True = Lazy.map f pred_True,
     pred_map = Lazy.map f pred_map,
     pred_rel = Lazy.map f pred_rel,
     pred_mono_strong0 = Lazy.map f pred_mono_strong0,
     pred_mono_strong = Lazy.map f pred_mono_strong,

 val map_id_of_bnf = Lazy.force o #map_id o #facts o rep_bnf;
 val map_ident0_of_bnf = Lazy.force o #map_ident0 o #facts o rep_bnf;
 val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
 val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
 val rel_eq_onp_of_bnf = Lazy.force o #rel_eq_onp o #facts o rep_bnf;
-val pred_rel_of_bnf = Lazy.force o #pred_rel o #facts o rep_bnf;
+val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
 val pred_map_of_bnf = Lazy.force o #pred_map o #facts o rep_bnf;
 val pred_mono_strong0_of_bnf = Lazy.force o #pred_mono_strong0 o #facts o rep_bnf;
 val pred_mono_strong_of_bnf = Lazy.force o #pred_mono_strong o #facts o rep_bnf;
 val pred_cong0_of_bnf = Lazy.force o #pred_cong0 o #facts o rep_bnf;
 val pred_cong_of_bnf = Lazy.force o #pred_cong o #facts o rep_bnf;
 val pred_cong_simp_of_bnf = Lazy.force o #pred_cong_simp o #facts o rep_bnf;
-val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
+val pred_rel_of_bnf = Lazy.force o #pred_rel o #facts o rep_bnf;
 val pred_set_of_bnf = #pred_set o #axioms o rep_bnf;
+val pred_transfer_of_bnf = Lazy.force o #pred_transfer o #facts o rep_bnf;
+val pred_True_of_bnf = Lazy.force o #pred_True o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
 val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
 val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
 val rel_cong0_of_bnf = Lazy.force o #rel_cong0 o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;

 val map_idN = "map_id";
 val map_identN = "map_ident";
 val map_transferN = "map_transfer";
 val pred_mono_strong0N = "pred_mono_strong0";
 val pred_mono_strongN = "pred_mono_strong";
+val pred_transferN = "pred_transfer";
 val pred_TrueN = "pred_True";
 val pred_mapN = "pred_map";
 val pred_relN = "pred_rel";
 val pred_setN = "pred_set";
 val pred_congN = "pred_cong";

            (pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []),
            (pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs),
            (pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []),
            (pred_mapN, [Lazy.force (#pred_map facts)], []),
            (pred_relN, [Lazy.force (#pred_rel facts)], []),
+           (pred_transferN, [Lazy.force (#pred_transfer facts)], []),
            (pred_TrueN, [Lazy.force (#pred_True facts)], []),
            (pred_setN, [#pred_set axioms], []),
            (rel_comppN, [Lazy.force (#rel_OO facts)], []),
            (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
            (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),

             |> Thm.close_derivation
           end;
 
         val map_transfer = Lazy.lazy mk_map_transfer;
 
+        fun mk_pred_transfer () =
+          let
+            val iff = HOLogic.eq_const HOLogic.boolT;
+            val prem_rels = map (fn T => mk_rel_fun T iff) Rs;
+            val prem_elems = mk_rel_fun (Term.list_comb (rel, Rs)) iff;
+            val goal = HOLogic.mk_Trueprop
+              (fold_rev mk_rel_fun prem_rels prem_elems $ pred $ pred');
+            val vars = Variable.add_free_names lthy goal [];
+          in
+            Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
+              mk_pred_transfer_tac ctxt live (Lazy.force in_rel) (Lazy.force pred_map)
+                (Lazy.force pred_cong))
+            |> Thm.close_derivation
+          end;
+
+        val pred_transfer = Lazy.lazy mk_pred_transfer;
+
         fun mk_rel_transfer () =
           let
             val iff = HOLogic.eq_const HOLogic.boolT;
             val prem_rels =
               map2 (fn T1 => fn T2 => mk_rel_fun T1 (mk_rel_fun T2 iff)) S_AsCs S_BsEs;

         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
           in_mono in_rel inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id
           map_ident0 map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp
           rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep
           rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp
-          pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong
-          pred_cong_simp;
+          pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0
+          pred_cong pred_cong_simp;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
         val bnf_rel =
           Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;