# HG changeset patch
# User blanchet
# Date 1407406661 -7200
# Node ID f97643a566153b6c01d773d931987f8ffc241ddd
# Parent  7a9aaddb3203c59a2fdc9b1ed4b8a0d881f78866
generate nicer 'set' theorems for (co)datatypes

diff -r 7a9aaddb3203 -r f97643a56615 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -1382,19 +1382,23 @@
                          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_set_thm fp_set_thm ctr_def' cxIn =
+
+              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 @
-                       abs_inverses)
+                       @{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);
 
-              fun mk_set_thms fp_set_thm = map2 (mk_set_thm fp_set_thm) ctr_defs' cxIns;
+              fun mk_set0_thms fp_set_thm = map2 (mk_set0_thm fp_set_thm) ctr_defs' cxIns;
 
               val map_thms = map2 mk_map_thm ctr_defs' cxIns;
-              val set_thmss = map mk_set_thms fp_set_thms;
-              val set_thms = flat set_thmss;
+              val set0_thmss = map mk_set0_thms fp_set_thms;
+              val set0_thms = flat set0_thmss;
+              val set_thms = set0_thms
+                |> map (unfold_thms lthy @{thms insert_is_Un[THEN sym] Un_empty_left
+                  Un_insert_left});
 
               val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
 
@@ -1426,7 +1430,7 @@
                   else
                     Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
                       (fn {context = ctxt, prems = _} =>
-                        mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
+                        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
@@ -1695,7 +1699,7 @@
                         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) set_thms)
+                              (flat sel_thmss) set0_thms)
                           |> Conjunction.elim_balanced (length goals)
                           |> Proof_Context.export names_lthy lthy
                     end;
@@ -1728,13 +1732,13 @@
                 |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) map_thms)
                 |> fp = Least_FP
                   ? Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) rel_eq_thms)
-                |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set_thms)
+                |> Spec_Rules.add Spec_Rules.Equational (`(single o lhs_head_of o hd) set0_thms)
                 |> Local_Theory.notes (anonymous_notes @ notes);
 
               val subst = Morphism.thm (substitute_noted_thm noted);
             in
               (((map subst map_thms, map subst rel_inject_thms, map subst rel_distinct_thms,
-                 map (map subst) set_thmss), ctr_sugar), lthy')
+                 map (map subst) set0_thmss), ctr_sugar), lthy')
             end;
 
         fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
diff -r 7a9aaddb3203 -r f97643a56615 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Aug 07 12:17:41 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Aug 07 12:17:41 2014 +0200
@@ -57,9 +57,8 @@
 
 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_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
-      Union_Un_distrib image_iff o_apply map_prod_simp
-      mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
+  @{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 sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc};
 
 fun hhf_concl_conv cv ctxt ct =