src/HOL/Tools/BNF/bnf_gfp_tactics.ML
changeset 61424 c3658c18b7bc
parent 60801 7664e0916eec
child 61841 4d3527b94f2a
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
     1.5  val sum_case_cong_weak = @{thm sum.case_cong_weak};
     1.6  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
     1.7 -val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
     1.8 +val Collect_splitD_set_mp = @{thm Collect_case_prodD[OF set_mp]};
     1.9  val rev_bspec = Drule.rotate_prems 1 bspec;
    1.10  val Un_cong = @{thm arg_cong2[of _ _ _ _ "op \<union>"]};
    1.11  val converse_shift = @{thm converse_subset_swap} RS iffD1;
    1.12 @@ -239,7 +239,7 @@
    1.13              etac ctxt @{thm image_mono}, rtac ctxt @{thm image_subsetI}, rtac ctxt CollectI,
    1.14              rtac ctxt @{thm case_prodI}, rtac ctxt refl]
    1.15            else EVERY' [rtac ctxt ord_eq_le_trans, rtac ctxt trans, rtac ctxt thm,
    1.16 -            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_split_in_rel_leI}])
    1.17 +            rtac ctxt trans_fun_cong_image_id_id_apply, etac ctxt @{thm Collect_case_prod_in_rel_leI}])
    1.18          (1 upto (m + n) ~~ set_map0s)];
    1.19  
    1.20      fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) =
    1.21 @@ -247,7 +247,7 @@
    1.22          etac ctxt allE, etac ctxt allE, etac ctxt impE, assume_tac ctxt,
    1.23          dtac ctxt (in_rel RS @{thm iffD1}),
    1.24          REPEAT_DETERM o eresolve_tac ctxt ([CollectE, conjE, exE] @
    1.25 -          @{thms CollectE Collect_split_in_rel_leE}),
    1.26 +          @{thms CollectE Collect_case_prod_in_rel_leE}),
    1.27          rtac ctxt bexI, rtac ctxt conjI, rtac ctxt trans, rtac ctxt map_comp0, rtac ctxt trans, rtac ctxt map_cong0,
    1.28          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
    1.29          REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
    1.30 @@ -255,7 +255,7 @@
    1.31          REPEAT_DETERM_N m o rtac ctxt (@{thm id_comp} RS fun_cong),
    1.32          REPEAT_DETERM_N n o rtac ctxt (@{thm comp_id} RS fun_cong),
    1.33          rtac ctxt trans, rtac ctxt map_cong0,
    1.34 -        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_splitD}, etac ctxt set_mp, assume_tac ctxt],
    1.35 +        REPEAT_DETERM_N m o EVERY' [rtac ctxt @{thm Collect_case_prodD}, etac ctxt set_mp, assume_tac ctxt],
    1.36          REPEAT_DETERM_N n o rtac ctxt refl,
    1.37          assume_tac ctxt, rtac ctxt CollectI,
    1.38          CONJ_WRAP' (fn (i, thm) =>
    1.39 @@ -772,8 +772,8 @@
    1.40      CONJ_WRAP' (fn rel_cong => EVERY' [rtac ctxt allI, rtac ctxt allI, rtac ctxt impI,
    1.41        REPEAT_DETERM o etac ctxt allE, rtac ctxt (rel_cong RS @{thm eq_refl} RS @{thm predicate2D}),
    1.42        REPEAT_DETERM_N m o rtac ctxt refl,
    1.43 -      REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_split_eq[symmetric]},
    1.44 -      etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm splitD}])
    1.45 +      REPEAT_DETERM_N (length rel_congs) o rtac ctxt @{thm in_rel_Collect_case_prod_eq[symmetric]},
    1.46 +      etac ctxt mp, etac ctxt CollectE, etac ctxt @{thm case_prodD}])
    1.47      rel_congs,
    1.48      rtac ctxt impI, REPEAT_DETERM o etac ctxt conjE,
    1.49      CONJ_WRAP' (K (EVERY' [rtac ctxt impI, rtac ctxt @{thm IdD}, etac ctxt set_mp,
    1.50 @@ -994,7 +994,7 @@
    1.51                  rtac ctxt @{thm SUP_cong[OF _ refl]}, rtac ctxt @{thm box_equals[OF _ _ refl]},
    1.52                  rtac ctxt active_set_map0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt @{thm UN_least},
    1.53                  dtac ctxt set_rev_mp, etac ctxt @{thm image_mono}, etac ctxt imageE,
    1.54 -                dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
    1.55 +                dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
    1.56                  REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
    1.57                    @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
    1.58                  hyp_subst_tac ctxt,
    1.59 @@ -1008,7 +1008,7 @@
    1.60            rtac ctxt @{thm box_equals}, rtac ctxt map_comp0, rtac ctxt (dtor_ctor RS sym RS arg_cong), rtac ctxt trans,
    1.61            rtac ctxt map_cong0, REPEAT_DETERM_N m o rtac ctxt @{thm fun_cong[OF comp_id]},
    1.62            EVERY' (map (fn in_Jrel => EVERY' [rtac ctxt trans, rtac ctxt o_apply, dtac ctxt set_rev_mp, assume_tac ctxt,
    1.63 -            dtac ctxt @{thm ssubst_mem[OF pair_collapse]},
    1.64 +            dtac ctxt @{thm ssubst_mem[OF prod.collapse]},
    1.65              REPEAT_DETERM o eresolve_tac ctxt (CollectE :: conjE ::
    1.66                @{thms case_prodE iffD1[OF prod.inject, elim_format]}),
    1.67              hyp_subst_tac ctxt, dtac ctxt (in_Jrel RS iffD1),