# HG changeset patch
# User blanchet
# Date 1388652622 -3600
# Node ID 136fe16e726af658dd28bf412efe79c4368e09cb
# Parent  7a01387c47d51c0268d85dcb9bff872510b3ab2e
generate 'disc_iff' property in 'primcorec'

diff -r 7a01387c47d5 -r 136fe16e726a src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -33,6 +33,7 @@
 val codeN = "code"
 val ctrN = "ctr"
 val discN = "disc"
+val disc_iffN = "disc_iff"
 val excludeN = "exclude"
 val nchotomyN = "nchotomy"
 val selN = "sel"
@@ -68,6 +69,7 @@
    calls: corec_call list,
    discI: thm,
    sel_thms: thm list,
+   disc_excludess: thm list list,
    collapse: thm,
    corec_thm: thm,
    disc_corec: thm,
@@ -92,6 +94,7 @@
 
 val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
 val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
+val mk_dnf = mk_disjs o map mk_conjs;
 
 val conjuncts_s = filter_out (curry (op =) @{const True}) o HOLogic.conjuncts;
 
@@ -411,31 +414,28 @@
          else No_Corec) g_i
       | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
 
-    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
-        disc_corec sel_corecs =
+    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse
+        corec_thm disc_corec sel_corecs =
       let val nullary = not (can dest_funT (fastype_of ctr)) in
-        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
+        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
          calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
-         collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
-         sel_corecs = sel_corecs}
+         disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
+         disc_corec = disc_corec, sel_corecs = sel_corecs}
       end;
 
-    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss coiter_thmsss
-        disc_coitersss sel_coiterssss =
+    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
+        sel_coiterssss =
       let
-        val ctrs = #ctrs (nth ctr_sugars index);
-        val discs = #discs (nth ctr_sugars index);
-        val selss = #selss (nth ctr_sugars index);
+        val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
+          nth ctr_sugars index;
         val p_ios = map SOME p_is @ [NONE];
         val discIs = #discIs (nth ctr_sugars index);
-        val sel_thmss = #sel_thmss (nth ctr_sugars index);
-        val collapses = #collapses (nth ctr_sugars index);
         val corec_thms = co_rec_of (nth coiter_thmsss index);
         val disc_corecs = co_rec_of (nth disc_coitersss index);
         val sel_corecss = co_rec_of (nth sel_coiterssss index);
       in
-        map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
-          corec_thms disc_corecs sel_corecss
+        map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
+          disc_excludesss collapses corec_thms disc_corecs sel_corecss
       end;
 
     fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
@@ -471,7 +471,7 @@
   fun_T: typ,
   fun_args: term list,
   ctr: term,
-  ctr_no: int, (*###*)
+  ctr_no: int, (*FIXME*)
   disc: term,
   prems: term list,
   auto_gen: bool,
@@ -838,6 +838,9 @@
     |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
   end;
 
+fun applied_fun_of fun_name fun_T fun_args =
+  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
+
 fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy =
   let
     val thy = Proof_Context.theory_of lthy;
@@ -877,7 +880,7 @@
           strong_coinduct_thms), lthy') =
       corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
     val actual_nn = length bs;
-    val corec_specs = take actual_nn corec_specs'; (*###*)
+    val corec_specs = take actual_nn corec_specs'; (*FIXME*)
     val ctr_specss = map #ctr_specs corec_specs;
 
     val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
@@ -908,8 +911,9 @@
  space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
 *)
 
-    val excludess'' = excludess' |> map (map (fn (idx, t) =>
-      (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (exclude_tac idx), t))));
+    val excludess'' = excludess' |> map (map (fn (idx, goal) =>
+      (idx, (Option.map (Goal.prove lthy [] [] goal #> Thm.close_derivation) (exclude_tac idx),
+         goal))));
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
     val (goal_idxss, goalss') = excludess''
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
@@ -920,13 +924,13 @@
 
     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
+        map (HOLogic.mk_Trueprop o mk_dnf o map #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
+        map (fn goal => Goal.prove lthy [] [] goal (the maybe_tac) |> Thm.close_derivation)
+          nchotomy_goals
       else
         [];
     val goalss =
@@ -973,22 +977,24 @@
             []
           else
             let
-              val {disc_corec, ...} = nth ctr_specs ctr_no;
+              val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
               val k = 1 + ctr_no;
               val m = length prems;
-              val t =
-                list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
-                |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*)
+              val goal =
+                applied_fun_of fun_name fun_T fun_args
+                |> curry betapply disc
                 |> HOLogic.mk_Trueprop
                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
             in
-              if prems = [@{term False}] then [] else
-              mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
-              |> K |> Goal.prove lthy [] [] t
-              |> Thm.close_derivation
-              |> pair (#disc (nth ctr_specs ctr_no))
-              |> single
+              if prems = [@{term False}] then
+                []
+              else
+                mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
+                |> K |> Goal.prove lthy [] [] goal
+                |> Thm.close_derivation
+                |> pair (#disc (nth ctr_specs ctr_no))
+                |> single
             end;
 
         fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec)
@@ -998,13 +1004,13 @@
             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 (s_not_conj o #prems) disc_eqns)
-                (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
+              (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
             val sel_corec = find_index (equal sel) (#sels ctr_spec)
               |> nth (#sel_corecs ctr_spec);
             val k = 1 + ctr_no;
             val m = length prems;
-            val t =
-              list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
+            val goal =
+              applied_fun_of fun_name fun_T fun_args
               |> curry betapply sel
               |> rpair (abstract (List.rev fun_args) rhs_term)
               |> HOLogic.mk_Trueprop o HOLogic.mk_eq
@@ -1014,7 +1020,7 @@
           in
             mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
               nested_map_comps sel_corec k m excludesss
-            |> K |> Goal.prove lthy [] [] t
+            |> K |> Goal.prove lthy [] [] goal
             |> Thm.close_derivation
             |> pair sel
           end;
@@ -1037,14 +1043,15 @@
                 ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #maybe_ctr_rhs x))
                 |> the o merge_options;
               val m = length prems;
-              val t = (if is_some maybe_rhs then the maybe_rhs else
-                  filter (equal ctr o #ctr) sel_eqns
-                  |> fst o finds ((op =) o apsnd #sel) sels
-                  |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
-                  |> curry list_comb ctr)
-                |> curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
-                  map Bound (length fun_args - 1 downto 0)))
-                |> HOLogic.mk_Trueprop
+              val goal =
+                (if is_some maybe_rhs then
+                   the maybe_rhs
+                 else
+                   filter (equal ctr o #ctr) sel_eqns
+                   |> fst o finds ((op =) o apsnd #sel) sels
+                   |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
+                   |> curry list_comb ctr)
+                |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                 |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
                 |> curry Logic.list_all (map dest_Free fun_args);
               val maybe_disc_thm = AList.lookup (op =) disc_alist disc;
@@ -1052,7 +1059,7 @@
             in
               if prems = [@{term False}] then [] else
                 mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms
-                |> K |> Goal.prove lthy [] [] t
+                |> K |> Goal.prove lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair ctr
                 |> single
@@ -1073,8 +1080,7 @@
               let
                 val bound_Ts = List.rev (map fastype_of fun_args);
 
-                val lhs =
-                  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
+                val lhs = applied_fun_of fun_name fun_T fun_args;
                 val maybe_rhs_info =
                   (case maybe_rhs of
                     SOME rhs =>
@@ -1101,21 +1107,22 @@
                             SOME (prems, t)
                           end;
                       val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs;
+                      fun is_syntactically_exhaustive () =
+                        forall null (map_filter (try (fst o the)) maybe_ctr_conds_argss)
+                        orelse forall is_some maybe_ctr_conds_argss
+                          andalso exists #auto_gen disc_eqns
                     in
                       let
-                        val rhs = (if exhaustive
-                              orelse map_filter (try (fst o the)) maybe_ctr_conds_argss
-                                |> forall (equal [])
-                              orelse forall is_some maybe_ctr_conds_argss
-                                andalso exists #auto_gen disc_eqns then
-                            split_last (map_filter I maybe_ctr_conds_argss) ||> snd
-                          else
-                            Const (@{const_name Code.abort}, @{typ String.literal} -->
-                                (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
-                              HOLogic.mk_literal fun_name $
-                              absdummy @{typ unit} (incr_boundvars 1 lhs)
-                            |> pair (map_filter I maybe_ctr_conds_argss))
-                          |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
+                        val rhs =
+                          (if exhaustive orelse is_syntactically_exhaustive () then
+                             split_last (map_filter I maybe_ctr_conds_argss) ||> snd
+                           else
+                             Const (@{const_name Code.abort}, @{typ String.literal} -->
+                                 (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
+                               HOLogic.mk_literal fun_name $
+                               absdummy @{typ unit} (incr_boundvars 1 lhs)
+                             |> pair (map_filter I maybe_ctr_conds_argss))
+                           |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
                       in SOME (rhs, rhs, map snd ctr_alist) end
                     end);
               in
@@ -1124,22 +1131,19 @@
                 | SOME (rhs, raw_rhs, ctr_thms) =>
                   let
                     val ms = map (Logic.count_prems o prop_of) ctr_thms;
-                    val (raw_t, t) = (raw_rhs, rhs)
-                      |> pairself
-                        (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
-                          map Bound (length fun_args - 1 downto 0)))
-                        #> HOLogic.mk_Trueprop
+                    val (raw_goal, goal) = (raw_rhs, rhs)
+                      |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
                         #> curry Logic.list_all (map dest_Free fun_args));
                     val (distincts, discIs, sel_splits, sel_split_asms) =
                       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_nchotomy
-                      |> K |> Goal.prove lthy [] [] raw_t
+                      |> K |> Goal.prove lthy [] [] raw_goal
                       |> Thm.close_derivation;
                   in
                     mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
-                    |> K |> Goal.prove lthy [] [] t
+                    |> K |> Goal.prove lthy [] [] goal
                     |> Thm.close_derivation
                     |> single
                   end)
@@ -1151,6 +1155,32 @@
         val disc_thmss = map (map snd) disc_alists;
         val sel_thmss = map (map snd) sel_alists;
 
+        fun prove_disc_iff ({ctr_specs, ...} : corec_spec) maybe_exhaust_thm discs
+            ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
+          if null discs orelse is_none maybe_exhaust_thm then
+            []
+          else
+            let
+              val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
+              val m = length prems;
+              val goal =
+                mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc,
+                  mk_conjs prems)
+                |> curry Logic.list_all (map dest_Free fun_args);
+            in
+              if prems = [@{term False}] then
+                []
+              else
+                mk_primcorec_disc_iff_tac lthy (ctr_no + 1) (the maybe_exhaust_thm) discs
+                  disc_excludess
+                |> K |> Goal.prove lthy [] [] goal
+                |> Thm.close_derivation
+                |> single
+            end;
+
+        val disc_iff_thmss = map4 (maps ooo prove_disc_iff) corec_specs maybe_exhaust_thms
+          disc_thmss disc_eqnss;
+
         val ctr_alists = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
           ctr_specss;
         val ctr_thmss = map (map snd) ctr_alists;
@@ -1167,6 +1197,7 @@
            (codeN, code_thmss, code_nitpicksimp_attrs),
            (ctrN, ctr_thmss, []),
            (discN, disc_thmss, simp_attrs),
+           (disc_iffN, disc_iff_thmss, []),
            (excludeN, exclude_thmss, []),
            (exhaustN, map the_list maybe_exhaust_thms, []),
            (nchotomyN, map the_list maybe_nchotomy_thms, []),
diff -r 7a01387c47d5 -r 136fe16e726a src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -76,18 +76,18 @@
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
   mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
 
-fun mk_primcorec_disc_iff_tac ctxt k exhaust discs disc_excludess =
+fun mk_primcorec_disc_iff_tac ctxt k fun_exhaust fun_discs disc_excludess =
   HEADGOAL (rtac iffI THEN'
-    rtac exhaust THEN'
+    rtac fun_exhaust THEN'
     EVERY' (map2 (fn disc => fn [] => REPEAT_DETERM o (atac ORELSE' etac conjI)
         | [disc_exclude] =>
           dtac disc THEN' (REPEAT_DETERM o atac) THEN' dtac disc_exclude THEN' etac notE THEN' atac)
-      discs disc_excludess) THEN'
-    etac (unfold_thms ctxt [atomize_conjL] (nth discs (k - 1))));
+      fun_discs disc_excludess) THEN'
+    etac (unfold_thms ctxt [atomize_conjL] (nth fun_discs (k - 1))));
 
-fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps f_sel k m
+fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m
     exclsss =
-  mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
+  mk_primcorec_prelude ctxt defs (fun_sel RS trans) THEN
   mk_primcorec_cases_tac ctxt k m exclsss THEN
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
     eresolve_tac falseEs ORELSE'
@@ -97,12 +97,12 @@
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
-      (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
+       (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
 
-fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
-  HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
-    (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
-  unfold_thms_tac ctxt (Let_def :: sel_fs) THEN HEADGOAL (rtac refl);
+fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_fun sel_funs =
+  HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
+    (the_default (K all_tac) (Option.map rtac maybe_disc_fun)) THEN' REPEAT_DETERM_N m o atac) THEN
+  unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl);
 
 fun inst_split_eq ctxt split =
   (case prop_of split of
@@ -119,13 +119,13 @@
 fun distinct_in_prems_tac distincts =
   eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
 
-fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
+fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
   let
     val splits' =
       map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
   in
     HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
-    mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
+    mk_primcorec_prelude ctxt [] (fun_ctr RS trans) THEN
     HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
       SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
       (rtac refl ORELSE' atac ORELSE'
@@ -139,23 +139,23 @@
 
 fun rulify_nchotomy 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
+fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs
     maybe_nchotomy =
   let
     val n = length ms;
-    val (ms', f_ctrs') =
+    val (ms', fun_ctrs') =
       (case maybe_nchotomy of
-        NONE => (ms, f_ctrs)
+        NONE => (ms, fun_ctrs)
       | SOME nchotomy =>
         (ms |> split_last ||> K [n - 1] |> op @,
-         f_ctrs
+         fun_ctrs
          |> split_last
          ||> unfold_thms ctxt [atomize_conjL]
          ||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
          |> op @));
   in
     EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
-      ms' f_ctrs') THEN
+      ms' fun_ctrs') THEN
     IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
       HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
   end;
diff -r 7a01387c47d5 -r 136fe16e726a src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -30,6 +30,10 @@
   val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
+  val map14:
+    ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o) ->
+    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
   val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
     'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
   val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
@@ -166,37 +170,44 @@
   | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map9 _ [] [] [] [] [] [] [] [] [] = []
-  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
-      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) =
+  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) =
     f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
   | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
-  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
-      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) =
+  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) (x10::x10s) =
     f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
   | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
-  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
-      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) =
+  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) (x10::x10s) (x11::x11s) =
     f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 :: map11 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s
   | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
-      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
+  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
     f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
       map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
   | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
 fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
-  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
-      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
+  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
     f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
       map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
   | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
 
+fun map14 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+  | map14 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
+      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) =
+    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ::
+      map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
+  | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
 fun fold_map4 _ [] [] [] [] acc = ([], acc)
   | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
     let
diff -r 7a01387c47d5 -r 136fe16e726a src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -24,6 +24,7 @@
      disc_thmss: thm list list,
      discIs: thm list,
      sel_thmss: thm list list,
+     disc_excludesss: thm list list list,
      disc_exhausts: thm list,
      sel_exhausts: thm list,
      collapses: thm list,
@@ -85,6 +86,7 @@
    disc_thmss: thm list list,
    discIs: thm list,
    sel_thmss: thm list list,
+   disc_excludesss: thm list list list,
    disc_exhausts: thm list,
    sel_exhausts: thm list,
    collapses: thm list,
@@ -99,7 +101,8 @@
 
 fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
     case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
-    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
+    disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
+    case_eq_ifs} =
   {ctrs = map (Morphism.term phi) ctrs,
    casex = Morphism.term phi casex,
    discs = map (Morphism.term phi) discs,
@@ -116,6 +119,7 @@
    disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    discIs = map (Morphism.thm phi) discIs,
    sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
+   disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
    disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    sel_exhausts = map (Morphism.thm phi) sel_exhausts,
    collapses = map (Morphism.thm phi) collapses,
@@ -657,10 +661,11 @@
           end;
 
         val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
-             disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
-             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
+             disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, sel_exhaust_thms,
+             all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
+             case_eq_if_thms) =
           if no_discs_sels then
-            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
+            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
           else
             let
               val udiscs = map (rapp u) discs;
@@ -873,9 +878,9 @@
                 end;
             in
               (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
-               nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
-               all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
-               [sel_split_asm_thm], [case_eq_if_thm])
+               nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
+               [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
+               [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
             end;
 
         val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
@@ -919,10 +924,10 @@
            nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
            case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
            split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
-           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
-           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
-           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
-           case_eq_ifs = case_eq_if_thms};
+           discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss,
+           disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms,
+           collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms,
+           sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms};
       in
         (ctr_sugar,
          lthy
diff -r 7a01387c47d5 -r 136fe16e726a src/HOL/Tools/Datatype/datatype_data.ML
--- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jan 02 09:50:22 2014 +0100
@@ -112,6 +112,7 @@
    disc_thmss = [],
    discIs = [],
    sel_thmss = [],
+   disc_excludesss = [],
    disc_exhausts = [],
    sel_exhausts = [],
    collapses = [],