generate 'corec_code' theorem for codatatypes

--- a/src/HOL/BNF_FP_Base.thy	Wed Jul 02 13:23:11 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy	Wed Jul 02 17:01:49 2014 +0200
@@ -187,6 +187,9 @@
 lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
   by (simp add: inj_on_def)
 
+lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
+  by simp
+
 ML_file "Tools/BNF/bnf_fp_util.ML"
 ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
 ML_file "Tools/BNF/bnf_lfp_size.ML"

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 02 13:23:11 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Jul 02 17:01:49 2014 +0200
@@ -27,8 +27,8 @@
 
   type gfp_sugar_thms =
     ((thm list * thm) list * (Args.src list * Args.src list))
-    * (thm list list * Args.src list)
-    * (thm list list * Args.src list)
+    * thm list list
+    * thm list list
     * (thm list list * Args.src list)
     * (thm list list list * Args.src list)
 
@@ -96,6 +96,8 @@
 open BNF_LFP_Size
 
 val EqN = "Eq_";
+
+val corec_codeN = "corec_code";
 val disc_map_iffN = "disc_map_iff";
 val sel_mapN = "sel_map";
 val sel_setN = "sel_set";
@@ -278,18 +280,18 @@
 
 type gfp_sugar_thms =
   ((thm list * thm) list * (Args.src list * Args.src list))
-  * (thm list list * Args.src list)
-  * (thm list list * Args.src list)
+  * thm list list
+  * thm list list
   * (thm list list * Args.src list)
   * (thm list list list * Args.src list);
 
 fun morph_gfp_sugar_thms phi ((coinducts_pairs, coinduct_attrs_pair),
-    (corecss, corec_attrs), (disc_corecss, disc_corec_attrs),
-    (disc_corec_iffss, disc_corec_iff_attrs), (sel_corecsss, sel_corec_attrs)) =
+    corecss, disc_corecss, (disc_corec_iffss, disc_corec_iff_attrs),
+    (sel_corecsss, sel_corec_attrs)) =
   ((map (apfst (map (Morphism.thm phi)) o apsnd (Morphism.thm phi)) coinducts_pairs,
     coinduct_attrs_pair),
-   (map (map (Morphism.thm phi)) corecss, corec_attrs),
-   (map (map (Morphism.thm phi)) disc_corecss, disc_corec_attrs),
+   map (map (Morphism.thm phi)) corecss,
+   map (map (Morphism.thm phi)) disc_corecss,
    (map (map (Morphism.thm phi)) disc_corec_iffss, disc_corec_iff_attrs),
    (map (map (map (Morphism.thm phi))) sel_corecsss, sel_corec_attrs)) : gfp_sugar_thms;
 
@@ -962,8 +964,8 @@
     val sel_corec_thmsss = mk_sel_corec_thms corec_thmss;
   in
     ((coinduct_thms_pairs, mk_coinduct_attrs fpTs ctr_sugars mss),
-     (corec_thmss, code_nitpicksimp_attrs),
-     (disc_corec_thmss, []),
+     corec_thmss,
+     disc_corec_thmss,
      (disc_corec_iff_thmss, simp_attrs),
      (sel_corec_thmsss, simp_attrs))
   end;
@@ -1629,13 +1631,25 @@
       let
         val (([(coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)],
               (coinduct_attrs, common_coinduct_attrs)),
-             (corec_thmss, corec_attrs), (disc_corec_thmss, disc_corec_attrs),
+             corec_thmss, disc_corec_thmss,
              (disc_corec_iff_thmss, disc_corec_iff_attrs), (sel_corec_thmsss, sel_corec_attrs)) =
           derive_coinduct_corecs_thms_for_types pre_bnfs (the corecs_args_types) xtor_co_induct
             dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss mss
             ns abs_inverses abs_inverses I ctr_defss ctr_sugars corecs corec_defs
             (Proof_Context.export lthy' no_defs_lthy) lthy;
 
+        fun distinct_prems ctxt th =
+          Goal.prove ctxt [] []
+            (th |> Thm.prop_of |> Logic.strip_horn |>> distinct (op aconv) |> Logic.list_implies)
+            (fn _ => HEADGOAL (cut_tac th THEN' atac) THEN ALLGOALS eq_assume_tac);
+
+        fun eq_ifIN _ [thm] = thm
+          | eq_ifIN ctxt (thm :: thms) =
+              distinct_prems ctxt (@{thm eq_ifI} OF
+                (map (unfold_thms ctxt @{thms atomize_imp[of _ "t = u" for t u]})
+                  [thm, eq_ifIN ctxt thms]));
+
+        val corec_code_thms = map (eq_ifIN lthy) corec_thmss
         val sel_corec_thmss = map flat sel_corec_thmsss;
 
         val coinduct_type_attr = Attrib.internal o K o Induct.coinduct_type;
@@ -1675,8 +1689,9 @@
         val notes =
           [(coinductN, map single coinduct_thms,
             fn T_name => coinduct_attrs @ [coinduct_type_attr T_name]),
-           (corecN, corec_thmss, K corec_attrs),
-           (disc_corecN, disc_corec_thmss, K disc_corec_attrs),
+           (corecN, corec_thmss, K []),
+           (corec_codeN, map single corec_code_thms, K code_nitpicksimp_attrs),
+           (disc_corecN, disc_corec_thmss, K []),
            (disc_corec_iffN, disc_corec_iff_thmss, K disc_corec_iff_attrs),
            (rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
            (sel_corecN, sel_corec_thmss, K sel_corec_attrs),

--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Jul 02 13:23:11 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Jul 02 17:01:49 2014 +0200
@@ -267,7 +267,7 @@
               dtor_injects dtor_ctors xtor_co_rec_thms live_nesting_bnfs fpTs Cs Xs ctrXs_Tsss kss
               mss ns fp_abs_inverses abs_inverses (fn thm => thm RS @{thm vimage2p_refl}) ctr_defss
               ctr_sugars co_recs co_rec_defs (Proof_Context.export lthy no_defs_lthy) lthy
-            |> `(fn ((coinduct_thms_pairs, _), (corec_thmss, _), (disc_corec_thmss, _), _,
+            |> `(fn ((coinduct_thms_pairs, _), corec_thmss, disc_corec_thmss, _,
                      (sel_corec_thmsss, _)) =>
               (map snd coinduct_thms_pairs, map fst coinduct_thms_pairs, corec_thmss,
                disc_corec_thmss, sel_corec_thmsss))

--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Jul 02 13:23:11 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Jul 02 17:01:49 2014 +0200
@@ -610,7 +610,7 @@
       map (fn thm => thm OF (passive @ active) RS @{thm ext}) map_cong0s;
     val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1;
     val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2;
-    
+
     fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong =>
       mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs;
     val rewrite1s = mk_rewrites map_cong1s;