select the right premise in "mk_induct_discharge_prem_prems_tac" instead of relying on backtracking

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 22:23:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Fri Sep 14 22:23:10 2012 +0200
@@ -562,48 +562,53 @@
                     in
                       flat (map2 (map o apfst o cons) xysets ppremss)
                     end)
-                | i => [([], (i, x))])
+                | i => [([], (i + 1, x))])
               | mk_raw_prem_prems _ _ = [];
 
-            fun close_prem_prem x' t =
+            fun close_prem_prem xs t =
               fold_rev Logic.all
-                (map Free (drop (nn + 1) (rev (Term.add_frees t (x' :: phis'))))) t;
+                (map Free (drop (2 * nn) (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
 
-            fun mk_prem_prem x (xysets, (i, x')) =
-              close_prem_prem (dest_Free x)
-                (Logic.list_implies (map (fn (x'', (y, set)) =>
-                     HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x''))) xysets,
-                   HOLogic.mk_Trueprop (nth phis i $ x')));
+            fun mk_prem_prem xs (xysets, (j, x)) =
+              close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
+                  HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
+                HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
 
             fun mk_raw_prem phi ctr ctr_Ts =
               let
                 val (xs, names_lthy') = names_lthy |> mk_Frees "x" ctr_Ts;
-                val pprems =
-                  maps (fn x => map (mk_prem_prem x) (mk_raw_prem_prems names_lthy' x)) xs;
+                val pprems = maps (mk_raw_prem_prems names_lthy') xs;
               in
                 (xs, pprems, HOLogic.mk_Trueprop (phi $ Term.list_comb (ctr, xs)))
               end;
 
             val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
 
-            fun mk_prem (xs, pprems, concl) =
-              fold_rev Logic.all xs (Logic.list_implies (pprems, concl));
+            fun mk_prem (xs, raw_pprems, concl) =
+              fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
 
             val goal =
               Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
                 HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
                   (map2 (curry (op $)) phis vs)));
 
-            (* ### WRONG *)
-            val rss = map (map (length o #2)) raw_premss;
-            val ppisss = map (map (fn r => map (pair r) (1 upto r))) rss;
+            fun mk_prem_prems_indices raw_pprems =
+              let
+                val rr = length raw_pprems;
+              in
+                map2 (fn pp => fn (xysets, (i, _)) => ((rr, pp), i)) (1 upto rr) raw_pprems
+              end;
+
+            val ppjjkksss = map (map (mk_prem_prems_indices o #2)) raw_premss;
+
+val _ = tracing ("PPJJISSS:\n" ^ PolyML.makestring (ppjjkksss)) (*###*)
 
             val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
 
             val induct_thm =
               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                mk_induct_tac ctxt ns mss ppisss (flat ctr_defss) fld_induct' nested_set_natural's
-                  pre_set_defss)
+                mk_induct_tac ctxt ns mss ppjjkksss (flat ctr_defss) fld_induct'
+                  nested_set_natural's pre_set_defss)
               |> singleton (Proof_Context.export names_lthy lthy)
           in
             `(conj_dests nn) induct_thm

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Fri Sep 14 22:23:10 2012 +0200
@@ -13,8 +13,8 @@
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_induct_tac: Proof.context -> int list -> int list list -> (int * int) list list list ->
-    thm list -> thm -> thm list -> thm list list -> tactic
+  val mk_induct_tac: Proof.context -> int list -> int list list ->
+    ((int * int) * int) list list list -> thm list -> thm -> thm list -> thm list list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> tactic
   val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
 end;
@@ -112,30 +112,33 @@
   @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
 
 (* TODO: Get rid of the "blast_tac" *)
-fun mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs =
-  EVERY' (maps (fn (pp, i) =>
-    [(* ### select_prem_tac pp (dtac meta_spec) i, *) dtac meta_spec, rotate_tac ~1, etac meta_mp,
+fun mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs =
+  EVERY' (maps (fn ((pp, jj), kk) =>
+    [select_prem_tac nn (dtac meta_spec) (nn - kk + 1), rotate_tac ~1, etac meta_mp,
      SELECT_GOAL (Local_Defs.unfold_tac ctxt pre_set_defs), (* ### why on a line of its own? *)
      SELECT_GOAL (Local_Defs.unfold_tac ctxt (set_natural's @ induct_prem_prem_thms)),
      SELECT_GOAL (Local_Defs.unfold_tac ctxt
        (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
-     TRY o rtac (mk_UnIN pp i), (*#####*)
+     TRY o rtac (mk_UnIN pp jj), (*#####*)
      atac ORELSE'
      rtac @{thm singletonI} ORELSE'
      (REPEAT_DETERM o (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
           etac @{thm induct_set_step}) THEN'
-      (atac ORELSE' blast_tac ctxt))]) (rev ppis)) 1;
+      (atac ORELSE' blast_tac ctxt))]) (rev ppjjkks)) 1;
 
-fun mk_induct_discharge_prem_tac ctxt n set_natural's pre_set_defs m k ppis =
+fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjkks =
   EVERY [mk_induct_prepare_prem_tac n m k,
-    mk_induct_prepare_prem_prems_tac (length ppis), atac 1,
-    mk_induct_discharge_prem_prems_tac ctxt ppis set_natural's pre_set_defs];
+    mk_induct_prepare_prem_prems_tac (length ppjjkks), atac 1,
+    mk_induct_discharge_prem_prems_tac ctxt nn ppjjkks set_natural's pre_set_defs];
 
-fun mk_induct_tac ctxt ns mss ppisss ctr_defs fld_induct' set_natural's pre_set_defss =
-  let val n = Integer.sum ns in
+fun mk_induct_tac ctxt ns mss ppjjkksss ctr_defs fld_induct' set_natural's pre_set_defss =
+  let
+    val nn = length ns;
+    val n = Integer.sum ns;
+  in
     mk_induct_prelude_tac ctxt ctr_defs fld_induct' THEN
-    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt n set_natural's)
-      pre_set_defss mss (unflat mss (1 upto n)) ppisss)
+    EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
+      pre_set_defss mss (unflat mss (1 upto n)) ppjjkksss)
   end;
 
 end;