merged
authorwenzelm
Tue, 12 Aug 2014 20:42:39 +0200
changeset 57919 a2a7c1de4752
parent 57898 f7f75b33d6c8 (diff)
parent 57918 f5d73caba4e5 (current diff)
child 57920 c1953856cfca
merged
src/Pure/GUI/jfx_thread.scala
src/Pure/System/isabelle_font.scala
--- a/src/Doc/Datatypes/Datatypes.thy	Tue Aug 12 20:18:27 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Tue Aug 12 20:42:39 2014 +0200
@@ -858,9 +858,16 @@
 @{thm list.set(1)[no_vars]} \\
 @{thm list.set(2)[no_vars]}
 
+\item[@{text "t."}\hthm{set_cases}\rm:] ~ \\
+@{thm list.set_cases[no_vars]}
+
 \item[@{text "t."}\hthm{set_empty}\rm:] ~ \\
 @{thm list.set_empty[no_vars]}
 
+\item[@{text "t."}\hthm{set_intros}\rm:] ~ \\
+@{thm list.set_intros(1)[no_vars]} \\
+@{thm list.set_intros(2)[no_vars]}
+
 \item[@{text "t."}\hthm{sel_set}\rm:] ~ \\
 @{thm list.sel_set[no_vars]}
 
--- a/src/HOL/BNF_GFP.thy	Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/BNF_GFP.thy	Tue Aug 12 20:42:39 2014 +0200
@@ -22,33 +22,33 @@
 *}
 
 lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
+  by simp
 
 lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (cases s) auto
+  by (cases s) auto
 
 lemma not_TrueE: "\<not> True \<Longrightarrow> P"
-by (erule notE, rule TrueI)
+  by (erule notE, rule TrueI)
 
 lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
-by fast
+  by fast
 
 lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
-by (auto split: sum.splits)
+  by (auto split: sum.splits)
 
 lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
-apply rule
- apply (rule ext, force split: sum.split)
-by (rule ext, metis case_sum_o_inj(2))
+  apply rule
+   apply (rule ext, force split: sum.split)
+  by (rule ext, metis case_sum_o_inj(2))
 
 lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
-by fast
+  by fast
 
 lemma equiv_proj:
-  assumes e: "equiv A R" and "z \<in> R"
+  assumes e: "equiv A R" and m: "z \<in> R"
   shows "(proj R o fst) z = (proj R o snd) z"
 proof -
-  from assms(2) have z: "(fst z, snd z) \<in> R" by auto
+  from m have z: "(fst z, snd z) \<in> R" by auto
   with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
     unfolding equiv_def sym_def trans_def by blast+
   then show ?thesis unfolding proj_def[abs_def] by auto
@@ -58,93 +58,93 @@
 definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
 
 lemma Id_on_Gr: "Id_on A = Gr A id"
-unfolding Id_on_def Gr_def by auto
+  unfolding Id_on_def Gr_def by auto
 
 lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
-unfolding image2_def by auto
+  unfolding image2_def by auto
 
 lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
-by auto
+  by auto
 
 lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
-unfolding image2_def Gr_def by auto
+  unfolding image2_def Gr_def by auto
 
 lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
-unfolding Gr_def by simp
+  unfolding Gr_def by simp
 
 lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
-unfolding Gr_def by simp
+  unfolding Gr_def by simp
 
 lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
-unfolding Gr_def by auto
+  unfolding Gr_def by auto
 
 lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
-by blast
+  by blast
 
 lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
-by blast
+  by blast
 
 lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
-unfolding fun_eq_iff by auto
+  unfolding fun_eq_iff by auto
 
 lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
-by auto
+  by auto
 
 lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
-by force
+  by force
 
 lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
-unfolding fun_eq_iff by auto
+  unfolding fun_eq_iff by auto
 
 lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
-unfolding fun_eq_iff by auto
+  unfolding fun_eq_iff by auto
 
 lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
-unfolding Gr_def Grp_def fun_eq_iff by auto
+  unfolding Gr_def Grp_def fun_eq_iff by auto
 
 definition relImage where
-"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
+  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
 
 definition relInvImage where
-"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
+  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
 
 lemma relImage_Gr:
-"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
-unfolding relImage_def Gr_def relcomp_def by auto
+  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
+  unfolding relImage_def Gr_def relcomp_def by auto
 
 lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
-unfolding Gr_def relcomp_def image_def relInvImage_def by auto
+  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
 
 lemma relImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
-unfolding relImage_def by auto
+  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
+  unfolding relImage_def by auto
 
 lemma relInvImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
-unfolding relInvImage_def by auto
+  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
+  unfolding relInvImage_def by auto
 
 lemma relInvImage_Id_on:
-"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
-unfolding relInvImage_def Id_on_def by auto
+  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
+  unfolding relInvImage_def Id_on_def by auto
 
 lemma relInvImage_UNIV_relImage:
-"R \<subseteq> relInvImage UNIV (relImage R f) f"
-unfolding relInvImage_def relImage_def by auto
+  "R \<subseteq> relInvImage UNIV (relImage R f) f"
+  unfolding relInvImage_def relImage_def by auto
 
 lemma relImage_proj:
-assumes "equiv A R"
-shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
-unfolding relImage_def Id_on_def
-using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
-by (auto simp: proj_preserves)
+  assumes "equiv A R"
+  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
+  unfolding relImage_def Id_on_def
+  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
+  by (auto simp: proj_preserves)
 
 lemma relImage_relInvImage:
-assumes "R \<subseteq> f ` A <*> f ` A"
-shows "relImage (relInvImage A R f) f = R"
-using assms unfolding relImage_def relInvImage_def by fast
+  assumes "R \<subseteq> f ` A <*> f ` A"
+  shows "relImage (relInvImage A R f) f = R"
+  using assms unfolding relImage_def relInvImage_def by fast
 
 lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
-by simp
+  by simp
 
 lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
 lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
@@ -159,76 +159,75 @@
 definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
 
 lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
-unfolding Shift_def Succ_def by simp
+  unfolding Shift_def Succ_def by simp
 
 lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
-unfolding Succ_def by simp
+  unfolding Succ_def by simp
 
 lemmas SuccE = SuccD[elim_format]
 
 lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
-unfolding Succ_def by simp
+  unfolding Succ_def by simp
 
 lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
-unfolding Shift_def by simp
+  unfolding Shift_def by simp
 
 lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
-unfolding Succ_def Shift_def by auto
+  unfolding Succ_def Shift_def by auto
 
 lemma length_Cons: "length (x # xs) = Suc (length xs)"
-by simp
+  by simp
 
 lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
-by simp
+  by simp
 
 (*injection into the field of a cardinal*)
 definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
 definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
 
 lemma ex_toCard_pred:
-"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
-unfolding toCard_pred_def
-using card_of_ordLeq[of A "Field r"]
-      ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
-by blast
+  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
+  unfolding toCard_pred_def
+  using card_of_ordLeq[of A "Field r"]
+    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
+  by blast
 
 lemma toCard_pred_toCard:
   "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
-unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
+  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
 
-lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
-  toCard A r x = toCard A r y \<longleftrightarrow> x = y"
-using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
+lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
+  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
 
 definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
 
 lemma fromCard_toCard:
-"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
-unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
+  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
+  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
 
 lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
+  unfolding Field_card_of csum_def by auto
 
 lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
+  unfolding Field_card_of csum_def by auto
 
 lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
-by auto
+  by auto
 
 lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
-by auto
+  by auto
 
 lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
-by auto
+  by auto
 
 lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
-by auto
+  by auto
 
 lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
-by simp
+  by simp
 
 lemma Collect_splitD: "x \<in> Collect (split A) \<Longrightarrow> A (fst x) (snd x)"
-by auto
+  by auto
 
 definition image2p where
   "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
@@ -250,20 +249,21 @@
 
 lemma equiv_Eps_in:
 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
-apply (rule someI2_ex)
-using in_quotient_imp_non_empty by blast
+  apply (rule someI2_ex)
+  using in_quotient_imp_non_empty by blast
 
 lemma equiv_Eps_preserves:
-assumes ECH: "equiv A r" and X: "X \<in> A//r"
-shows "Eps (%x. x \<in> X) \<in> A"
-apply (rule in_mono[rule_format])
- using assms apply (rule in_quotient_imp_subset)
-by (rule equiv_Eps_in) (rule assms)+
+  assumes ECH: "equiv A r" and X: "X \<in> A//r"
+  shows "Eps (%x. x \<in> X) \<in> A"
+  apply (rule in_mono[rule_format])
+   using assms apply (rule in_quotient_imp_subset)
+  by (rule equiv_Eps_in) (rule assms)+
 
 lemma proj_Eps:
-assumes "equiv A r" and "X \<in> A//r"
-shows "proj r (Eps (%x. x \<in> X)) = X"
-unfolding proj_def proof auto
+  assumes "equiv A r" and "X \<in> A//r"
+  shows "proj r (Eps (%x. x \<in> X)) = X"
+unfolding proj_def
+proof auto
   fix x assume x: "x \<in> X"
   thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
 next
@@ -276,7 +276,7 @@
 lemma univ_commute:
 assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
 shows "(univ f) (proj r x) = f x"
-unfolding univ_def proof -
+proof (unfold univ_def)
   have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
@@ -285,9 +285,8 @@
 qed
 
 lemma univ_preserves:
-assumes ECH: "equiv A r" and RES: "f respects r" and
-        PRES: "\<forall> x \<in> A. f x \<in> B"
-shows "\<forall>X \<in> A//r. univ f X \<in> B"
+  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall> x \<in> A. f x \<in> B"
+  shows "\<forall>X \<in> A//r. univ f X \<in> B"
 proof
   fix X assume "X \<in> A//r"
   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Tue Aug 12 20:42:39 2014 +0200
@@ -102,7 +102,9 @@
 val disc_map_iffN = "disc_map_iff";
 val sel_mapN = "sel_map";
 val sel_setN = "sel_set";
+val set_casesN = "set_cases";
 val set_emptyN = "set_empty";
+val set_introsN = "set_intros";
 val set_inductN = "set_induct";
 
 structure Data = Generic_Data
@@ -113,6 +115,12 @@
   fun merge data : T = Symtab.merge (K true) data;
 );
 
+fun zipping_map f =
+  let
+    fun zmap _ [] = []
+      | zmap xs (y :: ys) = f (xs, y, ys) :: zmap (xs @ [y]) ys
+  in zmap [] end;
+
 fun choose_binary_fun fs AB =
   find_first (fastype_of #> binder_types #> (fn [A, B] => AB = (A, B))) fs;
 fun build_binary_fun_app fs a b =
@@ -501,10 +509,10 @@
     val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
       (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts) IRs));
 
-    val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
-      (fn {context = ctxt, prems = prems} =>
-          mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
-            ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
+    val rel_induct0_thm =
+      Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems} =>
+        mk_rel_induct0_tac ctxt ctor_rel_induct prems (map (certify ctxt) IRs) exhausts ctor_defss
+          ctor_injects pre_rel_defs abs_inverses live_nesting_rel_eqs)
       |> singleton (Proof_Context.export names_lthy lthy)
       |> Thm.close_derivation;
   in
@@ -752,12 +760,12 @@
     val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
       IRs (map2 (build_the_rel lthy (Rs @ IRs) []) fpA_Ts fpB_Ts)));
 
-    val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
-      (fn {context = ctxt, prems = prems} =>
-          mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
-            (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
-            (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
-            rel_pre_defs abs_inverses live_nesting_rel_eqs)
+    val rel_coinduct0_thm =
+      Goal.prove_sorry lthy [] premises goal (fn {context = ctxt, prems} =>
+        mk_rel_coinduct0_tac ctxt dtor_rel_coinduct (map (certify ctxt) IRs) prems
+          (map #exhaust ctr_sugars) (map (flat o #disc_thmss) ctr_sugars)
+          (map (flat o #sel_thmss) ctr_sugars) ctor_defss dtor_ctors ctor_injects abs_injects
+          rel_pre_defs abs_inverses live_nesting_rel_eqs)
       |> singleton (Proof_Context.export names_lthy lthy)
       |> Thm.close_derivation;
   in
@@ -771,7 +779,7 @@
   let
     fun mk_prems A Ps ctr_args t ctxt =
       (case fastype_of t of
-        Type (type_name, xs) =>
+        Type (type_name, innerTs) =>
         (case bnf_of ctxt type_name of
           NONE => ([], ctxt)
         | SOME bnf =>
@@ -794,7 +802,7 @@
                    ctxt'))
               end;
           in
-            fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
+            fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt
             |>> flat
           end)
       | T =>
@@ -803,7 +811,7 @@
 
     fun mk_prems_for_ctr A Ps ctr ctxt =
       let
-        val (args, ctxt') = mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt;
+        val (args, ctxt') = mk_Frees "z" (binder_types (fastype_of ctr)) ctxt;
       in
         fold_map (mk_prems A Ps (list_comb (ctr, args))) args ctxt'
         |>> map (fold_rev Logic.all args) o flat
@@ -835,10 +843,11 @@
           |>> apfst (apsnd (Library.foldr1 HOLogic.mk_conj))
           |>> apsnd flat;
 
-        val thm =  Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion)
-          (fn {context = ctxt, prems = prems} =>
-             mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
-              set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
+        val thm =
+          Goal.prove_sorry lthy [] premises (HOLogic.mk_Trueprop conclusion)
+            (fn {context = ctxt, prems} =>
+               mk_set_induct0_tac ctxt (map (certify ctxt'') Ps) prems dtor_set_inducts exhausts
+                 set_pre_defs ctor_defs dtor_ctors Abs_pre_inverses)
           |> singleton (Proof_Context.export ctxt'' ctxt)
           |> Thm.close_derivation;
 
@@ -1267,6 +1276,7 @@
         disc_bindings), sel_bindingss), raw_sel_default_eqs) no_defs_lthy =
       let
         val fp_b_name = Binding.name_of fp_b;
+        val fpBT = B_ify fpT;
 
         val ctr_absT = domain_type (fastype_of ctor);
 
@@ -1389,11 +1399,10 @@
                          else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans))))
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);
 
-
               fun mk_set0_thm fp_set_thm ctr_def' cxIn =
                 fold_thms lthy [ctr_def']
                   (unfold_thms lthy (pre_set_defs @ fp_nesting_set_maps @ live_nesting_set_maps @
-                       (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_set @
+                       (if fp = Least_FP then [] else [dtor_ctor]) @ basic_sumprod_thms_set @
                        @{thms UN_Un sup_assoc[THEN sym]} @ abs_inverses)
                      (cterm_instantiate_pos [SOME cxIn] fp_set_thm))
                 |> singleton (Proof_Context.export names_lthy no_defs_lthy);
@@ -1438,9 +1447,9 @@
                     Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                       (fn {context = ctxt, prems = _} =>
                         mk_set_empty_tac ctxt (certify ctxt u) exhaust set0_thms (flat disc_thmss))
-                      |> Conjunction.elim_balanced (length goals)
-                      |> Proof_Context.export names_lthy lthy
-                      |> map Thm.close_derivation
+                    |> Conjunction.elim_balanced (length goals)
+                    |> Proof_Context.export names_lthy lthy
+                    |> map Thm.close_derivation
                 end;
 
               val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
@@ -1489,31 +1498,136 @@
                 map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
                   rel_inject_thms ms;
 
-              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms,
-                (rel_cases_thm, rel_cases_attrs)) =
+              val (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
+                   (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs)) =
                 let
-                  val (((Ds, As), Bs), names_lthy) = lthy
-                    |> mk_TFrees (dead_of_bnf fp_bnf)
-                    ||>> mk_TFrees (live_of_bnf fp_bnf)
-                    ||>> mk_TFrees (live_of_bnf fp_bnf);
-                  val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
-                  val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
-                  val fTs = map2 (curry op -->) As Bs;
-                  val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
-                  val ((((fs, Rs), ta), tb), names_lthy) = names_lthy
+                  val live_AsBs = filter (op <>) (As ~~ Bs);
+                  val fTs = map (op -->) live_AsBs;
+                  val rel = mk_rel live As Bs (rel_of_bnf fp_bnf);
+                  val (((((fs, Rs), ta), tb), thesis), names_lthy) = names_lthy
                     |> mk_Frees "f" fTs
-                    ||>> mk_Frees "R" (map2 mk_pred2T As Bs)
-                    ||>> yield_singleton (mk_Frees "a") TA
-                    ||>> yield_singleton (mk_Frees "b") TB;
-                  val map_term = mk_map_of_bnf Ds As Bs fp_bnf;
-                  val discAs = map (mk_disc_or_sel ADs) discs;
-                  val selAss = map (map (mk_disc_or_sel ADs)) selss;
+                    ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
+                    ||>> yield_singleton (mk_Frees "a") fpT
+                    ||>> yield_singleton (mk_Frees "b") fpBT
+                    ||>> apfst HOLogic.mk_Trueprop o
+                      yield_singleton (mk_Frees "thesis") HOLogic.boolT;
+                  val map_term = mk_map live As Bs (map_of_bnf fp_bnf);
+                  val ctrAs = map (mk_ctr As) ctrs;
+                  val setAs = map (mk_set As) (sets_of_bnf fp_bnf);
+                  val discAs = map (mk_disc_or_sel As) discs;
+                  val selAss = map (map (mk_disc_or_sel As)) selss;
                   val discAs_selAss = flat (map2 (map o pair) discAs selAss);
 
+                  val (set_cases_thms, set_cases_attrss) =
+                    let
+                      fun mk_prems assms elem t ctxt =
+                        (case fastype_of t of
+                          Type (type_name, xs) =>
+                          (case bnf_of ctxt type_name of
+                            NONE => ([], ctxt)
+                          | SOME bnf =>
+                            apfst flat (fold_map (fn set => fn ctxt =>
+                              let
+                                val X = HOLogic.dest_setT (range_type (fastype_of set));
+                                val new_var = not (X = fastype_of elem);
+                                val (x, ctxt') =
+                                  if new_var then yield_singleton (mk_Frees "x") X ctxt
+                                  else (elem, ctxt);
+                              in
+                                mk_prems (mk_Trueprop_mem (x, set $ t) :: assms) elem x ctxt'
+                                |>> map (if new_var then Logic.all x else I)
+                              end) (map (mk_set xs) (sets_of_bnf bnf)) ctxt))
+                        | T => rpair ctxt
+                          (if T = fastype_of elem then [fold (curry Logic.mk_implies) assms thesis]
+                           else []));
+                    in
+                      split_list (map (fn set =>
+                        let
+                          val A = HOLogic.dest_setT (range_type (fastype_of set));
+                          val (elem, names_lthy) = yield_singleton (mk_Frees "e") A names_lthy;
+                          val premss =
+                            map (fn ctr =>
+                              let
+                                val (args, names_lthy) =
+                                  mk_Frees "z" (binder_types (fastype_of ctr)) names_lthy;
+                              in
+                                flat (zipping_map (fn (prev_args, arg, next_args) =>
+                                  let
+                                    val (args_with_elem, args_without_elem) =
+                                      if fastype_of arg = A then
+                                        (prev_args @ [elem] @ next_args, prev_args @ next_args)
+                                      else
+                                        `I (prev_args @ [arg] @ next_args);
+                                  in
+                                    mk_prems
+                                      [mk_Trueprop_eq (ta, Term.list_comb (ctr, args_with_elem))]
+                                      elem arg names_lthy
+                                    |> fst
+                                    |> map (fold_rev Logic.all args_without_elem)
+                                  end) args)
+                              end) ctrAs;
+                          val goal = Logic.mk_implies (mk_Trueprop_mem (elem, set $ ta), thesis);
+                          val thm =
+                            Goal.prove_sorry lthy [] (flat premss) goal
+                              (fn {context = ctxt, prems} =>
+                                mk_set_cases_tac ctxt (certify ctxt ta) prems exhaust set_thms)
+                            |> singleton (Proof_Context.export names_lthy lthy)
+                            |> Thm.close_derivation
+                            |> rotate_prems ~1;
+                        in
+                          (thm, [](* TODO: [@{attributes [elim?]},
+                            Attrib.internal (K (Induct.cases_pred (name_of_set set)))] *))
+                        end) setAs)
+                    end;
+
+                  val set_intros_thms =
+                    let
+                      fun mk_goals A setA ctr_args t ctxt =
+                        (case fastype_of t of
+                          Type (type_name, innerTs) =>
+                          (case bnf_of ctxt type_name of
+                            NONE => ([], ctxt)
+                          | SOME bnf =>
+                            apfst flat (fold_map (fn set => fn ctxt =>
+                              let
+                                val X = HOLogic.dest_setT (range_type (fastype_of set));
+                                val (x, ctxt') = yield_singleton (mk_Frees "x") X ctxt;
+                                val assm = mk_Trueprop_mem (x, set $ t);
+                              in
+                                apfst (map (Logic.mk_implies o pair assm))
+                                  (mk_goals A setA ctr_args x ctxt')
+                              end) (map (mk_set innerTs) (sets_of_bnf bnf)) ctxt))
+                        | T =>
+                          (if T = A then [mk_Trueprop_mem (t, setA $ ctr_args)] else [], ctxt));
+
+                      val (goals, names_lthy) =
+                        apfst flat (fold_map (fn set => fn ctxt =>
+                          let
+                            val A = HOLogic.dest_setT (range_type (fastype_of set));
+                          in
+                            apfst flat (fold_map (fn ctr => fn ctxt =>
+                              let
+                                val (args, ctxt') =
+                                  mk_Frees "arg" (binder_types (fastype_of ctr)) ctxt;
+                                val ctr_args = Term.list_comb (ctr, args);
+                              in
+                                apfst flat (fold_map (mk_goals A set ctr_args) args ctxt')
+                              end) ctrAs ctxt)
+                          end) setAs lthy);
+                    in
+                      if null goals then []
+                      else
+                        Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
+                          (fn {context = ctxt, prems = _} => mk_set_intros_tac ctxt set0_thms)
+                        |> Conjunction.elim_balanced (length goals)
+                        |> Proof_Context.export names_lthy lthy
+                        |> map Thm.close_derivation
+                    end;
+
                   val rel_sel_thms =
                     let
-                      val discBs = map (mk_disc_or_sel BDs) discs;
-                      val selBss = map (map (mk_disc_or_sel BDs)) selss;
+                      val discBs = map (mk_disc_or_sel Bs) discs;
+                      val selBss = map (map (mk_disc_or_sel Bs)) selss;
                       val n = length discAs;
 
                       fun mk_rhs n k discA selAs discB selBs =
@@ -1539,18 +1653,15 @@
                             mk_rel_sel_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
                               (flat disc_thmss) (flat sel_thmss) rel_inject_thms distincts
                               rel_distinct_thms)
-                          |> Conjunction.elim_balanced (length goals)
-                          |> Proof_Context.export names_lthy lthy
+                        |> Conjunction.elim_balanced (length goals)
+                        |> Proof_Context.export names_lthy lthy
+                        |> map Thm.close_derivation
                     end;
 
                   val (rel_cases_thm, rel_cases_attrs) =
                     let
-                      val (thesis, names_lthy) = apfst HOLogic.mk_Trueprop
-                        (yield_singleton (mk_Frees "thesis") HOLogic.boolT names_lthy);
-
                       val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb;
-                      val ctrAs = map (mk_ctr ADs) ctrs;
-                      val ctrBs = map (mk_ctr BDs) ctrs;
+                      val ctrBs = map (mk_ctr Bs) ctrs;
 
                       fun mk_assms ctrA ctrB ctxt =
                         let
@@ -1572,9 +1683,10 @@
                         end;
 
                       val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy;
-                      val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms,
-                        thesis);
-                      val thm = Goal.prove_sorry lthy [] [] goal
+                      val goal =
+                        Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
+                      val thm =
+                        Goal.prove_sorry lthy [] [] goal
                           (fn {context = ctxt, prems = _} =>
                             mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
                               injects rel_inject_thms distincts rel_distinct_thms
@@ -1592,7 +1704,7 @@
 
                   val disc_map_iff_thms =
                     let
-                      val discsB = map (mk_disc_or_sel BDs) discs;
+                      val discsB = map (mk_disc_or_sel Bs) discs;
                       val discsA_t = map (fn disc1 => Term.betapply (disc1, ta)) discAs;
 
                       fun mk_goal (discA_t, discB) =
@@ -1611,8 +1723,9 @@
                           (fn {context = ctxt, prems = _} =>
                             mk_disc_map_iff_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
                               map_thms)
-                          |> Conjunction.elim_balanced (length goals)
-                          |> Proof_Context.export names_lthy lthy
+                        |> Conjunction.elim_balanced (length goals)
+                        |> Proof_Context.export names_lthy lthy
+                        |> map Thm.close_derivation
                     end;
 
                   val sel_map_thms =
@@ -1620,14 +1733,15 @@
                       fun mk_goal (discA, selA) =
                         let
                           val prem = Term.betapply (discA, ta);
-                          val selB = mk_disc_or_sel BDs selA;
+                          val selB = mk_disc_or_sel Bs selA;
                           val lhs = selB $ (Term.list_comb (map_term, fs) $ ta);
                           val lhsT = fastype_of lhs;
-                          val map_rhsT = map_atyps (perhaps (AList.lookup (op =) (Bs ~~ As))) lhsT;
+                          val map_rhsT =
+                            map_atyps (perhaps (AList.lookup (op =) (map swap live_AsBs))) lhsT;
                           val map_rhs = build_map lthy []
-                            (the o (AList.lookup (op =) ((As ~~ Bs) ~~ fs))) (map_rhsT, lhsT);
+                            (the o (AList.lookup (op =) (live_AsBs ~~ fs))) (map_rhsT, lhsT);
                           val rhs = (case map_rhs of
-                            Const (@{const_name id}, _) => selA $ ta
+                              Const (@{const_name id}, _) => selA $ ta
                             | _ => map_rhs $ (selA $ ta));
                           val concl = mk_Trueprop_eq (lhs, rhs);
                         in
@@ -1643,14 +1757,13 @@
                           (fn {context = ctxt, prems = _} =>
                             mk_sel_map_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
                               map_thms (flat sel_thmss))
-                          |> Conjunction.elim_balanced (length goals)
-                          |> Proof_Context.export names_lthy lthy
+                        |> Conjunction.elim_balanced (length goals)
+                        |> Proof_Context.export names_lthy lthy
+                        |> map Thm.close_derivation
                     end;
 
                   val sel_set_thms =
                     let
-                      val setsA = map (mk_set ADs) (sets_of_bnf fp_bnf);
-
                       fun mk_goal discA selA setA ctxt =
                         let
                           val prem = Term.betapply (discA, ta);
@@ -1659,7 +1772,7 @@
 
                           fun travese_nested_types t ctxt =
                             (case fastype_of t of
-                              Type (type_name, xs) =>
+                              Type (type_name, innerTs) =>
                               (case bnf_of ctxt type_name of
                                 NONE => ([], ctxt)
                               | SOME bnf =>
@@ -1674,7 +1787,7 @@
                                       |>> map (Logic.mk_implies o pair assm)
                                     end;
                                 in
-                                  fold_map (seq_assm t o mk_set xs) (sets_of_bnf bnf) ctxt
+                                  fold_map (seq_assm t o mk_set innerTs) (sets_of_bnf bnf) ctxt
                                   |>> flat
                                 end)
                             | T =>
@@ -1699,21 +1812,22 @@
                             ([], ctxt)
                         end;
                       val (goals, names_lthy) = apfst (flat o flat) (fold_map (fn (disc, sel) =>
-                        fold_map (mk_goal disc sel) setsA) discAs_selAss names_lthy);
+                        fold_map (mk_goal disc sel) setAs) discAs_selAss names_lthy);
                     in
                       if null goals then
                         []
                       else
                         Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                           (fn {context = ctxt, prems = _} =>
-                            mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
-                              (flat sel_thmss) set0_thms)
-                          |> Conjunction.elim_balanced (length goals)
-                          |> Proof_Context.export names_lthy lthy
+                             mk_sel_set_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss)
+                               (flat sel_thmss) set0_thms)
+                        |> Conjunction.elim_balanced (length goals)
+                        |> Proof_Context.export names_lthy lthy
+                        |> map Thm.close_derivation
                     end;
                 in
-                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms,
-                    (rel_cases_thm, rel_cases_attrs))
+                  (disc_map_iff_thms, sel_map_thms, sel_set_thms, rel_sel_thms, set_intros_thms,
+                    (set_cases_thms, set_cases_attrss), (rel_cases_thm, rel_cases_attrs))
                 end;
 
               val anonymous_notes =
@@ -1732,7 +1846,9 @@
                  (setN, set_thms, K (code_nitpicksimp_attrs @ simp_attrs)),
                  (sel_mapN, sel_map_thms, K []),
                  (sel_setN, sel_set_thms, K []),
-                 (set_emptyN, set_empty_thms, K [])]
+                 (set_casesN, set_cases_thms, nth set_cases_attrss),
+                 (set_emptyN, set_empty_thms, K []),
+                 (set_introsN, set_intros_thms, K [])]
                 |> massage_simple_notes fp_b_name;
 
               val (noted, lthy') =
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Aug 12 20:42:39 2014 +0200
@@ -10,6 +10,7 @@
 sig
   val sumprod_thms_map: thm list
   val sumprod_thms_set: thm list
+  val basic_sumprod_thms_set: thm list
   val sumprod_thms_rel: thm list
 
   val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
@@ -38,9 +39,11 @@
     thm list -> thm list -> tactic
   val mk_sel_map_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
   val mk_sel_set_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> tactic
+  val mk_set_cases_tac: Proof.context -> cterm -> thm list -> thm -> thm list -> tactic
   val mk_set_empty_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_set_induct0_tac: Proof.context -> cterm list -> thm list -> thm list -> thm list ->
     thm list -> thm list -> thm list -> thm list -> tactic
+  val mk_set_intros_tac: Proof.context -> thm list -> tactic
 end;
 
 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
@@ -56,9 +59,10 @@
 val simp_thms' = @{thms simp_thms(6,7,8,11,12,15,16,22,24)};
 
 val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
-val sumprod_thms_set =
-  @{thms UN_empty UN_insert UN_simps(10) UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
-      image_iff o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
+val basic_sumprod_thms_set =
+  @{thms UN_empty UN_insert  UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib
+       o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
+val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set;
 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
 
 fun hhf_concl_conv cv ctxt ct =
@@ -299,6 +303,14 @@
         hyp_subst_tac ctxt) THEN'
       (rtac @{thm singletonI} ORELSE' atac));
 
+fun mk_set_cases_tac ctxt ct assms exhaust sets =
+  HEADGOAL (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN
+  unfold_thms_tac ctxt sets THEN
+  REPEAT_DETERM (HEADGOAL
+    (eresolve_tac @{thms FalseE emptyE singletonE UnE UN_E insertE} ORELSE'
+     hyp_subst_tac ctxt ORELSE'
+     SELECT_GOAL (SOLVE (HEADGOAL (eresolve_tac assms THEN' REPEAT_DETERM o atac)))));
+
 fun mk_set_empty_tac ctxt ct exhaust sets discs =
   TRYALL Goal.conjunction_tac THEN
   ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
@@ -307,6 +319,13 @@
     SOME (thm RS eqFalseI) handle THM _ => NONE) discs) THEN
   ALLGOALS (rtac refl ORELSE' etac FalseE);
 
+fun mk_set_intros_tac ctxt sets =
+  TRYALL Goal.conjunction_tac THEN
+  unfold_thms_tac ctxt sets THEN
+  TRYALL (REPEAT o
+    (resolve_tac @{thms UnI1 UnI2} ORELSE'
+     eresolve_tac @{thms UN_I UN_I[rotated]}) THEN' (rtac @{thm singletonI} ORELSE' atac));
+
 fun mk_set_induct0_tac ctxt cts assms dtor_set_inducts exhausts set_pre_defs ctor_defs dtor_ctors
     Abs_pre_inverses =
   let
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Aug 12 20:42:39 2014 +0200
@@ -8,6 +8,7 @@
 signature BNF_FP_N2M_SUGAR =
 sig
   val unfold_lets_splits: term -> term
+  val unfold_splits_lets: term -> term
   val dest_map: Proof.context -> string -> term -> term * term list
 
   val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
@@ -60,18 +61,22 @@
   Local_Theory.declaration {syntax = false, pervasive = false}
     (fn phi => Data.map (Typtab.update (key, morph_n2m_sugar phi n2m_sugar)));
 
-fun unfold_lets_splits (Const (@{const_name Let}, _) $ arg1 $ arg2) =
-    unfold_lets_splits (betapply (arg2, arg1))
-  | unfold_lets_splits (t as Const (@{const_name case_prod}, _) $ u) =
-    (case unfold_lets_splits u of
+fun unfold_lets_splits (Const (@{const_name Let}, _) $ t $ u) =
+    unfold_lets_splits (betapply (unfold_splits_lets u, t))
+  | unfold_lets_splits (t $ u) = betapply (unfold_lets_splits t, unfold_lets_splits u)
+  | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
+  | unfold_lets_splits t = t
+and unfold_splits_lets ((t as Const (@{const_name case_prod}, _)) $ u) =
+    (case unfold_splits_lets u of
       u' as Abs (s1, T1, Abs (s2, T2, _)) =>
       let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in
         lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v])))
       end
-    | _ => t)
-  | unfold_lets_splits (t $ u) = betapply (pairself unfold_lets_splits (t, u))
-  | unfold_lets_splits (Abs (s, T, t)) = Abs (s, T, unfold_lets_splits t)
-  | unfold_lets_splits t = t;
+    | _ => t $ unfold_lets_splits u)
+  | unfold_splits_lets (t as Const (@{const_name Let}, _) $ _ $ _) = unfold_lets_splits t
+  | unfold_splits_lets (t $ u) = betapply (unfold_splits_lets t, unfold_lets_splits u)
+  | unfold_splits_lets (Abs (s, T, t)) = Abs (s, T, unfold_splits_lets t)
+  | unfold_splits_lets t = unfold_lets_splits t;
 
 fun mk_map_pattern ctxt s =
   let
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Aug 12 20:18:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Aug 12 20:42:39 2014 +0200
@@ -198,7 +198,7 @@
           end
         | (c as Const (@{const_name case_prod}, _), arg :: args) =>
           massage_rec bound_Ts
-            (unfold_lets_splits (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
+            (unfold_splits_lets (Term.list_comb (c $ Envir.eta_long bound_Ts arg, args)))
         | (Const (c, _), args as _ :: _ :: _) =>
           (case try strip_fun_type (Sign.the_const_type thy c) of
             SOME (gen_branch_Ts, gen_body_fun_T) =>
@@ -694,14 +694,6 @@
         handle ListPair.UnequalLengths =>
           primcorec_error_eqn "partially applied constructor in right-hand side" rhs;
 
-(*
-val _ = tracing ("reduced\n    " ^ Syntax.string_of_term @{context} concl ^ "\nto\n    \<cdot> " ^
- (is_some eqn_data_disc_opt ? K (Syntax.string_of_term @{context} disc_concl ^ "\n    \<cdot> ")) "" ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) sel_concls) ^
- "\nfor premise(s)\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term @{context}) prems));
-*)
-
     val eqns_data_sel =
       map (dissect_coeqn_sel lthy fun_names basic_ctr_specss eqn_pos
         (SOME (abstract (List.rev fun_args) rhs)) code_rhs_opt eqn0 (SOME ctr)) sel_concls;
@@ -890,11 +882,6 @@
       | currys Ts t = t $ mk_tuple1_balanced (List.rev Ts) (map Bound (length Ts - 1 downto 0))
           |> fold_rev (Term.abs o pair Name.uu) Ts;
 
-(*
-val _ = tracing ("corecursor arguments:\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (map (Syntax.string_of_term lthy) corec_args));
-*)
-
     val excludess' =
       disc_eqnss
       |> map (map (fn x => (#fun_args x, #ctr_no x, #prems x, #auto_gen x))
@@ -1006,10 +993,6 @@
       |> map2 (curry (op |>)) (map (map (fn {ctr, sels, ...} =>
         (ctr, map (K []) sels))) basic_ctr_specss);
 
-(*
-val _ = tracing ("callssss = " ^ @{make_string} callssss);
-*)
-
     val ((n2m, corec_specs', _, coinduct_thm, strong_coinduct_thm, coinduct_thms,
           strong_coinduct_thms), lthy') =
       corec_specs_of bs arg_Ts res_Ts frees callssss lthy;
@@ -1051,11 +1034,6 @@
       else
         tac_opt;
 
-(*
-val _ = tracing ("exclusiveness properties:\n    \<cdot> " ^
- space_implode "\n    \<cdot> " (maps (map (Syntax.string_of_term lthy o snd)) excludess'));
-*)
-
     val excludess'' = map3 (fn tac_opt => fn sequential => map (fn (j, goal) =>
         (j, (Option.map (Goal.prove_sorry lthy [] [] goal #> Thm.close_derivation)
            (exclude_tac tac_opt sequential j), goal))))