tuned tactics
authortraytel
Fri Sep 28 09:17:30 2012 +0200 (2012-09-28)
changeset 496309f6ca87ab405
parent 49629 99700c4e0b33
child 49637 996267ad6fa7
tuned tactics
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_comp_tactics.ML
src/HOL/BNF/Tools/bnf_tactics.ML
src/HOL/BNF/Tools/bnf_wrap_tactics.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 28 08:59:54 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Sep 28 09:17:30 2012 +0200
     1.3 @@ -158,17 +158,9 @@
     1.4      (*(inner_1.bd +c ... +c inner_m.bd) *c outer.bd*)
     1.5      val bd = Term.absdummy CCA (mk_cprod (Library.foldr1 (uncurry mk_csum) inner_bds) outer_bd);
     1.6  
     1.7 -    fun map_id_tac {context = ctxt, ...} =
     1.8 -      let
     1.9 -        (*order the theorems by reverse size to prevent bad interaction with nonconfluent rewrite
    1.10 -          rules*)
    1.11 -        val thms = (map map_id_of_bnf inners
    1.12 -          |> map (`(Term.size_of_term o Thm.prop_of))
    1.13 -          |> sort (rev_order o int_ord o pairself fst)
    1.14 -          |> map snd) @ [map_id_of_bnf outer];
    1.15 -      in
    1.16 -        (EVERY' (map (fn thm => subst_tac ctxt NONE [thm]) thms) THEN' rtac refl) 1
    1.17 -      end;
    1.18 +    fun map_id_tac _ =
    1.19 +      mk_comp_map_id_tac (map_id_of_bnf outer) (map_cong_of_bnf outer)
    1.20 +        (map map_id_of_bnf inners);
    1.21  
    1.22      fun map_comp_tac _ =
    1.23        mk_comp_map_comp_tac (map_comp_of_bnf outer) (map_cong_of_bnf outer)
     2.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 28 08:59:54 2012 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Fri Sep 28 09:17:30 2012 +0200
     2.3 @@ -14,6 +14,7 @@
     2.4    val mk_comp_in_bd_tac: thm -> thm list -> thm -> thm list -> thm -> tactic
     2.5    val mk_comp_map_comp_tac: thm -> thm -> thm list -> tactic
     2.6    val mk_comp_map_cong_tac: thm list -> thm -> thm list -> tactic
     2.7 +  val mk_comp_map_id_tac: thm -> thm -> thm list -> tactic
     2.8    val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
     2.9    val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
    2.10    val mk_comp_set_natural_tac: thm -> thm -> thm -> thm list -> tactic
    2.11 @@ -68,6 +69,10 @@
    2.12    unfold_thms_tac ctxt [collect_set_natural RS sym] THEN
    2.13    rtac refl 1;
    2.14  
    2.15 +fun mk_comp_map_id_tac Gmap_id Gmap_cong map_ids =
    2.16 +  EVERY' ([rtac ext, rtac (Gmap_cong RS trans)] @
    2.17 +    map (fn thm => rtac (thm RS fun_cong)) map_ids @ [rtac (Gmap_id RS fun_cong)]) 1;
    2.18 +
    2.19  fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
    2.20    EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
    2.21      rtac (Gmap_comp RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong] @
     3.1 --- a/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 28 08:59:54 2012 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML	Fri Sep 28 09:17:30 2012 +0200
     3.3 @@ -99,8 +99,8 @@
     3.4  
     3.5  fun mk_ctor_or_dtor_rel_tac srel_def IJrel_defs IJsrel_defs dtor_srel {context = ctxt, prems = _} =
     3.6    unfold_thms_tac ctxt IJrel_defs THEN
     3.7 -  subst_tac ctxt NONE [unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
     3.8 -    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel] 1 THEN
     3.9 +  rtac (unfold_thms ctxt (IJrel_defs @ IJsrel_defs @
    3.10 +    @{thms Collect_pair_mem_eq mem_Collect_eq fst_conv snd_conv}) dtor_srel RS trans) 1 THEN
    3.11    unfold_thms_tac ctxt (srel_def ::
    3.12      @{thms Collect_fst_snd_mem_eq mem_Collect_eq pair_mem_Collect_split fst_conv snd_conv
    3.13        split_conv}) THEN
     4.1 --- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Sep 28 08:59:54 2012 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Fri Sep 28 09:17:30 2012 +0200
     4.3 @@ -41,7 +41,8 @@
     4.4    EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
     4.5  
     4.6  fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
     4.7 -  EVERY' ([subst_tac ctxt NONE [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
     4.8 +  EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
     4.9 +    rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
    4.10      hyp_subst_tac, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    4.11      rtac distinct, rtac uexhaust] @
    4.12      (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])