author desharna Mon Jul 07 16:06:46 2014 +0200 (2014-07-07) changeset 57525 f9dd8a33f820 parent 57524 b8448367f9c7 child 57526 7027cf5c1f2c
generate 'rel_cases' theorem for (co)datatypes
```     1.1 --- a/src/HOL/BNF_FP_Base.thy	Sat Jul 05 20:51:24 2014 +0200
1.2 +++ b/src/HOL/BNF_FP_Base.thy	Mon Jul 07 16:06:46 2014 +0200
1.3 @@ -13,6 +13,12 @@
1.4  imports BNF_Comp Basic_BNFs
1.5  begin
1.6
1.7 +lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
1.8 +  by default simp_all
1.9 +
1.10 +lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
1.11 +  by default simp_all
1.12 +
1.13  lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
1.14  by auto
1.15
```
```     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sat Jul 05 20:51:24 2014 +0200
2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 07 16:06:46 2014 +0200
2.3 @@ -111,6 +111,9 @@
2.4    fun merge data : T = Symtab.merge (K true) data;
2.5  );
2.6
2.7 +fun choose_relator Rs AB = find_first
2.8 +  (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) Rs;
2.9 +
2.10  fun fp_sugar_of ctxt =
2.11    Symtab.lookup (Data.get (Context.Proof ctxt))
2.12    #> Option.map (transfer_fp_sugar ctxt);
2.13 @@ -472,12 +475,9 @@
2.14        ||>> mk_Freesss "a" ctrAs_Tsss
2.15        ||>> mk_Freesss "b" ctrBs_Tsss;
2.16
2.17 -    fun choose_relator AB = the (find_first
2.18 -      (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
2.19 -
2.20      val premises =
2.21        let
2.22 -        fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
2.23 +        fun build_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B);
2.24          fun build_rel_app a b = build_the_rel (fastype_of a) (fastype_of b) \$ a \$ b;
2.25
2.26          fun mk_prem ctrA ctrB argAs argBs =
2.27 @@ -489,8 +489,8 @@
2.28          flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
2.29        end;
2.30
2.31 -    val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
2.32 -      (map2 mk_leq (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)) IRs));
2.33 +    val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
2.34 +      (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts)) IRs));
2.35
2.36      val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
2.37        (fn {context = ctxt, prems = prems} =>
2.38 @@ -725,12 +725,9 @@
2.39           (mk_discss fpBs Bs, mk_selsss fpBs Bs))
2.40        end;
2.41
2.42 -    fun choose_relator AB = the (find_first
2.43 -      (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
2.44 -
2.45      val premises =
2.46        let
2.47 -        fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
2.48 +        fun build_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B);
2.49
2.50          fun build_rel_app selA_t selB_t =
2.51            (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) \$ selA_t \$ selB_t
2.52 @@ -755,8 +752,8 @@
2.53          map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
2.54        end;
2.55
2.56 -    val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
2.57 -      (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts))));
2.58 +    val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
2.59 +      IRs (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts))));
2.60
2.61      val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
2.62        (fn {context = ctxt, prems = prems} =>
2.63 @@ -1259,7 +1256,7 @@
2.64            end;
2.65
2.66          fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss,
2.67 -          sel_thmss, ...} : ctr_sugar, lthy) =
2.68 +          sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) =
2.69            if live = 0 then
2.70              ((([], [], [], []), ctr_sugar), lthy)
2.71            else
2.72 @@ -1314,14 +1311,93 @@
2.73
2.74                val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
2.75
2.76 -              val (disc_map_iff_thms, sel_map_thms, sel_set_thms) =
2.77 +              val set_empty_thms =
2.78 +                let
2.79 +                  val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
2.80 +                    binder_types o fastype_of) ctrs;
2.81 +                  val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
2.82 +                  val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
2.83 +
2.84 +                  fun mk_set_empty_goal disc set T =
2.85 +                    Logic.mk_implies (HOLogic.mk_Trueprop (disc \$ u),
2.86 +                      mk_Trueprop_eq (set \$ u, HOLogic.mk_set T []));
2.87 +
2.88 +                  val goals =
2.89 +                    if null discs then
2.90 +                      []
2.91 +                    else
2.92 +                      map_filter I (flat
2.93 +                        (map2 (fn names => fn disc =>
2.94 +                          map3 (fn name => fn setT => fn set =>
2.95 +                            if member (op =) names name then NONE
2.96 +                            else SOME (mk_set_empty_goal disc set setT))
2.97 +                          setT_names setTs sets)
2.98 +                        ctr_argT_namess discs));
2.99 +                in
2.100 +                  if null goals then
2.101 +                    []
2.102 +                  else
2.103 +                    Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
2.104 +                      (fn {context = ctxt, prems = _} =>
2.105 +                        mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
2.106 +                      |> Conjunction.elim_balanced (length goals)
2.107 +                      |> Proof_Context.export names_lthy lthy
2.108 +                end;
2.109 +
2.110 +              val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
2.111 +
2.112 +              fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
2.113 +                fold_thms lthy ctr_defs'
2.114 +                  (unfold_thms lthy (pre_rel_def :: abs_inverse ::
2.115 +                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
2.116 +                       @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
2.117 +                     (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
2.118 +                |> postproc
2.119 +                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
2.120 +
2.121 +              fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
2.122 +                mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
2.123 +
2.124 +              fun mk_rel_intro_thm thm =
2.125 +                let
2.126 +                  fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm)))
2.127 +                    handle THM _ => thm
2.128 +                in
2.129 +                  impl (thm RS iffD2)
2.130 +                  handle THM _ => thm
2.131 +                end;
2.132 +
2.133 +              fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
2.134 +                mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
2.135 +                  cxIn cyIn;
2.136 +
2.137 +              fun mk_other_half_rel_distinct_thm thm =
2.138 +                flip_rels lthy live thm
2.139 +                RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
2.140 +
2.141 +              val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
2.142 +              val rel_intro_thms = map mk_rel_intro_thm rel_inject_thms;
2.143 +
2.144 +              val half_rel_distinct_thmss =
2.145 +                map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
2.146 +              val other_half_rel_distinct_thmss =
2.147 +                map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
2.148 +              val (rel_distinct_thms, _) =
2.149 +                join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
2.150 +
2.151 +              val rel_eq_thms =
2.152 +                map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
2.153 +                map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
2.154 +                  rel_inject_thms ms;
2.155 +
2.156 +              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) =
2.157                  let
2.158                    val (((Ds, As), Bs), names_lthy) = lthy
2.160                      ||>> mk_TFrees (live_of_bnf fp_bnf)
2.161                      ||>> mk_TFrees (live_of_bnf fp_bnf);
2.162                    val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
2.163 -                  val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
2.164 +                  val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
2.165                    val fTs = map2 (curry op -->) As Bs;
2.166                    val ((fs, ta), names_lthy) = names_lthy
2.167                      |> mk_Frees "f" fTs
2.168 @@ -1331,6 +1407,60 @@
2.169                    val selssA = map (map (mk_disc_or_sel ADs)) selss;
2.170                    val disc_sel_pairs = flat (map2 (map o pair) discsA selssA);
2.171
2.172 +                  val (rel_cases_thm, rel_cases_attrs) =
2.173 +                    let
2.174 +                      val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
2.175 +                      val (((thesis, Rs), tb), names_lthy) =  names_lthy
2.176 +                        |> yield_singleton (mk_Frees "thesis") HOLogic.boolT
2.177 +                        |>> HOLogic.mk_Trueprop
2.178 +                        ||>> mk_Frees "R" (map2 mk_pred2T As Bs)
2.179 +                        ||>> yield_singleton (mk_Frees "b") TB;
2.180 +
2.181 +                      val _ = apfst HOLogic.mk_Trueprop;
2.182 +                      val rel_Rs_a_b = list_comb (rel, Rs) \$ ta \$ tb;
2.183 +                      val ctrAs = map (mk_ctr ADs) ctrs;
2.184 +                      val ctrBs = map (mk_ctr BDs) ctrs;
2.185 +
2.186 +                      fun mk_assms ctrA ctrB ctxt =
2.187 +                        let
2.188 +                          val argA_Ts = binder_types (fastype_of ctrA);
2.189 +                          val argB_Ts = binder_types (fastype_of ctrB);
2.190 +                          val ((argAs, argBs), names_ctxt) =  ctxt
2.191 +                            |> mk_Frees "x" argA_Ts
2.192 +                            ||>> mk_Frees "y" argB_Ts;
2.193 +                          val ctrA_args = list_comb (ctrA, argAs);
2.194 +                          val ctrB_args = list_comb (ctrB, argBs);
2.195 +                          fun build_the_rel A B =
2.196 +                            build_rel lthy [] (the o choose_relator Rs) (A, B);
2.197 +                          fun build_rel_app a b =
2.198 +                            build_the_rel (fastype_of a) (fastype_of b) \$ a \$ b;
2.199 +                        in
2.200 +                          (fold_rev Logic.all (argAs @ argBs) (Logic.list_implies
2.201 +                             (mk_Trueprop_eq (ta, ctrA_args) ::
2.202 +                                mk_Trueprop_eq (tb, ctrB_args) ::
2.203 +                                  map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs,
2.204 +                              thesis)),
2.205 +                           names_ctxt)
2.206 +                        end;
2.207 +
2.208 +                      val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy;
2.209 +                      val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms,
2.210 +                        thesis);
2.211 +                      val thm = Goal.prove_sorry lthy [] [] goal
2.212 +                          (fn {context = ctxt, prems = _} =>
2.213 +                            mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
2.214 +                              injects rel_inject_thms distincts rel_distinct_thms)
2.215 +                        |> singleton (Proof_Context.export names_lthy lthy)
2.216 +                        |> Thm.close_derivation;
2.217 +
2.218 +                      val ctr_names = quasi_unambiguous_case_names ((map name_of_ctr) ctrAs);
2.219 +                      val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
2.220 +                      val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
2.221 +                      val cases_pred_attr = Attrib.internal o K o Induct.cases_pred;
2.222 +                    in
2.223 +                      (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
2.224 +                    end;
2.225 +
2.226                    val disc_map_iff_thms =
2.227                      let
2.228                        val discsB = map (mk_disc_or_sel BDs) discs;
2.229 @@ -1453,88 +1583,9 @@
2.230                            |> Proof_Context.export names_lthy lthy
2.231                      end;
2.232                  in
2.233 -                  (disc_map_iff_thms, sel_map_thms, sel_set_thms)
2.234 -                end;
2.235 -
2.236 -              val set_empty_thms =
2.237 -                let
2.238 -                  val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
2.239 -                    binder_types o fastype_of) ctrs;
2.240 -                  val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
2.241 -                  val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
2.242 -
2.243 -                  fun mk_set_empty_goal disc set T =
2.244 -                    Logic.mk_implies (HOLogic.mk_Trueprop (disc \$ u),
2.245 -                      mk_Trueprop_eq (set \$ u, HOLogic.mk_set T []));
2.246 -
2.247 -                  val goals =
2.248 -                    if null discs then
2.249 -                      []
2.250 -                    else
2.251 -                      map_filter I (flat
2.252 -                        (map2 (fn names => fn disc =>
2.253 -                          map3 (fn name => fn setT => fn set =>
2.254 -                            if member (op =) names name then NONE
2.255 -                            else SOME (mk_set_empty_goal disc set setT))
2.256 -                          setT_names setTs sets)
2.257 -                        ctr_argT_namess discs));
2.258 -                in
2.259 -                  if null goals then
2.260 -                    []
2.261 -                  else
2.262 -                    Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
2.263 -                      (fn {context = ctxt, prems = _} =>
2.264 -                        mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
2.265 -                      |> Conjunction.elim_balanced (length goals)
2.266 -                      |> Proof_Context.export names_lthy lthy
2.267 +                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs))
2.268                  end;
2.269
2.270 -              val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
2.271 -
2.272 -              fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
2.273 -                fold_thms lthy ctr_defs'
2.274 -                  (unfold_thms lthy (pre_rel_def :: abs_inverse ::
2.275 -                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
2.276 -                       @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
2.277 -                     (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
2.278 -                |> postproc
2.279 -                |> singleton (Proof_Context.export names_lthy no_defs_lthy);
2.280 -
2.281 -              fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
2.282 -                mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
2.283 -
2.284 -              fun mk_rel_intro_thm thm =
2.285 -                let
2.286 -                  fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm)))
2.287 -                    handle THM _ => thm
2.288 -                in
2.289 -                  impl (thm RS iffD2)
2.290 -                  handle THM _ => thm
2.291 -                end;
2.292 -
2.293 -              fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
2.294 -                mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
2.295 -                  cxIn cyIn;
2.296 -
2.297 -              fun mk_other_half_rel_distinct_thm thm =
2.298 -                flip_rels lthy live thm
2.299 -                RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
2.300 -
2.301 -              val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
2.302 -              val rel_intro_thms = map mk_rel_intro_thm rel_inject_thms;
2.303 -
2.304 -              val half_rel_distinct_thmss =
2.305 -                map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
2.306 -              val other_half_rel_distinct_thmss =
2.307 -                map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
2.308 -              val (rel_distinct_thms, _) =
2.309 -                join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
2.310 -
2.311 -              val rel_eq_thms =
2.312 -                map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
2.313 -                map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
2.314 -                  rel_inject_thms ms;
2.315 -
2.316                val anonymous_notes =
2.317                  [([case_cong], fundefcong_attrs),
2.318                   (rel_eq_thms, code_nitpicksimp_attrs)]
2.319 @@ -1543,6 +1594,7 @@
2.320                val notes =
2.321                  [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
2.322                   (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
2.323 +                 (rel_casesN, [rel_cases_thm], rel_cases_attrs),
2.324                   (rel_distinctN, rel_distinct_thms, simp_attrs),
2.325                   (rel_injectN, rel_inject_thms, simp_attrs),
2.326                   (rel_introsN, rel_intro_thms, []),
```
```     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sat Jul 05 20:51:24 2014 +0200
3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 07 16:06:46 2014 +0200
3.3 @@ -26,6 +26,8 @@
3.4    val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
3.5    val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
3.6      tactic
3.7 +  val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
3.8 +    thm list -> thm list -> tactic
3.9    val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
3.10      thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
3.11      thm list -> thm list -> thm list -> tactic
3.12 @@ -211,6 +213,17 @@
3.13        (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
3.14        selsss));
3.15
3.16 +fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts =
3.17 +  HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
3.18 +    rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
3.19 +      hyp_subst_tac ctxt) THEN
3.20 +  Local_Defs.unfold_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
3.21 +    True_implies_equals conj_imp_eq_imp_imp} @
3.22 +    map (fn thm => iffD2 OF [@{thm eq_False}, thm]) (distincts @ rel_distincts) @
3.23 +    map (fn thm => thm RS @{thm eqTrueI}) rel_injects) THEN
3.24 +  TRYALL (atac ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o dtac @{thm meta_spec} THEN'
3.25 +    REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
3.26 +
3.27  fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
3.28    dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
3.29    rtac dtor_rel_coinduct 1 THEN
```
```     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Sat Jul 05 20:51:24 2014 +0200
4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Jul 07 16:06:46 2014 +0200
4.3 @@ -124,6 +124,7 @@
4.4    val morN: string
4.5    val nchotomyN: string
4.6    val recN: string
4.7 +  val rel_casesN: string
4.8    val rel_coinductN: string
4.9    val rel_inductN: string
4.10    val rel_injectN: string
4.11 @@ -406,6 +407,7 @@
4.12  val distinctN = "distinct"
4.13  val rel_distinctN = relN ^ "_" ^ distinctN
4.14  val injectN = "inject"
4.15 +val rel_casesN = relN ^ "_cases"
4.16  val rel_injectN = relN ^ "_" ^ injectN
4.17  val rel_introsN = relN ^ "_intros"
4.18  val rel_coinductN = relN ^ "_" ^ coinductN
```
```     5.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Sat Jul 05 20:51:24 2014 +0200
5.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML	Mon Jul 07 16:06:46 2014 +0200
5.3 @@ -54,7 +54,7 @@
5.4
5.5  fun mk_nchotomy_tac n exhaust =
5.6    HEADGOAL (rtac allI THEN' rtac exhaust THEN'
5.7 -   EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
5.8 +    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
5.9
5.10  fun mk_unique_disc_def_tac m uexhaust =
5.11    HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
```