tuned tactic
authortraytel
Mon Mar 10 14:46:22 2014 +0100 (2014-03-10)
changeset 560178d3df792d47e
parent 56016 8875cdcfc85b
child 56018 c3fc8692dbc1
tuned tactic
src/HOL/Tools/BNF/bnf_gfp.ML
src/HOL/Tools/BNF/bnf_gfp_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 10 13:23:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML	Mon Mar 10 14:46:22 2014 +0100
     1.3 @@ -231,7 +231,7 @@
     1.4      val rel_converseps = map rel_conversep_of_bnf bnfs;
     1.5      val rel_Grps = map rel_Grp_of_bnf bnfs;
     1.6      val rel_OOs = map rel_OO_of_bnf bnfs;
     1.7 -    val rel_OO_Grps = map rel_OO_Grp_of_bnf bnfs;
     1.8 +    val in_rels = map in_rel_of_bnf bnfs;
     1.9  
    1.10      val timer = time (timer "Extracted terms & thms");
    1.11  
    1.12 @@ -757,7 +757,7 @@
    1.13          Goal.prove_sorry lthy [] []
    1.14            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy)
    1.15              (Logic.list_implies (prems, concl)))
    1.16 -          (K ((hyp_subst_tac lthy THEN' atac) 1))
    1.17 +          (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1)
    1.18          |> Thm.close_derivation
    1.19        end;
    1.20  
    1.21 @@ -775,7 +775,7 @@
    1.22          Goal.prove_sorry lthy [] []
    1.23            (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs)
    1.24              (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs)))
    1.25 -          (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss))
    1.26 +          (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss))
    1.27          |> Thm.close_derivation
    1.28        end;
    1.29  
    1.30 @@ -1905,7 +1905,6 @@
    1.31        ||>> mk_Frees "S" activephiTs
    1.32        ||>> mk_Frees "JR" activeJphiTs;
    1.33      val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
    1.34 -    val in_rels = map in_rel_of_bnf bnfs;
    1.35  
    1.36      fun mk_Jrel_DEADID_coinduct_thm () = 
    1.37        mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
     2.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Mar 10 13:23:16 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Mar 10 14:46:22 2014 +0100
     2.3 @@ -13,7 +13,7 @@
     2.4    val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
     2.5    val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic
     2.6    val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
     2.7 -  val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
     2.8 +  val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list ->
     2.9      thm list list -> tactic
    2.10    val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic
    2.11    val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
    2.12 @@ -214,38 +214,36 @@
    2.13              (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
    2.14        (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1;
    2.15  
    2.16 -fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss =
    2.17 +fun mk_bis_rel_tac m bis_def in_rels map_comp0s map_cong0s set_map0ss =
    2.18    let
    2.19 -    val n = length rel_OO_Grps;
    2.20 -    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps);
    2.21 +    val n = length in_rels;
    2.22 +    val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels);
    2.23  
    2.24 -    fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) =
    2.25 +    fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
    2.26        EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
    2.27 -        etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
    2.28 -        rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}),
    2.29 -        rtac @{thm relcomppI}, rtac @{thm conversepI},
    2.30 -        EVERY' (map (fn thm =>
    2.31 -          EVERY' [rtac @{thm GrpI},
    2.32 -            rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
    2.33 -            REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac,
    2.34 -            REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
    2.35 -            CONJ_WRAP' (fn (i, thm) =>
    2.36 -              if i <= m
    2.37 -              then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
    2.38 -                etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
    2.39 -                rtac @{thm case_prodI}, rtac refl]
    2.40 -              else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    2.41 -                rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
    2.42 -            (1 upto (m + n) ~~ set_map0s)])
    2.43 -          @{thms fst_diag_id snd_diag_id})];
    2.44 +        etac allE, etac allE, etac impE, atac, etac bexE,
    2.45 +        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
    2.46 +        rtac (in_rel RS iffD2), rtac exI, rtac (Drule.rotate_prems 1 conjI),
    2.47 +        CONJ_WRAP' (fn thm => EVERY' [rtac trans, rtac trans, rtac map_comp0, rtac map_cong0,
    2.48 +          REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),
    2.49 +          atac])
    2.50 +        @{thms fst_diag_id snd_diag_id},
    2.51 +        rtac CollectI,
    2.52 +        CONJ_WRAP' (fn (i, thm) =>
    2.53 +          if i <= m
    2.54 +          then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans,
    2.55 +            etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI,
    2.56 +            rtac @{thm case_prodI}, rtac refl]
    2.57 +          else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    2.58 +            rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}])
    2.59 +        (1 upto (m + n) ~~ set_map0s)];
    2.60  
    2.61 -    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) =
    2.62 +    fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
    2.63        EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
    2.64          etac allE, etac allE, etac impE, atac,
    2.65 -        dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}),
    2.66 +        dtac (in_rel RS @{thm iffD1}),
    2.67          REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @
    2.68 -          @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}),
    2.69 -        hyp_subst_tac ctxt,
    2.70 +          @{thms CollectE Collect_split_in_rel_leE}),
    2.71          rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0,
    2.72          REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong),
    2.73          REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),