fixed and enabled generation of "coiters" theorems, including the recursive case

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 13:04:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sun Sep 09 17:14:39 2012 +0200
@@ -447,6 +447,24 @@
         Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
       end;
 
+    fun build_iter_like_call vs basic_Ts fiter_likes maybe_tick =
+      let
+        fun build (T, U) =
+          if T = U then
+            Const (@{const_name id}, T --> T)
+          else
+            (case (find_index (curry (op =) T) basic_Ts, (T, U)) of
+              (~1, (Type (s, Ts), Type (_, Us))) =>
+              let
+                val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
+                val mapx = mk_map Ts Us map0;
+                val TUs =
+                  map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
+                val args = map build TUs;
+              in Term.list_comb (mapx, args) end
+            | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
+      in build end;
+
     fun pour_more_sugar_on_lfps ((ctrss, iters, recs, vs, xsss, ctr_defss, iter_defs, rec_defs),
         lthy) =
       let
@@ -460,32 +478,14 @@
               fold_rev (fold_rev Logic.all) (xs :: fss)
                 (mk_Trueprop_eq (fiter_like $ xctr, Term.list_comb (f, fxs)));
 
-            fun build_call fiter_likes maybe_tick =
-              let
-                fun build (T, U) =
-                  if T = U then
-                    Const (@{const_name id}, T --> T)
-                  else
-                    (case (find_index (curry (op =) T) fpTs, (T, U)) of
-                      (~1, (Type (s, Ts), Type (_, Us))) =>
-                      let
-                        val map0 = map_of_bnf (the (bnf_of lthy (Long_Name.base_name s)));
-                        val mapx = mk_map Ts Us map0;
-                        val TUs =
-                          map dest_funT (fst (split_last (fst (strip_map_type (fastype_of mapx)))));
-                        val args = map build TUs;
-                      in Term.list_comb (mapx, args) end
-                    | (j, _) => maybe_tick (nth vs j) (nth fiter_likes j))
-              in build end;
-
             fun mk_U maybe_prodT =
               typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs);
 
             fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) =
               if member (op =) fpTs T then
-                maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
+                maybe_cons x [build_iter_like_call vs fpTs fiter_likes (K I) (T, mk_U (K I) T) $ x]
               else if exists_subtype (member (op =) fpTs) T then
-                [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
+                [build_iter_like_call vs fpTs fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
               else
                 [x];
 
@@ -526,17 +526,24 @@
 
         val (coiter_thmss, corec_thmss) =
           let
-            fun mk_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
+            fun mk_goal_cond pos = HOLogic.mk_Trueprop o (not pos ? HOLogic.mk_not);
 
             fun mk_goal_coiter_like pfss c cps fcoiter_like n k ctr cfs' =
               fold_rev (fold_rev Logic.all) ([c] :: pfss)
-                (Logic.list_implies (seq_conds mk_cond n k cps,
+                (Logic.list_implies (seq_conds mk_goal_cond n k cps,
                    mk_Trueprop_eq (fcoiter_like $ c, Term.list_comb (ctr, cfs'))));
 
-            fun repair_call fcoiter_likes (cf as Free (_, Type (_, [_, T])) $ _) =
-              (case find_index (curry (op =) T) Cs of ~1 => cf | j => nth fcoiter_likes j $ cf);
+            fun mk_U maybe_sumT =
+              typ_subst (map2 (fn C => fn fpT => (C, maybe_sumT C fpT)) Cs fpTs);
 
-            val cgsss = map (map (map (repair_call gcoiters))) cgsss;
+            fun repair_calls fiter_likes maybe_sumT maybe_tack
+                (cf as Free (_, Type (_, [_, T])) $ _) =
+              if exists_subtype (member (op =) Cs) T then
+                build_iter_like_call vs Cs fiter_likes maybe_tack (T, mk_U maybe_sumT T) $ cf
+              else
+                cf;
+
+            val cgsss = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
 
             val goal_coiterss =
               map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;

--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 13:04:57 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sun Sep 09 17:14:39 2012 +0200
@@ -51,19 +51,19 @@
   Local_Defs.unfold_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
 val iter_like_thms =
-  @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
-      split_conv};
+  @{thms case_unit comp_def convol_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
 
 fun mk_iter_like_tac pre_map_defs map_ids iter_like_defs fld_iter_like ctr_def ctxt =
   Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ pre_map_defs @ map_ids @
-    iter_like_thms) THEN rtac refl 1;
+    iter_like_thms) THEN Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
 
 val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val coiter_like_thms = @{thms map_pair_def sum_map.simps prod.cases};
 
 fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
   Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
   subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
-  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN rtac refl 1;
+  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
+  Local_Defs.unfold_tac ctxt @{thms id_def} THEN rtac refl 1;
 
 end;