1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature BNF_FP_SUGAR =
     1.6  sig
     1.7 +  (* TODO: programmatic interface *)
     1.8  end;
     1.9  
    1.10  structure BNF_FP_Sugar : BNF_FP_SUGAR =
    1.11 @@ -23,6 +24,8 @@
    1.12  val itersN = "iters";
    1.13  val recsN = "recs";
    1.14  
    1.15 +fun split_list7 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs);
    1.16 +
    1.17  fun retype_free (Free (s, _)) T = Free (s, T);
    1.18  
    1.19  fun flat_list_comb (f, xss) = fold (fn xs => fn t => Term.list_comb (t, xs)) xss f
    1.20 @@ -127,7 +130,8 @@
    1.21  
    1.22      val eqs = map dest_TFree Xs ~~ sum_prod_TsXs;
    1.23  
    1.24 -    val ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects), lthy) =
    1.25 +    val ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects, fp_iter_thms,
    1.26 +        fp_rec_thms), lthy) =
    1.27        fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs mixfixes As' eqs no_defs_lthy;
    1.28  
    1.29      val timer = time (Timer.startRealTimer ());
    1.30 @@ -257,10 +261,8 @@
    1.31            end;
    1.32  
    1.33          val inject_tacss =
    1.34 -          map2 (fn 0 => K []
    1.35 -                 | _ => fn ctr_def => [fn {context = ctxt, ...} =>
    1.36 -                     mk_inject_tac ctxt ctr_def fld_inject])
    1.37 -            ms ctr_defs;
    1.38 +          map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
    1.39 +              mk_inject_tac ctxt ctr_def fld_inject]) ms ctr_defs;
    1.40  
    1.41          val half_distinct_tacss =
    1.42            map (map (fn (def, def') => fn {context = ctxt, ...} =>
    1.43 @@ -308,23 +310,27 @@
    1.44              val iter = mk_iter_or_rec As Cs' iter0;
    1.45              val recx = mk_iter_or_rec As Cs' rec0;
    1.46            in
    1.47 -            ([[ctrs], [[iter]], [[recx]], xss], lthy)
    1.48 +            ((ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
    1.49            end;
    1.50  
    1.51 -        fun sugar_codatatype no_defs_lthy = ([], no_defs_lthy);
    1.52 +        fun sugar_codatatype no_defs_lthy =
    1.53 +          (([], @{term True}, @{term True}, [], [], TrueI, TrueI), no_defs_lthy);
    1.54        in
    1.55          wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
    1.56          |> (if gfp then sugar_codatatype else sugar_datatype)
    1.57        end;
    1.58  
    1.59 -    fun pour_more_sugar_on_datatypes ([[ctrss], [[iters]], [[recs]], xsss], lthy) =
    1.60 +    fun pour_more_sugar_on_datatypes ((ctrss, iters, recs, xsss, ctr_defss, iter_defs, rec_defs),
    1.61 +        lthy) =
    1.62        let
    1.63          val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
    1.64          val giters = map (fn iter => flat_list_comb (iter, gss)) iters;
    1.65          val hrecs = map (fn recx => flat_list_comb (recx, hss)) recs;
    1.66  
    1.67          val (iter_thmss, rec_thmss) =
    1.68 -          let
    1.69 +          if true then
    1.70 +            `I (map (map (K TrueI)) ctr_defss)
    1.71 +          else let
    1.72              fun mk_goal_iter_or_rec fss fc xctr f xs xs' =
    1.73                mk_Trueprop_eq (fc $ xctr, Term.list_comb (f, xs'));
    1.74  
    1.75 @@ -342,13 +348,14 @@
    1.76                map5 (map4 o mk_goal_iter_or_rec hss) hrecs xctrss hss xsss rec_xsss;
    1.77  
    1.78              val iter_tacss =
    1.79 -              map (map (K (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy)))) goal_iterss;
    1.80 -              (* ### map (map mk_iter_or_rec_tac); (* needs ctr_def, iter_def, fld_iter *) *)
    1.81 +              map2 (map o mk_iter_or_rec_tac bnf_map_defs iter_defs) fp_iter_thms ctr_defss;
    1.82              val rec_tacss =
    1.83 -              map (map (K (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy)))) goal_recss;
    1.84 +              map2 (map o mk_iter_or_rec_tac bnf_map_defs rec_defs) fp_rec_thms ctr_defss;
    1.85            in
    1.86 -            (map2 (map2 (Skip_Proof.prove lthy [] [])) goal_iterss iter_tacss,
    1.87 -             map2 (map2 (Skip_Proof.prove lthy [] [])) goal_recss rec_tacss)
    1.88 +            (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.89 +               goal_iterss iter_tacss,
    1.90 +             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.91 +               goal_recss rec_tacss)
    1.92            end;
    1.93  
    1.94          val notes =
    1.95 @@ -366,7 +373,8 @@
    1.96        |> fold_map pour_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ fp_recs ~~
    1.97          fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_binderss ~~ ctr_mixfixess ~~ ctr_Tsss ~~
    1.98          disc_binderss ~~ sel_bindersss)
    1.99 -      |> (if gfp then snd else pour_more_sugar_on_datatypes o apfst transpose);
   1.100 +      |>> split_list7
   1.101 +      |> (if gfp then snd else pour_more_sugar_on_datatypes);
   1.102  
   1.103      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
   1.104        (if gfp then "co" else "") ^ "datatype"));

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.3 @@ -13,6 +13,7 @@
     2.4      -> tactic
     2.5    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     2.6    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
     2.7 +  val mk_iter_or_rec_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
     2.8  end;
     2.9  
    2.10  structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
    2.11 @@ -48,4 +49,11 @@
    2.12    Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
    2.13    Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
    2.14  
    2.15 +val iter_or_rec_thms =
    2.16 +  @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
    2.17 +
    2.18 +fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def bnf_map_def ctxt =
    2.19 +  Local_Defs.unfold_tac ctxt (ctr_def :: bnf_map_def :: iter_or_rec_defs @ fld_iter_or_recs) THEN
    2.20 +  Local_Defs.unfold_tac ctxt iter_or_rec_thms THEN rtac refl 1;
    2.21 +
    2.22  end;

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
     3.3 @@ -11,7 +11,8 @@
     3.4  sig
     3.5    val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
     3.6      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
     3.7 -    (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
     3.8 +    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
     3.9 +      thm list) * local_theory
    3.10  end;
    3.11  
    3.12  structure BNF_GFP : BNF_GFP =
    3.13 @@ -2999,8 +3000,9 @@
    3.14              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    3.15            bs thmss)
    3.16    in
    3.17 -    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms),
    3.18 -      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    3.19 +    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, coiter_thms,
    3.20 +      corec_thms),
    3.21 +     lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    3.22    end;
    3.23  
    3.24  val _ =

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 21:04:26 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 21:04:26 2012 +0200
     4.3 @@ -8,9 +8,10 @@
     4.4  
     4.5  signature BNF_LFP =
     4.6  sig
     4.7 -  val bnf_lfp:  mixfix list -> (string * sort) list option -> binding list ->
     4.8 +  val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
     4.9      typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.10 -    (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
    4.11 +    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
    4.12 +      thm list) * local_theory
    4.13  end;
    4.14  
    4.15  structure BNF_LFP : BNF_LFP =
    4.16 @@ -1822,8 +1823,8 @@
    4.17              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    4.18            bs thmss)
    4.19    in
    4.20 -    ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms),
    4.21 -      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    4.22 +    ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
    4.23 +     lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    4.24    end;
    4.25  
    4.26  val _ =