generate 'ctr_transfer' for (co)datatypes

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 19 15:19:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 19 16:46:31 2014 +0200
@@ -98,6 +98,7 @@
 
 val EqN = "Eq_";
 
+val ctr_transferN = "ctr_transfer";
 val corec_codeN = "corec_code";
 val map_disc_iffN = "map_disc_iff";
 val map_selN = "map_sel";
@@ -131,6 +132,18 @@
 
 val name_of_set = name_of_const "set";
 
+
+fun mk_parametricity_goals ctxt Rs fs gs =
+  let
+    val prems =
+      map (foldr1 (uncurry mk_rel_fun) o
+          uncurry (map2 (build_the_rel ctxt Rs [])) o
+          pairself (fastype_of #> strip_type #> (fn (Ts, T) => Ts @ [T])))
+        (fs ~~ gs);
+  in
+    map3 (fn prem => fn f => fn g => HOLogic.mk_Trueprop (prem $ f $ g)) prems fs gs
+  end
+
 fun fp_sugar_of ctxt =
   Symtab.lookup (Data.get (Context.Proof ctxt))
   #> Option.map (transfer_fp_sugar ctxt);
@@ -1499,11 +1512,11 @@
                   rel_inject_thms ms;
 
               val (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
-                   (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
+                   ctr_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;
-                  val rel = mk_rel live As Bs (rel_of_bnf fp_bnf);
                   val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy
                     |> mk_Frees "f" fTs
                     ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
@@ -1513,11 +1526,24 @@
                       yield_singleton (mk_Frees "thesis") HOLogic.boolT;
                   val map_term = mk_map live As Bs (map_of_bnf fp_bnf);
                   val ctrAs = map (mk_ctr As) ctrs;
+                  val ctrBs = map (mk_ctr Bs) ctrs;
+                  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 selAss = map (map (mk_disc_or_sel As)) selss;
                   val discAs_selAss = flat (map2 (map o pair) discAs selAss);
 
+                  val ctr_transfer_thms =
+                    let
+                      val goals = mk_parametricity_goals names_lthy Rs ctrAs ctrBs;
+                    in
+                      Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                        (fn {context = ctxt, prems = _} => mk_ctr_transfer_tac rel_intro_thms)
+                      |> Conjunction.elim_balanced (length goals)
+                      |> Proof_Context.export names_lthy lthy
+                      |> map Thm.close_derivation
+                    end;
+
                   val (set_cases_thms, set_cases_attrss) =
                     let
                       fun mk_prems assms elem t ctxt =
@@ -1664,7 +1690,7 @@
 
                   val (rel_cases_thm, rel_cases_attrs) =
                     let
-                      val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb;
+                      val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb;
                       val ctrBs = map (mk_ctr Bs) ctrs;
 
                       fun mk_assms ctrA ctrB ctxt =
@@ -1831,7 +1857,8 @@
                     end;
                 in
                   (map_disc_iff_thms, map_sel_thms, set_sel_thms, rel_sel_thms, set_intros_thms,
-                    (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
+                    ctr_transfer_thms, (set_cases_thms, set_cases_attrss),
+                    (rel_cases_thm, rel_cases_attrs))
                 end;
 
               val anonymous_notes =
@@ -1840,7 +1867,8 @@
                 |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
 
               val notes =
-                [(mapN, map_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
+                [(ctr_transferN, ctr_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 []),
                  (rel_casesN, [rel_cases_thm], K rel_cases_attrs),

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Aug 19 15:19:16 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Aug 19 16:46:31 2014 +0200
@@ -20,6 +20,7 @@
   val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
   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_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 ->
@@ -96,6 +97,11 @@
       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)});