# HG changeset patch
# User traytel
# Date 1348816650 -7200
# Node ID 9f6ca87ab405b05796a4727a34230a00692633b7
# Parent  99700c4e0b33a4bcefd91ee9cec7011395dd2326
tuned tactics

diff -r 99700c4e0b33 -r 9f6ca87ab405 src/HOL/BNF/Tools/bnf_comp.ML
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 28 09:17:30 2012 +0200
@@ -158,17 +158,9 @@
     (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
     val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
 
-    fun map_id_tac {context = ctxt, ...} =
-      let
-        (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
-          rules*)
-        val thms = (map map_id_of_bnf inners
-          |> map (`(Term.size_of_term o Thm.prop_of))
-          |> sort (rev_order o int_ord o pairself fst)
-          |> map snd) @ [map_id_of_bnf outer];
-      in
-        (EVERY' (map (fn thm => subst_tac ctxt NONE [thm]) thms) THEN' rtac refl) 1
-      end;
+    fun map_id_tac _ =
+      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong_of_bnf outer)
+        (map map_id_of_bnf inners);
 
     fun map_comp_tac _ =
       mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
diff -r 99700c4e0b33 -r 9f6ca87ab405 src/HOL/BNF/Tools/bnf_comp_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 28 09:17:30 2012 +0200
@@ -14,6 +14,7 @@
   val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
   val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
   val mk_comp_map_cong_tac: thm list -> thm -> thm list -> tactic
+  val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
   val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
   val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
   val mk_comp_set_natural_tac: thm -> thm -> thm -> thm list -> tactic
@@ -68,6 +69,10 @@
   unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
   rtac refl 1;
 
+fun mk_comp_map_id_tac Gmap_id Gmap_cong map_ids =
+  EVERY' ([rtac ext, rtac (Gmap_cong RS trans)] @
+    map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
+
 fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
   EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
     rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong] @
diff -r 99700c4e0b33 -r 9f6ca87ab405 src/HOL/BNF/Tools/bnf_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 28 09:17:30 2012 +0200
@@ -99,8 +99,8 @@
 
 fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
   unfold_thms_tac ctxt IJrel_defs THEN
-  subst_tac ctxt NONE [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
-    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN
+  rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
+    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
   unfold_thms_tac ctxt (srel_def ::
     @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
       split_conv}) THEN
diff -r 99700c4e0b33 -r 9f6ca87ab405 src/HOL/BNF/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Sep 28 09:17:30 2012 +0200
@@ -41,7 +41,8 @@
   EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
 
 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
-  EVERY' ([subst_tac ctxt NONE [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
+  EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
+    rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
     hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
     rtac distinct, rtac uexhaust] @
     (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])