# HG changeset patch
# User blanchet
# Date 1482424588 -3600
# Node ID a42dbe9d2c1f3baa2e0f571ec8e426a33a347607
# Parent  255741c5f862ad1a062ca88e3178824c6fac12c2
export ML function

diff -r 255741c5f862 -r a42dbe9d2c1f src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Dec 22 10:42:08 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Thu Dec 22 17:36:28 2016 +0100
@@ -12,6 +12,8 @@
 
   val co_induct_inst_as_projs_tac: Proof.context -> int -> tactic
   val mk_case_transfer_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_coinduct_discharge_prem_tac: Proof.context -> thm list -> thm list -> int -> int -> int ->
+    thm -> thm -> thm -> thm -> thm -> thm list -> thm list list -> thm list list -> int -> tactic
   val mk_coinduct_tac: Proof.context -> thm list -> int -> int list -> thm -> thm list ->
     thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list list ->
     thm list list list -> tactic
@@ -350,13 +352,13 @@
   end;
 
 fun mk_coinduct_same_ctr_tac ctxt rel_eqs pre_rel_def pre_abs_inverse abs_inverse dtor_ctor ctr_def
-    discs sels =
+    discs sels extra_unfolds =
   hyp_subst_tac ctxt THEN'
   CONVERSION (hhf_concl_conv
     (Conv.top_conv (K (Conv.try_conv (Conv.rewr_conv ctr_def))) ctxt) ctxt) THEN'
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: dtor_ctor :: sels)) THEN'
   SELECT_GOAL (unfold_thms_tac ctxt (pre_rel_def :: pre_abs_inverse :: abs_inverse :: dtor_ctor ::
-    sels @ sumprod_thms_rel @ @{thms o_apply vimage2p_def})) THEN'
+    sels @ sumprod_thms_rel @ extra_unfolds @ @{thms o_apply vimage2p_def})) THEN'
   (assume_tac ctxt ORELSE' REPEAT o etac ctxt conjE THEN'
      full_simp_tac (ss_only (no_refl discs @ rel_eqs @ more_simp_thms) ctxt) THEN'
      REPEAT o etac ctxt conjE THEN_MAYBE' REPEAT o hyp_subst_tac ctxt THEN'
@@ -371,8 +373,8 @@
     full_simp_tac (ss_only (refl :: no_refl discs'' @ basic_simp_thms) ctxt)
   end;
 
-fun mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn kk n pre_rel_def pre_abs_inverse abs_inverse
-    dtor_ctor exhaust ctr_defs discss selss =
+fun mk_coinduct_discharge_prem_tac ctxt extra_unfolds rel_eqs' nn kk n pre_rel_def pre_abs_inverse
+    abs_inverse dtor_ctor exhaust ctr_defs discss selss =
   let val ks = 1 upto n in
     EVERY' ([rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
         select_prem_tac ctxt nn (dtac ctxt meta_spec) kk, dtac ctxt meta_spec, dtac ctxt meta_mp,
@@ -383,7 +385,7 @@
           map2 (fn k' => fn discs' =>
             if k' = k then
               mk_coinduct_same_ctr_tac ctxt rel_eqs' pre_rel_def pre_abs_inverse abs_inverse
-                dtor_ctor ctr_def discs sels
+                dtor_ctor ctr_def discs sels extra_unfolds
             else
               mk_coinduct_distinct_ctrs_tac ctxt discs discs') ks discss)) ks ctr_defs discss selss)
   end;
@@ -391,7 +393,7 @@
 fun mk_coinduct_tac ctxt rel_eqs' nn ns dtor_coinduct' pre_rel_defs pre_abs_inverses abs_inverses
     dtor_ctors exhausts ctr_defss discsss selsss =
   HEADGOAL (rtac ctxt dtor_coinduct' THEN'
-    EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt rel_eqs' nn)
+    EVERY' (@{map 10} (mk_coinduct_discharge_prem_tac ctxt [] rel_eqs' nn)
       (1 upto nn) ns pre_rel_defs pre_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss
       discsss selsss));