more careful simplification of sets (cf. abf91ebd0820)---yields smaller terms

--- a/src/HOL/BNF_Comp.thy	Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/BNF_Comp.thy	Thu Mar 06 12:17:26 2014 +0100
@@ -57,14 +57,6 @@
 lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
 by blast
 
-lemma mem_UN_compreh_ex_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
-by blast
-
-lemma UN_compreh_ex_eq_eq:
-"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
-"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
-by blast+
-
 lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
 by (unfold comp_apply collect_def SUP_def)
 

--- a/src/HOL/BNF_FP_Base.thy	Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/BNF_FP_Base.thy	Thu Mar 06 12:17:26 2014 +0100
@@ -98,13 +98,6 @@
 "setr (Inr x) = {x}"
 unfolding sum_set_defs by simp+
 
-lemma UN_compreh_eq_eq:
-"\<Union>{y. y = A} = A"
-by blast+
-
-lemma ex_in_single: "(\<exists>x \<in> {y}. P x) = P y"
-by blast
-
 lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
 by blast
 

--- a/src/HOL/Tools/BNF/bnf_comp.ML	Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Thu Mar 06 12:17:26 2014 +0100
@@ -197,7 +197,8 @@
         val setT = fastype_of set;
         val var_set' = Const (@{const_name id_bnf_comp}, setT --> setT) $ Var ((Name.uu, 0), setT);
         val goal = mk_Trueprop_eq (var_set', set);
-        fun tac {context = ctxt, prems = _} = mk_simplified_set_tac ctxt;
+        fun tac {context = ctxt, prems = _} =
+          mk_simplified_set_tac ctxt (collect_set_map_of_bnf outer);
         val set'_eq_set =
           Goal.prove names_lthy [] [] goal tac
           |> Thm.close_derivation;

--- a/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/Tools/BNF/bnf_comp_tactics.ML	Thu Mar 06 12:17:26 2014 +0100
@@ -31,7 +31,7 @@
   val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
   val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
   val mk_simple_wit_tac: thm list -> tactic
-  val mk_simplified_set_tac: Proof.context -> tactic
+  val mk_simplified_set_tac: Proof.context -> thm -> tactic
   val bd_ordIso_natLeq_tac: tactic
 end;
 
@@ -144,12 +144,13 @@
      rtac @{thm cprod_com}) 1
   end;
 
-val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert
-  Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
+val comp_in_alt_thms = @{thms o_apply collect_def image_insert image_empty Union_insert UN_insert
+  UN_empty Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
   conj_assoc};
 
 fun mk_comp_in_alt_tac ctxt comp_set_alts =
-  unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
+  unfold_thms_tac ctxt comp_set_alts THEN
+  unfold_thms_tac ctxt comp_in_alt_thms THEN
   unfold_thms_tac ctxt @{thms set_eq_subset} THEN
   rtac conjI 1 THEN
   REPEAT_DETERM (
@@ -161,13 +162,14 @@
        atac ORELSE'
        (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1));
 
-val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
+val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def UN_insert UN_empty Un_empty_right
   Union_image_insert Union_image_empty};
 
 fun mk_comp_wit_tac ctxt set'_eq_sets Gwit_thms collect_set_map Fwit_thms =
   unfold_thms_tac ctxt set'_eq_sets THEN
   ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
-  unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
+  unfold_thms_tac ctxt [collect_set_map] THEN
+  unfold_thms_tac ctxt comp_wit_thms THEN
   REPEAT_DETERM ((atac ORELSE'
     REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN'
     etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN'
@@ -236,13 +238,12 @@
 val cprod_thms =
   @{thms cprod_cong1 cprod_cong2 cprod_cong cprod_dup[OF natLeq_cinfinite natLeq_Card_order]};
 
-(*inspired by "bnf_fp_def_sugar_tactics.ML"*)
 val simplified_set_simps =
-  @{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_def map_pair_simp mem_Collect_eq
-      mem_UN_compreh_ex_eq UN_compreh_ex_eq_eq sum.set_map prod.set_map id_bnf_comp_def};
+  @{thms collect_def[abs_def] UN_insert UN_empty Un_empty_right Un_empty_left
+    o_def Union_Un_distrib Union_image_eq UN_empty2 UN_singleton id_bnf_comp_def};
 
-fun mk_simplified_set_tac ctxt =
+fun mk_simplified_set_tac ctxt collect_set_map =
+  unfold_thms_tac ctxt (collect_set_map :: @{thms comp_assoc}) THEN
   unfold_thms_tac ctxt simplified_set_simps THEN rtac refl 1;
 
 val bd_ordIso_natLeq_tac =

--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Wed Mar 05 17:23:28 2014 -0800
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Mar 06 12:17:26 2014 +0100
@@ -39,10 +39,9 @@
 
 val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
 val sum_prod_thms_set =
-  @{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_ex_eq prod_set_simps sum_map.simps sum_set_simps
-      UN_compreh_ex_eq_eq UN_compreh_eq_eq ex_in_single};
+  @{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
+      Union_Un_distrib image_iff o_apply map_pair_simp
+      mem_Collect_eq prod_set_simps sum_map.simps sum_set_simps};
 val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
 
 fun hhf_concl_conv cv ctxt ct =