generate 'disc_iff' property in 'primcorec'
authorblanchet
Thu Jan 02 09:50:22 2014 +0100 (2014-01-02)
changeset 54900136fe16e726a
parent 54899 7a01387c47d5
child 54901 0b8871677e0b
generate 'disc_iff' property in 'primcorec'
src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
src/HOL/BNF/Tools/bnf_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Datatype/datatype_data.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     1.3 @@ -33,6 +33,7 @@
     1.4  val codeN = "code"
     1.5  val ctrN = "ctr"
     1.6  val discN = "disc"
     1.7 +val disc_iffN = "disc_iff"
     1.8  val excludeN = "exclude"
     1.9  val nchotomyN = "nchotomy"
    1.10  val selN = "sel"
    1.11 @@ -68,6 +69,7 @@
    1.12     calls: corec_call list,
    1.13     discI: thm,
    1.14     sel_thms: thm list,
    1.15 +   disc_excludess: thm list list,
    1.16     collapse: thm,
    1.17     corec_thm: thm,
    1.18     disc_corec: thm,
    1.19 @@ -92,6 +94,7 @@
    1.20  
    1.21  val mk_conjs = try (foldr1 HOLogic.mk_conj) #> the_default @{const True};
    1.22  val mk_disjs = try (foldr1 HOLogic.mk_disj) #> the_default @{const False};
    1.23 +val mk_dnf = mk_disjs o map mk_conjs;
    1.24  
    1.25  val conjuncts_s = filter_out (curry (op =) @{const True}) o HOLogic.conjuncts;
    1.26  
    1.27 @@ -411,31 +414,28 @@
    1.28           else No_Corec) g_i
    1.29        | call_of _ [q_i] [g_i, g_i'] _ = Mutual_Corec (q_i, g_i, g_i');
    1.30  
    1.31 -    fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
    1.32 -        disc_corec sel_corecs =
    1.33 +    fun mk_ctr_spec ctr disc sels p_io q_iss f_iss f_Tss discI sel_thms disc_excludess collapse
    1.34 +        corec_thm disc_corec sel_corecs =
    1.35        let val nullary = not (can dest_funT (fastype_of ctr)) in
    1.36 -        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
    1.37 +        {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_io,
    1.38           calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
    1.39 -         collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
    1.40 -         sel_corecs = sel_corecs}
    1.41 +         disc_excludess = disc_excludess, collapse = collapse, corec_thm = corec_thm,
    1.42 +         disc_corec = disc_corec, sel_corecs = sel_corecs}
    1.43        end;
    1.44  
    1.45 -    fun mk_ctr_specs index (ctr_sugars : ctr_sugar list) p_is q_isss f_isss f_Tsss coiter_thmsss
    1.46 -        disc_coitersss sel_coiterssss =
    1.47 +    fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
    1.48 +        sel_coiterssss =
    1.49        let
    1.50 -        val ctrs = #ctrs (nth ctr_sugars index);
    1.51 -        val discs = #discs (nth ctr_sugars index);
    1.52 -        val selss = #selss (nth ctr_sugars index);
    1.53 +        val {ctrs, discs, selss, discIs, sel_thmss, disc_excludesss, collapses, ...} : ctr_sugar =
    1.54 +          nth ctr_sugars index;
    1.55          val p_ios = map SOME p_is @ [NONE];
    1.56          val discIs = #discIs (nth ctr_sugars index);
    1.57 -        val sel_thmss = #sel_thmss (nth ctr_sugars index);
    1.58 -        val collapses = #collapses (nth ctr_sugars index);
    1.59          val corec_thms = co_rec_of (nth coiter_thmsss index);
    1.60          val disc_corecs = co_rec_of (nth disc_coitersss index);
    1.61          val sel_corecss = co_rec_of (nth sel_coiterssss index);
    1.62        in
    1.63 -        map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
    1.64 -          corec_thms disc_corecs sel_corecss
    1.65 +        map14 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss
    1.66 +          disc_excludesss collapses corec_thms disc_corecs sel_corecss
    1.67        end;
    1.68  
    1.69      fun mk_spec ({T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
    1.70 @@ -471,7 +471,7 @@
    1.71    fun_T: typ,
    1.72    fun_args: term list,
    1.73    ctr: term,
    1.74 -  ctr_no: int, (*###*)
    1.75 +  ctr_no: int, (*FIXME*)
    1.76    disc: term,
    1.77    prems: term list,
    1.78    auto_gen: bool,
    1.79 @@ -838,6 +838,9 @@
    1.80      |> K |> nth_map sel_no |> AList.map_entry (op =) ctr
    1.81    end;
    1.82  
    1.83 +fun applied_fun_of fun_name fun_T fun_args =
    1.84 +  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
    1.85 +
    1.86  fun add_primcorec_ursive maybe_tac opts fixes specs maybe_of_specs lthy =
    1.87    let
    1.88      val thy = Proof_Context.theory_of lthy;
    1.89 @@ -877,7 +880,7 @@
    1.90            strong_coinduct_thms), lthy') =
    1.91        corec_specs_of bs arg_Ts res_Ts (get_indices fixes) callssss lthy;
    1.92      val actual_nn = length bs;
    1.93 -    val corec_specs = take actual_nn corec_specs'; (*###*)
    1.94 +    val corec_specs = take actual_nn corec_specs'; (*FIXME*)
    1.95      val ctr_specss = map #ctr_specs corec_specs;
    1.96  
    1.97      val disc_eqnss' = map_filter (try (fn Disc x => x)) eqns_data
    1.98 @@ -908,8 +911,9 @@
    1.99   space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
   1.100  *)
   1.101  
   1.102 -    val excludess'' = excludess' |> map (map (fn (idx, t) =>
   1.103 -      (idx, (Option.map (Goal.prove lthy [] [] t #> Thm.close_derivation) (exclude_tac idx), t))));
   1.104 +    val excludess'' = excludess' |> map (map (fn (idx, goal) =>
   1.105 +      (idx, (Option.map (Goal.prove lthy [] [] goal #> Thm.close_derivation) (exclude_tac idx),
   1.106 +         goal))));
   1.107      val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) excludess'';
   1.108      val (goal_idxss, goalss') = excludess''
   1.109        |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
   1.110 @@ -920,13 +924,13 @@
   1.111  
   1.112      val nchotomy_goals =
   1.113        if exhaustive then
   1.114 -        map (HOLogic.mk_Trueprop o mk_disjs o map (mk_conjs o #prems)) disc_eqnss
   1.115 -        |> list_all_fun_args
   1.116 +        map (HOLogic.mk_Trueprop o mk_dnf o map #prems) disc_eqnss |> list_all_fun_args
   1.117        else
   1.118          [];
   1.119      val nchotomy_taut_thms =
   1.120        if exhaustive andalso is_some maybe_tac then
   1.121 -        map (fn t => Goal.prove lthy [] [] t (the maybe_tac) |> Thm.close_derivation) nchotomy_goals
   1.122 +        map (fn goal => Goal.prove lthy [] [] goal (the maybe_tac) |> Thm.close_derivation)
   1.123 +          nchotomy_goals
   1.124        else
   1.125          [];
   1.126      val goalss =
   1.127 @@ -973,22 +977,24 @@
   1.128              []
   1.129            else
   1.130              let
   1.131 -              val {disc_corec, ...} = nth ctr_specs ctr_no;
   1.132 +              val {disc, disc_corec, ...} = nth ctr_specs ctr_no;
   1.133                val k = 1 + ctr_no;
   1.134                val m = length prems;
   1.135 -              val t =
   1.136 -                list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
   1.137 -                |> curry betapply (#disc (nth ctr_specs ctr_no)) (*###*)
   1.138 +              val goal =
   1.139 +                applied_fun_of fun_name fun_T fun_args
   1.140 +                |> curry betapply disc
   1.141                  |> HOLogic.mk_Trueprop
   1.142                  |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
   1.143                  |> curry Logic.list_all (map dest_Free fun_args);
   1.144              in
   1.145 -              if prems = [@{term False}] then [] else
   1.146 -              mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
   1.147 -              |> K |> Goal.prove lthy [] [] t
   1.148 -              |> Thm.close_derivation
   1.149 -              |> pair (#disc (nth ctr_specs ctr_no))
   1.150 -              |> single
   1.151 +              if prems = [@{term False}] then
   1.152 +                []
   1.153 +              else
   1.154 +                mk_primcorec_disc_tac lthy def_thms disc_corec k m excludesss
   1.155 +                |> K |> Goal.prove lthy [] [] goal
   1.156 +                |> Thm.close_derivation
   1.157 +                |> pair (#disc (nth ctr_specs ctr_no))
   1.158 +                |> single
   1.159              end;
   1.160  
   1.161          fun prove_sel ({nested_map_idents, nested_map_comps, ctr_specs, ...} : corec_spec)
   1.162 @@ -998,13 +1004,13 @@
   1.163              val SOME ctr_spec = find_first (equal ctr o #ctr) ctr_specs;
   1.164              val ctr_no = find_index (equal ctr o #ctr) ctr_specs;
   1.165              val prems = the_default (maps (s_not_conj o #prems) disc_eqns)
   1.166 -                (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
   1.167 +              (find_first (equal ctr_no o #ctr_no) disc_eqns |> Option.map #prems);
   1.168              val sel_corec = find_index (equal sel) (#sels ctr_spec)
   1.169                |> nth (#sel_corecs ctr_spec);
   1.170              val k = 1 + ctr_no;
   1.171              val m = length prems;
   1.172 -            val t =
   1.173 -              list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0))
   1.174 +            val goal =
   1.175 +              applied_fun_of fun_name fun_T fun_args
   1.176                |> curry betapply sel
   1.177                |> rpair (abstract (List.rev fun_args) rhs_term)
   1.178                |> HOLogic.mk_Trueprop o HOLogic.mk_eq
   1.179 @@ -1014,7 +1020,7 @@
   1.180            in
   1.181              mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_map_idents
   1.182                nested_map_comps sel_corec k m excludesss
   1.183 -            |> K |> Goal.prove lthy [] [] t
   1.184 +            |> K |> Goal.prove lthy [] [] goal
   1.185              |> Thm.close_derivation
   1.186              |> pair sel
   1.187            end;
   1.188 @@ -1037,14 +1043,15 @@
   1.189                  ||> Option.map (fn x => (#fun_name x, #fun_T x, #fun_args x, [], #maybe_ctr_rhs x))
   1.190                  |> the o merge_options;
   1.191                val m = length prems;
   1.192 -              val t = (if is_some maybe_rhs then the maybe_rhs else
   1.193 -                  filter (equal ctr o #ctr) sel_eqns
   1.194 -                  |> fst o finds ((op =) o apsnd #sel) sels
   1.195 -                  |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
   1.196 -                  |> curry list_comb ctr)
   1.197 -                |> curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
   1.198 -                  map Bound (length fun_args - 1 downto 0)))
   1.199 -                |> HOLogic.mk_Trueprop
   1.200 +              val goal =
   1.201 +                (if is_some maybe_rhs then
   1.202 +                   the maybe_rhs
   1.203 +                 else
   1.204 +                   filter (equal ctr o #ctr) sel_eqns
   1.205 +                   |> fst o finds ((op =) o apsnd #sel) sels
   1.206 +                   |> map (snd #> (fn [x] => (List.rev (#fun_args x), #rhs_term x)) #-> abstract)
   1.207 +                   |> curry list_comb ctr)
   1.208 +                |> curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
   1.209                  |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
   1.210                  |> curry Logic.list_all (map dest_Free fun_args);
   1.211                val maybe_disc_thm = AList.lookup (op =) disc_alist disc;
   1.212 @@ -1052,7 +1059,7 @@
   1.213              in
   1.214                if prems = [@{term False}] then [] else
   1.215                  mk_primcorec_ctr_of_dtr_tac lthy m collapse maybe_disc_thm sel_thms
   1.216 -                |> K |> Goal.prove lthy [] [] t
   1.217 +                |> K |> Goal.prove lthy [] [] goal
   1.218                  |> Thm.close_derivation
   1.219                  |> pair ctr
   1.220                  |> single
   1.221 @@ -1073,8 +1080,7 @@
   1.222                let
   1.223                  val bound_Ts = List.rev (map fastype_of fun_args);
   1.224  
   1.225 -                val lhs =
   1.226 -                  list_comb (Free (fun_name, fun_T), map Bound (length fun_args - 1 downto 0));
   1.227 +                val lhs = applied_fun_of fun_name fun_T fun_args;
   1.228                  val maybe_rhs_info =
   1.229                    (case maybe_rhs of
   1.230                      SOME rhs =>
   1.231 @@ -1101,21 +1107,22 @@
   1.232                              SOME (prems, t)
   1.233                            end;
   1.234                        val maybe_ctr_conds_argss = map prove_code_ctr ctr_specs;
   1.235 +                      fun is_syntactically_exhaustive () =
   1.236 +                        forall null (map_filter (try (fst o the)) maybe_ctr_conds_argss)
   1.237 +                        orelse forall is_some maybe_ctr_conds_argss
   1.238 +                          andalso exists #auto_gen disc_eqns
   1.239                      in
   1.240                        let
   1.241 -                        val rhs = (if exhaustive
   1.242 -                              orelse map_filter (try (fst o the)) maybe_ctr_conds_argss
   1.243 -                                |> forall (equal [])
   1.244 -                              orelse forall is_some maybe_ctr_conds_argss
   1.245 -                                andalso exists #auto_gen disc_eqns then
   1.246 -                            split_last (map_filter I maybe_ctr_conds_argss) ||> snd
   1.247 -                          else
   1.248 -                            Const (@{const_name Code.abort}, @{typ String.literal} -->
   1.249 -                                (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
   1.250 -                              HOLogic.mk_literal fun_name $
   1.251 -                              absdummy @{typ unit} (incr_boundvars 1 lhs)
   1.252 -                            |> pair (map_filter I maybe_ctr_conds_argss))
   1.253 -                          |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
   1.254 +                        val rhs =
   1.255 +                          (if exhaustive orelse is_syntactically_exhaustive () then
   1.256 +                             split_last (map_filter I maybe_ctr_conds_argss) ||> snd
   1.257 +                           else
   1.258 +                             Const (@{const_name Code.abort}, @{typ String.literal} -->
   1.259 +                                 (@{typ unit} --> body_type fun_T) --> body_type fun_T) $
   1.260 +                               HOLogic.mk_literal fun_name $
   1.261 +                               absdummy @{typ unit} (incr_boundvars 1 lhs)
   1.262 +                             |> pair (map_filter I maybe_ctr_conds_argss))
   1.263 +                           |-> fold_rev (fn (prems, u) => mk_If (s_conjs prems) u)
   1.264                        in SOME (rhs, rhs, map snd ctr_alist) end
   1.265                      end);
   1.266                in
   1.267 @@ -1124,22 +1131,19 @@
   1.268                  | SOME (rhs, raw_rhs, ctr_thms) =>
   1.269                    let
   1.270                      val ms = map (Logic.count_prems o prop_of) ctr_thms;
   1.271 -                    val (raw_t, t) = (raw_rhs, rhs)
   1.272 -                      |> pairself
   1.273 -                        (curry HOLogic.mk_eq (list_comb (Free (fun_name, fun_T),
   1.274 -                          map Bound (length fun_args - 1 downto 0)))
   1.275 -                        #> HOLogic.mk_Trueprop
   1.276 +                    val (raw_goal, goal) = (raw_rhs, rhs)
   1.277 +                      |> pairself (curry mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args)
   1.278                          #> curry Logic.list_all (map dest_Free fun_args));
   1.279                      val (distincts, discIs, sel_splits, sel_split_asms) =
   1.280                        case_thms_of_term lthy bound_Ts raw_rhs;
   1.281  
   1.282                      val raw_code_thm = mk_primcorec_raw_code_of_ctr_tac lthy distincts discIs
   1.283                          sel_splits sel_split_asms ms ctr_thms maybe_nchotomy
   1.284 -                      |> K |> Goal.prove lthy [] [] raw_t
   1.285 +                      |> K |> Goal.prove lthy [] [] raw_goal
   1.286                        |> Thm.close_derivation;
   1.287                    in
   1.288                      mk_primcorec_code_of_raw_code_tac lthy distincts sel_splits raw_code_thm
   1.289 -                    |> K |> Goal.prove lthy [] [] t
   1.290 +                    |> K |> Goal.prove lthy [] [] goal
   1.291                      |> Thm.close_derivation
   1.292                      |> single
   1.293                    end)
   1.294 @@ -1151,6 +1155,32 @@
   1.295          val disc_thmss = map (map snd) disc_alists;
   1.296          val sel_thmss = map (map snd) sel_alists;
   1.297  
   1.298 +        fun prove_disc_iff ({ctr_specs, ...} : corec_spec) maybe_exhaust_thm discs
   1.299 +            ({fun_name, fun_T, fun_args, ctr_no, prems, ...} : coeqn_data_disc) =
   1.300 +          if null discs orelse is_none maybe_exhaust_thm then
   1.301 +            []
   1.302 +          else
   1.303 +            let
   1.304 +              val {disc, disc_excludess, ...} = nth ctr_specs ctr_no;
   1.305 +              val m = length prems;
   1.306 +              val goal =
   1.307 +                mk_Trueprop_eq (applied_fun_of fun_name fun_T fun_args |> curry betapply disc,
   1.308 +                  mk_conjs prems)
   1.309 +                |> curry Logic.list_all (map dest_Free fun_args);
   1.310 +            in
   1.311 +              if prems = [@{term False}] then
   1.312 +                []
   1.313 +              else
   1.314 +                mk_primcorec_disc_iff_tac lthy (ctr_no + 1) (the maybe_exhaust_thm) discs
   1.315 +                  disc_excludess
   1.316 +                |> K |> Goal.prove lthy [] [] goal
   1.317 +                |> Thm.close_derivation
   1.318 +                |> single
   1.319 +            end;
   1.320 +
   1.321 +        val disc_iff_thmss = map4 (maps ooo prove_disc_iff) corec_specs maybe_exhaust_thms
   1.322 +          disc_thmss disc_eqnss;
   1.323 +
   1.324          val ctr_alists = map5 (maps oooo prove_ctr) disc_alists sel_alists disc_eqnss sel_eqnss
   1.325            ctr_specss;
   1.326          val ctr_thmss = map (map snd) ctr_alists;
   1.327 @@ -1167,6 +1197,7 @@
   1.328             (codeN, code_thmss, code_nitpicksimp_attrs),
   1.329             (ctrN, ctr_thmss, []),
   1.330             (discN, disc_thmss, simp_attrs),
   1.331 +           (disc_iffN, disc_iff_thmss, []),
   1.332             (excludeN, exclude_thmss, []),
   1.333             (exhaustN, map the_list maybe_exhaust_thms, []),
   1.334             (nchotomyN, map the_list maybe_nchotomy_thms, []),
     2.1 --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
     2.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 02 09:50:22 2014 +0100
     2.3 @@ -76,18 +76,18 @@
     2.4  fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
     2.5    mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
     2.6  
     2.7 -fun mk_primcorec_disc_iff_tac ctxt k exhaust discs disc_excludess =
     2.8 +fun mk_primcorec_disc_iff_tac ctxt k fun_exhaust fun_discs disc_excludess =
     2.9    HEADGOAL (rtac iffI THEN'
    2.10 -    rtac exhaust THEN'
    2.11 +    rtac fun_exhaust THEN'
    2.12      EVERY' (map2 (fn disc => fn [] => REPEAT_DETERM o (atac ORELSE' etac conjI)
    2.13          | [disc_exclude] =>
    2.14            dtac disc THEN' (REPEAT_DETERM o atac) THEN' dtac disc_exclude THEN' etac notE THEN' atac)
    2.15 -      discs disc_excludess) THEN'
    2.16 -    etac (unfold_thms ctxt [atomize_conjL] (nth discs (k - 1))));
    2.17 +      fun_discs disc_excludess) THEN'
    2.18 +    etac (unfold_thms ctxt [atomize_conjL] (nth fun_discs (k - 1))));
    2.19  
    2.20 -fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps f_sel k m
    2.21 +fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m
    2.22      exclsss =
    2.23 -  mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
    2.24 +  mk_primcorec_prelude ctxt defs (fun_sel RS trans) THEN
    2.25    mk_primcorec_cases_tac ctxt k m exclsss THEN
    2.26    HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
    2.27      eresolve_tac falseEs ORELSE'
    2.28 @@ -97,12 +97,12 @@
    2.29      eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    2.30      etac notE THEN' atac ORELSE'
    2.31      (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
    2.32 -      (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
    2.33 +       (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
    2.34  
    2.35 -fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
    2.36 -  HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
    2.37 -    (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
    2.38 -  unfold_thms_tac ctxt (Let_def :: sel_fs) THEN HEADGOAL (rtac refl);
    2.39 +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_fun sel_funs =
    2.40 +  HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
    2.41 +    (the_default (K all_tac) (Option.map rtac maybe_disc_fun)) THEN' REPEAT_DETERM_N m o atac) THEN
    2.42 +  unfold_thms_tac ctxt (Let_def :: sel_funs) THEN HEADGOAL (rtac refl);
    2.43  
    2.44  fun inst_split_eq ctxt split =
    2.45    (case prop_of split of
    2.46 @@ -119,13 +119,13 @@
    2.47  fun distinct_in_prems_tac distincts =
    2.48    eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
    2.49  
    2.50 -fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
    2.51 +fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
    2.52    let
    2.53      val splits' =
    2.54        map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
    2.55    in
    2.56      HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
    2.57 -    mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
    2.58 +    mk_primcorec_prelude ctxt [] (fun_ctr RS trans) THEN
    2.59      HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
    2.60        SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
    2.61        (rtac refl ORELSE' atac ORELSE'
    2.62 @@ -139,23 +139,23 @@
    2.63  
    2.64  fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
    2.65  
    2.66 -fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs
    2.67 +fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms fun_ctrs
    2.68      maybe_nchotomy =
    2.69    let
    2.70      val n = length ms;
    2.71 -    val (ms', f_ctrs') =
    2.72 +    val (ms', fun_ctrs') =
    2.73        (case maybe_nchotomy of
    2.74 -        NONE => (ms, f_ctrs)
    2.75 +        NONE => (ms, fun_ctrs)
    2.76        | SOME nchotomy =>
    2.77          (ms |> split_last ||> K [n - 1] |> op @,
    2.78 -         f_ctrs
    2.79 +         fun_ctrs
    2.80           |> split_last
    2.81           ||> unfold_thms ctxt [atomize_conjL]
    2.82           ||> (fn thm => [rulify_nchotomy n nchotomy RS thm])
    2.83           |> op @));
    2.84    in
    2.85      EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
    2.86 -      ms' f_ctrs') THEN
    2.87 +      ms' fun_ctrs') THEN
    2.88      IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
    2.89        HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
    2.90    end;
     3.1 --- a/src/HOL/BNF/Tools/bnf_util.ML	Thu Jan 02 09:50:22 2014 +0100
     3.2 +++ b/src/HOL/BNF/Tools/bnf_util.ML	Thu Jan 02 09:50:22 2014 +0100
     3.3 @@ -30,6 +30,10 @@
     3.4    val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
     3.5      'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
     3.6      'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
     3.7 +  val map14:
     3.8 +    ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n -> 'o) ->
     3.9 +    'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
    3.10 +    'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list -> 'o list
    3.11    val fold_map4: ('a -> 'b -> 'c -> 'd -> 'e -> 'f * 'e) ->
    3.12      'a list -> 'b list -> 'c list -> 'd list -> 'e -> 'f list * 'e
    3.13    val fold_map5: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g * 'f) ->
    3.14 @@ -166,37 +170,44 @@
    3.15    | map8 _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.16  
    3.17  fun map9 _ [] [] [] [] [] [] [] [] [] = []
    3.18 -  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
    3.19 -      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) =
    3.20 +  | map9 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    3.21 +      (x9::x9s) =
    3.22      f x1 x2 x3 x4 x5 x6 x7 x8 x9 :: map9 f x1s x2s x3s x4s x5s x6s x7s x8s x9s
    3.23    | map9 _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.24  
    3.25  fun map10 _ [] [] [] [] [] [] [] [] [] [] = []
    3.26 -  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
    3.27 -      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) =
    3.28 +  | map10 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    3.29 +      (x9::x9s) (x10::x10s) =
    3.30      f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 :: map10 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s
    3.31    | map10 _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.32  
    3.33  fun map11 _ [] [] [] [] [] [] [] [] [] [] [] = []
    3.34 -  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
    3.35 -      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) =
    3.36 +  | map11 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    3.37 +      (x9::x9s) (x10::x10s) (x11::x11s) =
    3.38      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
    3.39    | map11 _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.40  
    3.41  fun map12 _ [] [] [] [] [] [] [] [] [] [] [] [] = []
    3.42 -  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
    3.43 -      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
    3.44 +  | map12 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    3.45 +      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) =
    3.46      f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 ::
    3.47        map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
    3.48    | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.49  
    3.50  fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
    3.51 -  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
    3.52 -      (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
    3.53 +  | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    3.54 +      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
    3.55      f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
    3.56        map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
    3.57    | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.58  
    3.59 +fun map14 _ [] [] [] [] [] [] [] [] [] [] [] [] [] [] = []
    3.60 +  | map14 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) (x6::x6s) (x7::x7s) (x8::x8s)
    3.61 +      (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) (x14::x14s) =
    3.62 +    f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ::
    3.63 +      map14 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s
    3.64 +  | map14 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
    3.65 +
    3.66  fun fold_map4 _ [] [] [] [] acc = ([], acc)
    3.67    | fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
    3.68      let
     4.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     4.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Jan 02 09:50:22 2014 +0100
     4.3 @@ -24,6 +24,7 @@
     4.4       disc_thmss: thm list list,
     4.5       discIs: thm list,
     4.6       sel_thmss: thm list list,
     4.7 +     disc_excludesss: thm list list list,
     4.8       disc_exhausts: thm list,
     4.9       sel_exhausts: thm list,
    4.10       collapses: thm list,
    4.11 @@ -85,6 +86,7 @@
    4.12     disc_thmss: thm list list,
    4.13     discIs: thm list,
    4.14     sel_thmss: thm list list,
    4.15 +   disc_excludesss: thm list list list,
    4.16     disc_exhausts: thm list,
    4.17     sel_exhausts: thm list,
    4.18     collapses: thm list,
    4.19 @@ -99,7 +101,8 @@
    4.20  
    4.21  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    4.22      case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    4.23 -    disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms, case_eq_ifs} =
    4.24 +    disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
    4.25 +    case_eq_ifs} =
    4.26    {ctrs = map (Morphism.term phi) ctrs,
    4.27     casex = Morphism.term phi casex,
    4.28     discs = map (Morphism.term phi) discs,
    4.29 @@ -116,6 +119,7 @@
    4.30     disc_thmss = map (map (Morphism.thm phi)) disc_thmss,
    4.31     discIs = map (Morphism.thm phi) discIs,
    4.32     sel_thmss = map (map (Morphism.thm phi)) sel_thmss,
    4.33 +   disc_excludesss = map (map (map (Morphism.thm phi))) disc_excludesss,
    4.34     disc_exhausts = map (Morphism.thm phi) disc_exhausts,
    4.35     sel_exhausts = map (Morphism.thm phi) sel_exhausts,
    4.36     collapses = map (Morphism.thm phi) collapses,
    4.37 @@ -657,10 +661,11 @@
    4.38            end;
    4.39  
    4.40          val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
    4.41 -             disc_exclude_thms, disc_exhaust_thms, sel_exhaust_thms, all_collapse_thms,
    4.42 -             safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms, case_eq_if_thms) =
    4.43 +             disc_exclude_thms, disc_exclude_thmsss, disc_exhaust_thms, sel_exhaust_thms,
    4.44 +             all_collapse_thms, safe_collapse_thms, expand_thms, sel_split_thms, sel_split_asm_thms,
    4.45 +             case_eq_if_thms) =
    4.46            if no_discs_sels then
    4.47 -            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    4.48 +            ([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [])
    4.49            else
    4.50              let
    4.51                val udiscs = map (rapp u) discs;
    4.52 @@ -873,9 +878,9 @@
    4.53                  end;
    4.54              in
    4.55                (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
    4.56 -               nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], [sel_exhaust_thm],
    4.57 -               all_collapse_thms, safe_collapse_thms, [expand_thm], [sel_split_thm],
    4.58 -               [sel_split_asm_thm], [case_eq_if_thm])
    4.59 +               nontriv_discI_thms, disc_exclude_thms, disc_exclude_thmsss, [disc_exhaust_thm],
    4.60 +               [sel_exhaust_thm], all_collapse_thms, safe_collapse_thms, [expand_thm],
    4.61 +               [sel_split_thm], [sel_split_asm_thm], [case_eq_if_thm])
    4.62              end;
    4.63  
    4.64          val exhaust_case_names_attr = Attrib.internal (K (Rule_Cases.case_names exhaust_cases));
    4.65 @@ -919,10 +924,10 @@
    4.66             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    4.67             case_thms = case_thms, case_cong = case_cong_thm, weak_case_cong = weak_case_cong_thm,
    4.68             split = split_thm, split_asm = split_asm_thm, disc_thmss = disc_thmss,
    4.69 -           discIs = discI_thms, sel_thmss = sel_thmss, disc_exhausts = disc_exhaust_thms,
    4.70 -           sel_exhausts = sel_exhaust_thms, collapses = all_collapse_thms, expands = expand_thms,
    4.71 -           sel_splits = sel_split_thms, sel_split_asms = sel_split_asm_thms,
    4.72 -           case_eq_ifs = case_eq_if_thms};
    4.73 +           discIs = discI_thms, sel_thmss = sel_thmss, disc_excludesss = disc_exclude_thmsss,
    4.74 +           disc_exhausts = disc_exhaust_thms, sel_exhausts = sel_exhaust_thms,
    4.75 +           collapses = all_collapse_thms, expands = expand_thms, sel_splits = sel_split_thms,
    4.76 +           sel_split_asms = sel_split_asm_thms, case_eq_ifs = case_eq_if_thms};
    4.77        in
    4.78          (ctr_sugar,
    4.79           lthy
     5.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jan 02 09:50:22 2014 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Thu Jan 02 09:50:22 2014 +0100
     5.3 @@ -112,6 +112,7 @@
     5.4     disc_thmss = [],
     5.5     discIs = [],
     5.6     sel_thmss = [],
     5.7 +   disc_excludesss = [],
     5.8     disc_exhausts = [],
     5.9     sel_exhausts = [],
    5.10     collapses = [],