relator coinduction for codatatypes

--- a/src/HOL/BNF/BNF_GFP.thy	Thu May 09 03:58:28 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Thu May 09 20:44:37 2013 +0200
@@ -335,6 +335,12 @@
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
 by simp
 
+lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
+by auto
+
+lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
+by blast
+
 ML_file "Tools/bnf_gfp_util.ML"
 ML_file "Tools/bnf_gfp_tactics.ML"
 ML_file "Tools/bnf_gfp.ML"

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 09 03:58:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 09 20:44:37 2013 +0200
@@ -154,10 +154,10 @@
     val hrecTs = map fastype_of Zeros;
     val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
 
-    val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
+    val (((((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
       z's), As), As_copy), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
-      self_fs), all_fs), gs), all_gs), xFs), xFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
-      (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss),
+      self_fs), all_fs), gs), all_gs), xFs), xFs_copy), yFs), yFs_copy), RFs), (Rtuple, Rtuple')),
+      (hrecs, hrecs')), (nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss),
       names_lthy) = lthy
       |> mk_Frees' "b" activeAs
       ||>> mk_Frees "b" activeAs
@@ -181,6 +181,8 @@
       ||>> mk_Frees "g" all_gTs
       ||>> mk_Frees "x" FTsAs
       ||>> mk_Frees "x" FTsAs
+      ||>> mk_Frees "y" FTsBs
+      ||>> mk_Frees "y" FTsBs
       ||>> mk_Frees "x" FRTs
       ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "Rtuple") all_sbisT
       ||>> mk_Frees' "rec" hrecTs
@@ -275,14 +277,14 @@
 
     val map_arg_cong_thms =
       let
-        val prems = map2 (curry mk_Trueprop_eq) xFs xFs_copy;
-        val maps = map (fn mapx => Term.list_comb (mapx, all_fs)) mapsAsBs;
+        val prems = map2 (curry mk_Trueprop_eq) yFs yFs_copy;
+        val maps = map (fn mapx => Term.list_comb (mapx, all_gs)) mapsBsCs';
         val concls =
-          map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) xFs xFs_copy maps;
+          map3 (fn x => fn y => fn mapx => mk_Trueprop_eq (mapx $ x, mapx $ y)) yFs yFs_copy maps;
         val goals =
           map4 (fn prem => fn concl => fn x => fn y =>
-            fold_rev Logic.all (x :: y :: all_fs) (Logic.mk_implies (prem, concl)))
-          prems concls xFs xFs_copy;
+            fold_rev Logic.all (x :: y :: all_gs) (Logic.mk_implies (prem, concl)))
+          prems concls yFs yFs_copy;
       in
         map (fn goal => Goal.prove_sorry lthy [] [] goal
           (K ((hyp_subst_tac lthy THEN' rtac refl) 1)) |> Thm.close_derivation) goals
@@ -1859,11 +1861,12 @@
     val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
     val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs;
 
-    val (((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jzs1), Jzs2), Jpairs),
+    val ((((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jz's_copy), Jzs1), Jzs2), Jpairs),
       FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy
       |> mk_Frees' "z" Ts
-      ||>> mk_Frees' "z" Ts'
-      ||>> mk_Frees "z" Ts
+      ||>> mk_Frees' "y" Ts'
+      ||>> mk_Frees "z'" Ts
+      ||>> mk_Frees "y'" Ts'
       ||>> mk_Frees "z1" Ts
       ||>> mk_Frees "z2" Ts
       ||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts')
@@ -2297,17 +2300,29 @@
 
     val timer = time (timer "coinduction");
 
-    fun mk_dtor_map_DEADID_thm dtor_inject =
-      trans OF [iffD2 OF [dtor_inject, id_apply], id_apply RS sym];
-
-    fun mk_dtor_Irel_DEADID_thm dtor_inject bnf =
+    fun mk_dtor_map_DEADID_thm dtor_inject map_id =
+      trans OF [iffD2 OF [dtor_inject, id_apply], map_id RS sym];
+
+    fun mk_dtor_Jrel_DEADID_thm dtor_inject bnf =
       trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
 
+    val JphiTs = map2 mk_pred2T passiveAs passiveBs;
+    val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts';
+    val fstsTsTs' = map fst_const prodTsTs';
+    val sndsTsTs' = map snd_const prodTsTs';
+    val activeJphiTs = map2 mk_pred2T Ts Ts';
+    val ((Jphis, activeJphis), names_lthy) = names_lthy
+      |> mk_Frees "R" JphiTs
+      ||>> mk_Frees "JR" activeJphiTs;
+    val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
+    val in_rels = map in_rel_of_bnf bnfs;
+
     (*register new codatatypes as BNFs*)
-    val (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms, lthy) =
+    val (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms,
+      dtor_Jrel_thms, lthy) =
       if m = 0 then
-        (replicate n DEADID_bnf, map mk_dtor_map_DEADID_thm dtor_inject_thms, replicate n [],
-        map2 mk_dtor_Irel_DEADID_thm dtor_inject_thms bnfs, lthy)
+        (timer, replicate n DEADID_bnf, map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's,
+        replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val gTs = map2 (curry op -->) passiveBs passiveCs;
@@ -2317,16 +2332,14 @@
         val p2Ts = map2 (curry op -->) passiveXs passiveBs;
         val pTs = map2 (curry op -->) passiveXs passiveCs;
         val uTs = map2 (curry op -->) Ts Ts';
-        val JphiTs = map2 mk_pred2T passiveAs passiveBs;
-        val prodTs = map2 (curry HOLogic.mk_prodT) Ts Ts';
         val B1Ts = map HOLogic.mk_setT passiveAs;
         val B2Ts = map HOLogic.mk_setT passiveBs;
         val AXTs = map HOLogic.mk_setT passiveXs;
         val XTs = mk_Ts passiveXs;
         val YTs = mk_Ts passiveYs;
 
-        val (((((((((((((((((((fs, fs'), fs_copy), gs), us),
-          (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss), Jphis),
+        val ((((((((((((((((((fs, fs'), fs_copy), gs), us),
+          (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss),
           B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)),
           names_lthy) = names_lthy
           |> mk_Frees' "f" fTs
@@ -2336,7 +2349,6 @@
           ||>> mk_Frees' "b" Ts'
           ||>> mk_Frees' "b" Ts'
           ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
-          ||>> mk_Frees "P" JphiTs
           ||>> mk_Frees "B1" B1Ts
           ||>> mk_Frees "B2" B2Ts
           ||>> mk_Frees "A" AXTs
@@ -2375,19 +2387,17 @@
         val UNIV's = map HOLogic.mk_UNIV Ts';
         val CUNIVs = map HOLogic.mk_UNIV passiveCs;
         val UNIV''s = map HOLogic.mk_UNIV Ts'';
-        val fstsTsTs' = map fst_const prodTs;
-        val sndsTsTs' = map snd_const prodTs;
         val dtor''s = mk_dtors passiveCs;
         val f1s_maps = map (mk_map_id Ts f1s YTs dtors mk_mapsAY) ks;
         val f2s_maps = map (mk_map_id Ts' f2s YTs dtor's mk_mapsBY) ks;
         val pid_maps = map (mk_map_id XTs ps Ts'' Xdtors mk_mapsXC) ks;
         val pfst_Fmaps =
-          map (mk_Fmap fst_const p1s prodTs) (mk_mapsXA prodTs (fst o HOLogic.dest_prodT));
+          map (mk_Fmap fst_const p1s prodTsTs') (mk_mapsXA prodTsTs' (fst o HOLogic.dest_prodT));
         val psnd_Fmaps =
-          map (mk_Fmap snd_const p2s prodTs) (mk_mapsXB prodTs (snd o HOLogic.dest_prodT));
-        val p1id_Fmaps = map (mk_Fmap HOLogic.id_const p1s prodTs) (mk_mapsXA prodTs I);
-        val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTs) (mk_mapsXB prodTs I);
-        val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTs) (mk_mapsXC prodTs I);
+          map (mk_Fmap snd_const p2s prodTsTs') (mk_mapsXB prodTsTs' (snd o HOLogic.dest_prodT));
+        val p1id_Fmaps = map (mk_Fmap HOLogic.id_const p1s prodTsTs') (mk_mapsXA prodTsTs' I);
+        val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTsTs') (mk_mapsXB prodTsTs' I);
+        val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTsTs') (mk_mapsXC prodTsTs' I);
 
         val (dtor_map_thms, map_thms) =
           let
@@ -2904,13 +2914,10 @@
         val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
         val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
 
-        val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
         val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
 
         val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels;
         val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
-
-        val in_rels = map in_rel_of_bnf bnfs;
         val in_Jrels = map in_rel_of_bnf Jbnfs;
 
         val folded_dtor_map_thms = map fold_maps dtor_map_thms;
@@ -2956,15 +2963,131 @@
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        timer; (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms,
-          lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
+       (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms,
+          dtor_Jrel_thms, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
       end;
 
+      val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs;
+      val zip_ranTs = passiveABs @ prodTsTs';
+      val allJphis = Jphis @ activeJphis;
+      val zipFTs = mk_FTs zip_ranTs;
+      val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs;
+      val zip_zTs = mk_Ts passiveABs;
+      val (((zips, (abs, abs')), zip_zs), names_lthy) = names_lthy
+        |> mk_Frees "zip" zipTs
+        ||>> mk_Frees' "ab" passiveABs
+        ||>> mk_Frees "z" zip_zTs;
+
+      val Iphi_sets =
+        map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
+      val in_phis = map2 (mk_in Iphi_sets) (mk_setss zip_ranTs) zipFTs;
+      val fstABs = map fst_const passiveABs;
+      val all_fsts = fstABs @ fstsTsTs';
+      val map_all_fsts = map2 (fn Ds => fn bnf =>
+        Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveAs @ Ts) bnf, all_fsts)) Dss bnfs;
+      val Jmap_fsts = map2 (fn bnf => fn T => if m = 0 then HOLogic.id_const T
+        else Term.list_comb (mk_map_of_bnf deads passiveABs passiveAs bnf, fstABs)) Jbnfs Ts;
+
+      val sndABs = map snd_const passiveABs;
+      val all_snds = sndABs @ sndsTsTs';
+      val map_all_snds = map2 (fn Ds => fn bnf =>
+        Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs;
+      val Jmap_snds = map2 (fn bnf => fn T => if m = 0 then HOLogic.id_const T
+        else Term.list_comb (mk_map_of_bnf deads passiveABs passiveBs bnf, sndABs)) Jbnfs Ts;
+      val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
+      val zip_setss = map (mk_sets_of_bnf (replicate m deads) (replicate m passiveABs)) Jbnfs
+        |> transpose;
+      val in_Jrels = map in_rel_of_bnf Jbnfs;
+
+      val Jrel_coinduct_thm =
+        let
+          fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
+            let
+              val zipxy = zip $ x $ y;
+            in
+              HOLogic.mk_Trueprop (list_all_free [x, y]
+                (HOLogic.mk_imp (phi $ x $ y, HOLogic.mk_conj (HOLogic.mk_mem (zipxy, in_phi),
+                  HOLogic.mk_conj (HOLogic.mk_eq (map $ zipxy, dtor $ x),
+                    HOLogic.mk_eq (map' $ zipxy, dtor' $ y))))))
+            end;
+          val helper_prems = map9 mk_helper_prem
+            activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's;
+          fun mk_helper_coind_concl fst phi x alt y map zip_unfold =
+            HOLogic.mk_imp (list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y,
+              HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))),
+            HOLogic.mk_eq (alt, if fst then x else y));
+          val helper_coind1_concl =
+            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+              (map6 (mk_helper_coind_concl true)
+              activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds));
+          val helper_coind2_concl =
+            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+              (map6 (mk_helper_coind_concl false)
+              activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
+          val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comp's
+            map_cong0s map_arg_cong_thms set_map'ss dtor_unfold_thms folded_dtor_map_thms;
+          fun mk_helper_coind_thms vars concl =
+            Goal.prove_sorry lthy [] []
+              (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
+                (Logic.list_implies (helper_prems, concl)))
+              helper_coind_tac
+            |> Thm.close_derivation
+            |> split_conj_thm;
+          val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl;
+          val helper_coind2_thms = mk_helper_coind_thms (Jz's @ Jz's_copy) helper_coind2_concl;
+
+          fun mk_helper_ind_concl phi ab' ab fst snd z active_phi x y zip_unfold set =
+            mk_Ball (set $ z) (Term.absfree ab' (list_all_free [x, y] (HOLogic.mk_imp
+              (HOLogic.mk_conj (active_phi $ x $ y,
+                 HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))),
+              phi $ (fst $ ab) $ (snd $ ab)))));
+
+          val mk_helper_ind_concls =
+            map6 (fn Jphi => fn ab' => fn ab => fn fst => fn snd => fn zip_sets =>
+              map6 (mk_helper_ind_concl Jphi ab' ab fst snd)
+              zip_zs activeJphis Jzs Jz's zip_unfolds zip_sets)
+            Jphis abs' abs fstABs sndABs zip_setss
+            |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj);
+
+          val helper_ind_thmss = if m = 0 then replicate n [] else
+            map3 (fn concl => fn j => fn set_induct =>
+              Goal.prove_sorry lthy [] []
+                (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips)
+                  (Logic.list_implies (helper_prems, concl)))
+                (mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_map'ss j set_induct)
+              |> Thm.close_derivation
+              |> split_conj_thm)
+            mk_helper_ind_concls ls dtor_set_induct_thms
+            |> transpose;
+
+          val relphis = map (fn rel => Term.list_comb (rel, Jphis @ activeJphis)) rels;
+          fun mk_prem relphi phi x y dtor dtor' =
+            HOLogic.mk_Trueprop (list_all_free [x, y]
+              (HOLogic.mk_imp (phi $ x $ y, relphi $ (dtor $ x) $ (dtor' $ y))));
+          val prems = map6 mk_prem relphis activeJphis Jzs Jz's dtors dtor's;
+
+          val Jrels = if m = 0 then map HOLogic.eq_const Ts
+            else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
+          val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels;
+          val concl =
+            HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq activeJphis Jrelphis));
+        in
+          Goal.prove_sorry lthy [] []
+            (fold_rev Logic.all (Jphis @ activeJphis) (Logic.list_implies (prems, concl)))
+            (mk_rel_coinduct_tac in_rels in_Jrels
+               helper_ind_thmss helper_coind1_thms helper_coind2_thms)
+          |> Thm.close_derivation
+          |> (fn thm => thm OF (replicate n @{thm allI[OF allI[OF impI]]}))
+        end;
+
+      val timer = time (timer "relator coinduction");
+
       val common_notes =
         [(dtor_coinductN, [dtor_coinduct_thm]),
         (dtor_map_coinductN, [dtor_map_coinduct_thm]),
         (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]),
-        (dtor_strong_coinductN, [dtor_strong_coinduct_thm])]
+        (dtor_strong_coinductN, [dtor_strong_coinduct_thm]),
+        (rel_coinductN, [Jrel_coinduct_thm])]
         |> map (fn (thmN, thms) =>
           ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
 
@@ -2987,6 +3110,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
+    timer;
     ({Ts = Ts, bnfs = Jbnfs, ctors = ctors, dtors = dtors, un_folds = unfolds, co_recs = corecs,
       co_induct = dtor_coinduct_thm, strong_co_induct = dtor_strong_coinduct_thm,
       dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms,

--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu May 09 03:58:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Thu May 09 20:44:37 2013 +0200
@@ -102,6 +102,12 @@
     tactic
   val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
     thm list -> thm list -> thm -> thm list -> tactic
+  val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
+    {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_coinduct_coind_tac: int -> thm -> int list -> thm list -> thm list -> thm list ->
+    thm list list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_coinduct_ind_tac: int -> int list -> thm list -> thm list list -> int -> thm ->
+    {prems: 'a, context: Proof.context} -> tactic
   val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
   val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
   val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
@@ -145,6 +151,7 @@
 val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
 val sum_case_weak_cong = @{thm sum_case_weak_cong};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
+val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]}
 
 fun mk_coalg_set_tac coalg_def =
   dtac (coalg_def RS iffD1) 1 THEN
@@ -1569,4 +1576,86 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
+fun mk_rel_coinduct_coind_tac m coinduct ks map_comps map_congs map_arg_congs set_mapss 
+  dtor_unfolds dtor_maps {context = ctxt, prems = _} =
+  let val n = length ks;
+  in
+    EVERY' [DETERM o rtac coinduct,
+      EVERY' (map7 (fn i => fn map_comp => fn map_cong => fn map_arg_cong => fn set_maps =>
+          fn dtor_unfold => fn dtor_map =>
+        EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],
+          select_prem_tac (length ks) (dtac @{thm spec2}) i, dtac mp, atac,
+          REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
+          rtac exI, rtac conjI, rtac conjI,
+          rtac (map_comp RS trans), rtac (dtor_map RS trans RS sym),
+          rtac (dtor_unfold RS map_arg_cong RS trans), rtac (trans OF [map_comp, map_cong]),
+          REPEAT_DETERM_N m o rtac @{thm trans[OF fun_cong[OF o_id] sym[OF fun_cong[OF id_o]]]},
+          REPEAT_DETERM_N n o (rtac @{thm sym[OF trans[OF o_apply]]} THEN' rtac @{thm fst_conv}),
+          rtac (map_comp RS trans), rtac (map_cong RS trans),
+          REPEAT_DETERM_N m o rtac @{thm fun_cong[OF id_o]},
+          REPEAT_DETERM_N n o (rtac @{thm trans[OF o_apply]} THEN' rtac @{thm snd_conv}),
+          etac (@{thm prod.cases} RS map_arg_cong RS trans),
+          SELECT_GOAL (unfold_thms_tac ctxt @{thms prod.cases}), 
+          CONJ_WRAP' (fn set_map =>
+            EVERY' [REPEAT_DETERM o resolve_tac [allI, impI],
+              dtac (set_map RS equalityD1 RS set_mp),
+              REPEAT_DETERM o
+                eresolve_tac (imageE :: conjE :: @{thms iffD1[OF Pair_eq, elim_format]}),
+              hyp_subst_tac ctxt, rtac exI, rtac conjI, etac Collect_splitD_set_mp, atac,
+              rtac (o_apply RS trans), rtac (@{thm surjective_pairing} RS arg_cong)])
+          (drop m set_maps)])
+      ks map_comps map_congs map_arg_congs set_mapss dtor_unfolds dtor_maps)] 1
+  end;
+
+val split_id_unfolds = @{thms prod.cases image_id id_apply};
+
+fun mk_rel_coinduct_ind_tac m ks unfolds set_mapss j set_induct {context = ctxt, prems = _} =
+  let val n = length ks;
+  in
+    rtac set_induct 1 THEN
+    EVERY' (map3 (fn unfold => fn set_maps => fn i =>
+      EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
+        select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
+        REPEAT_DETERM o eresolve_tac [CollectE, conjE, Collect_splitD_set_mp, set_rev_mp],
+        hyp_subst_tac ctxt,
+        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, nth set_maps (j - 1)] @ split_id_unfolds)),
+        rtac subset_refl])
+    unfolds set_mapss ks) 1 THEN
+    EVERY' (map3 (fn unfold => fn set_maps => fn i =>
+      EVERY' (map (fn set_map =>
+        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], etac conjE,
+        select_prem_tac n (dtac @{thm spec2}) i, dtac mp, atac,
+        REPEAT_DETERM o eresolve_tac [CollectE, conjE], hyp_subst_tac ctxt,
+        SELECT_GOAL (unfold_thms_tac ctxt ([unfold, set_map] @ split_id_unfolds)),
+        etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [allE, mp],
+        rtac conjI, etac Collect_splitD_set_mp, atac, rtac (@{thm surjective_pairing} RS arg_cong)])
+      (drop m set_maps)))
+    unfolds set_mapss ks) 1
+  end;
+
+fun mk_rel_coinduct_tac in_rels in_Jrels helper_indss helper_coind1s helper_coind2s
+  {context = ctxt, prems = _} =
+  let val n = length in_rels;
+  in
+    unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
+    REPEAT_DETERM (etac exE 1) THEN
+    CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>
+      EVERY' [rtac @{thm predicate2I}, rtac (in_Jrel RS iffD2), rtac exI, rtac conjI,
+        if null helper_inds then rtac UNIV_I
+        else rtac CollectI THEN'
+          CONJ_WRAP' (fn helper_ind =>
+            EVERY' [rtac (helper_ind RS rev_mp), REPEAT_DETERM_N n o atac,
+              REPEAT_DETERM_N n o etac thin_rl, rtac impI,
+              REPEAT_DETERM o resolve_tac [subsetI, CollectI, @{thm iffD2[OF split_beta]}],
+              dtac bspec, atac, REPEAT_DETERM o eresolve_tac [allE, mp, conjE],
+              etac (refl RSN (2, conjI))])
+          helper_inds,
+        rtac conjI,
+        rtac (helper_coind1 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
+        rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI)),
+        rtac (helper_coind2 RS rev_mp), REPEAT_DETERM_N n o atac, REPEAT_DETERM_N n o etac thin_rl,
+        rtac impI, etac mp, rtac exI, etac (refl RSN (2, conjI))])
+    (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1
+  end;
+
 end;

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 09 03:58:28 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 09 20:44:37 2013 +0200
@@ -1360,8 +1360,8 @@
 
     val timer = time (timer "induction");
 
-    fun mk_ctor_map_DEADID_thm ctor_inject =
-      trans OF [id_apply, iffD2 OF [ctor_inject, id_apply RS sym]];
+    fun mk_ctor_map_DEADID_thm ctor_inject map_id =
+      trans OF [id_apply, iffD2 OF [ctor_inject, map_id RS sym]];
 
     fun mk_ctor_Irel_DEADID_thm ctor_inject bnf =
       trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
@@ -1374,10 +1374,10 @@
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
 
     (*register new datatypes as BNFs*)
-    val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
+    val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
       if m = 0 then
-        (replicate n DEADID_bnf, map mk_ctor_map_DEADID_thm ctor_inject_thms, replicate n [],
-        map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
+        (timer, replicate n DEADID_bnf, map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's,
+        replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy)
       else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val f1Ts = map2 (curry op -->) passiveAs passiveYs;
@@ -1803,7 +1803,7 @@
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        timer; (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
+        (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
           lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
       end;
 
@@ -1854,6 +1854,7 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
+    timer;
     ({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, un_folds = folds, co_recs = recs,
       co_induct = ctor_induct_thm, strong_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms,
       ctor_dtors = ctor_dtor_thms, ctor_injects = ctor_inject_thms, map_thms = folded_ctor_map_thms,