1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 18:50:27 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 21:44:43 2012 +0200
     1.3 @@ -24,11 +24,16 @@
     1.4  val caseN = "case";
     1.5  val coitersN = "coiters";
     1.6  val corecsN = "corecs";
     1.7 +val disc_coitersN = "disc_coiters";
     1.8 +val disc_corecsN = "disc_corecs";
     1.9  val itersN = "iters";
    1.10  val recsN = "recs";
    1.11 +val sel_coitersN = "sel_coiters";
    1.12 +val sel_corecsN = "sel_corecs";
    1.13  
    1.14 -fun split_list8 xs =
    1.15 -  (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.16 +fun split_list11 xs =
    1.17 +  (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.18 +   map #9 xs, map #10 xs, map #11 xs);
    1.19  
    1.20  fun strip_map_type (Type (@{type_name fun}, [T as Type _, T'])) = strip_map_type T' |>> cons T
    1.21    | strip_map_type T = ([], T);
    1.22 @@ -362,7 +367,7 @@
    1.23  
    1.24          val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
    1.25  
    1.26 -        fun some_lfp_sugar no_defs_lthy =
    1.27 +        fun some_lfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
    1.28            let
    1.29              val fpT_to_C = fpT --> C;
    1.30  
    1.31 @@ -397,10 +402,11 @@
    1.32  
    1.33              val [iter, recx] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.34            in
    1.35 -            ((ctrs, iter, recx, v, xss, ctr_defs, iter_def, rec_def), lthy)
    1.36 +            ((ctrs, selss, iter, recx, v, xss, ctr_defs, discIs, sel_thmss, iter_def, rec_def),
    1.37 +             lthy)
    1.38            end;
    1.39  
    1.40 -        fun some_gfp_sugar no_defs_lthy =
    1.41 +        fun some_gfp_sugar ((selss, discIs, sel_thmss), no_defs_lthy) =
    1.42            let
    1.43              val B_to_fpT = C --> fpT;
    1.44  
    1.45 @@ -439,7 +445,8 @@
    1.46  
    1.47              val [coiter, corec] = map (mk_iter_like As Cs o Morphism.term phi) csts;
    1.48            in
    1.49 -            ((ctrs, coiter, corec, v, xss, ctr_defs, coiter_def, corec_def), lthy)
    1.50 +            ((ctrs, selss, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
    1.51 +              corec_def), lthy)
    1.52            end;
    1.53        in
    1.54          wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
    1.55 @@ -462,8 +469,8 @@
    1.56          val args = map build_arg TUs;
    1.57        in Term.list_comb (mapx, args) end;
    1.58  
    1.59 -    fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs),
    1.60 -        lthy) =
    1.61 +    fun pour_more_sugar_on_lfps ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs,
    1.62 +        rec_defs), lthy) =
    1.63        let
    1.64          val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
    1.65          val giters = map (lists_bmoc gss) iters;
    1.66 @@ -506,9 +513,11 @@
    1.67              val rec_tacss =
    1.68                map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
    1.69            in
    1.70 -            (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.71 +            (map2 (map2 (fn goal => fn tac =>
    1.72 +                 Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
    1.73                 goal_iterss iter_tacss,
    1.74 -             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.75 +             map2 (map2 (fn goal => fn tac =>
    1.76 +                 Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
    1.77                 goal_recss rec_tacss)
    1.78            end;
    1.79  
    1.80 @@ -523,8 +532,8 @@
    1.81          lthy |> Local_Theory.notes notes |> snd
    1.82        end;
    1.83  
    1.84 -    fun pour_more_sugar_on_gfps ((ctrss, coiters, corecs, vs, _, ctr_defss, coiter_defs,
    1.85 -        corec_defs), lthy) =
    1.86 +    fun pour_more_sugar_on_gfps ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss, discIss,
    1.87 +        sel_thmsss, coiter_defs, corec_defs), lthy) =
    1.88        let
    1.89          val z = the_single zs;
    1.90  
    1.91 @@ -579,13 +588,39 @@
    1.92                 goal_corecss corec_tacss)
    1.93            end;
    1.94  
    1.95 +        fun mk_disc_coiter_like_thms [_] = K []
    1.96 +          | mk_disc_coiter_like_thms thms = map2 (curry (op RS)) thms;
    1.97 +
    1.98 +        val disc_coiter_thmss = map2 mk_disc_coiter_like_thms coiter_thmss discIss;
    1.99 +        val disc_corec_thmss = map2 mk_disc_coiter_like_thms corec_thmss discIss;
   1.100 +
   1.101 +        fun mk_sel_coiter_like_thm coiter_like_thm sel sel_thm =
   1.102 +          let
   1.103 +            val (domT, ranT) = dest_funT (fastype_of sel);
   1.104 +            val arg_cong' =
   1.105 +              Drule.instantiate' (map (SOME o certifyT lthy) [domT, ranT])
   1.106 +                [NONE, NONE, SOME (certify lthy sel)] arg_cong;
   1.107 +            val sel_thm' = sel_thm RSN (2, trans);
   1.108 +          in
   1.109 +            (coiter_like_thm RS arg_cong') RS sel_thm'
   1.110 +          end;
   1.111 +
   1.112 +        val sel_coiter_thmsss =
   1.113 +          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
   1.114 +        val sel_corec_thmsss =
   1.115 +          map3 (map3 (map2 o mk_sel_coiter_like_thm)) coiter_thmss selsss sel_thmsss;
   1.116 +
   1.117          val notes =
   1.118            [(coitersN, coiter_thmss),
   1.119 -           (corecsN, corec_thmss)]
   1.120 +           (disc_coitersN, disc_coiter_thmss),
   1.121 +           (sel_coitersN, map flat sel_coiter_thmsss),
   1.122 +           (corecsN, corec_thmss),
   1.123 +           (disc_corecsN, disc_corec_thmss),
   1.124 +           (sel_corecsN, map flat sel_corec_thmsss)]
   1.125            |> maps (fn (thmN, thmss) =>
   1.126 -            map2 (fn b => fn thms =>
   1.127 -                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
   1.128 -              bs thmss);
   1.129 +            map_filter (fn (_, []) => NONE | (b, thms) =>
   1.130 +              SOME ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []),
   1.131 +                [(thms, [])])) (bs ~~ thmss));
   1.132        in
   1.133          lthy |> Local_Theory.notes notes |> snd
   1.134        end;
   1.135 @@ -594,7 +629,7 @@
   1.136        |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
   1.137          fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
   1.138          ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
   1.139 -      |>> split_list8
   1.140 +      |>> split_list11
   1.141        |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps);
   1.142  
   1.143      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 18:50:27 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Mon Sep 10 21:44:43 2012 +0200
     2.3 @@ -11,7 +11,8 @@
     2.4    val mk_half_pairss: 'a list -> ('a * 'a) list list
     2.5    val mk_ctr: typ list -> term -> term
     2.6    val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     2.7 -    (term list * term) * (binding list * binding list list) -> local_theory -> local_theory
     2.8 +    (term list * term) * (binding list * binding list list) -> local_theory ->
     2.9 +    (term list list * thm list * thm list list) * local_theory
    2.10  end;
    2.11  
    2.12  structure BNF_Wrap : BNF_WRAP =
    2.13 @@ -501,7 +502,7 @@
    2.14            |> map (fn (thmN, thms) =>
    2.15              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
    2.16        in
    2.17 -        lthy |> Local_Theory.notes notes |> snd
    2.18 +        ((selss, discI_thms, sel_thmss), lthy |> Local_Theory.notes notes |> snd)
    2.19        end;
    2.20    in
    2.21      (goalss, after_qed, lthy')
    2.22 @@ -516,7 +517,7 @@
    2.23  val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
    2.24  
    2.25  val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
    2.26 -  Proof.theorem NONE after_qed (map (map (rpair [])) goalss) lthy) oo
    2.27 +  Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
    2.28    prepare_wrap_datatype Syntax.read_term;
    2.29  
    2.30  val _ =