# HG changeset patch
# User traytel
# Date 1387289759 -3600
# Node ID 641ea768f53514b793a313a8d53dc018e9d7ddc9
# Parent  3478fadb514e4b8448981f9d27e04e3bf9dea7fe
tuned

diff -r 3478fadb514e -r 641ea768f535 src/HOL/BNF/Tools/bnf_def_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML	Tue Dec 17 14:22:48 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML	Tue Dec 17 15:15:59 2013 +0100
@@ -68,8 +68,8 @@
     rtac set_map0) set_map0s) THEN'
   rtac @{thm image_empty}) 1;
 
-fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_map0s =
-  if null set_map0s then
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
+  if null set_maps then
     EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 1
   else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
     REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
@@ -77,44 +77,44 @@
     REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
     CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
       rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
-      set_map0s,
-    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp0 RS trans), rtac (map_comp0 RS trans),
-      rtac (map_comp0 RS trans RS sym), rtac map_cong0,
-      REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac (o_apply RS trans),
+      set_maps,
+    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
+      rtac (map_comp RS trans RS sym), rtac map_cong0,
+      REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans),
         rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
         rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
 
-fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_map0s
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps
   {context = ctxt, prems = _} =
   let
-    val n = length set_map0s;
+    val n = length set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac else rtac (hd rel_OO_Grps RS trans);
   in
-    if null set_map0s then
+    if null set_maps then
       unfold_thms_tac ctxt ((map_id0 RS @{thm Grp_UNIV_id}) :: rel_OO_Grps) THEN
       rtac @{thm Grp_UNIV_idI[OF refl]} 1
     else
       EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
         REPEAT_DETERM o
           eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
-        hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
+        hyp_subst_tac ctxt, rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
         REPEAT_DETERM_N n o EVERY' [rtac @{thm Collect_split_Grp_eqD}, etac @{thm set_mp}, atac],
         rtac CollectI,
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
           rtac @{thm image_subsetI}, rtac @{thm Collect_split_Grp_inD}, etac @{thm set_mp}, atac])
-        set_map0s,
+        set_maps,
         rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map2 (fn convol => fn map_id0 =>
-          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp0 RS sym, map_id0]),
+          EVERY' [rtac @{thm GrpI}, rtac (box_equals OF [map_cong0, map_comp RS sym, map_id0]),
             REPEAT_DETERM_N n o rtac (convol RS fun_cong),
             REPEAT_DETERM o eresolve_tac [CollectE, conjE],
             rtac CollectI,
             CONJ_WRAP' (fn thm =>
               EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm image_subsetI},
                 rtac @{thm convol_mem_GrpI}, etac set_mp, atac])
-            set_map0s])
+            set_maps])
           @{thms fst_convol snd_convol} [map_id, refl])] 1
   end;
 
@@ -137,15 +137,15 @@
       rtac @{thm Grp_mono}, rtac in_mono, REPEAT_DETERM o etac @{thm Collect_split_mono}] 1
   end;
 
-fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_map0s
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
   {context = ctxt, prems = _} =
   let
-    val n = length set_map0s;
+    val n = length set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
       else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
         rtac (hd rel_OO_Grps RS sym RS @{thm arg_cong[of _ _ conversep]} RSN (2, ord_le_eq_trans));
   in
-    if null set_map0s then rtac (rel_eq RS @{thm leq_conversepI}) 1
+    if null set_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1
     else
       EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I},
         REPEAT_DETERM o
@@ -153,9 +153,9 @@
         hyp_subst_tac ctxt, rtac @{thm conversepI}, rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac sym, rtac trans,
           rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
-          rtac (map_comp0 RS sym), rtac CollectI,
+          rtac (map_comp RS sym), rtac CollectI,
           CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
-            etac @{thm flip_pred}]) set_map0s]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
+            etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   end;
 
 fun mk_rel_conversep_tac le_conversep rel_mono =
@@ -163,63 +163,63 @@
     rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
     REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
 
-fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_map0s
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps
   {context = ctxt, prems = _} =
   let
-    val n = length set_map0s;
+    val n = length set_maps;
     fun in_tac nthO_in = rtac CollectI THEN'
         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
-          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_map0s;
+          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
     val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
       else rtac (hd rel_OO_Grps RS trans) THEN'
         rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
           (2, trans));
   in
-    if null set_map0s then rtac (rel_eq RS @{thm eq_OOI}) 1
+    if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
     else
       EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
         REPEAT_DETERM o
           eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
         hyp_subst_tac ctxt,
         rtac @{thm relcomppI}, rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
-        rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
+        rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
         REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
         in_tac @{thm fstOp_in},
-        rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac map_cong0,
+        rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
         REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, 
           rtac ballE, rtac subst,
           rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
           etac set_mp, atac],
         in_tac @{thm fstOp_in},
         rtac @{thm relcomppI}, rtac @{thm conversepI}, rtac @{thm GrpI},
-        rtac trans, rtac map_comp0, rtac map_cong0,
+        rtac trans, rtac map_comp, rtac map_cong0,
         REPEAT_DETERM_N n o rtac o_apply,
         in_tac @{thm sndOp_in},
-        rtac @{thm GrpI}, rtac trans, rtac map_comp0, rtac sym, rtac map_cong0,
+        rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
         REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
         in_tac @{thm sndOp_in},
         rtac @{thm predicate2I},
         REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}],
         hyp_subst_tac ctxt,
         rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
-        CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_map0s,
+        CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps,
         etac allE, etac impE, etac conjI, etac conjI, etac sym,
         REPEAT_DETERM o eresolve_tac [bexE, conjE],
         rtac @{thm relcomppI}, rtac @{thm conversepI},
         EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
           rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
-          rtac (map_comp0 RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
+          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
   end;
 
-fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} =
-  if null set_map0s then atac 1
+fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
+  if null set_maps then atac 1
   else
     unfold_tac [in_rel] ctxt THEN
     REPEAT_DETERM (eresolve_tac [exE, CollectE, conjE] 1) THEN
     hyp_subst_tac ctxt 1 THEN
-    unfold_tac set_map0s ctxt THEN
+    unfold_tac set_maps ctxt THEN
     EVERY' [rtac exI, rtac @{thm conjI[OF CollectI conjI[OF refl refl]]},
-      CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_map0s] 1;
+      CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_maps] 1;
 
 fun mk_map_transfer_tac rel_mono in_rel set_maps map_cong0 map_comp
   {context = ctxt, prems = _} =