--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Fri Sep 28 09:21:27 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)
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Fri Sep 28 09:21:27 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] @
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Fri Sep 28 09:21:27 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
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Fri Sep 28 09:12:50 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Fri Sep 28 09:21:27 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])