# HG changeset patch
# User traytel
# Date 1374663833 -7200
# Node ID ba2bbe825a5e8132309202ea878ad11d33659355
# Parent  f547266a9338ecba8551020bfb9c4b124358f244
proper transfer rule format for map_transfer

diff -r f547266a9338 -r ba2bbe825a5e src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Jul 24 07:39:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Jul 24 13:03:53 2013 +0200
@@ -757,11 +757,10 @@
     val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
 
     val pre_names_lthy = lthy;
-    val ((((((((((((((((((((((((((fs, f_transfers), gs), hs), x), y), (z, z')), zs), ys), As),
+    val (((((((((((((((((((((((((fs, gs), hs), x), y), (z, z')), zs), ys), As),
       As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
       transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
       |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
-      ||>> mk_Frees "g" (map2 (curry (op -->)) B1Ts B2Ts)
       ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
       ||>> mk_Frees "h" (map2 (curry (op -->)) As' Ts)
       ||>> yield_singleton (mk_Frees "x") CA'
@@ -1206,17 +1205,15 @@
 
         fun mk_map_transfer () =
           let
-            fun mk_prem R S f g = HOLogic.mk_Trueprop (mk_fun_rel R S $ f $ g);
-            val prems = map4 mk_prem transfer_domRs transfer_ranRs fs f_transfers;
-            val relA = Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs);
-            val relB = Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs);
-            val mapf = Term.list_comb (bnf_map_AsBs, fs);
-            val mapg = Term.list_comb (mk_bnf_map B1Ts B2Ts, f_transfers);
-            val concl = HOLogic.mk_Trueprop (mk_fun_rel relA relB $ mapf $ mapg);
+            val rels = map2 mk_fun_rel transfer_domRs transfer_ranRs;
+            val rel = mk_fun_rel
+              (Term.list_comb (mk_bnf_rel transfer_domRTs CA' CB1, transfer_domRs))
+              (Term.list_comb (mk_bnf_rel transfer_ranRTs CB' CB2, transfer_ranRs));
+            val concl = HOLogic.mk_Trueprop
+              (fold_rev mk_fun_rel rels rel $ bnf_map_AsBs $ mk_bnf_map B1Ts B2Ts);
           in
             Goal.prove_sorry lthy [] []
-              (fold_rev Logic.all (fs @ f_transfers @ transfer_domRs @ transfer_ranRs)
-                (Logic.list_implies (prems, concl)))
+              (fold_rev Logic.all (transfer_domRs @ transfer_ranRs) concl)
               (mk_map_transfer_tac (Lazy.force rel_mono) (Lazy.force in_rel)
                 (map Lazy.force set_map') (#map_cong0 axioms) (Lazy.force map_comp'))
             |> Thm.close_derivation
diff -r f547266a9338 -r ba2bbe825a5e src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Jul 24 07:39:37 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Wed Jul 24 13:03:53 2013 +0200
@@ -216,6 +216,7 @@
   let
     val n = length set_map's;
   in
+    REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN
     unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN
     HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac,
       rtac @{thm predicate2I}, dtac (in_rel RS iffD1),