transfer rule for {c,d}tor_{,un}fold
authortraytel
Thu Jul 25 16:46:53 2013 +0200 (2013-07-25)
changeset 52731dacd47a0633f
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
     1.1 --- a/src/HOL/BNF/BNF.thy	Thu Jul 25 12:25:07 2013 +0200
     1.2 +++ b/src/HOL/BNF/BNF.thy	Thu Jul 25 16:46:53 2013 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  imports More_BNFs
     1.5  begin
     1.6  
     1.7 -hide_const (open) vimagep Gr Grp collect fsts snds setl setr 
     1.8 +hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr 
     1.9    convol thePull pick_middlep fstOp sndOp csquare inver
    1.10    image2 relImage relInvImage prefCl PrefCl Succ Shift shift
    1.11  
     2.1 --- a/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 12:25:07 2013 +0200
     2.2 +++ b/src/HOL/BNF/BNF_Def.thy	Thu Jul 25 16:46:53 2013 +0200
     2.3 @@ -193,20 +193,20 @@
     2.4    ((\<lambda>i. if i \<in> g ` C then the_inv_into C g i else x) o g) i = id i"
     2.5  unfolding Func_def by (auto elim: the_inv_into_f_f)
     2.6  
     2.7 -definition vimagep where
     2.8 -  "vimagep f g R = (\<lambda>x y. R (f x) (g y))"
     2.9 +definition vimage2p where
    2.10 +  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
    2.11  
    2.12 -lemma vimagepI: "R (f x) (g y) \<Longrightarrow> vimagep f g R x y"
    2.13 -  unfolding vimagep_def by -
    2.14 +lemma vimage2pI: "R (f x) (g y) \<Longrightarrow> vimage2p f g R x y"
    2.15 +  unfolding vimage2p_def by -
    2.16  
    2.17 -lemma vimagepD: "vimagep f g R x y \<Longrightarrow> R (f x) (g y)"
    2.18 -  unfolding vimagep_def by -
    2.19 +lemma vimage2pD: "vimage2p f g R x y \<Longrightarrow> R (f x) (g y)"
    2.20 +  unfolding vimage2p_def by -
    2.21  
    2.22 -lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \<le> vimagep f g S)"
    2.23 -  unfolding fun_rel_def vimagep_def by auto
    2.24 +lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \<le> vimage2p f g S)"
    2.25 +  unfolding fun_rel_def vimage2p_def by auto
    2.26  
    2.27 -lemma convol_image_vimagep: "<f o fst, g o snd> ` Collect (split (vimagep f g R)) \<subseteq> Collect (split R)"
    2.28 -  unfolding vimagep_def convol_def by auto
    2.29 +lemma convol_image_vimage2p: "<f o fst, g o snd> ` Collect (split (vimage2p f g R)) \<subseteq> Collect (split R)"
    2.30 +  unfolding vimage2p_def convol_def by auto
    2.31  
    2.32  ML_file "Tools/bnf_def_tactics.ML"
    2.33  ML_file "Tools/bnf_def.ML"
     3.1 --- a/src/HOL/BNF/BNF_FP_Basic.thy	Thu Jul 25 12:25:07 2013 +0200
     3.2 +++ b/src/HOL/BNF/BNF_FP_Basic.thy	Thu Jul 25 16:46:53 2013 +0200
     3.3 @@ -113,6 +113,10 @@
     3.4  lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
     3.5  by blast
     3.6  
     3.7 +lemma fun_rel_def_butlast:
     3.8 +  "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
     3.9 +  unfolding fun_rel_def ..
    3.10 +
    3.11  ML_file "Tools/bnf_fp_util.ML"
    3.12  ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
    3.13  ML_file "Tools/bnf_fp_def_sugar.ML"
     4.1 --- a/src/HOL/BNF/BNF_GFP.thy	Thu Jul 25 12:25:07 2013 +0200
     4.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Thu Jul 25 16:46:53 2013 +0200
     4.3 @@ -307,6 +307,27 @@
     4.4  lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
     4.5  by auto
     4.6  
     4.7 +definition image2p where
     4.8 +  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
     4.9 +
    4.10 +lemma image2pI: "R x y \<Longrightarrow> (image2p f g R) (f x) (g y)"
    4.11 +  unfolding image2p_def by blast
    4.12 +
    4.13 +lemma image2p_eqI: "\<lbrakk>fx = f x; gy = g y; R x y\<rbrakk> \<Longrightarrow> (image2p f g R) fx gy"
    4.14 +  unfolding image2p_def by blast
    4.15 +
    4.16 +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"
    4.17 +  unfolding image2p_def by blast
    4.18 +
    4.19 +lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \<le> S)"
    4.20 +  unfolding fun_rel_def image2p_def by auto
    4.21 +
    4.22 +lemma convol_image_image2p: "<f o fst, g o snd> ` Collect (split R) \<subseteq> Collect (split (image2p f g R))"
    4.23 +  unfolding convol_def image2p_def by fastforce
    4.24 +
    4.25 +lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
    4.26 +  unfolding fun_rel_def image2p_def by auto
    4.27 +
    4.28  ML_file "Tools/bnf_gfp_util.ML"
    4.29  ML_file "Tools/bnf_gfp_tactics.ML"
    4.30  ML_file "Tools/bnf_gfp.ML"
     5.1 --- a/src/HOL/BNF/BNF_LFP.thy	Thu Jul 25 12:25:07 2013 +0200
     5.2 +++ b/src/HOL/BNF/BNF_LFP.thy	Thu Jul 25 16:46:53 2013 +0200
     5.3 @@ -226,6 +226,12 @@
     5.4    shows "PROP P x y"
     5.5  by (rule `(\<And>x y. PROP P x y)`)
     5.6  
     5.7 +lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
     5.8 +  unfolding fun_rel_def vimage2p_def by auto
     5.9 +
    5.10 +lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
    5.11 +  unfolding vimage2p_def by auto
    5.12 +
    5.13  ML_file "Tools/bnf_lfp_util.ML"
    5.14  ML_file "Tools/bnf_lfp_tactics.ML"
    5.15  ML_file "Tools/bnf_lfp.ML"
     6.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Jul 25 12:25:07 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Jul 25 16:46:53 2013 +0200
     6.3 @@ -374,7 +374,7 @@
     6.4  val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf;
     6.5  val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
     6.6  val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
     6.7 -val map_transfer_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
     6.8 +val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
     6.9  val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
    6.10  val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
    6.11  val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
     7.1 --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Jul 25 12:25:07 2013 +0200
     7.2 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Thu Jul 25 16:46:53 2013 +0200
     7.3 @@ -217,13 +217,13 @@
     7.4      val n = length set_map's;
     7.5    in
     7.6      REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
     7.7 -    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN
     7.8 +    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
     7.9      HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
    7.10        rtac @{thm predicate2I}, dtac (in_rel RS iffD1),
    7.11        REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt,
    7.12 -      rtac @{thm vimagepI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    7.13 +      rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
    7.14        CONJ_WRAP' (fn thm =>
    7.15 -        etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimagep]]}))
    7.16 +        etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]}))
    7.17        set_map's,
    7.18        rtac conjI,
    7.19        EVERY' (map (fn convol =>
     8.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jul 25 12:25:07 2013 +0200
     8.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Jul 25 16:46:53 2013 +0200
     8.3 @@ -54,6 +54,7 @@
     8.4    val ctor_injectN: string
     8.5    val ctor_foldN: string
     8.6    val ctor_fold_uniqueN: string
     8.7 +  val ctor_fold_transferN: string
     8.8    val ctor_mapN: string
     8.9    val ctor_map_uniqueN: string
    8.10    val ctor_recN: string
    8.11 @@ -82,6 +83,7 @@
    8.12    val dtor_strong_coinductN: string
    8.13    val dtor_unfoldN: string
    8.14    val dtor_unfold_uniqueN: string
    8.15 +  val dtor_unfold_transferN: string
    8.16    val exhaustN: string
    8.17    val foldN: string
    8.18    val hsetN: string
    8.19 @@ -169,6 +171,9 @@
    8.20    val mk_rel_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list ->
    8.21      term list -> term list -> term list -> term list ->
    8.22      ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
    8.23 +  val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list ->
    8.24 +    term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
    8.25 +    Proof.context -> thm list
    8.26  
    8.27    val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
    8.28        BNF_Def.bnf list -> local_theory -> 'a) ->
    8.29 @@ -240,6 +245,7 @@
    8.30  val foldN = "fold"
    8.31  val unfoldN = unN ^ foldN
    8.32  val uniqueN = "_unique"
    8.33 +val transferN = "_transfer"
    8.34  val simpsN = "simps"
    8.35  val ctorN = "ctor"
    8.36  val dtorN = "dtor"
    8.37 @@ -247,6 +253,8 @@
    8.38  val dtor_unfoldN = dtorN ^ "_" ^ unfoldN
    8.39  val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
    8.40  val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
    8.41 +val ctor_fold_transferN = ctor_foldN ^ transferN
    8.42 +val dtor_unfold_transferN = dtor_unfoldN ^ transferN
    8.43  val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN
    8.44  val ctor_mapN = ctorN ^ "_" ^ mapN
    8.45  val dtor_mapN = dtorN ^ "_" ^ mapN
    8.46 @@ -485,6 +493,25 @@
    8.47      |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
    8.48    end;
    8.49  
    8.50 +fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy =
    8.51 +  let
    8.52 +    val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
    8.53 +    val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
    8.54 +    fun flip f x y = if fp = Greatest_FP then f y x else f x y;
    8.55 +
    8.56 +    val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis;
    8.57 +    fun mk_transfer relphi pre_phi un_fold un_fold' =
    8.58 +      fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold';
    8.59 +    val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
    8.60 +
    8.61 +    val goal = fold_rev Logic.all (phis @ pre_phis)
    8.62 +      (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
    8.63 +  in
    8.64 +    Goal.prove_sorry lthy [] [] goal tac
    8.65 +    |> Thm.close_derivation
    8.66 +    |> split_conj_thm
    8.67 +  end;
    8.68 +
    8.69  fun fp_bnf construct_fp bs resBs eqs lthy =
    8.70    let
    8.71      val timer = time (Timer.startRealTimer ());
     9.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jul 25 12:25:07 2013 +0200
     9.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Jul 25 16:46:53 2013 +0200
     9.3 @@ -72,12 +72,12 @@
     9.4      val names_lthy = fold Variable.declare_typ deads lthy;
     9.5  
     9.6      (* tvars *)
     9.7 -    val ((((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
     9.8 +    val ((((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
     9.9        (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy
    9.10        |> mk_TFrees live
    9.11        |> apfst (`(chop m))
    9.12        ||> mk_TFrees live
    9.13 -      ||>> apfst (chop m)
    9.14 +      ||>> apfst (`(chop m))
    9.15        ||> mk_TFrees live
    9.16        ||>> apfst (chop m)
    9.17        ||>> mk_TFrees m
    9.18 @@ -1762,6 +1762,11 @@
    9.19      val phi = Proof_Context.export_morphism lthy_old lthy;
    9.20      val unfolds = map (Morphism.term phi) unfold_frees;
    9.21      val unfold_names = map (fst o dest_Const) unfolds;
    9.22 +    fun mk_unfolds passives actives =
    9.23 +      map3 (fn name => fn T => fn active =>
    9.24 +        Const (name, Library.foldr (op -->)
    9.25 +          (map2 (curry (op -->)) actives (mk_FTs (passives @ actives)), active --> T)))
    9.26 +      unfold_names (mk_Ts passives) actives;
    9.27      fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->)
    9.28        (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
    9.29      val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees;
    9.30 @@ -2116,9 +2121,11 @@
    9.31      val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts';
    9.32      val fstsTsTs' = map fst_const prodTsTs';
    9.33      val sndsTsTs' = map snd_const prodTsTs';
    9.34 +    val activephiTs = map2 mk_pred2T activeAs activeBs;
    9.35      val activeJphiTs = map2 mk_pred2T Ts Ts';
    9.36 -    val ((Jphis, activeJphis), names_lthy) = names_lthy
    9.37 +    val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy
    9.38        |> mk_Frees "R" JphiTs
    9.39 +      ||>> mk_Frees "S" activephiTs
    9.40        ||>> mk_Frees "JR" activeJphiTs;
    9.41      val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
    9.42      val in_rels = map in_rel_of_bnf bnfs;
    9.43 @@ -2867,6 +2874,14 @@
    9.44          mk_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
    9.45            Jrel_coinduct_tac lthy;
    9.46  
    9.47 +      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    9.48 +      val dtor_unfold_transfer_thms =
    9.49 +        mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis
    9.50 +          (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
    9.51 +          (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
    9.52 +            dtor_unfold_thms)
    9.53 +          lthy;
    9.54 +
    9.55        val timer = time (timer "relator coinduction");
    9.56  
    9.57        val common_notes =
    9.58 @@ -2874,7 +2889,8 @@
    9.59          (dtor_map_coinductN, [dtor_map_coinduct_thm]),
    9.60          (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
    9.61          (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
    9.62 -        (rel_coinductN, [Jrel_coinduct_thm])]
    9.63 +        (rel_coinductN, [Jrel_coinduct_thm]),
    9.64 +        (dtor_unfold_transferN, dtor_unfold_transfer_thms)]
    9.65          |> map (fn (thmN, thms) =>
    9.66            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    9.67  
    10.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Jul 25 12:25:07 2013 +0200
    10.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu Jul 25 16:46:53 2013 +0200
    10.3 @@ -115,6 +115,8 @@
    10.4    val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
    10.5      thm list -> thm list -> thm list list -> thm list list -> tactic
    10.6    val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
    10.7 +  val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
    10.8 +    {prems: thm list, context: Proof.context} -> tactic
    10.9    val mk_unique_mor_tac: thm list -> thm -> tactic
   10.10    val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
   10.11      {prems: 'a, context: Proof.context} -> tactic
   10.12 @@ -1458,4 +1460,23 @@
   10.13      (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
   10.14    end;
   10.15  
   10.16 +fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} =
   10.17 +  let
   10.18 +    val n = length map_transfers;
   10.19 +  in
   10.20 +    unfold_thms_tac ctxt
   10.21 +      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
   10.22 +    unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN
   10.23 +    HEADGOAL (EVERY'
   10.24 +      [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct,
   10.25 +      EVERY' (map (fn map_transfer => EVERY'
   10.26 +        [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt,
   10.27 +        SELECT_GOAL (unfold_thms_tac ctxt unfolds),
   10.28 +        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
   10.29 +        REPEAT_DETERM_N m o rtac @{thm id_transfer},
   10.30 +        REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p},
   10.31 +        etac @{thm predicate2D}, etac @{thm image2pI}])
   10.32 +      map_transfers)])
   10.33 +  end;
   10.34 +
   10.35  end;
    11.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Jul 25 12:25:07 2013 +0200
    11.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Jul 25 16:46:53 2013 +0200
    11.3 @@ -42,12 +42,12 @@
    11.4      val names_lthy = fold Variable.declare_typ deads lthy;
    11.5  
    11.6      (* tvars *)
    11.7 -    val (((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)),
    11.8 +    val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
    11.9        activeCs), passiveXs), passiveYs) = names_lthy
   11.10        |> mk_TFrees live
   11.11        |> apfst (`(chop m))
   11.12        ||> mk_TFrees live
   11.13 -      ||>> apfst (chop m)
   11.14 +      ||>> apfst (`(chop m))
   11.15        ||>> mk_TFrees n
   11.16        ||>> mk_TFrees m
   11.17        ||> fst o mk_TFrees m;
   11.18 @@ -1091,6 +1091,11 @@
   11.19      val phi = Proof_Context.export_morphism lthy_old lthy;
   11.20      val folds = map (Morphism.term phi) fold_frees;
   11.21      val fold_names = map (fst o dest_Const) folds;
   11.22 +    fun mk_folds passives actives =
   11.23 +      map3 (fn name => fn T => fn active =>
   11.24 +        Const (name, Library.foldr (op -->)
   11.25 +          (map2 (curry (op -->)) (mk_FTs (passives @ actives)) actives, T --> active)))
   11.26 +      fold_names (mk_Ts passives) actives;
   11.27      fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->)
   11.28        (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
   11.29      val fold_defs = map (Morphism.thm phi) fold_def_frees;
   11.30 @@ -1382,9 +1387,11 @@
   11.31        trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
   11.32  
   11.33      val IphiTs = map2 mk_pred2T passiveAs passiveBs;
   11.34 +    val activephiTs = map2 mk_pred2T activeAs activeBs;
   11.35      val activeIphiTs = map2 mk_pred2T Ts Ts';
   11.36 -    val ((Iphis, activeIphis), names_lthy) = names_lthy
   11.37 +    val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy
   11.38        |> mk_Frees "R" IphiTs
   11.39 +      ||>> mk_Frees "S" activephiTs
   11.40        ||>> mk_Frees "IR" activeIphiTs;
   11.41      val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
   11.42  
   11.43 @@ -1801,12 +1808,20 @@
   11.44            (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs))
   11.45            lthy;
   11.46  
   11.47 +      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
   11.48 +      val ctor_fold_transfer_thms =
   11.49 +        mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
   11.50 +          (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
   11.51 +          (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms)
   11.52 +          lthy;
   11.53 +
   11.54        val timer = time (timer "relator induction");
   11.55  
   11.56        val common_notes =
   11.57          [(ctor_inductN, [ctor_induct_thm]),
   11.58          (ctor_induct2N, [ctor_induct2_thm]),
   11.59 -        (rel_inductN, [Irel_induct_thm])]
   11.60 +        (rel_inductN, [Irel_induct_thm]),
   11.61 +        (ctor_fold_transferN, ctor_fold_transfer_thms)]
   11.62          |> map (fn (thmN, thms) =>
   11.63            ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
   11.64  
    12.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Jul 25 12:25:07 2013 +0200
    12.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Jul 25 16:46:53 2013 +0200
    12.3 @@ -34,6 +34,8 @@
    12.4      thm list -> tactic
    12.5    val mk_iso_alt_tac: thm list -> thm -> tactic
    12.6    val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic
    12.7 +  val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
    12.8 +    {prems: thm list, context: Proof.context} -> tactic
    12.9    val mk_least_min_alg_tac: thm -> thm -> tactic
   12.10    val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
   12.11      thm list list -> thm list list list -> thm list -> tactic
   12.12 @@ -838,4 +840,24 @@
   12.13        IHs ctor_rels rel_mono_strongs)] 1
   12.14    end;
   12.15  
   12.16 +fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} =
   12.17 +  let
   12.18 +    val n = length map_transfers;
   12.19 +  in
   12.20 +    unfold_thms_tac ctxt
   12.21 +      @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN
   12.22 +    unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN
   12.23 +    HEADGOAL (EVERY'
   12.24 +      [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct,
   12.25 +      EVERY' (map (fn map_transfer => EVERY'
   12.26 +        [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}],
   12.27 +        SELECT_GOAL (unfold_thms_tac ctxt folds),
   12.28 +        etac @{thm predicate2D_vimage2p},
   12.29 +        rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer),
   12.30 +        REPEAT_DETERM_N m o rtac @{thm id_transfer},
   12.31 +        REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel},
   12.32 +        atac])
   12.33 +      map_transfers)])
   12.34 +  end;
   12.35 +
   12.36  end;