generate exhaust from nchotomy

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Sat Dec 21 09:44:29 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Sat Dec 21 09:44:30 2013 +0100
@@ -918,24 +918,50 @@
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
       |> split_list o map split_list;
 
-    val nchotomy_props = if not exhaustive then [] else
-      map (HOLogic.mk_Trueprop o mk_disjs o map (mk_conjs o #prems)) disc_eqnss
-      |> map2 ((fn {fun_args, ...} =>
-        curry Logic.list_all (map dest_Free fun_args)) o hd) disc_eqnss;
-    val nchotomy_taut_thms = if exhaustive andalso is_some maybe_tac then
-        map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) nchotomy_props
-      else [];
-    val goalss = if exhaustive andalso is_none maybe_tac then
-      map (rpair []) nchotomy_props :: goalss' else goalss';
+    val list_all_fun_args =
+      map2 ((fn {fun_args, ...} => curry Logic.list_all (map dest_Free fun_args)) o hd) disc_eqnss;
+
+    val nchotomy_goals =
+      if exhaustive then
+        map (HOLogic.mk_Trueprop o mk_disjs o map (mk_conjs o #prems)) disc_eqnss
+        |> list_all_fun_args
+      else
+        [];
+    val nchotomy_taut_thms =
+      if exhaustive andalso is_some maybe_tac then
+        map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) nchotomy_goals
+      else
+        [];
+    val goalss =
+      if exhaustive andalso is_none maybe_tac then map (rpair []) nchotomy_goals :: goalss'
+      else goalss';
+
+    val p = Var (("P", 0), HOLogic.boolT); (* safe since there are no other variables around *)
+
+    fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
 
     fun prove thmss'' def_thms' lthy =
       let
         val def_thms = map (snd o snd) def_thms';
 
-        val maybe_nchotomy_thms = if not exhaustive then map (K NONE) def_thms else
-          map SOME (if is_none maybe_tac then hd thmss'' else nchotomy_taut_thms);
+        val maybe_nchotomy_thms =
+          if exhaustive then map SOME (if is_none maybe_tac then hd thmss'' else nchotomy_taut_thms)
+          else map (K NONE) def_thms;
         val exclude_thmss = if exhaustive andalso is_none maybe_tac then tl thmss'' else thmss'';
 
+        val maybe_exhaust_thms =
+          if exhaustive then
+            map (mk_imp_p o map (mk_imp_p o map HOLogic.mk_Trueprop o #prems)) disc_eqnss
+            |> list_all_fun_args
+            |> map3 (fn disc_eqns => fn SOME nchotomy_thm => fn goal =>
+                mk_primcorec_exhaust_tac (length disc_eqns) nchotomy_thm
+                |> K |> Goal.prove lthy [] [] goal
+                |> Thm.close_derivation
+                |> SOME)
+              disc_eqnss maybe_nchotomy_thms
+          else
+            map (K NONE) def_thms;
+
         val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
         fun mk_excludesss excludes n =
           (excludes, map (fn k => replicate k [TrueI] @ replicate (n - k) []) (0 upto n - 1))
@@ -1145,6 +1171,7 @@
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, simp_attrs),
            (excludeN, exclude_thmss, []),
+           (exhaustN, map the_list maybe_exhaust_thms, []),
            (nchotomyN, map the_list maybe_nchotomy_thms, []),
            (selN, sel_thmss, simp_attrs),
            (simpsN, simp_thmss, []),

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 21 09:44:29 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Sat Dec 21 09:44:30 2013 +0100
@@ -12,6 +12,7 @@
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
+  val mk_primcorec_exhaust_tac: int -> thm -> tactic
   val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
     thm list -> int list -> thm list -> thm option -> tactic
   val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
@@ -31,6 +32,16 @@
 val split_if_asm = @{thm split_if_asm};
 val split_connectI = @{thms allI impI conjI};
 
+fun mk_primcorec_exhaust_tac n nchotomy =
+  let val ks = 1 upto n in
+    HEADGOAL (cut_tac nchotomy THEN'
+     EVERY' (map (fn k =>
+        (if k < n then etac disjE else K all_tac) THEN'
+        REPEAT o (etac conjE THEN' dtac meta_mp THEN' atac) THEN'
+        dtac meta_mp THEN' atac THEN' atac)
+      ks))
+  end;
+
 fun mk_primcorec_assumption_tac ctxt discIs =
   SELECT_GOAL (unfold_thms_tac ctxt
       @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN

--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Dec 21 09:44:29 2013 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Dec 21 09:44:30 2013 +0100
@@ -97,10 +97,8 @@
   else
     let val ks = 1 upto n in
       HEADGOAL (rtac udisc_exhaust THEN'
-        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
-            fn uuncollapse =>
-          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
-            rtac sym, rtac vdisc_exhaust,
+        EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
+          EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac, rtac sym, rtac vdisc_exhaust,
             EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
               EVERY'
                 (if k' = k then