made tactics more robust

--- a/src/HOL/Tools/BNF/bnf_gfp.ML	Wed Feb 19 22:08:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Thu Feb 20 11:40:03 2014 +0100
@@ -1500,7 +1500,6 @@
 
     val UNIVs = map HOLogic.mk_UNIV Ts;
     val FTs = mk_FTs (passiveAs @ Ts);
-    val FTs' = mk_FTs (passiveBs @ Ts);
     val prodTs = map (HOLogic.mk_prodT o `I) Ts;
     val prodFTs = mk_FTs (passiveAs @ prodTs);
     val FTs_setss = mk_setss (passiveAs @ Ts);
@@ -2172,14 +2171,13 @@
               (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
                 HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)));
             val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
-            val cTs = map (SOME o certifyT lthy) FTs';
             val maps =
-              map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 =>
+              map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong =>
                 Goal.prove_sorry lthy [] [] goal
                   (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
-                     mk_map_tac m n cT unfold map_comp map_cong0)
+                     mk_map_tac m n map_arg_cong unfold map_comp map_cong0)
                 |> Thm.close_derivation)
-              goals cTs dtor_unfold_thms map_comps map_cong0s;
+              goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms;
           in
             map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
           end;
@@ -2398,10 +2396,10 @@
       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
+      val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy
         |> mk_Frees "zip" zipTs
         ||>> mk_Frees' "ab" passiveABs
-        ||>> mk_Frees "z" zip_zTs;
+        ||>> mk_Frees' "z" zip_zTs;
 
       val Iphi_sets =
         map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs;
@@ -2424,6 +2422,7 @@
 
       fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} =
         let
+val lthy = Config.put quick_and_dirty false lthy (*XXX*)
           fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' =
             let
               val zipxy = zip $ x $ y;
@@ -2435,53 +2434,76 @@
             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));
+          fun mk_helper_coind_phi fst phi x alt y map zip_unfold =
+            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)))))
+          val coind1_phis = map6 (mk_helper_coind_phi true)
+            activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds;
+          val coind2_phis = map6 (mk_helper_coind_phi false)
+              activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds;
+          fun mk_cts zs z's phis =
+            map3 (fn z => fn z' => fn phi =>
+              SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi)))
+            zs z's phis @
+            map (SOME o certify lthy) (splice z's zs);
+          val cts1 = mk_cts Jzs Jzs_copy coind1_phis;
+          val cts2 = mk_cts Jz's Jz's_copy coind2_phis;
+
+          fun mk_helper_coind_concl z alt coind_phi =
+            HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z));
           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));
+              (map3 mk_helper_coind_concl Jzs Jzs_copy coind1_phis));
           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));
-          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)))
+              (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis));
+
+          fun mk_helper_coind_thms concl cts =
+            Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
               (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m
-                dtor_map_coinduct_thm ks map_comps map_cong0s map_arg_cong_thms set_mapss
-                dtor_unfold_thms dtor_Jmap_thms)
+                (cterm_instantiate_pos cts dtor_map_coinduct_thm) ks map_comps map_cong0s
+                map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms)
             |> 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
+            |> split_conj_thm
+            |> Proof_Context.export names_lthy lthy;
+
+          val helper_coind1_thms = mk_helper_coind_thms helper_coind1_concl cts1;
+          val helper_coind2_thms = mk_helper_coind_thms helper_coind2_concl cts2;
+
+          fun mk_helper_ind_phi phi ab fst snd z active_phi x y zip_unfold =
+            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)))));
+              phi $ (fst $ ab) $ (snd $ ab)));
+          val helper_ind_phiss =
+            map4 (fn Jphi => fn ab => fn fst => fn snd =>
+              map5 (mk_helper_ind_phi Jphi ab fst snd)
+              zip_zs activeJphis Jzs Jz's zip_unfolds)
+            Jphis abs fstABs sndABs;
+          val ctss = map2 (fn ab' => fn phis =>
+              map2 (fn z' => fn phi =>
+                SOME (certify lthy (Term.absfree ab' (Term.absfree z' phi))))
+              zip_zs' phis @
+              map (SOME o certify lthy) zip_zs)
+            abs' helper_ind_phiss;
+          fun mk_helper_ind_concl ab' z ind_phi set =
+            mk_Ball (set $ z) (Term.absfree ab' ind_phi);
   
           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
+            map3 (fn ab' => fn ind_phis => fn zip_sets =>
+              map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets)
+            abs' helper_ind_phiss 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)))
+            map4 (fn concl => fn j => fn set_induct => fn cts =>
+              Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl))
                 (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks
-                  dtor_unfold_thms set_mapss j set_induct)
+                  dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct))
               |> Thm.close_derivation
-              |> split_conj_thm)
-            mk_helper_ind_concls ls dtor_Jset_induct_thms
+              |> split_conj_thm
+              |> Proof_Context.export names_lthy lthy)
+            mk_helper_ind_concls ls dtor_Jset_induct_thms ctss
             |> transpose;
         in
           mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels

--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Wed Feb 19 22:08:47 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Thu Feb 20 11:40:03 2014 +0100
@@ -43,7 +43,7 @@
   val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
     thm list list -> thm list list -> thm list list list -> tactic
   val mk_map_id0_tac: thm list -> thm -> thm -> tactic
-  val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
+  val mk_map_tac: int -> int -> thm -> thm -> thm -> thm -> tactic
   val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic
   val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic
   val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list ->
@@ -795,12 +795,12 @@
         rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
   end;
 
-fun mk_map_tac m n cT unfold map_comp map_cong0 =
+fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 =
   EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym),
     rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), rtac map_cong0,
     REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
     REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
-    rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1;
+    rtac map_arg_cong, rtac (o_apply RS sym)] 1;
 
 fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss =
   EVERY' [rtac hset_minimal,
@@ -1018,7 +1018,7 @@
   dtor_unfolds dtor_maps =
   let val n = length ks;
   in
-    EVERY' [DETERM o rtac coinduct,
+    EVERY' [rtac coinduct,
       EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s =>
           fn dtor_unfold => fn dtor_map =>
         EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],