generate 'corec_transfer' for codatatypes
authordesharna
Thu Sep 25 16:35:56 2014 +0200 (2014-09-25)
changeset 58448a1d4e7473c98
parent 58447 ea23ce403a3e
child 58449 e2d3c296b9fe
generate 'corec_transfer' for codatatypes
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Lifting_Product.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 16:35:54 2014 +0200
     1.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Thu Sep 25 16:35:56 2014 +0200
     1.3 @@ -213,6 +213,28 @@
     1.4    "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
     1.5    unfolding rel_fun_def by simp
     1.6  
     1.7 +lemma If_transfer: "rel_fun (op =) (rel_fun A (rel_fun A A)) If If"
     1.8 +  unfolding rel_fun_def by simp
     1.9 +
    1.10 +lemma Abs_transfer:
    1.11 +  assumes type_copy1: "type_definition Rep1 Abs1 UNIV"
    1.12 +  assumes type_copy2: "type_definition Rep2 Abs2 UNIV"
    1.13 +  shows "rel_fun R (vimage2p Rep1 Rep2 R) Abs1 Abs2"
    1.14 +  unfolding vimage2p_def rel_fun_def
    1.15 +    type_definition.Abs_inverse[OF type_copy1 UNIV_I]
    1.16 +    type_definition.Abs_inverse[OF type_copy2 UNIV_I] by simp
    1.17 +
    1.18 +lemma Inl_transfer:
    1.19 +  "rel_fun S (rel_sum S T) Inl Inl"
    1.20 +  by auto
    1.21 +
    1.22 +lemma Inr_transfer:
    1.23 +  "rel_fun T (rel_sum S T) Inr Inr"
    1.24 +  by auto
    1.25 +
    1.26 +lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair"
    1.27 +  unfolding rel_fun_def rel_prod_def by simp
    1.28 +
    1.29  ML_file "Tools/BNF/bnf_fp_util.ML"
    1.30  ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
    1.31  ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
     2.1 --- a/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 16:35:54 2014 +0200
     2.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Thu Sep 25 16:35:56 2014 +0200
     2.3 @@ -189,14 +189,6 @@
     2.4    "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"
     2.5    unfolding rel_prod_def rel_fun_def convol_def by auto
     2.6  
     2.7 -lemma Inl_transfer:
     2.8 -  "rel_fun S (rel_sum S T) Inl Inl"
     2.9 -  by auto
    2.10 -
    2.11 -lemma Inr_transfer:
    2.12 -  "rel_fun T (rel_sum S T) Inr Inr"
    2.13 -  by auto
    2.14 -
    2.15  lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
    2.16    by (rule ssubst)
    2.17  
     3.1 --- a/src/HOL/Lifting_Product.thy	Thu Sep 25 16:35:54 2014 +0200
     3.2 +++ b/src/HOL/Lifting_Product.thy	Thu Sep 25 16:35:56 2014 +0200
     3.3 @@ -19,9 +19,7 @@
     3.4  begin
     3.5  interpretation lifting_syntax .
     3.6  
     3.7 -lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
     3.8 -  unfolding rel_fun_def rel_prod_def by simp
     3.9 -
    3.10 +declare Pair_transfer [transfer_rule]
    3.11  declare fst_transfer [transfer_rule]
    3.12  declare snd_transfer [transfer_rule]
    3.13  declare case_prod_transfer [transfer_rule]
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 16:35:54 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Sep 25 16:35:56 2014 +0200
     4.3 @@ -73,7 +73,8 @@
     4.4       (term list
     4.5        * (typ list list * typ list list list list * term list list * term list list list list) option
     4.6        * (string * term list * term list list
     4.7 -         * ((term list list * term list list list) * typ list)) option)
     4.8 +         * (((term list list * term list list * term list list list list * term list list list list)
     4.9 +             * term list list list) * typ list)) option)
    4.10       * Proof.context
    4.11    val repair_nullary_single_ctr: typ list list -> typ list list
    4.12    val mk_corec_p_pred_types: typ list -> int list -> typ list list
    4.13 @@ -88,8 +89,9 @@
    4.14      (string -> binding) -> typ list -> typ list -> term list -> term -> Proof.context ->
    4.15      (term * thm) * Proof.context
    4.16    val define_corec: 'a * term list * term list list
    4.17 -      * ((term list list * term list list list) * typ list) -> (string -> binding) -> 'b list ->
    4.18 -    typ list -> term list -> term -> local_theory -> (term * thm) * local_theory
    4.19 +      * (((term list list * term list list * term list list list list * term list list list list)
    4.20 +          * term list list list) * typ list) -> (string -> binding) -> 'b list -> typ list ->
    4.21 +    term list -> term -> local_theory -> (term * thm) * local_theory
    4.22    val mk_induct_attrs: term list list -> Token.src list
    4.23    val mk_coinduct_attrs: typ list -> term list list -> term list list -> int list list ->
    4.24      Token.src list * Token.src list
    4.25 @@ -99,7 +101,9 @@
    4.26       typ list list list -> thm list -> thm list -> thm list -> term list list -> thm list list ->
    4.27       term list -> thm list -> Proof.context -> lfp_sugar_thms
    4.28    val derive_coinduct_corecs_thms_for_types: BNF_Def.bnf list ->
    4.29 -    string * term list * term list list * ((term list list * term list list list) * typ list) ->
    4.30 +    string * term list * term list list
    4.31 +      * (((term list list * term list list * term list list list list * term list list list list)
    4.32 +          * term list list list) * typ list) ->
    4.33      thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> typ list -> typ list ->
    4.34      typ list -> typ list list list -> int list list -> int list list -> int list -> thm list ->
    4.35      thm list -> (thm -> thm) -> thm list list -> Ctr_Sugar.ctr_sugar list -> term list ->
    4.36 @@ -138,6 +142,7 @@
    4.37  val ctr_transferN = "ctr_transfer";
    4.38  val disc_transferN = "disc_transfer";
    4.39  val corec_codeN = "corec_code";
    4.40 +val corec_transferN = "corec_transfer";
    4.41  val map_disc_iffN = "map_disc_iff";
    4.42  val map_selN = "map_sel";
    4.43  val rec_transferN = "rec_transfer";
    4.44 @@ -1002,7 +1007,7 @@
    4.45      val cgssss = map2 (map o map o map o rapp) cs gssss;
    4.46      val cqgsss = map3 (map3 (map3 build_dtor_corec_arg)) g_Tsss cqssss cgssss;
    4.47    in
    4.48 -    ((x, cs, cpss, ((pgss, cqgsss), corec_types)), lthy)
    4.49 +    ((x, cs, cpss, (((pgss, pss, qssss, gssss), cqgsss), corec_types)), lthy)
    4.50    end;
    4.51  
    4.52  fun mk_co_recs_prelims fp ctr_Tsss fpTs Cs absTs repTs ns mss xtor_co_recs0 lthy =
    4.53 @@ -1064,7 +1069,7 @@
    4.54             ctor_rec_absTs reps fss xssss)))
    4.55    end;
    4.56  
    4.57 -fun define_corec (_, cs, cpss, ((pgss, cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
    4.58 +fun define_corec (_, cs, cpss, (((pgss, _, _, _), cqgsss), f_absTs)) mk_binding fpTs Cs abss dtor_corec =
    4.59    let
    4.60      val nn = length fpTs;
    4.61      val fpT = range_type (snd (strip_typeN nn (fastype_of dtor_corec)));
    4.62 @@ -1485,7 +1490,7 @@
    4.63        end) (transpose setss)
    4.64    end;
    4.65  
    4.66 -fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, ((pgss, cqgsss), _))
    4.67 +fun derive_coinduct_corecs_thms_for_types pre_bnfs (x, cs, cpss, (((pgss, _, _, _), cqgsss), _))
    4.68      dtor_coinduct dtor_injects dtor_ctors dtor_corec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss
    4.69      kss mss ns fp_abs_inverses abs_inverses mk_vimage2p ctr_defss (ctr_sugars : ctr_sugar list)
    4.70      corecs corec_defs export_args lthy =
    4.71 @@ -1799,7 +1804,7 @@
    4.72               dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
    4.73               ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss, xtor_rel_thms,
    4.74               xtor_co_rec_thms, rel_xtor_co_induct_thm, dtor_set_induct_thms,
    4.75 -             ctor_rec_transfer_thms, ...},
    4.76 +             xtor_co_rec_transfer_thms, ...},
    4.77             lthy)) =
    4.78        fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
    4.79          (map dest_TFree killed_As) fp_eqs no_defs_lthy
    4.80 @@ -2005,7 +2010,7 @@
    4.81          rel_distincts setss =
    4.82        injects @ distincts @ case_thms @ co_recs @ mapsx @ rel_injects @ rel_distincts @ flat setss;
    4.83  
    4.84 -    fun derive_rec_transfer_thms lthy recs rec_defs ns =
    4.85 +    fun mk_co_rec_transfer_goals lthy co_recs =
    4.86        let
    4.87          val liveAsBs = filter (op <>) (As ~~ Bs);
    4.88          val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
    4.89 @@ -2014,14 +2019,17 @@
    4.90            |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
    4.91            ||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
    4.92  
    4.93 -        val recBs = map B_ify recs;
    4.94 -        val goals = map2 (mk_parametricity_goal lthy (Rs @ Ss)) recs recBs;
    4.95 +        val co_recBs = map B_ify co_recs;
    4.96        in
    4.97 +        (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy)
    4.98 +      end;
    4.99 +
   4.100 +    fun derive_rec_transfer_thms lthy recs rec_defs =
   4.101 +      let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in
   4.102          Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   4.103            (fn {context = ctxt, prems = _} =>
   4.104 -             mk_rec_transfer_tac names_lthy nn ns (map (certify ctxt) Ss)
   4.105 -               (map (certify ctxt) Rs) rec_defs ctor_rec_transfer_thms pre_rel_defs
   4.106 -               live_nesting_rel_eqs)
   4.107 +             mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs
   4.108 +               xtor_co_rec_transfer_thms pre_rel_defs live_nesting_rel_eqs)
   4.109          |> Conjunction.elim_balanced nn
   4.110          |> Proof_Context.export names_lthy lthy
   4.111          |> map Thm.close_derivation
   4.112 @@ -2038,8 +2046,7 @@
   4.113  
   4.114          val rec_transfer_thmss =
   4.115            if live = 0 then replicate nn []
   4.116 -          else
   4.117 -            map single (derive_rec_transfer_thms lthy recs rec_defs ns);
   4.118 +          else map single (derive_rec_transfer_thms lthy recs rec_defs);
   4.119  
   4.120          val induct_type_attr = Attrib.internal o K o Induct.induct_type;
   4.121          val induct_pred_attr = Attrib.internal o K o Induct.induct_pred;
   4.122 @@ -2090,6 +2097,21 @@
   4.123            rel_injectss rel_distinctss
   4.124        end;
   4.125  
   4.126 +    fun derive_corec_transfer_thms lthy corecs corec_defs =
   4.127 +      let
   4.128 +        val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy corecs;
   4.129 +        val (_, _, _, (((pgss, pss, qssss, gssss), _), _)) = the corecs_args_types;
   4.130 +      in
   4.131 +        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
   4.132 +          (fn {context = ctxt, prems = _} =>
   4.133 +             mk_corec_transfer_tac ctxt (map (certify ctxt) Ss) (map (certify ctxt) Rs)
   4.134 +               type_definitions corec_defs xtor_co_rec_transfer_thms pre_rel_defs
   4.135 +               live_nesting_rel_eqs (flat pgss) pss qssss gssss)
   4.136 +        |> Conjunction.elim_balanced (length goals)
   4.137 +        |> Proof_Context.export names_lthy lthy
   4.138 +        |> map Thm.close_derivation
   4.139 +      end;
   4.140 +
   4.141      fun derive_note_coinduct_corecs_thms_for_types
   4.142          ((((mapss, rel_injectss, rel_distinctss, setss), (_, _, ctr_defss, ctr_sugars)),
   4.143            (corecs, corec_defs)), lthy) =
   4.144 @@ -2122,6 +2144,10 @@
   4.145  
   4.146          val flat_corec_thms = append oo append;
   4.147  
   4.148 +        val corec_transfer_thmss =
   4.149 +          if live = 0 then replicate nn []
   4.150 +          else map single (derive_corec_transfer_thms lthy corecs corec_defs);
   4.151 +
   4.152          val ((rel_coinduct_thmss, common_rel_coinduct_thms),
   4.153               (rel_coinduct_attrs, common_rel_coinduct_attrs)) =
   4.154            if live = 0 then
   4.155 @@ -2168,6 +2194,7 @@
   4.156             (corec_discN, corec_disc_thmss, K []),
   4.157             (corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
   4.158             (corec_selN, corec_sel_thmss, K corec_sel_attrs),
   4.159 +           (corec_transferN, corec_transfer_thmss, K []),
   4.160             (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
   4.161             (simpsN, simp_thmss, K [])]
   4.162            |> massage_multi_notes fp_b_names fpTs;
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 16:35:54 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Sep 25 16:35:56 2014 +0200
     5.3 @@ -19,6 +19,9 @@
     5.4      thm list list list -> tactic
     5.5    val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
     5.6    val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
     5.7 +  val mk_corec_transfer_tac: Proof.context -> cterm list -> cterm list -> thm list -> thm list ->
     5.8 +    thm list -> thm list -> thm list -> ''a list -> ''a list list -> ''a list list list list ->
     5.9 +    ''a list list list list -> tactic
    5.10    val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
    5.11      tactic
    5.12    val mk_ctr_transfer_tac: Proof.context -> thm list -> thm list -> tactic
    5.13 @@ -214,6 +217,71 @@
    5.14        (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
    5.15      (map rtac case_splits' @ [K all_tac]) corecs discs);
    5.16  
    5.17 +fun mk_corec_transfer_tac ctxt actives passives type_definitions corec_defs dtor_corec_transfers
    5.18 +    rel_pre_T_defs rel_eqs pgs pss qssss gssss =
    5.19 +  let
    5.20 +    val num_pgs = length pgs;
    5.21 +    fun prem_no_of x = 1 + find_index (curry (op =) x) pgs;
    5.22 +
    5.23 +    val Inl_Inr_Pair_tac = REPEAT_DETERM o
    5.24 +      (rtac (mk_rel_funDN 1 @{thm Inl_transfer}) ORELSE'
    5.25 +       rtac (mk_rel_funDN 1 @{thm Inr_transfer}) ORELSE'
    5.26 +       rtac (mk_rel_funDN 2 @{thm Pair_transfer}));
    5.27 +
    5.28 +    fun mk_unfold_If_tac total pos =
    5.29 +      HEADGOAL (Inl_Inr_Pair_tac THEN'
    5.30 +        rtac (mk_rel_funDN 3 @{thm If_transfer}) THEN'
    5.31 +        select_prem_tac total (dtac asm_rl) pos THEN'
    5.32 +        dtac rel_funD THEN' atac THEN' atac);
    5.33 +
    5.34 +    fun mk_unfold_Inl_Inr_Pair_tac total pos =
    5.35 +      HEADGOAL (Inl_Inr_Pair_tac THEN'
    5.36 +        select_prem_tac total (dtac asm_rl) pos THEN'
    5.37 +        dtac rel_funD THEN' atac THEN' atac);
    5.38 +
    5.39 +    fun mk_unfold_arg_tac qs gs =
    5.40 +      EVERY (map (mk_unfold_If_tac num_pgs o prem_no_of) qs) THEN
    5.41 +      EVERY (map (mk_unfold_Inl_Inr_Pair_tac num_pgs o prem_no_of) gs);
    5.42 +
    5.43 +    fun mk_unfold_ctr_tac type_definition qss gss =
    5.44 +      HEADGOAL (rtac (mk_rel_funDN 1 (@{thm Abs_transfer} OF
    5.45 +        [type_definition, type_definition])) THEN' Inl_Inr_Pair_tac) THEN
    5.46 +      (case (qss, gss) of
    5.47 +        ([], []) => HEADGOAL (rtac refl)
    5.48 +      | _ => EVERY (map2 mk_unfold_arg_tac qss gss));
    5.49 +
    5.50 +    fun mk_unfold_type_tac type_definition ps qsss gsss =
    5.51 +      let
    5.52 +        val p_tacs = map (mk_unfold_If_tac num_pgs o prem_no_of) ps;
    5.53 +        val qg_tacs = map2 (mk_unfold_ctr_tac type_definition) qsss gsss;
    5.54 +        fun mk_unfold_ty [] [qg_tac] = qg_tac
    5.55 +          | mk_unfold_ty (p_tac :: p_tacs) (qg_tac :: qg_tacs) =
    5.56 +            p_tac THEN qg_tac THEN mk_unfold_ty p_tacs qg_tacs
    5.57 +      in
    5.58 +        HEADGOAL (rtac rel_funI) THEN mk_unfold_ty p_tacs qg_tacs
    5.59 +      end;
    5.60 +
    5.61 +    fun mk_unfold_corec_type_tac dtor_corec_transfer corec_def =
    5.62 +      let
    5.63 +        val active :: actives' = actives;
    5.64 +        val dtor_corec_transfer' = cterm_instantiate_pos
    5.65 +          (SOME active :: map SOME passives @ map SOME actives') dtor_corec_transfer;
    5.66 +      in
    5.67 +        HEADGOAL Goal.conjunction_tac THEN
    5.68 +        REPEAT_DETERM (HEADGOAL (rtac rel_funI)) THEN
    5.69 +        unfold_thms_tac ctxt [corec_def] THEN
    5.70 +        HEADGOAL (etac (mk_rel_funDN_rotated (1 + length actives) dtor_corec_transfer')) THEN
    5.71 +        unfold_thms_tac ctxt (rel_pre_T_defs @ rel_eqs)
    5.72 +      end;
    5.73 +
    5.74 +    fun mk_unfold_prop_tac dtor_corec_transfer corec_def =
    5.75 +      mk_unfold_corec_type_tac dtor_corec_transfer corec_def THEN
    5.76 +      EVERY (map4 mk_unfold_type_tac type_definitions pss qssss gssss);
    5.77 +  in
    5.78 +    HEADGOAL Goal.conjunction_tac THEN
    5.79 +    EVERY (map2 mk_unfold_prop_tac dtor_corec_transfers corec_defs)
    5.80 +  end;
    5.81 +
    5.82  fun solve_prem_prem_tac ctxt =
    5.83    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
    5.84      hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
     6.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:54 2014 +0200
     6.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Thu Sep 25 16:35:56 2014 +0200
     6.3 @@ -478,7 +478,7 @@
     6.4          xtor_co_rec_o_map_thms = fp_rec_o_maps (*theorems about old constants*),
     6.5          rel_xtor_co_induct_thm = rel_xtor_co_induct_thm,
     6.6          dtor_set_induct_thms = [],
     6.7 -        ctor_rec_transfer_thms = []}
     6.8 +        xtor_co_rec_transfer_thms = []}
     6.9         |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy))));
    6.10    in
    6.11      (fp_res, lthy)
     7.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 16:35:54 2014 +0200
     7.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 16:35:56 2014 +0200
     7.3 @@ -28,7 +28,7 @@
     7.4       xtor_co_rec_o_map_thms: thm list,
     7.5       rel_xtor_co_induct_thm: thm,
     7.6       dtor_set_induct_thms: thm list,
     7.7 -     ctor_rec_transfer_thms: thm list}
     7.8 +     xtor_co_rec_transfer_thms: thm list}
     7.9  
    7.10    val morph_fp_result: morphism -> fp_result -> fp_result
    7.11  
    7.12 @@ -220,12 +220,12 @@
    7.13     xtor_co_rec_o_map_thms: thm list,
    7.14     rel_xtor_co_induct_thm: thm,
    7.15     dtor_set_induct_thms: thm list,
    7.16 -   ctor_rec_transfer_thms: thm list};
    7.17 +   xtor_co_rec_transfer_thms: thm list};
    7.18  
    7.19  fun morph_fp_result phi {Ts, bnfs, ctors, dtors, xtor_co_recs, xtor_co_induct,
    7.20      dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_map_thms, xtor_set_thmss,
    7.21      xtor_rel_thms, xtor_co_rec_thms, xtor_co_rec_o_map_thms, rel_xtor_co_induct_thm,
    7.22 -    dtor_set_induct_thms, ctor_rec_transfer_thms} =
    7.23 +    dtor_set_induct_thms, xtor_co_rec_transfer_thms} =
    7.24    {Ts = map (Morphism.typ phi) Ts,
    7.25     bnfs = map (morph_bnf phi) bnfs,
    7.26     ctors = map (Morphism.term phi) ctors,
    7.27 @@ -243,7 +243,7 @@
    7.28     xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
    7.29     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm,
    7.30     dtor_set_induct_thms = map (Morphism.thm phi) dtor_set_induct_thms,
    7.31 -   ctor_rec_transfer_thms = map (Morphism.thm phi) ctor_rec_transfer_thms};
    7.32 +   xtor_co_rec_transfer_thms = map (Morphism.thm phi) xtor_co_rec_transfer_thms};
    7.33  
    7.34  fun time ctxt timer msg = (if Config.get ctxt bnf_timing
    7.35    then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
     8.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:54 2014 +0200
     8.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 16:35:56 2014 +0200
     8.3 @@ -2542,7 +2542,8 @@
     8.4         xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
     8.5         xtor_rel_thms = dtor_Jrel_thms, xtor_co_rec_thms = dtor_corec_thms,
     8.6         xtor_co_rec_o_map_thms = dtor_corec_o_Jmap_thms, rel_xtor_co_induct_thm = Jrel_coinduct_thm,
     8.7 -       dtor_set_induct_thms = dtor_Jset_induct_thms, ctor_rec_transfer_thms = []};
     8.8 +       dtor_set_induct_thms = dtor_Jset_induct_thms,
     8.9 +       xtor_co_rec_transfer_thms = dtor_corec_transfer_thms};
    8.10    in
    8.11      timer; (fp_res, lthy')
    8.12    end;
     9.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 16:35:54 2014 +0200
     9.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 16:35:56 2014 +0200
     9.3 @@ -1156,7 +1156,7 @@
     9.4      val rec_names = map (fst o dest_Const) recs;
     9.5      fun mk_recs Ts passives actives =
     9.6        let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
     9.7 -      in 
     9.8 +      in
     9.9          map3 (fn name => fn T => fn active =>
    9.10            Const (name, Library.foldr (op -->)
    9.11              (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
    9.12 @@ -1829,7 +1829,7 @@
    9.13         xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
    9.14         xtor_rel_thms = ctor_Irel_thms, xtor_co_rec_thms = ctor_rec_thms,
    9.15         xtor_co_rec_o_map_thms = ctor_rec_o_Imap_thms, rel_xtor_co_induct_thm = Irel_induct_thm,
    9.16 -       dtor_set_induct_thms = [], ctor_rec_transfer_thms = ctor_rec_transfer_thms};
    9.17 +       dtor_set_induct_thms = [], xtor_co_rec_transfer_thms = ctor_rec_transfer_thms};
    9.18    in
    9.19      timer; (fp_res, lthy')
    9.20    end;
    10.1 --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 16:35:54 2014 +0200
    10.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML	Thu Sep 25 16:35:56 2014 +0200
    10.3 @@ -48,7 +48,7 @@
    10.4     xtor_co_rec_o_map_thms = [ctor_rec_o_map],
    10.5     rel_xtor_co_induct_thm = xtor_rel_induct,
    10.6     dtor_set_induct_thms = [],
    10.7 -   ctor_rec_transfer_thms = []};
    10.8 +   xtor_co_rec_transfer_thms = []};
    10.9  
   10.10  fun fp_sugar_of_sum ctxt =
   10.11    let
    11.1 --- a/src/HOL/Transfer.thy	Thu Sep 25 16:35:54 2014 +0200
    11.2 +++ b/src/HOL/Transfer.thy	Thu Sep 25 16:35:56 2014 +0200
    11.3 @@ -449,8 +449,7 @@
    11.4    shows "((A ===> op =) ===> op =) Ex Ex"
    11.5    using assms unfolding bi_total_def rel_fun_def by fast
    11.6  
    11.7 -lemma If_transfer [transfer_rule]: "(op = ===> A ===> A ===> A) If If"
    11.8 -  unfolding rel_fun_def by simp
    11.9 +declare If_transfer [transfer_rule]
   11.10  
   11.11  lemma Let_transfer [transfer_rule]: "(A ===> (A ===> B) ===> B) Let Let"
   11.12    unfolding rel_fun_def by simp