generate 'disc_transfer' for (co)datatypes

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Aug 29 14:21:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Aug 29 14:36:51 2014 +0200
@@ -100,6 +100,7 @@
 
 val case_transferN = "case_transfer";
 val ctr_transferN = "ctr_transfer";
+val disc_transferN = "disc_transfer";
 val corec_codeN = "corec_code";
 val map_disc_iffN = "map_disc_iff";
 val map_selN = "map_sel";
@@ -1370,7 +1371,8 @@
           end;
 
         fun derive_maps_sets_rels (ctr_sugar as {casex, case_cong, case_thms, discs, selss, ctrs,
-            exhaust, disc_thmss, sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) =
+            exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss,
+            ...} : ctr_sugar, lthy) =
           if live = 0 then
             ((([], [], [], []), ctr_sugar), lthy)
           else
@@ -1470,8 +1472,8 @@
                   rel_inject_thms ms;
 
               val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
-                   case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss),
-                   (rel_cases_thm, rel_cases_attrs)) =
+                   case_transfer_thms, ctr_transfer_thms, disc_transfer_thms,
+                   (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
                 let
                   val live_AsBs = filter (op <>) (As ~~ Bs);
                   val fTs = map (op -->) live_AsBs;
@@ -1488,6 +1490,7 @@
                   val relAsBs = mk_rel live As Bs (rel_of_bnf fp_bnf);
                   val setAs = map (mk_set As) (sets_of_bnf fp_bnf);
                   val discAs = map (mk_disc_or_sel As) discs;
+                  val discBs = map (mk_disc_or_sel Bs) discs;
                   val selAss = map (map (mk_disc_or_sel As)) selss;
                   val discAs_selAss = flat (map2 (map o pair) discAs selAss);
 
@@ -1614,7 +1617,6 @@
 
                   val rel_sel_thms =
                     let
-                      val discBs = map (mk_disc_or_sel Bs) discs;
                       val selBss = map (map (mk_disc_or_sel Bs)) selss;
                       val n = length discAs;
 
@@ -1706,6 +1708,21 @@
                       |> Thm.close_derivation
                     end;
 
+                  val disc_transfer_thms =
+                    let
+                      val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs;
+                    in
+                      if null goals then []
+                      else
+                        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                          (fn {context = ctxt, prems = _} =>
+                            mk_disc_transfer_tac ctxt (the_single rel_sel_thms)
+                              (the_single exhaust_discs) (flat (flat distinct_discsss)))
+                          |> Conjunction.elim_balanced (length goals)
+                        |> Proof_Context.export names_lthy lthy
+                        |> map Thm.close_derivation
+                    end;
+
                   val map_disc_iff_thms =
                     let
                       val discsB = map (mk_disc_or_sel Bs) discs;
@@ -1832,8 +1849,8 @@
                     end;
                 in
                   (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
-                    case_transfer_thms, ctr_transfer_thms, (set_cases_thms, set_cases_attrss),
-                    (rel_cases_thm, rel_cases_attrs))
+                    case_transfer_thms, ctr_transfer_thms, disc_transfer_thms,
+                    (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
                 end;
 
               val anonymous_notes =
@@ -1844,6 +1861,7 @@
               val notes =
                 [(case_transferN, [case_transfer_thms], K []),
                  (ctr_transferN, ctr_transfer_thms, K []),
+                 (disc_transferN, disc_transfer_thms, K []),
                  (mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
                  (map_disc_iffN, map_disc_iff_thms, K simp_attrs),
                  (map_selN, map_sel_thms, K []),

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Aug 29 14:21:25 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Aug 29 14:36:51 2014 +0200
@@ -22,6 +22,7 @@
   val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     tactic
   val mk_ctr_transfer_tac: thm list -> tactic
+  val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
@@ -97,6 +98,24 @@
     ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD}))
   end;
 
+fun mk_ctr_transfer_tac rel_intros =
+  HEADGOAL Goal.conjunction_tac THEN
+  ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
+    REPEAT_DETERM o atac));
+
+fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc=
+  let
+    fun last_disc_tac iffD =
+      HEADGOAL (rtac (rotate_prems ~1 exhaust_disc) THEN' atac THEN'
+      REPEAT_DETERM o (rotate_tac ~1 THEN' dtac (rotate_prems 1 iffD) THEN' atac THEN'
+        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 o (etac conjE) THEN' (atac ORELSE' rtac iffI))) THEN
+    TRY (last_disc_tac iffD2) THEN TRY (last_disc_tac iffD1)
+  end;
+
 fun mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor sumEN' =
   unfold_thms_tac ctxt (ctor_iff_dtor :: ctr_defs) THEN HEADGOAL (rtac sumEN') THEN
   HEADGOAL (EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k,
@@ -109,11 +128,6 @@
       SELECT_GOAL (unfold_thms_tac ctxt [th]) THEN'
       atac) [rev cTs, cTs] [cdtor, cctor] [dtor_ctor, ctor_dtor]));
 
-fun mk_ctr_transfer_tac rel_intros =
-  HEADGOAL Goal.conjunction_tac THEN
-  ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
-    REPEAT_DETERM o atac));
-
 fun mk_half_distinct_tac ctxt ctor_inject abs_inject ctr_defs =
   unfold_thms_tac ctxt (ctor_inject :: abs_inject :: @{thms sum.inject} @ ctr_defs) THEN
   HEADGOAL (rtac @{thm sum.distinct(1)});