# HG changeset patch
# User blanchet
# Date 1473689307 -7200
# Node ID 0a6b145879f4ec83713d67a0011527f44e86db72
# Parent  1a1fd3f3a24c24c2dc933ff3673ad29a362a5b71
strengthened tactic

diff -r 1a1fd3f3a24c -r 0a6b145879f4 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 12 13:35:29 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 12 16:08:27 2016 +0200
@@ -9,8 +9,6 @@
 signature BNF_FP_DEF_SUGAR_TACTICS =
 sig
   val sumprod_thms_rel: thm list
-  val sumprod_thms_set: thm list (* FIXME *)
-  val basic_sumprod_thms_set: thm list
 
   val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
   val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
@@ -82,8 +80,8 @@
 val sumprod_thms_map = @{thms id_apply map_prod_simp prod.case sum.case map_sum.simps};
 val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc};
 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};
+  @{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;
 
 fun is_def_looping def =
@@ -498,10 +496,14 @@
 fun mk_set0_tac ctxt abs_inverses pre_set_defs dtor_ctor fp_sets fp_nesting_set_maps
     live_nesting_set_maps ctr_defs' extra_unfolds =
   TRYALL Goal.conjunction_tac THEN
-  unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_sets @ fp_nesting_set_maps @
-    live_nesting_set_maps @ ctr_defs' @ extra_unfolds @ basic_sumprod_thms_set @
+  unfold_thms_tac ctxt ctr_defs' THEN
+  ALLGOALS (subst_tac ctxt NONE fp_sets) THEN
+  unfold_thms_tac ctxt (dtor_ctor :: abs_inverses @ pre_set_defs @ fp_nesting_set_maps @
+    live_nesting_set_maps @ extra_unfolds @ basic_sumprod_thms_set @
     @{thms UN_UN_flatten UN_Un sup_assoc[THEN sym]}) THEN
-  ALLGOALS (rtac ctxt refl);
+  ALLGOALS (rtac ctxt @{thm set_eqI[OF iffI]}) THEN
+  ALLGOALS (REPEAT_DETERM o etac ctxt UnE) THEN
+  ALLGOALS (REPEAT o resolve_tac ctxt @{thms UnI1 UnI2} THEN' assume_tac ctxt);
 
 fun mk_set_sel_tac ctxt ct exhaust discs sels sets =
   TRYALL Goal.conjunction_tac THEN