src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

     thm list list list -> tactic
   val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
   val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     tactic
   val mk_disc_corec_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+  val mk_disc_map_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
   val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list ->
     thm list -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
   val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic

 end;
 
 structure BNF_FP_Def_Sugar_Tactics : BNF_FP_DEF_SUGAR_TACTICS =
 struct
 
+open Ctr_Sugar_Util
 open BNF_Tactics
 open BNF_Util
 open BNF_FP_Util
 
 val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};

   EVERY (map3 (fn case_split_tac => fn corec_thm => fn disc =>
       HEADGOAL case_split_tac THEN unfold_thms_tac ctxt [corec_thm] THEN
       HEADGOAL (asm_simp_tac (ss_only basic_simp_thms ctxt)) THEN
       (if is_refl disc then all_tac else HEADGOAL (rtac disc)))
     (map rtac case_splits' @ [K all_tac]) corecs discs);
+
+fun mk_disc_map_iff_tac ctxt ct exhaust discs maps =
+  TRYALL Goal.conjunction_tac THEN
+    ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+      REPEAT_DETERM o hyp_subst_tac ctxt) THEN
+    unfold_thms_tac ctxt maps THEN
+    unfold_thms_tac ctxt (map (fn thm => thm RS @{thm iffD2[OF eq_False]}
+      handle THM _ => thm RS @{thm iffD2[OF eq_True]}) discs) THEN
+    ALLGOALS (rtac refl ORELSE' rtac TrueI);
 
 fun solve_prem_prem_tac ctxt =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
     hyp_subst_tac ctxt ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});

       (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
       selsss));
 
 fun mk_set_empty_tac ctxt ct exhaust sets discs =
   TRYALL Goal.conjunction_tac THEN
-  ALLGOALS(rtac (Ctr_Sugar_Util.cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
+  ALLGOALS (rtac (cterm_instantiate_pos [SOME ct] exhaust) THEN_ALL_NEW
     REPEAT_DETERM o hyp_subst_tac ctxt) THEN
   unfold_thms_tac ctxt (sets @ map_filter (fn thm =>
     SOME (thm RS @{thm iffD2[OF eq_False]}) handle THM _ => NONE) discs) THEN
-  ALLGOALS(rtac refl ORELSE' etac FalseE);
+  ALLGOALS (rtac refl ORELSE' etac FalseE);
 
 end;