# HG changeset patch
# User blanchet
# Date 1348101768 -7200
# Node ID fa8302c8dea1d333d594f26863bcc630f633d6cc
# Parent  3cd2622d44664e8ad0a05d76f2f1b9f611bcb0a4
adapted BNF composition to new relator approach

diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Examples/Misc_Data.thy
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Thu Sep 20 02:42:48 2012 +0200
@@ -9,11 +9,28 @@
 header {* Miscellaneous Datatype Declarations *}
 
 theory Misc_Data
-imports "../Codatatype"
+imports (* "../Codatatype" *) "../BNF_LFP"
 begin
 
+declare [[bnf_note_all = false]]
+
+local_setup {* fn lthy =>
+snd (snd (BNF_Comp.bnf_of_typ BNF_Def.Dont_Inline (Binding.qualify true "xxx")
+  BNF_Comp.default_comp_sort
+  @{typ "('a \<Rightarrow> 'a) + ('a + 'b) + 'c"} (BNF_Comp.empty_unfold, lthy)))
+*}
+
+data 'a lst = Nl | Cns 'a "'a lst"
+
+thm pre_lst.rel_unfold
+    pre_lst.pred_unfold
+    lst.rel_unfold
+    lst.pred_unfold
+
 data simple = X1 | X2 | X3 | X4
 
+thm simple.rel_unfold
+
 data simple' = X1' unit | X2' unit | X3' unit | X4' unit
 
 data 'a mylist = MyNil | MyCons 'a "'a mylist"
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -13,7 +13,6 @@
   val map_unfolds_of: unfold_thms -> thm list
   val set_unfoldss_of: unfold_thms -> thm list list
   val rel_unfolds_of: unfold_thms -> thm list
-  val pred_unfolds_of: unfold_thms -> thm list
 
   val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
@@ -37,34 +36,29 @@
 type unfold_thms = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
-  rel_unfolds: thm list,
-  pred_unfolds: thm list
+  rel_unfolds: thm list
 };
 
 fun add_to_thms thms NONE = thms
   | add_to_thms thms (SOME new) = if Thm.is_reflexive new then thms else insert Thm.eq_thm new thms;
 fun adds_to_thms thms NONE = thms
-  | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_refl news) thms;
+  | adds_to_thms thms (SOME news) = insert (eq_set Thm.eq_thm) (filter_out_refl news) thms;
 
-fun mk_unfold_thms maps setss rels preds =
-  {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds};
+fun mk_unfold_thms maps setss rels = {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels};
 
-val empty_unfold = mk_unfold_thms [] [] [] [];
+val empty_unfold = mk_unfold_thms [] [] [];
 
-fun add_to_unfold_opt map_opt sets_opt rel_opt pred_opt
-  {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels, pred_unfolds = preds} = {
+fun add_to_unfold_opt map_opt sets_opt rel_opt
+  {map_unfolds = maps, set_unfoldss = setss, rel_unfolds = rels} = {
     map_unfolds = add_to_thms maps map_opt,
     set_unfoldss = adds_to_thms setss sets_opt,
-    rel_unfolds = add_to_thms rels rel_opt,
-    pred_unfolds = add_to_thms preds pred_opt};
+    rel_unfolds = add_to_thms rels rel_opt};
 
-fun add_to_unfold map sets rel pred =
-  add_to_unfold_opt (SOME map) (SOME sets) (SOME rel) (SOME pred);
+fun add_to_unfold map sets rel = add_to_unfold_opt (SOME map) (SOME sets) (SOME rel);
 
 val map_unfolds_of = #map_unfolds;
 val set_unfoldss_of = #set_unfoldss;
 val rel_unfolds_of = #rel_unfolds;
-val pred_unfolds_of = #pred_unfolds;
 
 val bdTN = "bdT";
 
@@ -73,10 +67,7 @@
 fun mk_permuteN src dest =
   "_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
 
-val no_thm = refl;
-val Collect_split_box_equals = box_equals RS @{thm Collect_split_cong};
-val abs_pred_sym = sym RS @{thm abs_pred_def};
-val abs_pred_sym_pred_abs = abs_pred_sym RS @{thm pred_def_abs};
+val subst_rel_def = @{thm subst_rel_def};
 
 (*copied from Envir.expand_term_free*)
 fun expand_term_const defs =
@@ -111,9 +102,10 @@
       (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
     val Bss_repl = replicate olive Bs;
 
-    val (((fs', Asets), xs), _(*names_lthy*)) = lthy
+    val ((((fs', Rs'), Asets), xs), _(*names_lthy*)) = lthy
       |> apfst snd o mk_Frees' "f" (map2 (curry (op -->)) As Bs)
-      ||>> mk_Frees "A" (map (HOLogic.mk_setT) As)
+      ||>> apfst snd o mk_Frees' "R" (map2 (curry mk_relT) As Bs)
+      ||>> mk_Frees "A" (map HOLogic.mk_setT As)
       ||>> mk_Frees "x" As;
 
     val CAs = map3 mk_T_of_bnf Dss Ass_repl inners;
@@ -129,6 +121,11 @@
       (Term.list_comb (mk_map_of_bnf oDs CAs CBs outer,
         map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
           mk_map_of_bnf Ds As Bs) Dss inners));
+    (*%R1 ... Rn. outer.rel (inner_1.rel R1 ... Rn) ... (inner_m.rel R1 ... Rn)*)
+    val rel = fold_rev Term.abs Rs'
+      (Term.list_comb (mk_rel_of_bnf oDs CAs CBs outer,
+        map2 (fn Ds => (fn f => Term.list_comb (f, map Bound ((ilive - 1) downto 0))) o
+          mk_rel_of_bnf Ds As Bs) Dss inners));
 
     (*Union o collect {outer.set_1 ... outer.set_m} o outer.map inner_1.set_i ... inner_m.set_i*)
     (*Union o collect {image inner_1.set_i o outer.set_1 ... image inner_m.set_i o outer.set_m}*)
@@ -185,7 +182,7 @@
 
     val set_alt_thms =
       if ! quick_and_dirty then
-        replicate ilive no_thm
+        []
       else
         map (fn goal =>
           Skip_Proof.prove lthy [] [] goal
@@ -233,8 +230,21 @@
     fun map_wpull_tac _ =
       mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
 
-    val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
-      bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
+    fun rel_O_Gr_tac _ =
+      let
+        val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
+        val outer_rel_cong = rel_cong_of_bnf outer;
+      in
+        rtac (trans OF [in_alt_thm RS subst_rel_def,
+                trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
+                  [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
+                    rel_converse_of_bnf outer RS sym], outer_rel_Gr],
+                  trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
+                    (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]] RS sym) 1
+      end
+
+    val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
 
     val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
 
@@ -259,25 +269,8 @@
       bnf_def const_policy (K Derive_Some_Facts) qualify tacs wit_tac (SOME (oDs @ flat Dss))
         (((((b, mapx), sets), bd), wits), rel) lthy;
 
-    val outer_rel_Gr = rel_Gr_of_bnf outer RS sym;
-    val outer_rel_cong = rel_cong_of_bnf outer;
-
-    val rel_unfold_thm =
-      trans OF [rel_O_Gr_of_bnf bnf',
-        trans OF [in_alt_thm RS @{thm subst_rel_def},
-          trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-            [trans OF [outer_rel_Gr RS @{thm arg_cong[of _ _ converse]},
-              rel_converse_of_bnf outer RS sym], outer_rel_Gr],
-            trans OF [rel_O_of_bnf outer RS sym, outer_rel_cong OF
-              (map (fn bnf => rel_O_Gr_of_bnf bnf RS sym) inners)]]]];
-
-    val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
-      pred_def_of_bnf bnf' RS abs_pred_sym,
-        trans OF [outer_rel_cong OF (map (fn bnf => pred_def_of_bnf bnf RS abs_pred_sym) inners),
-          pred_def_of_bnf outer RS abs_pred_sym]];
-
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
-      pred_unfold_thm unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+      unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -301,7 +294,7 @@
       (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
 
     val ((Asets, lives), _(*names_lthy*)) = lthy
-      |> mk_Frees "A" (map (HOLogic.mk_setT) (drop n As))
+      |> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
       ||>> mk_Frees "x" (drop n As);
     val xs = map (fn T => HOLogic.choice_const T $ absdummy T @{term True}) killedAs @ lives;
 
@@ -309,6 +302,8 @@
 
     (*bnf.map id ... id*)
     val mapx = Term.list_comb (mk_map_of_bnf Ds As Bs bnf, map HOLogic.id_const killedAs);
+    (*bnf.rel Id ... Id*)
+    val rel = Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, map Id_const killedAs);
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = drop n bnf_sets;
@@ -345,8 +340,21 @@
         (bd_Cinfinite_of_bnf bnf) (bd_Cnotzero_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
-      bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
+    fun rel_O_Gr_tac _ =
+      let
+        val rel_Gr = rel_Gr_of_bnf bnf RS sym
+      in
+        rtac (trans OF [in_alt_thm RS subst_rel_def,
+                trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
+                  [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]},
+                    rel_converse_of_bnf bnf RS sym], rel_Gr],
+                  trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
+                    (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
+                     replicate (live - n) @{thm Gr_fst_snd})]]] RS sym) 1
+      end;
+
+    val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
 
     val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
 
@@ -357,26 +365,10 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME (killedAs @ Ds))
-        ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
-
-    val rel_Gr = rel_Gr_of_bnf bnf RS sym;
+        (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
 
-    val rel_unfold_thm =
-      trans OF [rel_O_Gr_of_bnf bnf',
-        trans OF [in_alt_thm RS @{thm subst_rel_def},
-          trans OF [@{thm arg_cong2[of _ _ _ _ relcomp]} OF
-            [trans OF [rel_Gr RS @{thm arg_cong[of _ _ converse]}, rel_converse_of_bnf bnf RS sym],
-              rel_Gr],
-            trans OF [rel_O_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
-              (replicate n @{thm trans[OF Gr_UNIV_id[OF refl] Id_alt[symmetric]]} @
-               replicate (live - n) @{thm Gr_fst_snd})]]]];
-
-    val pred_unfold_thm = Collect_split_box_equals OF
-      [Local_Defs.unfold lthy' @{thms Id_def'} rel_unfold_thm, pred_def_of_bnf bnf' RS abs_pred_sym,
-        pred_def_of_bnf bnf RS abs_pred_sym];
-
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
-      pred_unfold_thm unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+      unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -400,13 +392,16 @@
       (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
 
     val (Asets, _(*names_lthy*)) = lthy
-      |> mk_Frees "A" (map (HOLogic.mk_setT) (newAs @ As));
+      |> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
 
     val T = mk_T_of_bnf Ds As bnf;
 
     (*%f1 ... fn. bnf.map*)
     val mapx =
       fold_rev Term.absdummy (map2 (curry (op -->)) newAs newBs) (mk_map_of_bnf Ds As Bs bnf);
+    (*%R1 ... Rn. bnf.rel*)
+    val rel =
+      fold_rev Term.absdummy (map2 (curry mk_relT) newAs newBs) (mk_rel_of_bnf Ds As Bs bnf);
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = map (fn A => absdummy T (HOLogic.mk_set A [])) newAs @ bnf_sets;
@@ -446,8 +441,11 @@
     fun in_bd_tac _ = mk_lift_in_bd_tac n in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
-      bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
+    fun rel_O_Gr_tac _ =
+      rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+
+    val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
@@ -455,17 +453,10 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
-        ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
-
-    val rel_unfold_thm =
-      trans OF [rel_O_Gr_of_bnf bnf',
-        trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_O_Gr_of_bnf bnf RS sym]];
+        (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
 
-    val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
-      pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
-
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
-      pred_unfold_thm unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+      unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -489,14 +480,16 @@
       (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
 
     val (Asets, _(*names_lthy*)) = lthy
-      |> mk_Frees "A" (map (HOLogic.mk_setT) (permute As));
+      |> mk_Frees "A" (map HOLogic.mk_setT (permute As));
 
     val T = mk_T_of_bnf Ds As bnf;
 
     (*%f(1) ... f(n). bnf.map f\<sigma>(1) ... f\<sigma>(n)*)
     val mapx = fold_rev Term.absdummy (permute (map2 (curry op -->) As Bs))
-      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf,
-        permute_rev (map Bound ((live - 1) downto 0))));
+      (Term.list_comb (mk_map_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
+    (*%R(1) ... R(n). bnf.rel R\<sigma>(1) ... R\<sigma>(n)*)
+    val rel = fold_rev Term.absdummy (permute (map2 (curry mk_relT) As Bs))
+      (Term.list_comb (mk_rel_of_bnf Ds As Bs bnf, permute_rev (map Bound ((live - 1) downto 0))));
 
     val bnf_sets = mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf;
     val sets = permute bnf_sets;
@@ -526,8 +519,11 @@
       mk_permute_in_bd_tac src dest in_alt_thm (in_bd_of_bnf bnf) (bd_Card_order_of_bnf bnf);
     fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
 
-    val tacs = [map_id_tac, map_comp_tac, map_cong_tac] @ set_natural_tacs @ [bd_card_order_tac,
-      bd_cinfinite_tac] @ set_bd_tacs @ [in_bd_tac, map_wpull_tac];
+    fun rel_O_Gr_tac _ =
+      rtac (trans OF [rel_O_Gr_of_bnf bnf, in_alt_thm RS subst_rel_def RS sym]) 1;
+
+    val tacs = zip_goals map_id_tac map_comp_tac map_cong_tac set_natural_tacs bd_card_order_tac
+      bd_cinfinite_tac set_bd_tacs in_bd_tac map_wpull_tac rel_O_Gr_tac;
 
     val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
@@ -535,17 +531,10 @@
 
     val (bnf', lthy') =
       bnf_def Smart_Inline (K Derive_Some_Facts) qualify tacs wit_tac (SOME Ds)
-        ((((b, mapx), sets), Term.absdummy T bd), wits) lthy;
-
-    val rel_unfold_thm =
-      trans OF [rel_O_Gr_of_bnf bnf',
-        trans OF [in_alt_thm RS @{thm subst_rel_def}, rel_O_Gr_of_bnf bnf RS sym]];
+        (((((b, mapx), sets), Term.absdummy T bd), wits), rel) lthy;
 
-    val pred_unfold_thm = Collect_split_box_equals OF [rel_unfold_thm,
-      pred_def_of_bnf bnf' RS abs_pred_sym, pred_def_of_bnf bnf RS abs_pred_sym];
-
-    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') rel_unfold_thm
-      pred_unfold_thm unfold;
+    val unfold' = add_to_unfold (map_def_of_bnf bnf') (set_defs_of_bnf bnf') (rel_def_of_bnf bnf')
+      unfold;
   in
     (bnf', (unfold', lthy'))
   end;
@@ -619,13 +608,16 @@
     val (Bs, _) = apfst (map TFree)
       (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
 
-    val map_unfolds = filter_refl (map_unfolds_of unfold);
-    val set_unfoldss = map filter_refl (set_unfoldss_of unfold);
+    val map_unfolds = filter_out_refl (map_unfolds_of unfold);
+    val set_unfoldss = map filter_out_refl (set_unfoldss_of unfold);
+    val rel_unfolds = filter_out_refl (rel_unfolds_of unfold);
 
     val expand_maps = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
       map_unfolds);
     val expand_sets = fold expand_term_const (map (map (Logic.dest_equals o Thm.prop_of))
       set_unfoldss);
+    val expand_rels = fold expand_term_const (map (single o Logic.dest_equals o Thm.prop_of)
+      rel_unfolds);
     val unfold_maps = fold (Local_Defs.unfold lthy o single) map_unfolds;
     val unfold_sets = fold (Local_Defs.unfold lthy) set_unfoldss;
     val unfold_defs = unfold_sets o unfold_maps;
@@ -633,6 +625,7 @@
     val bnf_sets = map (expand_maps o expand_sets)
       (mk_sets_of_bnf (replicate live Ds) (replicate live As) bnf);
     val bnf_bd = mk_bd_of_bnf Ds As bnf;
+    val bnf_rel = expand_rels (mk_rel_of_bnf Ds As Bs bnf);
     val T = mk_T_of_bnf Ds As bnf;
 
     (*bd should only depend on dead type variables!*)
@@ -667,11 +660,11 @@
 
     fun mk_tac thm {context = ctxt, prems = _} = (rtac (unfold_defs thm) THEN'
       SOLVE o REPEAT_DETERM o (atac ORELSE' Goal.assume_rule_tac ctxt)) 1;
-    val tacs =
-      map mk_tac ([map_id_of_bnf bnf, map_comp_of_bnf bnf, map_cong_of_bnf bnf] @
-        set_natural_of_bnf bnf) @
-      map K [rtac bd_card_order 1, rtac bd_cinfinite 1] @
-      map mk_tac (set_bds @ [in_bd, map_wpull_of_bnf bnf]);
+
+    val tacs = zip_goals (mk_tac (map_id_of_bnf bnf)) (mk_tac (map_comp_of_bnf bnf))
+      (mk_tac (map_cong_of_bnf bnf)) (map mk_tac (set_natural_of_bnf bnf))
+      (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
+      (mk_tac (map_wpull_of_bnf bnf)) (mk_tac (rel_O_Gr_of_bnf bnf));
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
 
@@ -680,40 +673,15 @@
     val policy = user_policy Derive_All_Facts;
 
     val (bnf', lthy') = bnf_def Hardly_Inline policy I tacs wit_tac (SOME deads)
-      ((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits) lthy;
-
-    val defs' = filter_refl (map_def_of_bnf bnf' :: set_defs_of_bnf bnf');
-    val unfold_defs' = unfold_defs o Local_Defs.unfold lthy' defs';
-
-    val rel_O_Gr = unfold_defs' (rel_O_Gr_of_bnf bnf');
-    val rel_unfold = Local_Defs.unfold lthy'
-      (map unfold_defs (filter_refl (rel_unfolds_of unfold))) rel_O_Gr;
-
-    val unfold_defs'' = unfold_defs' o Local_Defs.unfold lthy' (filter_refl [rel_O_Gr_of_bnf bnf']);
-
-    val pred_def = unfold_defs'' (pred_def_of_bnf bnf' RS abs_pred_sym_pred_abs);
-    val pred_unfold = Local_Defs.unfold lthy'
-      (map unfold_defs (filter_refl (pred_unfolds_of unfold))) pred_def;
-
-    val notes =
-      [(rel_unfoldN, [rel_unfold]),
-      (pred_unfoldN, [pred_unfold])]
-      |> map (fn (thmN, thms) =>
-        ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+      (((((b, bnf_map), bnf_sets), Term.absdummy T bnf_bd'), bnf_wits), bnf_rel) lthy;
   in
-    ((bnf', deads), lthy' |> Local_Theory.notes notes |> snd)
+    ((bnf', deads), lthy')
   end;
 
 val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
 val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
 
-val ID_rel_O_Gr = rel_O_Gr_of_bnf ID_bnf;
-val ID_rel_O_Gr' = ID_rel_O_Gr RS sym;
-val ID_pred_def' = Local_Defs.unfold @{context} [ID_rel_O_Gr] (pred_def_of_bnf ID_bnf) RS sym;
-
-fun bnf_of_typ _ _ _ (T as TFree _) (unfold, lthy) =
-    ((ID_bnf, ([], [T])),
-      (add_to_unfold_opt NONE NONE (SOME ID_rel_O_Gr') (SOME ID_pred_def') unfold, lthy))
+fun bnf_of_typ _ _ _ (T as TFree _) accum = ((ID_bnf, ([], [T])), accum)
   | bnf_of_typ _ _ _ (TVar _) _ = error "Unexpected schematic variable"
   | bnf_of_typ const_policy qualify' sort (T as Type (C, Ts)) (unfold, lthy) =
     let
@@ -732,10 +700,7 @@
             val deads_lives =
               pairself (map (Term.typ_subst_TVars (map fst tvars' ~~ map TFree tfrees)))
                 (deads, lives);
-            val rel_O_Gr = rel_O_Gr_of_bnf bnf;
-            val unfold' = add_to_unfold_opt NONE NONE (SOME (rel_O_Gr RS sym))
-              (SOME (Local_Defs.unfold lthy [rel_O_Gr] (pred_def_of_bnf bnf) RS sym)) unfold;
-          in ((bnf, deads_lives), (unfold', lthy)) end
+          in ((bnf, deads_lives), (unfold, lthy)) end
         else
           let
             val name = Long_Name.base_name C;
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -27,8 +27,6 @@
   val relN: string
   val predN: string
   val mk_setN: int -> string
-  val rel_unfoldN: string
-  val pred_unfoldN: string
 
   val map_of_bnf: BNF -> term
 
@@ -79,6 +77,9 @@
   val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
   val wits_of_bnf: BNF -> nonemptiness_witness list
 
+  val filter_out_refl: thm list -> thm list
+  val zip_goals: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
+
   datatype const_policy = Dont_Inline | Hardly_Inline | Smart_Inline | Do_Inline
   datatype fact_policy =
     Derive_Some_Facts | Derive_All_Facts | Derive_All_Facts_Note_Most | Note_All_Facts_and_Axioms
@@ -91,10 +92,6 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> typ list option ->
     ((((binding * term) * term list) * term) * term list) * term -> local_theory ->
     BNF * local_theory
-
-  val filter_refl: thm list -> thm list
-  val bnf_def_cmd: ((((binding * string) * string list) * string) * string list) * string ->
-    local_theory -> Proof.state
 end;
 
 structure BNF_Def : BNF_DEF =
@@ -478,8 +475,6 @@
 fun mk_witN i = witN ^ nonzero_string_of_int i;
 val relN = "rel";
 val predN = "pred";
-val rel_unfoldN = relN ^ "_unfold";
-val pred_unfoldN = predN ^ "_unfold";
 
 val bd_card_orderN = "bd_card_order";
 val bd_cinfiniteN = "bd_cinfinite";
@@ -529,8 +524,10 @@
       handle TERM _ => false
   end;
 
-val filter_refl = filter_out is_reflexive;
+val filter_out_refl = filter_out is_reflexive;
 
+fun zip_goals mid mcomp mcong snat bdco bdinf sbd inbd wpull rel =
+  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull, rel];
 
 
 (* Define new BNFs *)
@@ -577,10 +574,9 @@
       in map2 pair bs wit_rhss end;
     val rel_bind_def = (fn () => Binding.suffix_name ("_" ^ relN) b, rel_rhs);
 
-    fun maybe_define needed_for_extra_facts (b, rhs) lthy =
+    fun maybe_define (b, rhs) lthy =
       let
         val inline =
-          (not needed_for_extra_facts orelse fact_policy = Derive_Some_Facts) andalso
           (case const_policy of
             Dont_Inline => false
           | Hardly_Inline => Term.is_Free rhs orelse Term.is_Const rhs
@@ -601,17 +597,16 @@
       (bnf_set_terms, raw_set_defs)),
       (bnf_bd_term, raw_bd_def)),
       (bnf_wit_terms, raw_wit_defs)),
-      (bnf_rel_term, raw_rel_def)), (lthy', lthy)) =
+      (bnf_rel_term, raw_rel_def)), (lthy1, lthy0)) =
         no_defs_lthy
-        |> maybe_define false map_bind_def
-        ||>> apfst split_list o fold_map (maybe_define false) set_binds_defs
-        ||>> maybe_define false bd_bind_def
-        ||>> apfst split_list o fold_map (maybe_define false) wit_binds_defs
-        ||>> maybe_define false rel_bind_def
+        |> maybe_define map_bind_def
+        ||>> apfst split_list o fold_map maybe_define set_binds_defs
+        ||>> maybe_define bd_bind_def
+        ||>> apfst split_list o fold_map maybe_define wit_binds_defs
+        ||>> maybe_define rel_bind_def
         ||> `(maybe_restore no_defs_lthy);
 
-    (*transforms defined frees into consts (and more)*)
-    val phi = Proof_Context.export_morphism lthy lthy';
+    val phi = Proof_Context.export_morphism lthy0 lthy1;
 
     val bnf_map_def = Morphism.thm phi raw_map_def;
     val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
@@ -620,12 +615,7 @@
     val bnf_rel_def = Morphism.thm phi raw_rel_def;
 
     val one_step_defs =
-      filter_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
-
-    val _ = case map_filter (try dest_Free)
-        (bnf_map_term :: bnf_set_terms @ [bnf_bd_term] @ bnf_wit_terms) of
-        [] => ()
-      | frees => Proof_Display.print_consts true lthy (K false) frees;
+      filter_out_refl (bnf_map_def :: bnf_bd_def :: bnf_set_defs @ bnf_wit_defs @ [bnf_rel_def]);
 
     val bnf_map = Morphism.term phi bnf_map_term;
 
@@ -659,7 +649,7 @@
     (*TODO: check type of bnf_rel*)
 
     val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''),
-      (Ts, T)) = lthy'
+      (Ts, T)) = lthy1
       |> mk_TFrees live
       ||>> mk_TFrees live
       ||>> mk_TFrees live
@@ -679,7 +669,7 @@
     fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
     fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
 
-    fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy setRTs CA' CB' bnf_rel;
+    fun mk_bnf_rel setRTs CA' CB' = normalize_rel lthy1 setRTs CA' CB' bnf_rel;
 
     val (setRTs, RTs) = map_split (`HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Bs');
     val setRTsAsCs = map (HOLogic.mk_setT o HOLogic.mk_prodT) (As' ~~ Cs);
@@ -705,7 +695,7 @@
 
     val ((((((((((((((((((((((((fs, fs_copy), gs), hs), (x, x')), (y, y')), (z, z')), zs), As),
       As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), Rs), Rs_copy), Ss),
-      (Qs, Qs')), _) = lthy'
+      (Qs, Qs')), _) = lthy1
       |> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
       ||>> mk_Frees "f" (map2 (curry (op -->)) As' Bs')
       ||>> mk_Frees "g" (map2 (curry (op -->)) Bs' Cs)
@@ -737,23 +727,31 @@
         Qs As' Bs')));
     val pred_bind_def = (fn () => Binding.suffix_name ("_" ^ predN) b, pred_rhs);
 
-    val ((bnf_pred_term, raw_pred_def), (lthy''', lthy'')) =
-      lthy
-      |> maybe_define true pred_bind_def
-      ||> `(maybe_restore lthy');
+    val ((bnf_pred_term, raw_pred_def), (lthy3, lthy2)) =
+      lthy1
+      |> maybe_define pred_bind_def
+      ||> `(maybe_restore lthy1);
 
-    val phi = Proof_Context.export_morphism lthy'' lthy''';
-    val bnf_pred = Morphism.term phi bnf_pred_term;
+    val _ = case filter_out_refl (raw_map_def :: raw_set_defs @ [raw_bd_def] @
+        raw_wit_defs @ [raw_rel_def, raw_pred_def]) of
+        [] => ()
+      | defs => Proof_Display.print_consts true lthy2 (K false)
+          (map (dest_Free o fst o Logic.dest_equals o prop_of) defs);
 
-    fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy''' QTs CA' CB' bnf_pred;
+    val phi = Proof_Context.export_morphism lthy2 lthy3;
 
-    val pred = mk_bnf_pred QTs CA' CB';
     val bnf_pred_def =
       if fact_policy <> Derive_Some_Facts then
         mk_unabs_def (live + 2) (Morphism.thm phi raw_pred_def RS meta_eq_to_obj_eq)
       else
         no_fact;
 
+    val bnf_pred = Morphism.term phi bnf_pred_term;
+
+    fun mk_bnf_pred QTs CA' CB' = normalize_pred lthy3 QTs CA' CB' bnf_pred;
+
+    val pred = mk_bnf_pred QTs CA' CB';
+
     val goal_map_id =
       let
         val bnf_map_app_id = Term.list_comb (bnf_map_AsAs, map HOLogic.id_const As');
@@ -857,10 +855,8 @@
         fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (relAsBs, Rs), rhs))
       end;
 
-    val goals =
-      [goal_map_id, goal_map_comp, goal_map_cong] @ goal_set_naturals @
-      [goal_card_order_bd, goal_cinfinite_bd] @ goal_set_bds @
-      [goal_in_bd, goal_map_wpull, goal_rel_O_Gr];
+    val goals = zip_goals goal_map_id goal_map_comp goal_map_cong goal_set_naturals
+      goal_card_order_bd goal_cinfinite_bd goal_set_bds goal_in_bd goal_map_wpull goal_rel_O_Gr;
 
     fun mk_wit_goals (I, wit) =
       let
@@ -1162,24 +1158,30 @@
                 I))
       end;
   in
-    (key, goals, wit_goalss, after_qed, lthy''', one_step_defs)
+    (key, goals, wit_goalss, after_qed, lthy3, one_step_defs)
   end;
 
 fun register_bnf key (bnf, lthy) =
   (bnf, Local_Theory.declaration {syntax = false, pervasive = true}
     (fn phi => Data.map (Symtab.update_new (key, morph_bnf phi bnf))) lthy);
 
+(* TODO: Once the invariant "nwits > 0" holds, remove "mk_conjunction_balanced'" and "rtac TrueI"
+   below *)
+fun mk_conjunction_balanced' [] = @{prop True}
+  | mk_conjunction_balanced' ts = Logic.mk_conjunction_balanced ts;
+
 fun bnf_def const_policy fact_policy qualify tacs wit_tac Ds =
   (fn (_, goals, wit_goalss, after_qed, lthy, defs) =>
   let
-    val wits_tac = K (TRYALL Goal.conjunction_tac) THEN' unfold_defs_tac lthy defs wit_tac;
-    val wit_goals = wit_goalss |> map Logic.mk_conjunction_balanced;
-    val wit_goal = Logic.mk_conjunction_balanced wit_goals;
+    val wits_tac =
+      K (TRYALL Goal.conjunction_tac) THEN' K (TRYALL (rtac TrueI)) THEN'
+      unfold_defs_tac lthy defs wit_tac;
+    val wit_goals = map mk_conjunction_balanced' wit_goalss;
     val wit_thms =
-      Skip_Proof.prove lthy [] [] wit_goal wits_tac
+      Skip_Proof.prove lthy [] [] (mk_conjunction_balanced' wit_goals) wits_tac
       |> Conjunction.elim_balanced (length wit_goals)
       |> map2 (Conjunction.elim_balanced o length) wit_goalss
-      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0))
+      |> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
   in
     map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
       goals (map (unfold_defs_tac lthy defs) tacs)
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_fp_util.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -53,10 +53,12 @@
   val nchotomyN: string
   val pred_coinductN: string
   val pred_coinduct_uptoN: string
+  val pred_simpN: string
   val recN: string
   val recsN: string
   val rel_coinductN: string
   val rel_coinduct_uptoN: string
+  val rel_simpN: string
   val rvN: string
   val sel_coitersN: string
   val sel_corecsN: string
@@ -129,8 +131,6 @@
   val mk_sum_casesN: int -> int -> thm
   val mk_sum_casesN_balanced: int -> int -> thm
 
-  val mk_tactics: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list
-
   val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
 
   val fp_bnf: (mixfix list -> (string * sort) list option -> binding list ->
@@ -223,6 +223,9 @@
 val unf_coinductN = unfN ^ "_" ^ coinductN
 val rel_coinductN = relN ^ "_" ^ coinductN
 val pred_coinductN = predN ^ "_" ^ coinductN
+val simpN = "_simp";
+val rel_simpN = relN ^ simpN;
+val pred_simpN = predN ^ simpN;
 val uptoN = "upto"
 val unf_coinduct_uptoN = unf_coinductN ^ "_" ^ uptoN
 val rel_coinduct_uptoN = rel_coinductN ^ "_" ^ uptoN
@@ -364,9 +367,6 @@
     Balanced_Tree.access {left = mk_sum_step @{thm sum.cases(1)} @{thm sum_case_step(1)},
       right = mk_sum_step @{thm sum.cases(2)} @{thm sum_case_step(2)}, init = refl} n k;
 
-fun mk_tactics mid mcomp mcong snat bdco bdinf sbd inbd wpull =
-  [mid, mcomp, mcong] @ snat @ [bdco, bdinf] @ sbd @ [inbd, wpull];
-
 (* FIXME: because of "@ lhss", the output could contain type variables that are not in the input;
    also, "fp_sort" should put the "resBs" first and in the order in which they appear *)
 fun fp_sort lhss NONE Ass = Library.sort (Term_Ord.typ_ord o pairself TFree)
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -2669,8 +2669,13 @@
           map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
             mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
 
-        val tacss = map9 mk_tactics map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss bd_co_tacs
-          bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs;
+        (* ### *)
+        fun rel_O_Gr_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
+
+        val rel_O_gr_tacs = replicate n rel_O_Gr_tac;
+
+        val tacss = map10 zip_goals map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs;
 
         val (hset_unf_incl_thmss, hset_hset_unf_incl_thmsss, hset_induct_thms) =
           let
@@ -2859,7 +2864,7 @@
         val (Jbnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn (thms, wits) => fn lthy =>
             bnf_def Dont_Inline policy I tacs (wit_tac thms) (SOME deads)
-              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+              (((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits), @{term True}(*###*)) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
 
@@ -2894,7 +2899,7 @@
         val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
 
-        val Jrel_unfold_thms =
+        val Jrel_simp_thms =
           let
             fun mk_goal Jz Jz' unf unf' JrelR relR = fold_rev Logic.all (Jz :: Jz' :: JRs)
               (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (Jz, Jz'), JrelR),
@@ -2905,23 +2910,23 @@
               fn map_simp => fn set_simps => fn unf_inject => fn unf_fld =>
               fn set_naturals => fn set_incls => fn set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
-                (K (mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
+                (K (mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps
                   unf_inject unf_fld set_naturals set_incls set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
               unf_inject_thms unf_fld_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
           end;
 
-        val Jpred_unfold_thms =
+        val Jpred_simp_thms =
           let
             fun mk_goal Jz Jz' unf unf' Jpredphi predphi = fold_rev Logic.all (Jz :: Jz' :: Jphis)
               (mk_Trueprop_eq (Jpredphi $ Jz $ Jz', predphi $ (unf $ Jz) $ (unf' $ Jz')));
             val goals = map6 mk_goal Jzs Jz's unfs unf's Jpredphis predphis;
           in
-            map3 (fn goal => fn pred_def => fn Jrel_unfold =>
-              Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Jpred_defs Jrel_unfold)
+            map3 (fn goal => fn pred_def => fn Jrel_simp =>
+              Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Jpred_defs Jrel_simp)
               |> Thm.close_derivation)
-            goals pred_defs Jrel_unfold_thms
+            goals pred_defs Jrel_simp_thms
           end;
 
         val timer = time (timer "additional properties");
@@ -2938,8 +2943,8 @@
           [(map_simpsN, map single folded_map_simp_thms),
           (set_inclN, set_incl_thmss),
           (set_set_inclN, map flat set_set_incl_thmsss),
-          (rel_unfoldN, map single Jrel_unfold_thms),
-          (pred_unfoldN, map single Jpred_unfold_thms)] @
+          (rel_simpN, map single Jrel_simp_thms),
+          (pred_simpN, map single Jpred_simp_thms)] @
           map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -90,7 +90,7 @@
   val mk_rel_coinduct_tac: 'a list -> thm -> thm -> tactic
   val mk_rel_coinduct_upto_tac: int -> ctyp option list -> cterm option list -> thm -> thm list ->
     thm list -> tactic
-  val mk_rel_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
+  val mk_rel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     thm list -> thm list -> thm list list -> tactic
   val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
   val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
@@ -1499,7 +1499,7 @@
   ALLGOALS (TRY o
     FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
 
-fun mk_rel_unfold_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld
+fun mk_rel_simp_tac in_Jrels i in_rel map_comp map_cong map_simp set_simps unf_inject unf_fld
   set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_lfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -1670,8 +1670,13 @@
           in_incl_min_alg_thms card_of_min_alg_thms;
         val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
 
-        val tacss = map9 mk_tactics map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss bd_co_tacs
-          bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs;
+        (* ### *)
+        fun rel_O_Gr_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
+
+        val rel_O_gr_tacs = replicate n rel_O_Gr_tac;
+
+        val tacss = map10 zip_goals map_id_tacs map_comp_tacs map_cong_tacs set_nat_tacss
+          bd_co_tacs bd_cinf_tacs set_bd_tacss in_bd_tacs map_wpull_tacs rel_O_gr_tacs;
 
         val fld_witss =
           let
@@ -1705,7 +1710,7 @@
         val (Ibnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn map => fn sets => fn T => fn wits => fn lthy =>
             bnf_def Dont_Inline policy I tacs wit_tac (SOME deads)
-              ((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits) lthy
+              (((((b, fold_rev Term.absfree fs' map), sets), absdummy T bd), wits), @{term True}(*###*)) lthy
             |> register_bnf (Local_Theory.full_name lthy b))
           tacss bs fs_maps setss_by_bnf Ts fld_witss lthy;
 
@@ -1739,7 +1744,7 @@
         val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
         val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
 
-        val Irel_unfold_thms =
+        val Irel_simp_thms =
           let
             fun mk_goal xF yF fld fld' IrelR relR = fold_rev Logic.all (xF :: yF :: IRs)
               (mk_Trueprop_eq (HOLogic.mk_mem (HOLogic.mk_prod (fld $ xF, fld' $ yF), IrelR),
@@ -1750,23 +1755,23 @@
               fn map_simp => fn set_simps => fn fld_inject => fn fld_unf =>
               fn set_naturals => fn set_incls => fn set_set_inclss =>
               Skip_Proof.prove lthy [] [] goal
-               (K (mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
+               (K (mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps
                  fld_inject fld_unf set_naturals set_incls set_set_inclss))
               |> Thm.close_derivation)
             ks goals in_rels map_comp's map_congs folded_map_simp_thms folded_set_simp_thmss'
               fld_inject_thms fld_unf_thms set_natural'ss set_incl_thmss set_set_incl_thmsss
           end;
 
-        val Ipred_unfold_thms =
+        val Ipred_simp_thms =
           let
             fun mk_goal xF yF fld fld' Ipredphi predphi = fold_rev Logic.all (xF :: yF :: Iphis)
               (mk_Trueprop_eq (Ipredphi $ (fld $ xF) $ (fld' $ yF), predphi $ xF $ yF));
             val goals = map6 mk_goal xFs yFs flds fld's Ipredphis predphis;
           in
-            map3 (fn goal => fn pred_def => fn Irel_unfold =>
-              Skip_Proof.prove lthy [] [] goal (mk_pred_unfold_tac pred_def Ipred_defs Irel_unfold)
+            map3 (fn goal => fn pred_def => fn Irel_simp =>
+              Skip_Proof.prove lthy [] [] goal (mk_pred_simp_tac pred_def Ipred_defs Irel_simp)
               |> Thm.close_derivation)
-            goals pred_defs Irel_unfold_thms
+            goals pred_defs Irel_simp_thms
           end;
 
         val timer = time (timer "additional properties");
@@ -1782,8 +1787,8 @@
           [(map_simpsN, map single folded_map_simp_thms),
           (set_inclN, set_incl_thmss),
           (set_set_inclN, map flat set_set_incl_thmsss),
-          (rel_unfoldN, map single Irel_unfold_thms),
-          (pred_unfoldN, map single Ipred_unfold_thms)] @
+          (rel_simpN, map single Irel_simp_thms),
+          (pred_simpN, map single Ipred_simp_thms)] @
           map2 (fn i => fn thms => (mk_set_simpsN i, map single thms)) ls' folded_set_simp_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -61,7 +61,7 @@
     thm list -> tactic
   val mk_mor_str_tac: 'a list -> thm -> tactic
   val mk_rec_tac: thm list -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_unfold_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
+  val mk_rel_simp_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm ->
     thm -> thm list -> thm list -> thm list list -> tactic
   val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
     {prems: 'a, context: Proof.context} -> tactic
@@ -774,7 +774,7 @@
           EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
-fun mk_rel_unfold_tac in_Irels i in_rel map_comp map_cong map_simp set_simps fld_inject
+fun mk_rel_simp_tac in_Irels i in_rel map_comp map_cong map_simp set_simps fld_inject
   fld_unf set_naturals set_incls set_set_inclss =
   let
     val m = length set_incls;
diff -r 3cd2622d4466 -r fa8302c8dea1 src/HOL/Codatatype/Tools/bnf_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -24,7 +24,7 @@
   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
   val mk_Abs_inj_thm: thm -> thm
 
-  val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_pred_simp_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
 
   val mk_map_comp_id_tac: thm -> tactic
   val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
@@ -91,14 +91,12 @@
     gen_tac
   end;
 
-fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
+fun mk_pred_simp_tac pred_def pred_defs rel_simp {context = ctxt, prems = _} =
   Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
-  rtac rel_unfold 1;
+  rtac rel_simp 1;
 
 fun mk_map_comp_id_tac map_comp =
-  (rtac trans THEN' rtac map_comp) 1 THEN
-  REPEAT_DETERM (stac @{thm o_id} 1) THEN
-  rtac refl 1;
+  (rtac trans THEN' rtac map_comp THEN' REPEAT_DETERM o stac @{thm o_id} THEN' rtac refl) 1;
 
 fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
   EVERY' [rtac mp, rtac map_cong,