# HG changeset patch
# User blanchet
# Date 1348646459 -7200
# Node ID 5c4a125504914488510b8029bbb6ba5f74b67043
# Parent  4339aa33535571717a616e0193c7c94de223cfc7
generate high-level "maps", "sets", and "rels" properties

diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/BNF_FP.thy
--- a/src/HOL/BNF/BNF_FP.thy	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/BNF_FP.thy	Wed Sep 26 10:00:59 2012 +0200
@@ -14,6 +14,9 @@
   "defaults"
 begin
 
+lemma eq_sym_Unity_imp: "x = (() = ()) \<Longrightarrow> x"
+by blast
+
 lemma unit_case_Unity: "(case u of () => f) = f"
 by (cases u) (hypsubst, rule unit.cases)
 
@@ -97,6 +100,11 @@
 lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
 by blast
 
+lemma UN_compreh_eq_eq:
+"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
+"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
+by blast+
+
 lemma prod_set_simps:
 "fsts (x, y) = {x}"
 "snds (x, y) = {y}"
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -8,6 +8,9 @@
 
 signature BNF_COMP =
 sig
+  val ID_bnf: BNF_Def.BNF
+  val DEADID_bnf: BNF_Def.BNF
+
   type unfold_set
   val empty_unfolds: unfold_set
   val map_unfolds_of: unfold_set -> thm list
@@ -34,6 +37,10 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
+val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
+val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
+
+(* TODO: Replace by "BNF_Defs.defs list" *)
 type unfold_set = {
   map_unfolds: thm list,
   set_unfoldss: thm list list,
@@ -677,9 +684,6 @@
     ((bnf', deads), lthy')
   end;
 
-val ID_bnf = the (bnf_of @{context} "Basic_BNFs.ID");
-val DEADID_bnf = the (bnf_of @{context} "Basic_BNFs.DEADID");
-
 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_set, lthy) =
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -101,7 +101,7 @@
     else rtac map_cong 1 THEN
       EVERY' (map_index (fn (i, map_cong) =>
         rtac map_cong THEN' EVERY' (map_index (fn (k, set_alt) =>
-          EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac @{thm meta_mp},
+          EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
             rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
             rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
             rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2},
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_def.ML
--- a/src/HOL/BNF/Tools/bnf_def.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -29,6 +29,8 @@
   val srelN: string
 
   val map_of_bnf: BNF -> term
+  val sets_of_bnf: BNF -> term list
+  val rel_of_bnf: BNF -> term
 
   val mk_T_of_bnf: typ list -> typ list -> BNF -> typ
   val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
@@ -63,7 +65,6 @@
   val set_defs_of_bnf: BNF -> thm list
   val set_natural'_of_bnf: BNF -> thm list
   val set_natural_of_bnf: BNF -> thm list
-  val sets_of_bnf: BNF -> term list
   val srel_def_of_bnf: BNF -> thm
   val srel_Gr_of_bnf: BNF -> thm
   val srel_Id_of_bnf: BNF -> thm
@@ -704,9 +705,9 @@
       ||>> mk_Frees "p1" (map2 (curry (op -->)) domTs B1Ts)
       ||>> mk_Frees "p2" (map2 (curry (op -->)) domTs B2Ts)
       ||>> mk_Frees "b" As'
-      ||>> mk_Frees' "S" setRTs
-      ||>> mk_Frees "S" setRTs
-      ||>> mk_Frees "T" setRTsBsCs
+      ||>> mk_Frees' "r" setRTs
+      ||>> mk_Frees "r" setRTs
+      ||>> mk_Frees "s" setRTsBsCs
       ||>> mk_Frees' "R" QTs;
 
     (*Gr (in R1 .. Rn) (map fst .. fst)^-1 O Gr (in R1 .. Rn) (map snd .. snd)*)
@@ -1117,13 +1118,13 @@
         fun mk_rel_flip () =
           let
             val srel_converse_thm = Lazy.force srel_converse;
-            val Rs' = Term.add_vars (prop_of srel_converse_thm) [];
-            val cts = map (pairself (certify lthy)) (map Var Rs' ~~ sQs);
-            val srel_converse_thm' = Drule.cterm_instantiate cts srel_converse_thm;
+            val cts = map (SOME o certify lthy) sQs;
+            val srel_converse_thm' = cterm_instantiate_pos cts srel_converse_thm;
           in
             unfold_thms lthy (bnf_srel_def :: @{thm converse_iff} :: mem_Collect_etc)
               (srel_converse_thm' RS eqset_imp_iff_pair)
-            |> Drule.zero_var_indexes |> Thm.generalize ([], map fst Qs') 1
+            |> Drule.zero_var_indexes
+            |> Thm.generalize (map (fst o dest_TFree) (As' @ Bs'), map fst Qs') 1
           end;
 
         val rel_flip = Lazy.lazy mk_rel_flip;
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_fp.ML
--- a/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -39,9 +39,9 @@
   val ctor_set_inclN: string
   val ctor_set_set_inclN: string
   val ctor_srelN: string
-  val disc_unfold_iffN: string
+  val disc_unfold_iffsN: string
   val disc_unfoldsN: string
-  val disc_corec_iffN: string
+  val disc_corec_iffsN: string
   val disc_corecsN: string
   val dtorN: string
   val dtor_coinductN: string
@@ -74,6 +74,7 @@
   val isNodeN: string
   val lsbisN: string
   val map_uniqueN: string
+  val mapsN: string
   val min_algN: string
   val morN: string
   val nchotomyN: string
@@ -86,6 +87,7 @@
   val sel_unfoldsN: string
   val set_inclN: string
   val set_set_inclN: string
+  val setsN: string
   val simpsN: string
   val strTN: string
   val str_initN: string
@@ -96,13 +98,10 @@
   val unfoldsN: string
   val uniqueN: string
 
+  (* TODO: Don't index set facts. Isabelle packages traditionally generate uniform names. *)
   val mk_ctor_setN: int -> string
   val mk_dtor_setN: int -> string
   val mk_dtor_set_inductN: int -> string
-  val mk_exhaustN: string -> string
-  val mk_injectN: string -> string
-  val mk_nchotomyN: string -> string
-  val mk_setsN: int -> string
   val mk_set_inductN: int -> string
 
   val mk_common_name: string list -> string
@@ -189,6 +188,7 @@
 val ctor_fold_uniqueN = ctor_foldN ^ uniqueN
 val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN
 val ctor_dtor_unfoldsN = ctorN ^ "_" ^ dtor_unfoldN ^ "s"
+val mapsN = mapN ^ "s"
 val ctor_mapN = ctorN ^ "_" ^ mapN
 val dtor_mapN = dtorN ^ "_" ^ mapN
 val map_uniqueN = mapN ^ uniqueN
@@ -206,7 +206,7 @@
 val LevN = "Lev"
 val rvN = "recover"
 val behN = "beh"
-fun mk_setsN i = mk_setN i ^ "s"
+val setsN = "sets"
 val mk_ctor_setN = prefix (ctorN ^ "_") o mk_setN
 val mk_dtor_setN = prefix (dtorN ^ "_") o mk_setN
 fun mk_set_inductN i = mk_setN i ^ "_induct"
@@ -226,15 +226,12 @@
 val ctor_dtorN = ctorN ^ "_" ^ dtorN
 val dtor_ctorN = dtorN ^ "_" ^ ctorN
 val nchotomyN = "nchotomy"
-fun mk_nchotomyN s = s ^ "_" ^ nchotomyN
 val injectN = "inject"
-fun mk_injectN s = s ^ "_" ^ injectN
 val exhaustN = "exhaust"
-fun mk_exhaustN s = s ^ "_" ^ exhaustN
-val ctor_injectN = mk_injectN ctorN
-val ctor_exhaustN = mk_exhaustN ctorN
-val dtor_injectN = mk_injectN dtorN
-val dtor_exhaustN = mk_exhaustN dtorN
+val ctor_injectN = ctorN ^ "_" ^ injectN
+val ctor_exhaustN = ctorN ^ "_" ^ exhaustN
+val dtor_injectN = dtorN ^ "_" ^ injectN
+val dtor_exhaustN = dtorN ^ "_" ^ exhaustN
 val ctor_relN = ctorN ^ "_" ^ relN
 val dtor_relN = dtorN ^ "_" ^ relN
 val ctor_srelN = ctorN ^ "_" ^ srelN
@@ -263,9 +260,9 @@
 val discN = "disc"
 val disc_unfoldsN = discN ^ "_" ^ unfoldsN
 val disc_corecsN = discN ^ "_" ^ corecsN
-val iffN = "_iff"
-val disc_unfold_iffN = discN ^ "_" ^ unfoldN ^ iffN
-val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
+val iffsN = "_iffs"
+val disc_unfold_iffsN = discN ^ "_" ^ unfoldN ^ iffsN
+val disc_corec_iffsN = discN ^ "_" ^ corecN ^ iffsN
 val relsN = relN ^ "s"
 val selN = "sel"
 val sel_relsN = selN ^ "_" ^ relsN
@@ -401,7 +398,7 @@
   | fp_sort lhss (SOME resBs) Ass =
     (subtract (op =) lhss (filter (fn T => exists (fn Ts => member (op =) Ts T) Ass) resBs)) @ lhss;
 
-fun mk_fp_bnf timer construct resBs bs sort lhss bnfs deadss livess unfold_set lthy =
+fun mk_fp_bnf timer construct_fp resBs bs sort lhss bnfs deadss livess unfold_set lthy =
   let
     val name = mk_common_name (map Binding.name_of bs);
     fun qualify i =
@@ -429,14 +426,14 @@
 
     val timer = time (timer "Normalization & sealing of BNFs");
 
-    val res = construct resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
+    val res = construct_fp resBs bs (map TFree resDs, deadss) bnfs'' lthy'';
 
     val timer = time (timer "FP construction in total");
   in
     timer; (bnfs'', res)
   end;
 
-fun fp_bnf construct bs mixfixes resBs eqs lthy =
+fun fp_bnf construct_fp bs mixfixes resBs eqs lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
@@ -446,10 +443,10 @@
       (fold_map2 (fn b => bnf_of_typ Smart_Inline (qualify b) sort) bs rhss
         (empty_unfolds, lthy));
   in
-    mk_fp_bnf timer (construct mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
+    mk_fp_bnf timer (construct_fp mixfixes) (SOME resBs) bs sort lhss bnfs Dss Ass unfold_set lthy'
   end;
 
-fun fp_bnf_cmd construct (bs, (raw_lhss, raw_bnfs)) lthy =
+fun fp_bnf_cmd construct_fp (bs, (raw_lhss, raw_bnfs)) lthy =
   let
     val timer = time (Timer.startRealTimer ());
     val lhss = map (dest_TFree o Syntax.read_typ lthy) raw_lhss;
@@ -461,7 +458,7 @@
       bs raw_bnfs (empty_unfolds, lthy));
   in
     snd (mk_fp_bnf timer
-      (construct (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
+      (construct_fp (map (K NoSyn) bs)) NONE bs sort lhss bnfs Dss Ass unfold_set lthy')
   end;
 
 end;
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_fp_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -10,16 +10,18 @@
   val datatypes: bool ->
     (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 * term list * thm * thm list * thm list *
-         thm list * thm list * thm list) * local_theory) ->
+      (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
+         thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
+      local_theory) ->
     bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
       (binding * typ) list) * (binding * term) list) * mixfix) list) list ->
     local_theory -> local_theory
   val parse_datatype_cmd: bool ->
     (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 * term list * thm * thm list * thm list *
-         thm list * thm list * thm list) * local_theory) ->
+      (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
+         thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
+      local_theory) ->
     (local_theory -> local_theory) parser
 end;
 
@@ -33,10 +35,9 @@
 open BNF_FP_Sugar_Tactics
 
 val simp_attrs = @{attributes [simp]};
+val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
 
-fun split_list9 xs =
-  (map #1 xs, map #2 xs, map #3 xs, map #4 xs, map #5 xs, map #6 xs, map #7 xs, map #8 xs,
-   map #9 xs);
+fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
@@ -60,6 +61,18 @@
 fun mk_uncurried2_fun f xss =
   mk_tupled_fun (HOLogic.mk_tuple (map HOLogic.mk_tuple xss)) f (flat xss);
 
+fun mk_flip (x, Type (_, [T1, Type (_, [T2, T3])])) =
+  Abs ("x", T1, Abs ("y", T2, Var (x, T2 --> T1 --> T3) $ Bound 0 $ Bound 1));
+
+fun flip_rels lthy n thm =
+  let
+    val Rs = Term.add_vars (prop_of thm) [];
+    val Rs' = rev (drop (length Rs - n) Rs);
+    val cRs = map (fn f => (certify lthy (Var f), certify lthy (mk_flip f))) Rs';
+  in
+    Drule.cterm_instantiate cRs thm
+  end;
+
 fun mk_ctor_or_dtor get_T Ts t =
   let val Type (_, Ts0) = get_T (fastype_of t) in
     Term.subst_atomic_types (Ts0 ~~ Ts) t
@@ -83,13 +96,10 @@
     Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
   end;
 
-fun mk_rel Ts Us t =
-  let
-    val ((Type (_, Ts0), Type (_, Us0)), body) =
-      strip_type (fastype_of t) |>> split_last |>> apfst List.last;
-  in
-    Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
-  end;
+fun liveness_of_fp_bnf n bnf =
+  (case T_of_bnf bnf of
+    Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
+  | _ => replicate n false);
 
 fun tick u f = Term.lambda u (HOLogic.mk_prod (u, f $ u));
 
@@ -120,7 +130,7 @@
 fun defaults_of ((_, ds), _) = ds;
 fun ctr_mixfix_of (_, mx) = mx;
 
-fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct (no_dests, specs)
+fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp (no_dests, specs)
     no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
@@ -143,11 +153,13 @@
     val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
     val unsorted_As = Library.foldr1 merge_type_args unsorted_Ass0;
 
-    val ((Xs, Cs), no_defs_lthy) =
+    val (((Bs0, Cs), Xs), no_defs_lthy) =
       no_defs_lthy0
       |> fold (Variable.declare_typ o resort_tfree dummyS) unsorted_As
-      |> variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS) |>> map TFree
-      ||>> mk_TFrees nn;
+      |> mk_TFrees (length unsorted_As)
+      ||>> mk_TFrees nn
+      ||>> apfst (map TFree) o
+        variant_types (map (prefix "'") fp_b_names) (replicate nn HOLogic.typeS);
 
     (* TODO: cleaner handling of fake contexts, without "background_theory" *)
     (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
@@ -208,9 +220,13 @@
     val fp_eqs =
       map dest_TFree Xs ~~ map (Term.typ_subst_atomic (As ~~ unsorted_As)) ctr_sum_prod_TsXs;
 
-    val (pre_bnfs, ((dtors0, ctors0, rels0, fp_folds0, fp_recs0, fp_induct, dtor_ctors, ctor_dtors,
-           ctor_injects, fp_fold_thms, fp_rec_thms), lthy)) =
-      fp_bnf construct fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+    (* TODO: clean up list *)
+    val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
+           dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss, fp_rel_thms,
+           fp_fold_thms, fp_rec_thms), lthy)) =
+      fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
+
+    val timer = time (Timer.startRealTimer ());
 
     fun add_nesty_bnf_names Us =
       let
@@ -227,11 +243,23 @@
     val nesting_bnfs = nesty_bnfs As;
     val nested_bnfs = nesty_bnfs Xs;
 
-    val timer = time (Timer.startRealTimer ());
+    val pre_map_defs = map map_def_of_bnf pre_bnfs;
+    val pre_set_defss = map set_defs_of_bnf pre_bnfs;
+    val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
+    val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
+    val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
+    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
+
+    val live = live_of_bnf any_fp_bnf;
+
+    val Bs =
+      map3 (fn alive => fn A as TFree (_, S) => fn B => if alive then resort_tfree S B else A)
+        (liveness_of_fp_bnf (length As) any_fp_bnf) As Bs0;
+
+    val B_ify = Term.typ_subst_atomic (As ~~ Bs);
 
     val ctors = map (mk_ctor As) ctors0;
     val dtors = map (mk_dtor As) dtors0;
-    val rels = map (mk_rel As As) rels0; (*FIXME*)
 
     val fpTs = map (domain_type o fastype_of) dtors;
 
@@ -243,11 +271,11 @@
     val mss = map (map length) ctr_Tsss;
     val Css = map2 replicate ns Cs;
 
-    val fp_folds as fp_fold1 :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
-    val fp_recs as fp_rec1 :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
+    val fp_folds as any_fp_fold :: _ = map (mk_rec_like lfp As Cs) fp_folds0;
+    val fp_recs as any_fp_rec :: _ = map (mk_rec_like lfp As Cs) fp_recs0;
 
-    val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of fp_fold1)));
-    val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
+    val fp_fold_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_fold)));
+    val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of any_fp_rec)));
 
     val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
           (zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
@@ -351,9 +379,10 @@
              (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss)))), lthy)
         end;
 
-    fun define_ctrs_case_for_type ((((((((((((((((((fp_b, fpT), C), ctor), dtor), fp_fold), fp_rec),
-          ctor_dtor), dtor_ctor), ctor_inject), n), ks), ms), ctr_bindings), ctr_mixfixes), ctr_Tss),
-        disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
+    fun define_ctrs_case_for_type (((((((((((((((((((((((((fp_bnf, fp_b), fpT), C), ctor), dtor),
+            fp_fold), fp_rec), ctor_dtor), dtor_ctor), ctor_inject), pre_map_def), pre_set_defs),
+          pre_rel_def), fp_map_thm), fp_set_thms), fp_rel_thm), n), ks), ms), ctr_bindings),
+        ctr_mixfixes), ctr_Tss), disc_bindings), sel_bindingss), raw_sel_defaultss) no_defs_lthy =
       let
         val fp_b_name = Binding.name_of fp_b;
 
@@ -367,14 +396,17 @@
           |> yield_singleton (mk_Frees "w") dtorT
           ||>> mk_Frees "f" case_Ts
           ||>> mk_Freess "x" ctr_Tss
-          ||>> mk_Freess "y" ctr_Tss
+          ||>> mk_Freess "y" (map (map B_ify) ctr_Tss)
           ||>> yield_singleton Variable.variant_fixes fp_b_name;
 
         val u = Free (u', fpT);
 
+        val tuple_xs = map HOLogic.mk_tuple xss;
+        val tuple_ys = map HOLogic.mk_tuple yss;
+
         val ctr_rhss =
-          map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $
-            mk_InN_balanced ctr_sum_prod_T n (HOLogic.mk_tuple xs) k)) ks xss;
+          map3 (fn k => fn xs => fn tuple_x => fold_rev Term.lambda xs (ctor $
+            mk_InN_balanced ctr_sum_prod_T n tuple_x k)) ks xss tuple_xs;
 
         val case_binding = Binding.suffix_name ("_" ^ caseN) fp_b;
 
@@ -391,6 +423,8 @@
         val phi = Proof_Context.export_morphism lthy lthy';
 
         val ctr_defs = map (Morphism.thm phi) raw_ctr_defs;
+        val ctr_defs' =
+          map2 (fn m => fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) ms ctr_defs;
         val case_def = Morphism.thm phi raw_case_def;
 
         val ctrs0 = map (Morphism.term phi) raw_ctrs;
@@ -398,45 +432,130 @@
 
         val ctrs = map (mk_ctr As) ctrs0;
 
-        fun exhaust_tac {context = ctxt, ...} =
+        fun wrap lthy =
           let
-            val ctor_iff_dtor_thm =
+            fun exhaust_tac {context = ctxt, ...} =
               let
-                val goal =
-                  fold_rev Logic.all [w, u]
-                    (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+                val ctor_iff_dtor_thm =
+                  let
+                    val goal =
+                      fold_rev Logic.all [w, u]
+                        (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+                  in
+                    Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+                      mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
+                        (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
+                    |> Thm.close_derivation
+                    |> Morphism.thm phi
+                  end;
+
+                val sumEN_thm' =
+                  unfold_thms lthy @{thms all_unit_eq}
+                    (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
+                       (mk_sumEN_balanced n))
+                  |> Morphism.thm phi;
               in
-                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                  mk_ctor_iff_dtor_tac ctxt (map (SOME o certifyT lthy) [dtorT, fpT])
-                    (certify lthy ctor) (certify lthy dtor) ctor_dtor dtor_ctor)
-                |> Thm.close_derivation
-                |> Morphism.thm phi
+                mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
               end;
 
-            val sumEN_thm' =
-              unfold_thms lthy @{thms all_unit_eq}
-                (Drule.instantiate' (map (SOME o certifyT lthy) ctr_prod_Ts) []
-                   (mk_sumEN_balanced n))
-              |> Morphism.thm phi;
+            val inject_tacss =
+              map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
+                  mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+
+            val half_distinct_tacss =
+              map (map (fn (def, def') => fn {context = ctxt, ...} =>
+                mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss (`I ctr_defs));
+
+            val case_tacs =
+              map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
+                mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
+
+            val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+
+            val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss
           in
-            mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
+            wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
+              sel_defaultss))) lthy
           end;
 
-        val inject_tacss =
-          map2 (fn 0 => K [] | _ => fn ctr_def => [fn {context = ctxt, ...} =>
-              mk_inject_tac ctxt ctr_def ctor_inject]) ms ctr_defs;
+        fun derive_maps_sets_rels (wrap_res, lthy) =
+          let
+            val rel_flip = rel_flip_of_bnf fp_bnf;
+            val nones = replicate live NONE;
+
+            val ctor_cong =
+              if lfp then Drule.dummy_thm
+              else cterm_instantiate_pos [NONE, NONE, SOME (certify lthy ctor)] arg_cong;
+
+            fun mk_cIn ify =
+              certify lthy o (not lfp ? curry (op $) (map_types ify ctor)) oo
+              mk_InN_balanced (ify ctr_sum_prod_T) n;
+
+            val cxIns = map2 (mk_cIn I) tuple_xs ks;
+            val cyIns = map2 (mk_cIn B_ify) tuple_ys ks;
+
+            fun thaw xs = Thm.generalize ([], map (fst o dest_Free) xs) 1 o Drule.zero_var_indexes;
 
-        val half_distinct_tacss =
-          map (map (fn (def, def') => fn {context = ctxt, ...} =>
-            mk_half_distinct_tac ctxt ctor_inject [def, def'])) (mk_half_pairss ctr_defs);
+            fun mk_map_thm ctr_def' xs cxIn =
+              fold_thms lthy [ctr_def']
+                (unfold_thms lthy (pre_map_def ::
+                     (if lfp then [] else [ctor_dtor, dtor_ctor]) @ sum_prod_thms_map)
+                   (cterm_instantiate_pos (nones @ [SOME cxIn])
+                      (if lfp then fp_map_thm else fp_map_thm RS ctor_cong)))
+              |> thaw xs;
+
+            fun mk_set_thm fp_set_thm ctr_def' xs cxIn =
+              fold_thms lthy [ctr_def']
+                (unfold_thms lthy (pre_set_defs @ nested_set_natural's @ nesting_set_natural's @
+                     (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_set)
+                   (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
+              |> thaw xs;
+
+            fun mk_set_thms fp_set_thm = map3 (mk_set_thm fp_set_thm) ctr_defs' xss cxIns;
+
+            val map_thms = map3 mk_map_thm ctr_defs' xss cxIns;
+            val set_thmss = map mk_set_thms fp_set_thms;
 
-        val case_tacs =
-          map3 (fn k => fn m => fn ctr_def => fn {context = ctxt, ...} =>
-            mk_case_tac ctxt n k m case_def ctr_def dtor_ctor) ks ms ctr_defs;
+            val rel_infos = (ctr_defs' ~~ xss ~~ cxIns, ctr_defs' ~~ yss ~~ cyIns);
+
+            fun mk_rel_thm finish_off ctr_defs' xs cxIn ys cyIn =
+              fold_thms lthy ctr_defs'
+                 (unfold_thms lthy (pre_rel_def ::
+                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+                    (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
+              |> finish_off |> thaw (xs @ ys);
+
+            fun mk_pos_rel_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
+              mk_rel_thm (perhaps (try (fn th => th RS @{thm eq_sym_Unity_imp}))) [ctr_def']
+                xs cxIn ys cyIn;
+
+            val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
+
+            fun mk_half_neg_rel_thm (((xctr_def', xs), cxIn), ((yctr_def', ys), cyIn)) =
+              mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
+                xs cxIn ys cyIn;
 
-        val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
+            fun mk_other_half_neg_rel_thm thm =
+              flip_rels lthy live thm RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
+
+            val half_neg_rel_thmss = map (map mk_half_neg_rel_thm) (mk_half_pairss rel_infos);
+            val other_half_neg_rel_thmss = map (map mk_other_half_neg_rel_thm) half_neg_rel_thmss;
+            val (neg_rel_thms, _) = join_halves n half_neg_rel_thmss other_half_neg_rel_thmss;
+
+            val rel_thms = pos_rel_thms @ neg_rel_thms;
 
-        fun define_fold_rec (wrap_res, no_defs_lthy) =
+            val notes =
+              [(mapsN, map_thms, code_simp_attrs),
+               (relsN, rel_thms, code_simp_attrs),
+               (setsN, flat set_thmss, code_simp_attrs)]
+              |> filter_out (null o #2)
+              |> map (fn (thmN, thms, attrs) =>
+                ((Binding.qualify true fp_b_name (Binding.name thmN), attrs), [(thms, [])]));
+          in
+            (wrap_res, lthy |> Local_Theory.notes notes |> snd)
+          end;
+
+        fun define_fold_rec no_defs_lthy =
           let
             val fpT_to_C = fpT --> C;
 
@@ -468,10 +587,10 @@
 
             val [foldx, recx] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
           in
-            ((wrap_res, ctrs, foldx, recx, xss, yss, ctr_defs, fold_def, rec_def), lthy)
+            ((foldx, recx, fold_def, rec_def), lthy)
           end;
 
-        fun define_unfold_corec (wrap_res, no_defs_lthy) =
+        fun define_unfold_corec no_defs_lthy =
           let
             val B_to_fpT = C --> fpT;
 
@@ -508,27 +627,20 @@
 
             val [unfold, corec] = map (mk_rec_like lfp As Cs o Morphism.term phi) csts;
           in
-            ((wrap_res, ctrs, unfold, corec, xss, yss, ctr_defs, unfold_def, corec_def), lthy)
-          end;
-
-        fun wrap lthy =
-          let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
-            wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_bindings, (sel_bindingss,
-              sel_defaultss))) lthy
+            ((unfold, corec, unfold_def, corec_def), lthy)
           end;
 
         val define_rec_likes = if lfp then define_fold_rec else define_unfold_corec;
+
+        fun massage_res ((wrap_res, rec_like_res), lthy) =
+          (((ctrs, xss, ctr_defs, wrap_res), rec_like_res), lthy);
       in
-        ((wrap, define_rec_likes), lthy')
+        (wrap #> (live > 0 ? derive_maps_sets_rels) ##>> define_rec_likes #> massage_res, lthy')
       end;
 
-    fun wrap_types_and_define_rec_likes ((wraps, define_rec_likess), lthy) =
-      fold_map2 (curry (op o)) define_rec_likess wraps lthy |>> split_list9
-
-    val pre_map_defs = map map_def_of_bnf pre_bnfs;
-    val pre_set_defss = map set_defs_of_bnf pre_bnfs;
-    val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
-    val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
+    fun wrap_types_and_more (wrap_types_and_mores, lthy) =
+      fold_map I wrap_types_and_mores lthy
+      |>> apsnd split_list4 o apfst split_list4 o split_list;
 
     fun build_map build_arg (Type (s, Ts)) (Type (_, Us)) =
       let
@@ -539,12 +651,13 @@
         val args = map build_arg TUs;
       in Term.list_comb (mapx, args) end;
 
+    (* TODO: Add map, sets, rel simps *)
     val mk_simp_thmss =
       map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
         injects @ distincts @ cases @ rec_likes @ fold_likes);
 
-    fun derive_induct_fold_rec_thms_for_types ((wrap_ress, ctrss, folds, recs, xsss, _, ctr_defss,
-        fold_defs, rec_defs), lthy) =
+    fun derive_induct_fold_rec_thms_for_types (((ctrss, xsss, ctr_defss, wrap_ress), (folds, recs,
+        fold_defs, rec_defs)), lthy) =
       let
         val (((phis, phis'), us'), names_lthy) =
           lthy
@@ -687,8 +800,6 @@
         val induct_case_names_attr = Attrib.internal (K (Rule_Cases.case_names induct_cases));
         fun induct_type_attr T_name = Attrib.internal (K (Induct.induct_type T_name));
 
-        (* TODO: Also note "recs", "simps", and "splits" if "nn > 1" (for compatibility with the
-           old package)? And for codatatypes as well? *)
         val common_notes =
           (if nn > 1 then [(inductN, [induct_thm], [induct_case_names_attr])] else [])
           |> map (fn (thmN, thms, attrs) =>
@@ -697,9 +808,9 @@
         val notes =
           [(inductN, map single induct_thms,
             fn T_name => [induct_case_names_attr, induct_type_attr T_name]),
-           (foldsN, fold_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
-           (recsN, rec_thmss, K (Code.add_default_eqn_attrib :: simp_attrs)),
-           (simpsN, simp_thmss, K [])] (* TODO: Add relator simps *)
+           (foldsN, fold_thmss, K (code_simp_attrs)),
+           (recsN, rec_thmss, K (code_simp_attrs)),
+           (simpsN, simp_thmss, K [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map3 (fn b => fn Type (T_name, _) => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs T_name),
@@ -708,8 +819,8 @@
         lthy |> Local_Theory.notes (common_notes @ notes) |> snd
       end;
 
-    fun derive_coinduct_unfold_corec_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, _, _,
-        ctr_defss, unfold_defs, corec_defs), lthy) =
+    fun derive_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress), (unfolds,
+        corecs, unfold_defs, corec_defs)), lthy) =
       let
         val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
         val selsss = map #2 wrap_ress;
@@ -725,6 +836,9 @@
 
         val (coinduct_thms, coinduct_thm) =
           let
+(*            val goal =
+  *)
+
             val coinduct_thm = fp_induct;
           in
             `(conj_dests nn) coinduct_thm
@@ -874,13 +988,13 @@
         val notes =
           [(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
            (corecsN, corec_thmss, []),
-           (disc_unfold_iffN, disc_unfold_iff_thmss, simp_attrs),
+           (disc_corec_iffsN, disc_corec_iff_thmss, simp_attrs),
+           (disc_corecsN, disc_corec_thmss, simp_attrs),
+           (disc_unfold_iffsN, disc_unfold_iff_thmss, simp_attrs),
            (disc_unfoldsN, disc_unfold_thmss, simp_attrs),
-           (disc_corec_iffN, disc_corec_iff_thmss, simp_attrs),
-           (disc_corecsN, disc_corec_thmss, simp_attrs),
            (sel_unfoldsN, sel_unfold_thmss, simp_attrs),
            (sel_corecsN, sel_corec_thmss, simp_attrs),
-           (simpsN, simp_thmss, []), (* TODO: Add relator simps *)
+           (simpsN, simp_thmss, []),
            (unfoldsN, unfold_thmss, [])]
           |> maps (fn (thmN, thmss, attrs) =>
             map_filter (fn (_, []) => NONE | (b, thms) =>
@@ -890,86 +1004,15 @@
         lthy |> Local_Theory.notes (anonymous_notes @ common_notes @ notes) |> snd
       end;
 
-    fun derive_rel_thms_for_types ((wrap_ress, ctrss, unfolds, corecs, xsss, ysss, ctr_defss,
-        unfold_defs, corec_defs), lthy) =
-      let
-        val selsss = map #2 wrap_ress;
-
-        val theta_Ts =  [] (*###*)
-
-        val (thetas, _) =
-          lthy
-          |> mk_Frees "Q" (map mk_pred1T theta_Ts);
-
-        val (rel_thmss, rel_thmsss) =
-          let
-            val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
-            val yctrss = map2 (map2 (curry Term.list_comb)) ctrss ysss;
-            val threls = map (fold_rev rapp thetas) rels;
-
-            fun mk_goal threl (xctr, xs) (yctr, ys) =
-              let
-                val lhs = threl $ xctr $ yctr;
-
-                (* ### fixme: lift rel *)
-                fun mk_conjunct x y = HOLogic.mk_eq (x, y);
-
-                fun mk_rhs () =
-                  Library.foldr1 HOLogic.mk_conj (map2 mk_conjunct xs ys);
-              in
-                HOLogic.mk_Trueprop
-                  (if Term.head_of xctr = Term.head_of yctr then
-                     if null xs then
-                       lhs
-                     else
-                       HOLogic.mk_eq (lhs, mk_rhs ())
-                   else
-                     HOLogic.mk_not lhs)
-              end;
-
-(*###*)
-          (* TODO: Prove and exploit symmetry of relators to halve the number of goals. *)
-          fun mk_goals threl xctrs xss yctrs yss =
-            map_product (mk_goal threl) (xctrs ~~ xss) (yctrs ~~ yss);
-
-          val goalsss = map5 mk_goals threls xctrss xsss yctrss ysss;
-
-(*###
-            val goalsss = map6 (fn threl =>
-              map5 (fn xctr => fn xs => fn sels =>
-                map2 (mk_goal threl xctr xs sels))) threls xctrss xsss selsss yctrss ysss;
-*)
-(* val _ = tracing ("goalsss: " ^ PolyML.makestring goalsss) (*###*) *)
-          in
-            ([], [])
-          end;
-
-        val (sel_rel_thmss, sel_rel_thmsss) =
-          let
-          in
-            ([], [])
-          end;
-
-        val notes =
-          [(* (relsN, rel_thmss, []),
-           (sel_relsN, sel_rel_thmss, []) *)]
-          |> maps (fn (thmN, thmss, attrs) =>
-            map2 (fn b => fn thms =>
-                ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), attrs),
-              [(thms, [])])) fp_bs thmss);
-      in
-        lthy |> Local_Theory.notes notes |> snd
-      end;
-
     val lthy' = lthy
-      |> fold_map define_ctrs_case_for_type (fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~ fp_folds ~~
-        fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ ns ~~ kss ~~ mss ~~ ctr_bindingss ~~
-        ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~ raw_sel_defaultsss)
-      |>> split_list |> wrap_types_and_define_rec_likes
-      |> `(if lfp then derive_induct_fold_rec_thms_for_types
-           else derive_coinduct_unfold_corec_thms_for_types)
-      |> swap |>> fst
-      |> (if null rels then snd else derive_rel_thms_for_types);
+      |> fold_map define_ctrs_case_for_type (fp_bnfs ~~ fp_bs ~~ fpTs ~~ Cs ~~ ctors ~~ dtors ~~
+        fp_folds ~~ fp_recs ~~ ctor_dtors ~~ dtor_ctors ~~ ctor_injects ~~ pre_map_defs ~~
+        pre_set_defss ~~ pre_rel_defs ~~ fp_map_thms ~~ fp_set_thmss ~~ fp_rel_thms ~~ ns ~~ kss ~~
+        mss ~~ ctr_bindingss ~~ ctr_mixfixess ~~ ctr_Tsss ~~ disc_bindingss ~~ sel_bindingsss ~~
+        raw_sel_defaultsss)
+      |> wrap_types_and_more
+      |> (if lfp then derive_induct_fold_rec_thms_for_types
+          else derive_coinduct_unfold_corec_thms_for_types);
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
       (if lfp then "" else "co") ^ "datatype"));
@@ -995,6 +1038,6 @@
 
 val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
 
-fun parse_datatype_cmd lfp construct = parse_datatype >> datatype_cmd lfp construct;
+fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
 
 end;
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -7,6 +7,10 @@
 
 signature BNF_FP_SUGAR_TACTICS =
 sig
+  val sum_prod_thms_map: thm list
+  val sum_prod_thms_set: thm list
+  val sum_prod_thms_rel: thm list
+
   val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
   val mk_corec_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
   val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
@@ -27,8 +31,16 @@
 open BNF_Util
 open BNF_FP
 
-val meta_mp = @{thm meta_mp};
-val meta_spec = @{thm meta_spec};
+val sum_prod_thms_map = @{thms id_apply map_pair_simp sum_map.simps prod.cases};
+
+val sum_prod_thms_set0 =
+  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
+      Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
+      mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
+
+val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
+
+val sum_prod_thms_rel = @{thms prod.cases prod_rel_def sum.cases sum_rel_def};
 
 fun inst_spurious_fs lthy thm =
   let
@@ -70,8 +82,7 @@
   unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
   unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
-(* TODO: Try "map_pair_simp" instead of "map_pair_def" everywhere. *)
-
+(*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*)
 val rec_like_unfold_thms =
   @{thms comp_def convol_def id_apply map_pair_def prod_case_Pair_iden sum.simps(5,6) sum_map.simps
       split_conv unit_case_Unity};
@@ -81,12 +92,11 @@
     rec_like_unfold_thms) THEN unfold_thms_tac ctxt @{thms id_def} THEN rtac refl 1;
 
 val corec_like_ss = ss_only @{thms if_True if_False};
-val corec_like_unfold_thms = @{thms id_apply map_pair_def prod.cases sum_map.simps};
 
 fun mk_corec_like_tac corec_like_defs map_ids ctor_dtor_corec_like pre_map_def ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: corec_like_defs) THEN
   subst_tac ctxt [ctor_dtor_corec_like] 1 THEN asm_simp_tac corec_like_ss 1 THEN
-  unfold_thms_tac ctxt (pre_map_def :: corec_like_unfold_thms @ map_ids) THEN
+  unfold_thms_tac ctxt (pre_map_def :: sum_prod_thms_map @ map_ids) THEN
   unfold_thms_tac ctxt @{thms id_def} THEN
   TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
 
@@ -102,14 +112,9 @@
     hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
 
-val induct_prem_prem_thms =
-  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
-      Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
-      mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
-
 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
   EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
-     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
+     SELECT_GOAL (unfold_thms_tac ctxt (pre_set_defs @ set_natural's @ sum_prod_thms_set0)),
      solve_prem_prem_tac]) (rev kks)) 1;
 
 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -9,10 +9,11 @@
 
 signature BNF_GFP =
 sig
-  val bnf_gfp: mixfix list -> (string * sort) list option -> binding list ->
+  val construct_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 * term list * thm * thm list * thm list *
-      thm list * thm list * thm list) * local_theory
+    (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
+      thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
+    local_theory
 end;
 
 structure BNF_GFP : BNF_GFP =
@@ -21,6 +22,7 @@
 open BNF_Def
 open BNF_Util
 open BNF_Tactics
+open BNF_Comp
 open BNF_FP
 open BNF_FP_Sugar
 open BNF_GFP_Util
@@ -55,7 +57,7 @@
      ((i, I), nth (nth lwitss i) nwit) :: maps (tree_to_coind_wits lwitss) subtrees;
 
 (*all BNFs have the same lives*)
-fun bnf_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
+fun construct_gfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -2285,8 +2287,12 @@
     val timer = time (timer "coinduction");
 
     (*register new codatatypes as BNFs*)
-    val (Jrels, lthy) = if m = 0 then ([], lthy) else
-      let
+    val (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms, lthy) =
+      if m = 0 then
+        let val dummy_thms = replicate n Drule.dummy_thm in
+          (replicate n DEADID_bnf, dummy_thms, replicate n [], dummy_thms, lthy)
+        end
+      else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val gTs = map2 (curry op -->) passiveBs passiveCs;
         val f1Ts = map2 (curry op -->) passiveAs passiveYs;
@@ -2425,7 +2431,7 @@
         val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks;
         val setss_by_range = transpose setss_by_bnf;
 
-        val set_simp_thmss =
+        val dtor_set_thmss =
           let
             fun mk_simp_goal relate pas_set act_sets sets dtor z set =
               relate (set $ z, mk_union (pas_set $ (dtor $ z),
@@ -2454,7 +2460,7 @@
           in
             map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets =>
               Skip_Proof.prove lthy [] [] goal
-                (K (mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets))
+                (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets))
               |> Thm.close_derivation))
             simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
           end;
@@ -2860,7 +2866,7 @@
           coind_wit_thms (map (pair []) ctor_witss)
           |> map (apsnd (map snd o minimize_wits));
 
-        val wit_tac = mk_wit_tac n dtor_ctor_thms (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
+        val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Jbnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn (thms, wits) => fn lthy =>
@@ -2870,10 +2876,10 @@
           tacss bs fs_maps setss_by_bnf Ts all_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
-          mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Jbnfs);
+          mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
 
         val fold_sets = fold_thms lthy (maps (fn bnf =>
-         map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Jbnfs);
+         map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Jbnfs);
 
         val timer = time (timer "registered new codatatypes as BNFs");
 
@@ -2897,8 +2903,8 @@
         val Jrel_defs = map rel_def_of_bnf Jbnfs;
 
         val folded_dtor_map_thms = map fold_maps dtor_map_thms;
-        val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
-        val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
+        val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
+        val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss;
 
         val dtor_Jsrel_thms =
           let
@@ -2914,7 +2920,7 @@
                 (K (mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map dtor_sets
                   dtor_inject dtor_ctor set_naturals dtor_set_incls dtor_set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_set_simp_thmss'
+            ks goals in_srels map_comp's map_congs folded_dtor_map_thms folded_dtor_set_thmss'
               dtor_inject_thms dtor_ctor_thms set_natural'ss dtor_set_incl_thmss
               dtor_set_set_incl_thmsss
           end;
@@ -2951,13 +2957,14 @@
              [(dtor_srelN, map single dtor_Jsrel_thms)]
            else
              []) @
-          map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_set_simp_thmss
+          map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_dtor_set_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        timer; (Jrels, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
+        timer; (Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms,
+          lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd)
       end;
 
       val common_notes =
@@ -2991,8 +2998,9 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((dtors, ctors, Jrels, unfolds, corecs, dtor_map_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
-      ctor_inject_thms, ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
+    ((Jbnfs, dtors, ctors, unfolds, corecs, dtor_map_coinduct_thm, dtor_ctor_thms, ctor_dtor_thms,
+      ctor_inject_thms, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_Jrel_thms,
+      ctor_dtor_unfold_thms, ctor_dtor_corec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
@@ -3001,10 +3009,10 @@
     "define BNF-based coinductive datatypes (low-level)"
     (Parse.and_list1
       ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
-      (snd oo fp_bnf_cmd bnf_gfp o apsnd split_list o split_list));
+      (snd oo fp_bnf_cmd construct_gfp o apsnd split_list o split_list));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
-    (parse_datatype_cmd false bnf_gfp);
+    (parse_datatype_cmd false construct_gfp);
 
 end;
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -40,6 +40,7 @@
   val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
   val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
     thm -> thm -> tactic
+  val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
   val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
   val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
     thm list -> thm list -> tactic
@@ -110,7 +111,6 @@
   val mk_set_natural_tac: thm -> thm -> tactic
   val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
     thm list list -> thm list list -> tactic
-  val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
   val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
     cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
     thm list list -> thm list list -> thm -> thm list list -> tactic
@@ -157,11 +157,9 @@
 fun mk_mor_incl_tac mor_def map_id's =
   (stac mor_def THEN'
   rtac conjI THEN'
-  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac @{thm id_apply}, atac]))
-    map_id's THEN'
+  CONJ_WRAP' (K (EVERY' [rtac ballI, etac set_mp, stac id_apply, atac])) map_id's THEN'
   CONJ_WRAP' (fn thm =>
-   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (@{thm id_apply} RS arg_cong)]))
-  map_id's) 1;
+   (EVERY' [rtac ballI, rtac (thm RS trans), rtac sym, rtac (id_apply RS arg_cong)])) map_id's) 1;
 
 fun mk_mor_comp_tac mor_def mor_images morEs map_comp_ids =
   let
@@ -410,7 +408,7 @@
         hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
         rtac (mk_sum_casesN n i), rtac CollectI,
         EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
-          etac ((trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]) RS ord_eq_le_trans)])
+          etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
           passive_sets),
         CONJ_WRAP' (fn (i, thm) => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac CollectI, rtac exI, rtac exI, rtac conjI, rtac refl,
@@ -564,7 +562,7 @@
         then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
           rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
           rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
-          rtac (trans OF [@{thm image_id} RS fun_cong, @{thm id_apply}]),
+          rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]),
           rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
         else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
           REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
@@ -1114,8 +1112,8 @@
   unfold_thms_tac ctxt [ctor_def] THEN EVERY' [rtac ext, rtac trans, rtac o_apply,
     rtac trans, rtac unfold, rtac trans, rtac map_comp_id, rtac trans, rtac map_congL,
     EVERY' (map (fn thm =>
-      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, @{thm id_apply}])) unfold_o_dtors),
-    rtac sym, rtac @{thm id_apply}] 1;
+      rtac ballI THEN' rtac (trans OF [thm RS fun_cong, id_apply])) unfold_o_dtors),
+    rtac sym, rtac id_apply] 1;
 
 fun mk_corec_tac m corec_defs unfold map_cong corec_Inls {context = ctxt, prems = _} =
   unfold_thms_tac ctxt corec_defs THEN EVERY' [rtac trans, rtac (o_apply RS arg_cong),
@@ -1168,7 +1166,7 @@
 fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
   EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
     EVERY' (map (fn i =>
-      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
+      EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac meta_mp,
         atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,
         rtac impI, dtac conjunct2, dtac (mk_conjunctN (length ks) i), REPEAT_DETERM o etac allE,
         etac impE, etac @{thm diag_UNIV_I}, REPEAT_DETERM o eresolve_tac [bexE, conjE, CollectE],
@@ -1196,7 +1194,7 @@
           EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
       (1 upto n) set_hsets set_hset_hsetss)] 1;
 
-fun mk_set_simp_tac n set_le set_incl_hset set_hset_incl_hsets =
+fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets =
   EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
     REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
     EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
@@ -1232,11 +1230,11 @@
         set_hset_hsetss) =>
         [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
          rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
-         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
+         REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
          REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
          rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
          EVERY' (maps (fn set_hset =>
-           [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
+           [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
            REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
          REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
          CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
@@ -1473,10 +1471,10 @@
         rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
     (pick_cols ~~ hset_defs)] 1;
 
-fun mk_wit_tac n dtor_ctors set_simp wit coind_wits {context = ctxt, prems = _} =
+fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} =
   ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
   REPEAT_DETERM (atac 1 ORELSE
-    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
     K (unfold_thms_tac ctxt dtor_ctors),
     REPEAT_DETERM_N n o etac UnE,
     REPEAT_DETERM o
@@ -1484,7 +1482,7 @@
         (eresolve_tac wit ORELSE'
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
             K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
@@ -1524,8 +1522,8 @@
     val only_if_tac =
       EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
-          EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
+        CONJ_WRAP' (fn (dtor_set, passive_set_natural) =>
+          EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
             rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -8,10 +8,11 @@
 
 signature BNF_LFP =
 sig
-  val bnf_lfp: mixfix list -> (string * sort) list option -> binding list ->
+  val construct_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 * term list * thm * thm list * thm list *
-      thm list * thm list * thm list) * local_theory
+    (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
+      thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
+    local_theory
 end;
 
 structure BNF_LFP : BNF_LFP =
@@ -20,13 +21,14 @@
 open BNF_Def
 open BNF_Util
 open BNF_Tactics
+open BNF_Comp
 open BNF_FP
 open BNF_FP_Sugar
 open BNF_LFP_Util
 open BNF_LFP_Tactics
 
 (*all BNFs have the same lives*)
-fun bnf_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
+fun construct_lfp mixfixes resBs bs (resDs, Dss) bnfs lthy =
   let
     val timer = time (Timer.startRealTimer ());
 
@@ -208,8 +210,8 @@
       end;
 
     val map_congL_thms = map5 mk_map_congL xFs mapsAsAs setssAs map_congs map_id's;
-    val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs
-    val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs
+    val in_mono'_thms = map (fn bnf => in_mono_of_bnf bnf OF (replicate m subset_refl)) bnfs;
+    val in_cong'_thms = map (fn bnf => in_cong_of_bnf bnf OF (replicate m refl)) bnfs;
 
     val timer = time (timer "Derived simple theorems");
 
@@ -1346,8 +1348,12 @@
     val timer = time (timer "induction");
 
     (*register new datatypes as BNFs*)
-    val (Irels, lthy) = if m = 0 then ([], lthy) else
-      let
+    val (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) =
+      if m = 0 then
+        let val dummy_thms = replicate n Drule.dummy_thm in
+          (replicate n DEADID_bnf, dummy_thms, replicate n [], dummy_thms, lthy)
+        end
+      else let
         val fTs = map2 (curry op -->) passiveAs passiveBs;
         val f1Ts = map2 (curry op -->) passiveAs passiveYs;
         val f2Ts = map2 (curry op -->) passiveBs passiveYs;
@@ -1457,7 +1463,7 @@
         val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
         val setss_by_bnf = transpose setss_by_range;
 
-        val set_simp_thmss =
+        val ctor_set_thmss =
           let
             fun mk_goal sets ctor set col map =
               mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
@@ -1480,19 +1486,19 @@
 
             val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
                 Skip_Proof.prove lthy [] [] goal
-                  (K (mk_set_simp_tac set (nth set_nats (i - 1)) (drop m set_nats)))
+                  (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
                 |> Thm.close_derivation)
               set_natural'ss) ls simp_goalss setss;
           in
             ctor_setss
           end;
 
-        fun mk_set_thms set_simp = (@{thm xt1(3)} OF [set_simp, @{thm Un_upper1}]) ::
-          map (fn i => (@{thm xt1(3)} OF [set_simp, @{thm Un_upper2}]) RS
+        fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
+          map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
             (mk_Un_upper n i RS subset_trans) RSN
             (2, @{thm UN_upper} RS subset_trans))
             (1 upto n);
-        val Fset_set_thmsss = transpose (map (map mk_set_thms) set_simp_thmss);
+        val Fset_set_thmsss = transpose (map (map mk_set_thms) ctor_set_thmss);
 
         val timer = time (timer "set functions for the new datatypes");
 
@@ -1529,7 +1535,7 @@
                 singleton (Proof_Context.export names_lthy lthy)
                   (Skip_Proof.prove lthy [] [] goal (mk_tac induct csets ctor_sets i))
                 |> Thm.close_derivation)
-              goals csetss set_simp_thmss inducts ls;
+              goals csetss ctor_set_thmss inducts ls;
           in
             map split_conj_thm thms
           end;
@@ -1556,7 +1562,7 @@
                 singleton (Proof_Context.export names_lthy lthy)
                   (Skip_Proof.prove lthy [] [] goal (mk_tac induct ctor_sets i))
                 |> Thm.close_derivation)
-              goals set_simp_thmss inducts ls;
+              goals ctor_set_thmss inducts ls;
           in
             map split_conj_thm thms
           end;
@@ -1654,7 +1660,7 @@
             val thm = singleton (Proof_Context.export names_lthy lthy)
               (Skip_Proof.prove lthy [] [] goal
               (K (mk_lfp_map_wpull_tac m (rtac induct) map_wpulls ctor_map_thms
-                (transpose set_simp_thmss) Fset_set_thmsss ctor_inject_thms)))
+                (transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
               |> Thm.close_derivation;
           in
             split_conj_thm thm
@@ -1704,7 +1710,7 @@
               ctors (0 upto n - 1) witss
           end;
 
-        fun wit_tac _ = mk_wit_tac n (flat set_simp_thmss) (maps wit_thms_of_bnf bnfs);
+        fun wit_tac _ = mk_wit_tac n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
 
         val (Ibnfs, lthy) =
           fold_map6 (fn tacs => fn b => fn mapx => fn sets => fn T => fn wits => fn lthy =>
@@ -1714,10 +1720,10 @@
           tacss bs fs_maps setss_by_bnf Ts ctor_witss lthy;
 
         val fold_maps = fold_thms lthy (map (fn bnf =>
-          mk_unabs_def m (map_def_of_bnf bnf RS @{thm meta_eq_to_obj_eq})) Ibnfs);
+          mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
 
         val fold_sets = fold_thms lthy (maps (fn bnf =>
-          map (fn thm => thm RS @{thm meta_eq_to_obj_eq}) (set_defs_of_bnf bnf)) Ibnfs);
+          map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Ibnfs);
 
         val timer = time (timer "registered new datatypes as BNFs");
 
@@ -1740,8 +1746,8 @@
         val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
         val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
         val folded_ctor_map_thms = map fold_maps ctor_map_thms;
-        val folded_set_simp_thmss = map (map fold_sets) set_simp_thmss;
-        val folded_set_simp_thmss' = transpose folded_set_simp_thmss;
+        val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
+        val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
 
         val ctor_Isrel_thms =
           let
@@ -1757,7 +1763,7 @@
                (K (mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets
                  ctor_inject ctor_dtor set_naturals ctor_set_incls ctor_set_set_inclss))
               |> Thm.close_derivation)
-            ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_set_simp_thmss'
+            ks goals in_srels map_comp's map_congs folded_ctor_map_thms folded_ctor_set_thmss'
               ctor_inject_thms ctor_dtor_thms set_natural'ss ctor_set_incl_thmss
               ctor_set_set_incl_thmsss
           end;
@@ -1793,13 +1799,14 @@
              [(ctor_srelN, map single ctor_Isrel_thms)]
            else
              []) @
-          map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_set_simp_thmss
+          map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss
           |> maps (fn (thmN, thmss) =>
             map2 (fn b => fn thms =>
               ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
             bs thmss)
       in
-        timer; (Irels, lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
+        timer; (Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
+          lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd)
       end;
 
       val common_notes =
@@ -1824,8 +1831,9 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((dtors, ctors, Irels, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms,
-      ctor_inject_thms, ctor_fold_thms, ctor_rec_thms),
+    ((Ibnfs, dtors, ctors, folds, recs, ctor_induct_thm, dtor_ctor_thms, ctor_dtor_thms,
+      ctor_inject_thms, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms,
+      ctor_fold_thms, ctor_rec_thms),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
@@ -1834,10 +1842,10 @@
     "define BNF-based inductive datatypes (low-level)"
     (Parse.and_list1
       ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
-      (snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
+      (snd oo fp_bnf_cmd construct_lfp o apsnd split_list o split_list));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
-    (parse_datatype_cmd true bnf_lfp);
+    (parse_datatype_cmd true construct_lfp);
 
 end;
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_lfp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -22,6 +22,7 @@
     thm list -> tactic
   val mk_ctor_induct2_tac: ctyp option list -> cterm option list -> thm -> thm list ->
     {prems: 'a, context: Proof.context} -> tactic
+  val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
   val mk_ctor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
     thm list -> thm list -> thm list list -> tactic
   val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -69,7 +70,6 @@
   val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
     thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
   val mk_set_natural_tac: thm -> tactic
-  val mk_set_simp_tac: thm -> thm -> thm list -> tactic
   val mk_set_tac: thm -> tactic
   val mk_wit_tac: int -> thm list -> thm list -> tactic
   val mk_wpull_tac: thm -> tactic
@@ -83,8 +83,6 @@
 open BNF_Util
 
 val fst_snd_convs = @{thms fst_conv snd_conv};
-val id_apply = @{thm id_apply};
-val meta_mp = @{thm meta_mp};
 val ord_eq_le_trans = @{thm ord_eq_le_trans};
 val subset_trans = @{thm subset_trans};
 val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
@@ -594,7 +592,7 @@
 fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
   rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
 
-fun mk_set_simp_tac set set_natural' set_natural's =
+fun mk_ctor_set_tac set set_natural' set_natural's =
   let
     val n = length set_natural's;
     fun mk_UN thm = rtac (thm RS @{thm arg_cong[of _ _ Union]} RS trans) THEN'
@@ -615,9 +613,9 @@
       rtac refl, Goal.assume_rule_tac ctxt, rtac sym, rtac trans, rtac @{thm UN_cong},
       rtac set_nat, rtac refl, rtac @{thm UN_simps(10)}];
 
-    fun mk_set_nat cset ctor_map set_simp set_nats =
-      EVERY' [rtac trans, rtac @{thm image_cong}, rtac set_simp, rtac refl,
-        rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, set_simp RS trans]),
+    fun mk_set_nat cset ctor_map ctor_set set_nats =
+      EVERY' [rtac trans, rtac @{thm image_cong}, rtac ctor_set, rtac refl,
+        rtac sym, rtac (trans OF [ctor_map RS HOL_arg_cong cset, ctor_set RS trans]),
         rtac sym, EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
         rtac sym, rtac (nth set_nats (i - 1)),
         REPEAT_DETERM_N (n - 1) o EVERY' (map rtac (trans :: @{thms image_Un Un_cong})),
@@ -633,8 +631,8 @@
     fun useIH set_bd = EVERY' [rtac @{thm UNION_Cinfinite_bound}, rtac set_bd, rtac ballI,
       Goal.assume_rule_tac ctxt, rtac bd_Cinfinite];
 
-    fun mk_set_nat set_simp set_bds =
-      EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac set_simp,
+    fun mk_set_nat ctor_set set_bds =
+      EVERY' [rtac @{thm ordIso_ordLeq_trans}, rtac @{thm card_of_ordIso_subst}, rtac ctor_set,
         rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})), rtac (nth set_bds (i - 1)),
         REPEAT_DETERM_N (n - 1) o rtac (bd_Cinfinite RSN (3, @{thm Un_Cinfinite_bound})),
         EVERY' (map useIH (drop m set_bds))];
@@ -759,15 +757,15 @@
   EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
     rtac wpull, REPEAT_DETERM o atac] 1;
 
-fun mk_wit_tac n set_simp wit =
+fun mk_wit_tac n ctor_set wit =
   REPEAT_DETERM (atac 1 ORELSE
-    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+    EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
     REPEAT_DETERM o
       (TRY o REPEAT_DETERM o etac UnE THEN' TRY o etac @{thm UN_E} THEN'
         (eresolve_tac wit ORELSE'
         (dresolve_tac wit THEN'
           (etac FalseE ORELSE'
-          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac set_simp,
+          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
             REPEAT_DETERM_N n o etac UnE]))))] 1);
 
 fun mk_ctor_srel_tac in_Isrels i in_srel map_comp map_cong ctor_map ctor_sets ctor_inject
@@ -806,8 +804,8 @@
     val only_if_tac =
       EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
         rtac (in_Isrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
-        CONJ_WRAP' (fn (set_simp, passive_set_natural) =>
-          EVERY' [rtac ord_eq_le_trans, rtac set_simp, rtac @{thm Un_least},
+        CONJ_WRAP' (fn (ctor_set, passive_set_natural) =>
+          EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
             rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
             rtac passive_set_natural, rtac trans_fun_cong_image_id_id_apply, atac,
             CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_util.ML
--- a/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -121,13 +121,16 @@
   val mk_ordLeq_csum: int -> int -> thm -> thm
   val mk_UnIN: int -> int -> thm
 
+  val Pair_eqD: thm
+  val Pair_eqI: thm
   val ctrans: thm
+  val id_apply: thm
+  val meta_mp: thm
+  val meta_spec: thm
   val o_apply: thm
   val set_mp: thm
   val set_rev_mp: thm
   val subset_UNIV: thm
-  val Pair_eqD: thm
-  val Pair_eqI: thm
   val mk_sym: thm -> thm
   val mk_trans: thm -> thm -> thm
   val mk_unabs_def: int -> thm -> thm
@@ -136,6 +139,7 @@
   val no_refl: thm list -> thm list
   val no_reflexive: thm list -> thm list
 
+  val cterm_instantiate_pos: cterm option list -> thm -> thm
   val fold_thms: Proof.context -> thm list -> thm -> thm
   val unfold_thms: Proof.context -> thm list -> thm -> thm
 
@@ -525,13 +529,16 @@
 fun mk_sym thm = sym OF [thm];
 
 (*TODO: antiquote heavily used theorems once*)
+val Pair_eqD = @{thm iffD1[OF Pair_eq]};
+val Pair_eqI = @{thm iffD2[OF Pair_eq]};
 val ctrans = @{thm ordLeq_transitive};
+val id_apply = @{thm id_apply};
+val meta_mp = @{thm meta_mp};
+val meta_spec = @{thm meta_spec};
 val o_apply = @{thm o_apply};
 val set_mp = @{thm set_mp};
 val set_rev_mp = @{thm set_rev_mp};
 val subset_UNIV = @{thm subset_UNIV};
-val Pair_eqD = @{thm iffD1[OF Pair_eq]};
-val Pair_eqI = @{thm iffD2[OF Pair_eq]};
 
 fun mk_nthN 1 t 1 = t
   | mk_nthN _ t 1 = HOLogic.mk_fst t
@@ -607,8 +614,7 @@
       map (f false) negs @ [f true pos]
     end;
 
-fun mk_unabs_def 0 thm = thm
-  | mk_unabs_def n thm = mk_unabs_def (n - 1) thm RS @{thm spec[OF iffD1[OF fun_eq_iff]]};
+fun mk_unabs_def n = funpow n (fn thm => thm RS fun_cong);
 
 fun is_refl thm =
   op aconv (HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.prop_of thm)))
@@ -617,6 +623,17 @@
 val no_refl = filter_out is_refl;
 val no_reflexive = filter_out Thm.is_reflexive;
 
+fun cterm_instantiate_pos cts thm =
+  let
+    val cert = Thm.cterm_of (Thm.theory_of_thm thm);
+    val vars = Term.add_vars (prop_of thm) [];
+    val vars' = rev (drop (length vars - length cts) vars);
+    val ps = map_filter (fn (_, NONE) => NONE
+      | (var, SOME ct) => SOME (cert (Var var), ct)) (vars' ~~ cts);
+  in
+    Drule.cterm_instantiate ps thm
+  end;
+
 fun fold_thms ctxt thms = Local_Defs.fold ctxt (distinct Thm.eq_thm_prop thms);
 fun unfold_thms ctxt thms = Local_Defs.unfold ctxt (distinct Thm.eq_thm_prop thms);
 
diff -r 4339aa335355 -r 5c4a12550491 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Wed Sep 26 10:00:59 2012 +0200
@@ -7,10 +7,14 @@
 
 signature BNF_WRAP =
 sig
-  val mk_half_pairss: 'a list -> ('a * 'a) list list
+  val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
+  val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
+
   val mk_ctr: typ list -> term -> term
   val mk_disc_or_sel: typ list -> term -> term
+
   val base_name_of_ctr: term -> string
+
   val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
     ((bool * term list) * term) *
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
@@ -60,11 +64,11 @@
 
 fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
 
-fun mk_half_pairss' _ [] = []
-  | mk_half_pairss' indent (x :: xs) =
-    indent @ fold_rev (cons o single o pair x) xs (mk_half_pairss' ([] :: indent) xs);
+fun mk_half_pairss' _ ([], []) = []
+  | mk_half_pairss' indent (x :: xs, y :: ys) =
+    indent @ fold_rev (cons o single o pair x) ys (mk_half_pairss' ([] :: indent) (xs, ys));
 
-fun mk_half_pairss xs = mk_half_pairss' [[]] xs;
+fun mk_half_pairss p = mk_half_pairss' [[]] p;
 
 fun join_halves n half_xss other_half_xss =
   let
@@ -72,7 +76,7 @@
       map2 (map2 append) (Library.chop_groups n half_xss)
         (transpose (Library.chop_groups n other_half_xss))
     val xs = interleave (flat half_xss) (flat other_half_xss);
-  in (xs, xsss |> `transpose) end;
+  in (xs, xsss) end;
 
 fun mk_undefined T = Const (@{const_name undefined}, T);
 
@@ -337,7 +341,7 @@
           fold_rev Logic.all (xs @ xs')
             (HOLogic.mk_Trueprop (HOLogic.mk_not (HOLogic.mk_eq (xc, xc'))));
       in
-        map (map mk_goal) (mk_half_pairss (xss ~~ xctrs))
+        map (map mk_goal) (mk_half_pairss (`I (xss ~~ xctrs)))
       end;
 
     val cases_goal =
@@ -366,7 +370,7 @@
         val other_half_distinct_thmss = map (map (fn thm => thm RS not_sym)) half_distinct_thmss;
 
         val (distinct_thms, (distinct_thmsss', distinct_thmsss)) =
-          join_halves n half_distinct_thmss other_half_distinct_thmss;
+          join_halves n half_distinct_thmss other_half_distinct_thmss ||> `transpose;
 
         val nchotomy_thm =
           let
@@ -463,8 +467,7 @@
 
                   fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
 
-                  val infos = ms ~~ discD_thms ~~ udiscs;
-                  val half_pairss = mk_half_pairss infos;
+                  val half_pairss = mk_half_pairss (`I (ms ~~ discD_thms ~~ udiscs));
 
                   val half_goalss = map mk_goal half_pairss;
                   val half_thmss =
@@ -477,7 +480,7 @@
                     map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
                       other_half_goalss;
                 in
-                  join_halves n half_thmss other_half_thmss
+                  join_halves n half_thmss other_half_thmss ||> `transpose
                   |>> has_alternate_disc_def ? K []
                 end;