src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML

 Tactics for datatype and codatatype sugar.
 *)
 
 signature BNF_FP_DEF_SUGAR_TACTICS =
 sig
+  val sumprod_thms_rel: thm list
   val sumprod_thms_set: thm list
   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 ->

   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
-  val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
+  val mk_map_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic
   val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
   val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list ->
     thm list -> tactic
   val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
     tactic
   val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
     term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic
-  val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
+  val mk_rel_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> thm list -> tactic
   val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list ->
     thm list -> thm list -> tactic
   val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
     thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
     thm list -> thm list -> thm list -> tactic

   HEADGOAL (rtac ctxt dtor_coinduct' THEN'
     EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
       (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
       selsss));
 
-fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' ctr_defs' =
+fun mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map' live_nesting_map_ident0s ctr_defs' =
   TRYALL Goal.conjunction_tac THEN
-  unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @ ctr_defs' @ o_apply ::
-    sumprod_thms_map) THEN
+  unfold_thms_tac ctxt (pre_map_def :: dtor_ctor :: fp_map' :: abs_inverses @
+    live_nesting_map_ident0s @
+    ctr_defs' @ sumprod_thms_map @ @{thms o_def[abs_def] id_def}) THEN
   ALLGOALS (rtac ctxt refl);
 
 fun mk_map_disc_iff_tac ctxt ct exhaust discs maps =
   TRYALL Goal.conjunction_tac THEN
   ALLGOALS (rtac ctxt (infer_instantiate' ctxt [SOME ct] exhaust) THEN_ALL_NEW

     @{thms not_True_eq_False not_False_eq_True}) THEN
   TRYALL (etac ctxt FalseE ORELSE' etac ctxt @{thm TrueE}) THEN
   unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN
   ALLGOALS (rtac ctxt refl);
 
-fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel ctr_defs' =
+fun mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel live_nesting_rel_eqs ctr_defs' =
   TRYALL Goal.conjunction_tac THEN
-  unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ ctr_defs' @ o_apply ::
-    sumprod_thms_rel @ @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]
-      not_False_eq_True}) THEN
+  unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: fp_rel :: abs_inverses @ live_nesting_rel_eqs @
+    ctr_defs' @ sumprod_thms_rel @ @{thms vimage2p_def o_apply sum.inject
+      sum.distinct(1)[THEN eq_False[THEN iffD2]] not_False_eq_True}) THEN
   ALLGOALS (resolve_tac ctxt [TrueI, refl]);
 
 fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs =
   HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW
     rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW