--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Aug 29 22:56:39 2013 +0200
@@ -50,7 +50,7 @@
fun mk_map_cong_tac ctxt cong0 =
(hyp_subst_tac ctxt THEN' rtac cong0 THEN'
REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
-fun mk_set_map' set_map = set_map RS @{thm comp_eq_dest};
+fun mk_set_map' set_map0 = set_map0 RS @{thm comp_eq_dest};
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
else (rtac subsetI THEN'
rtac CollectI) 1 THEN
@@ -59,15 +59,15 @@
((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
(etac subset_trans THEN' atac) 1;
-fun mk_collect_set_map_tac set_maps =
+fun mk_collect_set_map_tac set_map0s =
(rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
- EVERY' (map (fn set_map =>
+ EVERY' (map (fn set_map0 =>
rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
- rtac set_map) set_maps) THEN'
+ 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_maps =
- if null set_maps then
+fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp0 set_map0s =
+ if null set_map0s 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,
@@ -75,20 +75,20 @@
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_maps,
+ 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_maps) o EVERY' [rtac (o_apply RS trans),
+ REPEAT_DETERM_N (length set_map0s) 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_maps
+fun mk_rel_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp0 set_map0s
{context = ctxt, prems = _} =
let
- val n = length set_maps;
+ val n = length set_map0s;
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_maps then
+ if null set_map0s 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
@@ -100,7 +100,7 @@
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_maps,
+ set_map0s,
rtac @{thm predicate2I}, REPEAT_DETERM o eresolve_tac [@{thm GrpE}, exE, conjE],
hyp_subst_tac ctxt,
rtac @{thm relcomppI}, rtac @{thm conversepI},
@@ -112,7 +112,7 @@
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_maps])
+ set_map0s])
@{thms fst_convol snd_convol} [map_id, refl])] 1
end;
@@ -135,15 +135,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_maps
+fun mk_rel_conversep_le_tac rel_OO_Grps rel_eq map_cong0 map_comp0 set_map0s
{context = ctxt, prems = _} =
let
- val n = length set_maps;
+ val n = length set_map0s;
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_maps then rtac (rel_eq RS @{thm leq_conversepI}) 1
+ if null set_map0s then rtac (rel_eq RS @{thm leq_conversepI}) 1
else
EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I},
REPEAT_DETERM o
@@ -153,7 +153,7 @@
rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
rtac (map_comp0 RS sym), rtac CollectI,
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
- etac @{thm flip_pred}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
+ etac @{thm flip_pred}]) set_map0s]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
end;
fun mk_rel_conversep_tac le_conversep rel_mono =
@@ -161,19 +161,19 @@
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_maps
+fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp0 set_map0s
{context = ctxt, prems = _} =
let
- val n = length set_maps;
+ val n = length set_map0s;
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_maps;
+ rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_map0s;
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_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
+ if null set_map0s then rtac (rel_eq RS @{thm eq_OOI}) 1
else
EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
REPEAT_DETERM o
@@ -200,7 +200,7 @@
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_maps,
+ CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_map0s,
etac allE, etac impE, etac conjI, etac conjI, etac sym,
REPEAT_DETERM o eresolve_tac [bexE, conjE],
rtac @{thm relcomppI}, rtac @{thm conversepI},
@@ -216,15 +216,15 @@
REPEAT_DETERM o eresolve_tac [exE, conjE], rtac @{thm relcomppI}, rtac @{thm conversepI},
etac @{thm GrpI}, atac, etac @{thm GrpI}, atac] 1;
-fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
- if null set_maps then atac 1
+fun mk_rel_mono_strong_tac in_rel set_map0s {context = ctxt, prems = _} =
+ if null set_map0s 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_maps ctxt THEN
+ unfold_tac set_map0s 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_maps] 1;
+ CONJ_WRAP' (K (etac @{thm Collect_split_mono_strong} THEN' atac)) set_map0s] 1;
fun mk_map_transfer_tac rel_mono in_rel set_map's map_cong0 map_comp
{context = ctxt, prems = _} =