generate 'rel_cases' theorem for (co)datatypes
authordesharna
Mon Jul 07 16:06:46 2014 +0200 (2014-07-07)
changeset 57525f9dd8a33f820
parent 57524 b8448367f9c7
child 57526 7027cf5c1f2c
generate 'rel_cases' theorem for (co)datatypes
src/HOL/BNF_FP_Base.thy
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML
     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.159                      |> mk_TFrees (dead_of_bnf fp_bnf)
   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]);