implemented 'exhaustive' option in tactic

--- a/src/Doc/Datatypes/Datatypes.thy	Thu Dec 19 20:07:06 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Dec 19 21:49:30 2013 +0100
@@ -467,7 +467,7 @@
 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
 manual \cite{isabelle-isar-ref}.
 %
-The optional target is optionally followed by datatype-specific options:
+The optional target is potentially followed by datatype-specific options:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
@@ -2251,7 +2251,7 @@
   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
 "}
 
-The optional target is optionally followed by a corecursion-specific option:
+The optional target is potentially followed by a corecursion-specific option:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Dec 19 20:07:06 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Dec 19 21:49:30 2013 +0100
@@ -916,22 +916,22 @@
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
       |> split_list o map split_list;
 
-    val exh_props = if not exhaustive then [] else
+    val exhaust_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 exh_taut_thms = if exhaustive andalso is_some maybe_tac then
-        map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) exh_props
+    val exhaust_taut_thms = if exhaustive andalso is_some maybe_tac then
+        map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) exhaust_props
       else [];
     val goalss = if exhaustive andalso is_none maybe_tac then
-      map (rpair []) exh_props :: goalss' else goalss';
+      map (rpair []) exhaust_props :: goalss' else goalss';
 
     fun prove thmss'' def_thms' lthy =
       let
         val def_thms = map (snd o snd) def_thms';
 
-        val maybe_exh_thms = if not exhaustive then map (K NONE) def_thms else
-          map SOME (if is_none maybe_tac then hd thmss'' else exh_taut_thms);
+        val maybe_exhaust_thms = if not exhaustive then map (K NONE) def_thms else
+          map SOME (if is_none maybe_tac then hd thmss'' else exhaust_taut_thms);
         val thmss' = if exhaustive andalso is_none maybe_tac then tl thmss'' else thmss'';
 
         val exclss' = map (op ~~) (goal_idxss ~~ thmss');
@@ -1032,7 +1032,7 @@
                 |> single
             end;
 
-        fun prove_code disc_eqns sel_eqns maybe_exh ctr_alist ctr_specs =
+        fun prove_code disc_eqns sel_eqns maybe_exhaust ctr_alist ctr_specs =
           let
             val maybe_fun_data =
               (find_first (member (op =) (map #ctr ctr_specs) o #ctr) disc_eqns,
@@ -1108,7 +1108,7 @@
                       case_thms_of_term lthy bound_Ts raw_rhs;
 
                     val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
-                        sel_splits sel_split_asms ms ctr_thms maybe_exh
+                        sel_splits sel_split_asms ms ctr_thms maybe_exhaust
                       |> K |> Goal.prove lthy [] [] raw_t
                       |> Thm.close_derivation;
                   in
@@ -1129,7 +1129,8 @@
           ctr_specss;
         val ctr_thmss = map (map snd) ctr_alists;
 
-        val code_thmss = map5 prove_code disc_eqnss sel_eqnss maybe_exh_thms ctr_alists ctr_specss;
+        val code_thmss = map5 prove_code disc_eqnss sel_eqnss maybe_exhaust_thms ctr_alists
+          ctr_specss;
 
         val simp_thmss = map2 append disc_thmss sel_thmss
 

--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Dec 19 20:07:06 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Dec 19 21:49:30 2013 +0100
@@ -97,7 +97,6 @@
 fun distinct_in_prems_tac distincts =
   eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
 
-(* TODO: reduce code duplication with selector tactic above *)
 fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
   let
     val splits' =
@@ -116,12 +115,24 @@
        (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
   end;
 
-(* TODO: implement "exhaustive" (maybe_exh) *)
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs maybe_exh =
-  EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms
-    f_ctrs) THEN
-  IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
-    HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)));
+fun rulify_exhaust n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
+
+fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs
+    maybe_exhaust =
+  let
+    val n = length ms;
+    val (ms', f_ctrs') =
+      (case maybe_exhaust of
+        NONE => (ms, f_ctrs)
+      | SOME exhaust =>
+        (ms |> split_last ||> K [n - 1] |> op @,
+         f_ctrs |> split_last ||> (fn thm => [rulify_exhaust n exhaust RS thm]) |> op @));
+  in
+    EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+      ms' f_ctrs') THEN
+    IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
+      HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
+  end;
 
 fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
   HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'