# HG changeset patch
# User blanchet
# Date 1473601029 -7200
# Node ID f738df816abfa397824ee0f763fde565a714a86d
# Parent  813a574da7461db2802c9237daaffe0b23c10a0a
strengthened tactics

diff -r 813a574da746 -r f738df816abf src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Sep 11 15:37:09 2016 +0200
@@ -119,9 +119,9 @@
     local_theory -> Ctr_Sugar.ctr_sugar * local_theory
   val derive_map_set_rel_pred_thms: (string -> bool) -> BNF_Util.fp_kind -> int -> typ list ->
     typ list -> typ -> typ -> thm list -> thm list -> thm list -> thm list -> thm list ->
-    thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list -> typ -> term ->
-    thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm -> typ list list -> term ->
-    Ctr_Sugar.ctr_sugar -> Proof.context ->
+    thm list -> thm list -> thm list -> thm list -> string -> BNF_Def.bnf -> BNF_Def.bnf list ->
+    typ -> term -> thm -> thm -> thm -> thm list -> thm -> thm -> thm list -> thm ->
+    typ list list -> term -> Ctr_Sugar.ctr_sugar -> local_theory ->
     (thm list * thm list * thm list list * thm list * thm list * thm list * thm list * thm list
      * thm list * thm list * thm list list list list * thm list list list list * thm list
      * thm list * thm list * thm list * thm list) * local_theory
@@ -701,9 +701,9 @@
   end;
 
 fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs fp_nesting_set_maps
-    fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
-    live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor pre_map_def
-    pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
+    fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_map_ident0s live_nesting_set_maps
+    live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
+    dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
     ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
       injects, distincts, distinct_discsss, ...} : ctr_sugar)
     lthy =
@@ -871,7 +871,8 @@
               else fp_map_thm RS ctor_cong RS (ctor_dtor RS sym RS trans);
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
-               mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm' ctr_defs')
+              mk_map_tac ctxt abs_inverses pre_map_def dtor_ctor fp_map_thm'
+                live_nesting_map_ident0s ctr_defs')
             |> Thm.close_derivation
             |> Conjunction.elim_balanced (length goals)
           end;
@@ -896,7 +897,8 @@
             val vars = Variable.add_free_names lthy goal [];
           in
             Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
-               mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs')
+              mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm live_nesting_rel_eqs
+                ctr_defs')
             |> Thm.close_derivation
             |> Conjunction.elim_balanced (length goals)
           end;
@@ -925,7 +927,8 @@
                    val vars = Variable.add_free_names lthy goal [];
                  in
                    Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
-                     mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm ctr_defs')
+                     mk_rel_tac ctxt abs_inverses pre_rel_def dtor_ctor fp_rel_thm
+                       live_nesting_rel_eqs ctr_defs')
                    |> Thm.close_derivation
                    |> Conjunction.elim_balanced (length goals)
                  end)
@@ -2462,10 +2465,11 @@
            disc_bindings sel_bindingss sel_default_eqs ctrs0 ctor_iff_dtor_thm ctr_defs
          #> (fn (ctr_sugar, lthy) =>
            derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs
-             fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
-             live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
-             ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
-             fp_rel_thm ctr_Tss abs ctr_sugar lthy
+             fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s
+             live_nesting_map_ident0s live_nesting_set_maps live_nesting_rel_eqs
+             live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor dtor_ctor
+             pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
+             ctr_sugar lthy
            |>> pair ctr_sugar)
          ##>>
            (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
diff -r 813a574da746 -r f738df816abf src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Sep 11 13:35:27 2016 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Sep 11 15:37:09 2016 +0200
@@ -8,6 +8,7 @@
 
 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
 
@@ -31,7 +32,7 @@
   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
@@ -39,7 +40,7 @@
     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 ->
@@ -389,10 +390,11 @@
       (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 =
@@ -414,11 +416,11 @@
   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 =