use needed case theorems

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 10:20:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 10:26:00 2013 +0200
@@ -785,7 +785,7 @@
         fun prove_sel {ctr_specs, nested_maps, nested_map_idents, nested_map_comps, ...}
             disc_eqns exclsss {fun_name, fun_T, fun_args, ctr, sel, rhs_term, ...} =
           let
-            val (SOME ctr_spec) = find_first (equal ctr o #ctr) ctr_specs;
+            val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
             val ctr_no = find_index (equal ctr o #ctr) ctr_specs;
             val prems = the_default (maps (negate_conj o #prems) disc_eqns)
                 (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
@@ -800,9 +800,10 @@
               |> HOLogic.mk_Trueprop o HOLogic.mk_eq
               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
               |> curry Logic.list_all (map dest_Free fun_args);
+            val (_, _, _, splits, split_asms) = case_thms_of_term lthy [] rhs_term;
           in
             mk_primcorec_sel_tac lthy def_thms sel_corec k m exclsss nested_maps nested_map_idents
-              nested_map_comps [] []
+              nested_map_comps splits split_asms
             |> K |> Goal.prove lthy [] [] t
             |> pair sel
           end;

--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 10:20:23 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 10:26:00 2013 +0200
@@ -69,6 +69,8 @@
     typ list -> term -> term
   val fold_rev_corec_code_rhs: Proof.context -> (term list -> term -> term list -> 'a -> 'a) ->
     typ list -> term -> 'a -> 'a
+  val case_thms_of_term: Proof.context -> typ list -> term ->
+    thm list * thm list * thm list * thm list * thm list
 
   val rec_specs_of: binding list -> typ list -> typ list -> (term -> int list) ->
     ((term * term list list) list) list -> local_theory ->
@@ -220,7 +222,7 @@
     massage_call
   end;
 
-fun fold_rev_let_if_case ctxt f bound_Ts =
+fun fold_rev_let_if_case ctxt f bound_Ts t =
   let
     val thy = Proof_Context.theory_of ctxt;
 
@@ -236,16 +238,17 @@
             (case fastype_of1 (bound_Ts, nth args n) of
               Type (s, Ts) =>
               (case dest_case ctxt s Ts t of
-                NONE => f conds t
+                NONE => apsnd (f conds t)
               | SOME (conds', branches) =>
-                fold_rev (uncurry fld) (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
-            | _ => f conds t)
+                apfst (cons s) o fold_rev (uncurry fld)
+                  (map (append conds o HOLogic.conjuncts) conds' ~~ branches))
+            | _ => apsnd (f conds t))
           else
-            f conds t
+            apsnd (f conds t)
         end
-      | _ => f conds t)
+      | _ => apsnd (f conds t))
   in
-    fld []
+    fld [] t o pair []
   end;
 
 fun case_of ctxt = ctr_sugar_of ctxt #> Option.map (fst o dest_Const o #casex);
@@ -387,7 +390,16 @@
     (fn bound_Ts => uncurry (massage_ctr bound_Ts) o Term.strip_comb);
 
 fun fold_rev_corec_code_rhs ctxt f =
-  fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
+  snd ooo fold_rev_let_if_case ctxt (fn conds => uncurry (f conds) o Term.strip_comb);
+
+fun case_thms_of_term ctxt bound_Ts t =
+  let
+    val (caseT_names, _) = fold_rev_let_if_case ctxt (K (K I)) bound_Ts t ();
+    val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
+  in
+    (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
+     map #split ctr_sugars, map #split_asm ctr_sugars)
+  end;
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;
 fun indexedd xss = fold_map indexed xss;