completed iter/rec proofs

--- 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
@@ -130,8 +130,8 @@
 
     val eqs = map dest_TFree Xs ~~ sum_prod_TsXs;
 
-    val ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects, fp_iter_thms,
-        fp_rec_thms), lthy) =
+    val (pre_map_defs, ((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 ());
@@ -328,11 +328,10 @@
         val hrecs = map (fn recx => flat_list_comb (recx, hss)) recs;
 
         val (iter_thmss, rec_thmss) =
-          if true then
-            `I (map (map (K TrueI)) ctr_defss)
-          else let
+          let
             fun mk_goal_iter_or_rec fss fc xctr f xs xs' =
-              mk_Trueprop_eq (fc $ xctr, Term.list_comb (f, xs'));
+              fold_rev (fold_rev Logic.all) (xs :: fss)
+                (mk_Trueprop_eq (fc $ xctr, Term.list_comb (f, xs')));
 
             fun fix_iter_free (x as Free (_, T)) =
               (case find_index (eq_fpT T) fpTs of ~1 => x | j => nth giters j $ x);
@@ -348,9 +347,9 @@
               map5 (map4 o mk_goal_iter_or_rec hss) hrecs xctrss hss xsss rec_xsss;
 
             val iter_tacss =
-              map2 (map o mk_iter_or_rec_tac bnf_map_defs iter_defs) fp_iter_thms ctr_defss;
+              map2 (map o mk_iter_or_rec_tac pre_map_defs iter_defs) fp_iter_thms ctr_defss;
             val rec_tacss =
-              map2 (map o mk_iter_or_rec_tac bnf_map_defs rec_defs) fp_rec_thms ctr_defss;
+              map2 (map o mk_iter_or_rec_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss;
           in
             (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_iterss iter_tacss,

--- 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
@@ -52,8 +52,8 @@
 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
+fun mk_iter_or_rec_tac iter_or_rec_defs fld_iter_or_recs ctr_def pre_map_def ctxt =
+  Local_Defs.unfold_tac ctxt (ctr_def :: pre_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;

--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -104,7 +104,7 @@
   val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
     typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     binding list -> mixfix list -> (string * sort) list -> ((string * sort) * typ) list ->
-    local_theory -> 'a
+    local_theory -> thm list * 'a
   val fp_bnf_cmd: (mixfix list -> (string * sort) list option -> binding list ->
     typ list * typ list list -> BNF_Def.BNF list -> local_theory -> 'a) ->
     binding list * (string list * string list) -> local_theory -> 'a
@@ -302,13 +302,15 @@
       fold_map3 (seal_bnf unfold') (map (Binding.suffix_name "BNF") bs) Dss bnfs' lthy'
       |>> split_list;
 
+    val pre_map_defs = map map_def_of_bnf bnfs'';
+
     val timer = time (timer "Normalization & sealing of BNFs");
 
     val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
 
     val timer = time (timer "FP construction in total");
   in
-    res
+    (pre_map_defs, res)
   end;
 
 fun fp_bnf construct bs mixfixes resBs eqs lthy =
@@ -333,7 +335,7 @@
         (bnf_of_typ Smart_Inline (Binding.suffix_name "RAW" b) I sort (Syntax.read_typ lthy rawT)))
       bs raw_bnfs (empty_unfold, lthy));
   in
-    mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy'
+    snd (mk_fp_bnf timer (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold lthy')
   end;
 
 end;