src/HOL/Codatatype/Tools/bnf_fp_sugar.ML

 open BNF_FP_Util
 open BNF_FP_Sugar_Tactics
 
 val simp_attrs = @{attributes [simp]};
 
-fun split_list10 xs =
-  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
-   map #9 xs, map #10 xs);
+fun split_list8 xs =
+  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
 fun typ_subst inst (T as Type (s, Ts)) =
     (case AList.lookup (op =) inst T of

           map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
             mk_case_tac ctxt n k m case_def ctr_def unf_fld) ks ms ctr_defs;
 
         val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
 
-        fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) =
+        fun define_iter_rec (wrap_res, no_defs_lthy) =
           let
             val fpT_to_C = fpT --> C;
 
             fun generate_iter_like (suf, fp_iter_like, (fss, f_Tss, xssss)) =
               let

 
             val [iter_def, rec_def] = map (Morphism.thm phi) defs;
 
             val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
           in
-            ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy)
-          end;
-
-        fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
+            ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
+          end;
+
+        fun define_coiter_corec (wrap_res, no_defs_lthy) =
           let
             val B_to_fpT = C --> fpT;
 
             fun mk_preds_getterss_join c n cps sum_prod_T cqfss =
               Term.lambda c (mk_IfN sum_prod_T cps

 
             val [coiter_def, corec_def] = map (Morphism.thm phi) defs;
 
             val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
           in
-            ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def),
-             lthy)
+            ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
           end;
 
         fun wrap lthy =
           let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
             wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,

         val mapx = mk_map live Ts Us (map_of_bnf bnf);
         val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
         val args = map build_arg TUs;
       in Term.list_comb (mapx, args) end;
 
-    fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
+    fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
         iter_defs, rec_defs), lthy) =
       let
+        val inject_thmss = map #2 wrap_ress;
+        val distinct_thmss = map #3 wrap_ress;
+        val case_thmss = map #4 wrap_ress;
+
         val (((phis, phis'), vs'), names_lthy) =
           lthy
           |> mk_Frees' "P" (map mk_predT fpTs)
           ||>> Variable.variant_fixes (map Binding.name_of fp_bs);
 

               |> singleton (Proof_Context.export names_lthy lthy)
           in
             `(conj_dests nn) induct_thm
           end;
 
+        (* TODO: Generate nicer names in case of clashes *)
         val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
 
         val (iter_thmss, rec_thmss) =
           let
             val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;

                goal_iterss iter_tacss,
              map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_recss rec_tacss)
           end;
 
+        val simp_thmss =
+          map4 (fn injects => fn distincts => fn cases => fn recs =>
+            injects @ distincts @ cases @ recs) inject_thmss distinct_thmss case_thmss rec_thmss;
+
         val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
 
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])

 
         val notes =
           [(inductN, map single induct_thms,
             fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
            (itersN, iter_thmss, K simp_attrs),
-           (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs))]
+           (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
+           (simpsN, simp_thmss, K [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map3 (fn b => fn Type (T_name, _) => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
                 [(thms, [])])) fp_bs fpTs thmss);
       in
         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
       end;
 
-    fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
-        discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
+    fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
+        ctr_defss, coiter_defs, corec_defs), lthy) =
       let
+        val selsss0 = map #1 wrap_ress;
+        val discIss = map #5 wrap_ress;
+        val sel_thmsss = map #6 wrap_ress;
+
         val (vs', _) =
           lthy
           |> Variable.variant_fixes (map Binding.name_of fp_bs);
 
         val vs = map2 (curry Free) vs' fpTs;

           in
             coiter_like_thm RS arg_cong' RS sel_thm'
           end;
 
         val sel_coiter_thmsss =
-          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
+          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss0 sel_thmsss;
         val sel_corec_thmsss =
-          map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
+          map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss0 sel_thmsss;
 
         val common_notes =
           (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
           |> map (fn (thmN, thms, attrs) =>
               ((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));

       in
         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
       end;
 
     fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
-      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10
+      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
 
     val lthy' = lthy
       |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
         fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
         ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)