1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 18 11:42:11 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Tue Sep 18 11:42:22 2012 +0200
     1.3 @@ -34,9 +34,8 @@
     1.4  
     1.5  val simp_attrs = @{attributes [simp]};
     1.6  
     1.7 -fun split_list10 xs =
     1.8 -  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
     1.9 -   map #9 xs, map #10 xs);
    1.10 +fun split_list8 xs =
    1.11 +  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs);
    1.12  
    1.13  fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    1.14  
    1.15 @@ -406,7 +405,7 @@
    1.16  
    1.17          val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
    1.18  
    1.19 -        fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) =
    1.20 +        fun define_iter_rec (wrap_res, no_defs_lthy) =
    1.21            let
    1.22              val fpT_to_C = fpT --> C;
    1.23  
    1.24 @@ -438,10 +437,10 @@
    1.25  
    1.26              val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.27            in
    1.28 -            ((ctrs, selss0, iter, recx, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def), lthy)
    1.29 +            ((wrap_res, ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
    1.30            end;
    1.31  
    1.32 -        fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
    1.33 +        fun define_coiter_corec (wrap_res, no_defs_lthy) =
    1.34            let
    1.35              val B_to_fpT = C --> fpT;
    1.36  
    1.37 @@ -478,8 +477,7 @@
    1.38  
    1.39              val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.40            in
    1.41 -            ((ctrs, selss0, coiter, corec, xss, ctr_defs, discIs, sel_thmss, coiter_def, corec_def),
    1.42 -             lthy)
    1.43 +            ((wrap_res, ctrs, coiter, corec, xss, ctr_defs, coiter_def, corec_def), lthy)
    1.44            end;
    1.45  
    1.46          fun wrap lthy =
    1.47 @@ -514,9 +512,13 @@
    1.48          val args = map build_arg TUs;
    1.49        in Term.list_comb (mapx, args) end;
    1.50  
    1.51 -    fun derive_induct_iter_rec_thms_for_types ((ctrss, _, iters, recs, xsss, ctr_defss, _, _,
    1.52 +    fun derive_induct_iter_rec_thms_for_types ((wrap_ress, ctrss, iters, recs, xsss, ctr_defss,
    1.53          iter_defs, rec_defs), lthy) =
    1.54        let
    1.55 +        val inject_thmss = map #2 wrap_ress;
    1.56 +        val distinct_thmss = map #3 wrap_ress;
    1.57 +        val case_thmss = map #4 wrap_ress;
    1.58 +
    1.59          val (((phis, phis'), vs'), names_lthy) =
    1.60            lthy
    1.61            |> mk_Frees' "P" (map mk_predT fpTs)
    1.62 @@ -603,6 +605,7 @@
    1.63              `(conj_dests nn) induct_thm
    1.64            end;
    1.65  
    1.66 +        (* TODO: Generate nicer names in case of clashes *)
    1.67          val induct_cases = Datatype_Prop.indexify_names (maps (map base_name_of_ctr) ctrss);
    1.68  
    1.69          val (iter_thmss, rec_thmss) =
    1.70 @@ -653,6 +656,10 @@
    1.71                 goal_recss rec_tacss)
    1.72            end;
    1.73  
    1.74 +        val simp_thmss =
    1.75 +          map4 (fn injects => fn distincts => fn cases => fn recs =>
    1.76 +            injects @ distincts @ cases @ recs) inject_thmss distinct_thmss case_thmss rec_thmss;
    1.77 +
    1.78          val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
    1.79          fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
    1.80  
    1.81 @@ -665,7 +672,8 @@
    1.82            [(inductN, map single induct_thms,
    1.83              fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
    1.84             (itersN, iter_thmss, K simp_attrs),
    1.85 -           (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs))]
    1.86 +           (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
    1.87 +           (simpsN, simp_thmss, K [])]
    1.88            |> maps (fn (thmN, thmss, attrs) =>
    1.89              map3 (fn b => fn Type (T_name, _) => fn thms =>
    1.90                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
    1.91 @@ -674,9 +682,13 @@
    1.92          lthy |> Local_Theory.notes (common_notes @ notes) |> snd
    1.93        end;
    1.94  
    1.95 -    fun derive_coinduct_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, _, ctr_defss,
    1.96 -        discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
    1.97 +    fun derive_coinduct_coiter_corec_thms_for_types ((wrap_ress, ctrss, coiters, corecs, _,
    1.98 +        ctr_defss, coiter_defs, corec_defs), lthy) =
    1.99        let
   1.100 +        val selsss0 = map #1 wrap_ress;
   1.101 +        val discIss = map #5 wrap_ress;
   1.102 +        val sel_thmsss = map #6 wrap_ress;
   1.103 +
   1.104          val (vs', _) =
   1.105            lthy
   1.106            |> Variable.variant_fixes (map Binding.name_of fp_bs);
   1.107 @@ -765,9 +777,9 @@
   1.108            end;
   1.109  
   1.110          val sel_coiter_thmsss =
   1.111 -          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
   1.112 +          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss0 sel_thmsss;
   1.113          val sel_corec_thmsss =
   1.114 -          map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss sel_thmsss;
   1.115 +          map3 (map3 (map2 o mk_sel_coiter_like_thm)) corec_thmss selsss0 sel_thmsss;
   1.116  
   1.117          val common_notes =
   1.118            (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
   1.119 @@ -791,7 +803,7 @@
   1.120        end;
   1.121  
   1.122      fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
   1.123 -      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list10
   1.124 +      fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list8
   1.125  
   1.126      val lthy' = lthy
   1.127        |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 18 11:42:11 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Tue Sep 18 11:42:22 2012 +0200
     2.3 @@ -62,6 +62,7 @@
     2.4    val sel_corecsN: string
     2.5    val set_inclN: string
     2.6    val set_set_inclN: string
     2.7 +  val simpsN: string
     2.8    val strTN: string
     2.9    val str_initN: string
    2.10    val sum_bdN: string
    2.11 @@ -164,6 +165,7 @@
    2.12  val coiterN = coN ^ iterN
    2.13  val coitersN = coiterN ^ "s"
    2.14  val uniqueN = "_unique"
    2.15 +val simpsN = "simps"
    2.16  val fldN = "fld"
    2.17  val unfN = "unf"
    2.18  val fld_iterN = fldN ^ "_" ^ iterN
    2.19 @@ -173,7 +175,7 @@
    2.20  val fld_iter_uniqueN = fld_iterN ^ uniqueN
    2.21  val unf_coiter_uniqueN = unf_coiterN ^ uniqueN
    2.22  val fld_unf_coitersN = fldN ^ "_" ^ unf_coiterN ^ "s"
    2.23 -val map_simpsN = mapN ^ "_simps"
    2.24 +val map_simpsN = mapN ^ "_" ^ simpsN
    2.25  val map_uniqueN = mapN ^ uniqueN
    2.26  val min_algN = "min_alg"
    2.27  val morN = "mor"
    2.28 @@ -187,7 +189,7 @@
    2.29  val LevN = "Lev"
    2.30  val rvN = "recover"
    2.31  val behN = "beh"
    2.32 -fun mk_set_simpsN i = mk_setN i ^ "_simps"
    2.33 +fun mk_set_simpsN i = mk_setN i ^ "_" ^ simpsN
    2.34  fun mk_set_minimalN i = mk_setN i ^ "_minimal"
    2.35  fun mk_set_inductN i = mk_setN i ^ "_induct"
    2.36  

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 11:42:11 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 18 11:42:22 2012 +0200
     3.3 @@ -13,7 +13,7 @@
     3.4    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     3.5      ((bool * term list) * term) *
     3.6        (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     3.7 -    (term list list * thm list * thm list list) * local_theory
     3.8 +    (term list list * thm list * thm list * thm list * thm list * thm list list) * local_theory
     3.9    val parse_wrap_options: bool parser
    3.10    val parse_bound_term: (binding * string) parser
    3.11  end;
    3.12 @@ -327,6 +327,8 @@
    3.13          val ([exhaust_thm], (inject_thmss, (half_distinct_thmss, [case_thms]))) =
    3.14            (hd thmss, apsnd (chop (n * n)) (chop n (tl thmss)));
    3.15  
    3.16 +        val inject_thms = flat inject_thmss;
    3.17 +
    3.18          val exhaust_thm' =
    3.19            let val Tinst = map (pairself (certifyT lthy)) (map Logic.varifyT_global As ~~ As) in
    3.20              Drule.instantiate' [] [SOME (certify lthy v)]
    3.21 @@ -571,7 +573,7 @@
    3.22             (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
    3.23             (distinctN, distinct_thms, simp_attrs @ induct_simp_attrs),
    3.24             (exhaustN, [exhaust_thm], [exhaust_case_names_attr, cases_type_attr]),
    3.25 -           (injectN, flat inject_thmss, iff_attrs @ induct_simp_attrs),
    3.26 +           (injectN, inject_thms, iff_attrs @ induct_simp_attrs),
    3.27             (nchotomyN, [nchotomy_thm], []),
    3.28             (selsN, all_sel_thms, simp_attrs),
    3.29             (splitN, [split_thm], []),
    3.30 @@ -586,7 +588,8 @@
    3.31            [(map (fn th => th RS notE) distinct_thms, safe_elim_attrs)]
    3.32            |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
    3.33        in
    3.34 -        ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
    3.35 +        ((selss, inject_thms, distinct_thms, case_thms, discI_thms, sel_thmss),
    3.36 +         lthy |> Local_Theory.notes (notes' @ notes) |> snd)
    3.37        end;
    3.38    in
    3.39      (goalss, after_qed, lthy')