# HG changeset patch
# User blanchet
# Date 1347137677 -7200
# Node ID 510c6d4a73ec3d4cacaf11b0a27d2150dbc9866d
# Parent  a9295b1f401b797cc39832b6a7e52c06c40b3bc1
fixed and enabled iterator/recursor theorems

diff -r a9295b1f401b -r 510c6d4a73ec src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:52:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 22:54:37 2012 +0200
@@ -145,10 +145,23 @@
 
     val eqs = map dest_TFree Xs ~~ sum_prod_TsXs;
 
-    val (pre_map_defs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
+    val (pre_bnfs, ((unfs0, flds0, fp_iters0, fp_recs0, unf_flds, fld_unfs, fld_injects,
         fp_iter_thms, fp_rec_thms), lthy)) =
       fp_bnf (if lfp then bnf_lfp else bnf_gfp) bs mixfixes As' eqs no_defs_lthy;
 
+    val add_nested_bnf_names =
+      let
+        fun add (Type (s, Ts)) ss =
+            let val (needs, ss') = fold_map add Ts ss in
+              if exists I needs then (true, insert (op =) s ss') else (false, ss')
+            end
+          | add T ss = (member (op =) As T, ss);
+      in snd oo add end;
+
+    val nested_bnfs =
+      map_filter (bnf_of lthy o Long_Name.base_name)
+        (fold (fold (fold add_nested_bnf_names)) ctr_TsssXs []);
+
     val timer = time (Timer.startRealTimer ());
 
     fun mk_unf_or_fld get_T Ts t =
@@ -426,6 +439,9 @@
         |> (if lfp then some_lfp_sugar else some_gfp_sugar)
       end;
 
+    val pre_map_defs = map map_def_of_bnf pre_bnfs;
+    val map_id's = map map_id'_of_bnf nested_bnfs;
+
     fun mk_map Ts Us t =
       let val (Type (_, Ts0), Type (_, Us0)) = strip_map_type (fastype_of t) |>> List.last in
         Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
@@ -484,28 +500,23 @@
             val goal_recss = map5 (map4 o mk_goal_iter_like hss) hrecs xctrss hss xsss hxsss;
 
             val iter_tacss =
-              map2 (map o mk_iter_like_tac pre_map_defs iter_defs) fp_iter_thms ctr_defss;
+              map2 (map o mk_iter_like_tac pre_map_defs map_id's iter_defs) fp_iter_thms ctr_defss;
             val rec_tacss =
-              map2 (map o mk_iter_like_tac pre_map_defs rec_defs) fp_rec_thms ctr_defss;
+              map2 (map o mk_iter_like_tac pre_map_defs map_id's rec_defs) fp_rec_thms ctr_defss;
           in
-            ([], [])
-(* NOTYET
             (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 = [];
-(* NOTYET
+        val notes =
           [(itersN, iter_thmss),
            (recsN, rec_thmss)]
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
                 ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
               bs thmss);
-*)
       in
         lthy |> Local_Theory.notes notes |> snd
       end;
@@ -538,7 +549,8 @@
               map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
 
             val coiter_tacss =
-              map3 (map oo mk_coiter_like_tac coiter_defs) fp_iter_thms pre_map_defs ctr_defss;
+              map3 (map oo mk_coiter_like_tac coiter_defs map_id's) fp_iter_thms pre_map_defs
+                ctr_defss;
           in
             (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
                goal_coiterss coiter_tacss,
diff -r a9295b1f401b -r 510c6d4a73ec src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:52:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 22:54:37 2012 +0200
@@ -8,13 +8,13 @@
 signature BNF_FP_SUGAR_TACTICS =
 sig
   val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
-  val mk_coiter_like_tac: thm list -> thm -> thm -> thm -> Proof.context -> tactic
+  val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> tactic
-  val mk_iter_like_tac: thm list -> thm list -> thm -> thm -> Proof.context -> tactic
+  val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
 end;
 
 structure BNF_FP_Sugar_Tactics : BNF_FP_SUGAR_TACTICS =
@@ -51,20 +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_def map_pair_def sum.simps(5,6) sum_map.simps split_conv};
+  @{thms case_unit comp_def convol_def id_apply map_pair_def sum.simps(5,6) sum_map.simps
+      split_conv};
 
-fun mk_iter_like_tac map_defs iter_like_defs fld_iter_like ctr_def ctxt =
-  Local_Defs.unfold_tac ctxt (ctr_def :: fld_iter_like :: iter_like_defs @ map_defs) THEN
-  Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
+fun mk_iter_like_tac pre_map_defs map_id's 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_id's @
+    iter_like_thms) THEN rtac refl 1;
 
 val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_thms = @{thms id_def map_pair_def sum_map.simps prod.cases};
+val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
 
-fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
+fun mk_coiter_like_tac coiter_like_defs map_id's 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) THEN
-  rtac refl 1;
+  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_id's) THEN rtac refl 1;
 
 end;
diff -r a9295b1f401b -r 510c6d4a73ec src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 21:52:17 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Sat Sep 08 22:54:37 2012 +0200
@@ -108,7 +108,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 -> thm list * 'a
+    local_theory -> BNF_Def.BNF 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
@@ -313,15 +313,13 @@
       fold_map3 (seal_bnf unfold') (map (Binding.prefix_name preN) 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
-    (pre_map_defs, res)
+    (bnfs'', res)
   end;
 
 fun fp_bnf construct bs mixfixes resBs eqs lthy =