--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Apr 24 17:03:43 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Apr 24 17:47:22 2013 +0200
@@ -17,7 +17,7 @@
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
+ val mk_comp_set_map_tac: thm -> thm -> thm -> thm list -> tactic
val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
val mk_kill_bd_card_order_tac: int -> thm -> tactic
@@ -64,9 +64,9 @@
(* Composition *)
-fun mk_comp_set_alt_tac ctxt collect_set_natural =
+fun mk_comp_set_alt_tac ctxt collect_set_map =
unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
- unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
+ unfold_thms_tac ctxt [collect_set_map RS sym] THEN
rtac refl 1;
fun mk_comp_map_id_tac Gmap_id Gmap_cong0 map_ids =
@@ -78,21 +78,21 @@
rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
map (fn thm => rtac (thm RS sym RS fun_cong)) map_comps) 1;
-fun mk_comp_set_natural_tac Gmap_comp Gmap_cong0 Gset_natural set_naturals =
+fun mk_comp_set_map_tac Gmap_comp Gmap_cong0 Gset_map set_maps =
EVERY' ([rtac ext] @
replicate 3 (rtac trans_o_apply) @
[rtac (arg_cong_Union RS trans),
rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans),
rtac Gmap_cong0] @
- map (fn thm => rtac (thm RS fun_cong)) set_naturals @
- [rtac (Gset_natural RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
+ map (fn thm => rtac (thm RS fun_cong)) set_maps @
+ [rtac (Gset_map RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
- rtac (@{thm image_cong} OF [Gset_natural RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
+ rtac (@{thm image_cong} OF [Gset_map RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
rtac @{thm trans[OF pointfreeE[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
- [REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac @{thm trans[OF image_insert]},
+ [REPEAT_DETERM_N (length set_maps) o EVERY' [rtac @{thm trans[OF image_insert]},
rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
@@ -217,9 +217,9 @@
val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
Union_image_insert Union_image_empty};
-fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
+fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms =
ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
- unfold_thms_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
+ unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
REPEAT_DETERM (
atac 1 ORELSE
REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN