goal generation for xtor_co_rec_transfer

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Sep 25 13:30:57 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Sep 01 14:14:47 2014 +0200
@@ -138,6 +138,8 @@
   val mk_proj: typ -> int -> int -> term
 
   val mk_convol: term * term -> term
+  val mk_rel_prod: term -> term -> term
+  val mk_rel_sum: term -> term -> term
 
   val Inl_const: typ -> typ -> term
   val Inr_const: typ -> typ -> term
@@ -174,9 +176,9 @@
   val mk_rel_xtor_co_induct_thm: BNF_Util.fp_kind -> term list -> term list -> term list ->
     term list -> term list -> term list -> term list -> term list ->
     ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm
-  val mk_un_fold_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
-    term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) ->
-    Proof.context -> thm list
+  val mk_co_iter_transfer_thms: BNF_Util.fp_kind -> term list -> term list -> term list ->
+    term list -> term list -> term list -> term list ->
+    ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm list
   val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
     thm list -> thm list -> thm list
 
@@ -376,6 +378,20 @@
     val convolT = fTU --> gTU --> gT --> HOLogic.mk_prodT (fU, gU);
   in Const (@{const_name convol}, convolT) $ f $ g end;
 
+fun mk_rel_prod R S =
+  let
+    val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
+    val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
+    val rel_prodT = RT --> ST --> mk_pred2T (HOLogic.mk_prodT (A1, B1)) (HOLogic.mk_prodT (A2, B2));
+  in Const (@{const_name rel_prod}, rel_prodT) $ R $ S end;
+
+fun mk_rel_sum R S =
+  let
+    val ((A1, A2), RT) = `dest_pred2T (fastype_of R);
+    val ((B1, B2), ST) = `dest_pred2T (fastype_of S);
+    val rel_sumT = RT --> ST --> mk_pred2T (mk_sumT (A1, B1)) (mk_sumT (A2, B2));
+  in Const (@{const_name rel_sum}, rel_sumT) $ R $ S end;
+
 fun Inl_const LT RT = Const (@{const_name Inl}, LT --> mk_sumT (LT, RT));
 fun mk_Inl RT t = Inl_const (fastype_of t) RT $ t;
 
@@ -498,18 +514,18 @@
     |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]}))
   end;
 
-fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy =
+fun mk_co_iter_transfer_thms fp pre_rels pre_iphis pre_ophis rels phis un_folds un_folds' tac lthy =
   let
-    val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels;
+    val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_iphis)) pre_rels;
     val relphis = map (fn rel => Term.list_comb (rel, phis)) rels;
     fun flip f x y = if fp = Greatest_FP then f y x else f x y;
 
-    val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_phis;
+    val arg_rels = map2 (flip mk_rel_fun) pre_relphis pre_ophis;
     fun mk_transfer relphi pre_phi un_fold un_fold' =
       fold_rev mk_rel_fun arg_rels (flip mk_rel_fun relphi pre_phi) $ un_fold $ un_fold';
-    val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds';
+    val transfers = map4 mk_transfer relphis pre_ophis un_folds un_folds';
 
-    val goal = fold_rev Logic.all (phis @ pre_phis)
+    val goal = fold_rev Logic.all (phis @ pre_ophis)
       (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers));
   in
     Goal.prove_sorry lthy [] [] goal tac

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Sep 25 13:30:57 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Sep 01 14:14:47 2014 +0200
@@ -1541,6 +1541,14 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val corecs = map (Morphism.term phi) corec_frees;
     val corec_names = map (fst o dest_Const) corecs;
+    fun mk_corecs Ts passives actives =
+      let val Tactives = map2 (curry mk_sumT) Ts actives;
+      in
+        map3 (fn name => fn T => fn active =>
+          Const (name, Library.foldr (op -->)
+            (map2 (curry op -->) actives (mk_FTs (passives @ Tactives)), active --> T)))
+        corec_names Ts actives
+      end;
     fun mk_corec ss i = Term.list_comb (Const (nth corec_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss);
     val corec_defs = map (fn def =>
@@ -2474,16 +2482,27 @@
       sym_map_comps map_cong0s;
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+    val Jrels = if m = 0 then map HOLogic.eq_const Ts
+      else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
 
     val dtor_unfold_transfer_thms =
-      mk_un_fold_transfer_thms Greatest_FP rels activephis
-        (if m = 0 then map HOLogic.eq_const Ts
-          else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
+      mk_co_iter_transfer_thms Greatest_FP rels activephis activephis Jrels Jphis
         (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_unfold_transfer_tac ctxt m Jrel_coinduct_thm
           (map map_transfer_of_bnf bnfs) dtor_unfold_thms)
         lthy;
 
+    val corec_allAs = passiveAs @ map2 (curry mk_sumT) Ts activeAs;
+    val corec_allBs = passiveBs @ map2 (curry mk_sumT) Ts' activeBs;
+    val corec_rels = map2 (fn Ds => mk_rel_of_bnf Ds corec_allAs corec_allBs) Dss bnfs;
+    val corec_activephis =
+      map2 (fn Jrel => mk_rel_sum (Term.list_comb (Jrel, Jphis))) Jrels activephis;
+    val dtor_corec_transfer_thms =
+      mk_co_iter_transfer_thms Greatest_FP corec_rels corec_activephis activephis Jrels Jphis
+        (mk_corecs Ts passiveAs activeAs) (mk_corecs Ts' passiveBs activeBs)
+        (fn {context = ctxt, prems = _} => print_tac ctxt "xxx" THEN Skip_Proof.cheat_tac 1)
+        lthy;
+
     val timer = time (timer "relator coinduction");
 
     val common_notes =

--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Thu Sep 25 13:30:57 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Sep 01 14:14:47 2014 +0200
@@ -1154,6 +1154,14 @@
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val recs = map (Morphism.term phi) rec_frees;
     val rec_names = map (fst o dest_Const) recs;
+    fun mk_recs Ts passives actives =
+      let val Tactives = map2 (curry HOLogic.mk_prodT) Ts actives;
+      in 
+        map3 (fn name => fn T => fn active =>
+          Const (name, Library.foldr (op -->)
+            (map2 (curry op -->) (mk_FTs (passives @ Tactives)) actives, T --> active)))
+        rec_names Ts actives
+      end;
     fun mk_rec ss i = Term.list_comb (Const (nth rec_names (i - 1), Library.foldr (op -->)
       (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss);
     val rec_defs = map (fn def =>
@@ -1764,12 +1772,23 @@
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     val ctor_fold_transfer_thms =
-      mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis
+      mk_co_iter_transfer_thms Least_FP rels activephis activephis Irels Iphis
         (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs)
         (fn {context = ctxt, prems = _} => mk_fold_transfer_tac ctxt m Irel_induct_thm
           (map map_transfer_of_bnf bnfs) ctor_fold_thms)
         lthy;
 
+    val rec_allAs = passiveAs @ map2 (curry HOLogic.mk_prodT) Ts activeAs;
+    val rec_allBs = passiveBs @ map2 (curry HOLogic.mk_prodT) Ts' activeBs;
+    val rec_rels = map2 (fn Ds => mk_rel_of_bnf Ds rec_allAs rec_allBs) Dss bnfs;
+    val rec_activephis =
+      map2 (fn Irel => mk_rel_prod (Term.list_comb (Irel, Iphis))) Irels activephis;
+    val ctor_rec_transfer_thms =
+      mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
+        (mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
+        (fn {context = ctxt, prems = _} => print_tac ctxt "xxx" THEN Skip_Proof.cheat_tac 1)
+        lthy;
+
     val timer = time (timer "relator induction");
 
     val common_notes =