--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:39:46 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 29 22:56:39 2013 +0200
@@ -72,7 +72,7 @@
{prems: 'a, context: Proof.context} -> tactic
val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
- val mk_set_map_tac: thm -> tactic
+ val mk_set_map0_tac: thm -> tactic
val mk_set_tac: thm -> tactic
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
val mk_wpull_tac: thm -> tactic
@@ -724,7 +724,7 @@
(rtac sym THEN' rtac unique' THEN' EVERY' (map2 mk_comp map_comp0s' ctor_maps')) 1
end;
-fun mk_set_map_tac set_nat =
+fun mk_set_map0_tac set_nat =
EVERY' (map rtac [ext, trans, o_apply, sym, trans, o_apply, set_nat]) 1;
fun mk_bd_card_order_tac bd_card_orders =
@@ -747,31 +747,31 @@
REPEAT_DETERM_N n o etac UnE]))))] 1);
fun mk_ctor_rel_tac ctxt in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets ctor_inject
- ctor_dtor set_maps ctor_set_incls ctor_set_set_inclss =
+ ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss =
let
val m = length ctor_set_incls;
val n = length ctor_set_set_inclss;
- val (passive_set_maps, active_set_maps) = chop m set_maps;
+ val (passive_set_map0s, active_set_map0s) = chop m set_map0s;
val in_Irel = nth in_Irels (i - 1);
val le_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS ord_eq_le_trans;
val eq_arg_cong_ctor_dtor = ctor_dtor RS arg_cong RS trans;
val if_tac =
EVERY' [dtac (in_Irel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
- EVERY' (map2 (fn set_map => fn ctor_set_incl =>
- EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
+ EVERY' (map2 (fn set_map0 => fn ctor_set_incl =>
+ EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map0,
rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
rtac (ctor_set_incl RS subset_trans), etac le_arg_cong_ctor_dtor])
- passive_set_maps ctor_set_incls),
- CONJ_WRAP' (fn (in_Irel, (set_map, ctor_set_set_incls)) =>
- EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI}, rtac CollectI,
+ passive_set_map0s ctor_set_incls),
+ CONJ_WRAP' (fn (in_Irel, (set_map0, ctor_set_set_incls)) =>
+ EVERY' [rtac ord_eq_le_trans, rtac set_map0, rtac @{thm image_subsetI}, rtac CollectI,
rtac @{thm prod_caseI}, rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
CONJ_WRAP' (fn thm =>
EVERY' (map etac [thm RS subset_trans, le_arg_cong_ctor_dtor]))
ctor_set_set_incls,
rtac conjI, rtac refl, rtac refl])
- (in_Irels ~~ (active_set_maps ~~ ctor_set_set_inclss)),
+ (in_Irels ~~ (active_set_map0s ~~ ctor_set_set_inclss)),
CONJ_WRAP' (fn conv =>
EVERY' [rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
@@ -782,13 +782,13 @@
val only_if_tac =
EVERY' [dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
rtac (in_Irel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
- CONJ_WRAP' (fn (ctor_set, passive_set_map) =>
+ CONJ_WRAP' (fn (ctor_set, passive_set_map0) =>
EVERY' [rtac ord_eq_le_trans, rtac ctor_set, rtac @{thm Un_least},
rtac ord_eq_le_trans, rtac @{thm box_equals[OF _ refl]},
- rtac passive_set_map, rtac trans_fun_cong_image_id_id_apply, atac,
+ rtac passive_set_map0, rtac trans_fun_cong_image_id_id_apply, atac,
CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
- (fn (active_set_map, in_Irel) => EVERY' [rtac ord_eq_le_trans,
- rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map, rtac @{thm UN_least},
+ (fn (active_set_map0, in_Irel) => EVERY' [rtac ord_eq_le_trans,
+ rtac @{thm UN_cong[OF _ refl]}, rtac active_set_map0, rtac @{thm UN_least},
dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
dtac @{thm ssubst_mem[OF pair_collapse]},
REPEAT_DETERM o eresolve_tac (CollectE :: conjE ::
@@ -798,8 +798,8 @@
TRY o
EVERY' [dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac, hyp_subst_tac ctxt],
REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
- (rev (active_set_maps ~~ in_Irels))])
- (ctor_sets ~~ passive_set_maps),
+ (rev (active_set_map0s ~~ in_Irels))])
+ (ctor_sets ~~ passive_set_map0s),
rtac conjI,
REPEAT_DETERM_N 2 o EVERY' [rtac trans, rtac ctor_map, rtac (ctor_inject RS iffD2),
rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,