# HG changeset patch
# User blanchet
# Date 1347131066 -7200
# Node ID 674f04c737e013dc5d5cb3dc2bd9b5015b329a47
# Parent  0b735fb2602eae9544db08aa4b8e88ab8fd5b1c3
implemented "mk_iter_or_rec_tac"

diff -r 0b735fb2602e -r 674f04c737e0 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -7,6 +7,7 @@
 
 signature BNF_FP_SUGAR =
 sig
+  (* TODO: programmatic interface *)
 end;
 
 structure BNF_FP_Sugar : BNF_FP_SUGAR =
@@ -23,6 +24,8 @@
 val itersN = "iters";
 val recsN = "recs";
 
+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);
+
 fun retype_free (Free (s, _)) T = Free (s, T);
 
 fun flat_list_comb (f, xss) = fold (fn xs => fn t => Term.list_comb (t, xs)) xss f
@@ -127,7 +130,8 @@
 
     val eqs = map dest_TFree Xs ~~ sum_prod_TsXs;
 
-    val ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects), lthy) =
+    val ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects, fp_iter_thms,
+        fp_rec_thms), lthy) =
       fp_bnf (if gfp then bnf_gfp else bnf_lfp) bs mixfixes As' eqs no_defs_lthy;
 
     val timer = time (Timer.startRealTimer ());
@@ -257,10 +261,8 @@
           end;
 
         val inject_tacss =
-          map2 (fn 0 => K []
-                 | _ => fn ctr_def => [fn {context = ctxt, ...} =>
-                     mk_inject_tac ctxt ctr_def fld_inject])
-            ms ctr_defs;
+          map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
+              mk_inject_tac ctxt ctr_def fld_inject]) ms ctr_defs;
 
         val half_distinct_tacss =
           map (map (fn (def, def') => fn {context = ctxt, ...} =>
@@ -308,23 +310,27 @@
             val iter = mk_iter_or_rec As Cs' iter0;
             val recx = mk_iter_or_rec As Cs' rec0;
           in
-            ([[ctrs], [[iter]], [[recx]], xss], lthy)
+            ((ctrs, iter, recx, xss, ctr_defs, iter_def, rec_def), lthy)
           end;
 
-        fun sugar_codatatype no_defs_lthy = ([], no_defs_lthy);
+        fun sugar_codatatype no_defs_lthy =
+          (([], @{term True}, @{term True}, [], [], TrueI, TrueI), no_defs_lthy);
       in
         wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
         |> (if gfp then sugar_codatatype else sugar_datatype)
       end;
 
-    fun pour_more_sugar_on_datatypes ([[ctrss], [[iters]], [[recs]], xsss], lthy) =
+    fun pour_more_sugar_on_datatypes ((ctrss, iters, recs, xsss, ctr_defss, iter_defs, rec_defs),
+        lthy) =
       let
         val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
         val giters = map (fn iter => flat_list_comb (iter, gss)) iters;
         val hrecs = map (fn recx => flat_list_comb (recx, hss)) recs;
 
         val (iter_thmss, rec_thmss) =
-          let
+          if true then
+            `I (map (map (K TrueI)) ctr_defss)
+          else let
             fun mk_goal_iter_or_rec fss fc xctr f xs xs' =
               mk_Trueprop_eq (fc $ xctr, Term.list_comb (f, xs'));
 
@@ -342,13 +348,14 @@
               map5 (map4 o mk_goal_iter_or_rec hss) hrecs xctrss hss xsss rec_xsss;
 
             val iter_tacss =
-              map (map (K (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy)))) goal_iterss;
-              (* ### map (map mk_iter_or_rec_tac); (* needs ctr_def, iter_def, fld_iter *) *)
+              map2 (map o mk_iter_or_rec_tac bnf_map_defs iter_defs) fp_iter_thms ctr_defss;
             val rec_tacss =
-              map (map (K (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy)))) goal_recss;
+              map2 (map o mk_iter_or_rec_tac bnf_map_defs rec_defs) fp_rec_thms ctr_defss;
           in
-            (map2 (map2 (Skip_Proof.prove lthy [] [])) goal_iterss iter_tacss,
-             map2 (map2 (Skip_Proof.prove lthy [] [])) goal_recss rec_tacss)
+            (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
+               goal_iterss iter_tacss,
+             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
+               goal_recss rec_tacss)
           end;
 
         val notes =
@@ -366,7 +373,8 @@
       |> fold_map pour_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~ fp_recs ~~
         fld_unfs ~~ unf_flds ~~ fld_injects ~~ ctr_binderss ~~ ctr_mixfixess ~~ ctr_Tsss ~~
         disc_binderss ~~ sel_bindersss)
-      |> (if gfp then snd else pour_more_sugar_on_datatypes o apfst transpose);
+      |>> split_list7
+      |> (if gfp then snd else pour_more_sugar_on_datatypes);
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       (if gfp then "co" else "") ^ "datatype"));
diff -r 0b735fb2602e -r 674f04c737e0 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -13,6 +13,7 @@
     -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> tactic
+  val mk_iter_or_rec_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
 end;
 
 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
@@ -48,4 +49,11 @@
   Local_Defs.unfold_tac ctxt [ctr_def] THEN rtac (fld_inject RS ssubst) 1 THEN
   Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
+val iter_or_rec_thms =
+  @{thms sum_map.simps sum.simps(5,6) convol_def case_unit map_pair_def split_conv id_def};
+
+fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def bnf_map_def ctxt =
+  Local_Defs.unfold_tac ctxt (ctr_def :: bnf_map_def :: iter_or_rec_defs @ fld_iter_or_recs) THEN
+  Local_Defs.unfold_tac ctxt iter_or_rec_thms THEN rtac refl 1;
+
 end;
diff -r 0b735fb2602e -r 674f04c737e0 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -11,7 +11,8 @@
 sig
   val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
     typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
-    (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
+    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
+      thm list) * local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -2999,8 +3000,9 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms),
-      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
+    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, coiter_thms,
+      corec_thms),
+     lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =
diff -r 0b735fb2602e -r 674f04c737e0 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -8,9 +8,10 @@
 
 signature BNF_LFP =
 sig
-  val bnf_lfp:  mixfix list -> (string * sort) list option -> binding list ->
+  val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
     typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
-    (term list * term list * term list * term list * thm list * thm list * thm list) * local_theory
+    (term list * term list * term list * term list * thm list * thm list * thm list * thm list *
+      thm list) * local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -1822,8 +1823,8 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms),
-      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
+    ((unfs, flds, iters, recs, unf_fld_thms, fld_unf_thms, fld_inject_thms, iter_thms, rec_thms),
+     lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
 val _ =